This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.
It matches that base class almost exactly, with cosmetic changes.
Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.
This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.
{
}
-bool InferenceManagerBuffered::hasProcessed() const
+bool InferenceManagerBuffered::hasPending() const
{
- return d_theoryState.isInConflict() || !d_pendingLem.empty()
- || !d_pendingFact.empty();
+ return hasPendingFact() || hasPendingLemma();
}
bool InferenceManagerBuffered::hasPendingFact() const
ProofNodeManager* pnm);
virtual ~InferenceManagerBuffered() {}
/**
- * Have we processed an inference during this call to check? In particular,
- * this returns true if we have a pending fact or lemma, or have encountered
- * a conflict.
+ * Do we have a pending fact or lemma?
*/
- bool hasProcessed() const;
+ bool hasPending() const;
/**
* Do we have a pending fact to add as an internal fact to the equality
* engine?
namespace theory {
namespace sets {
-CardinalityExtension::CardinalityExtension(SolverState& s,
- InferenceManager& im,
- context::Context* c,
- context::UserContext* u)
+CardinalityExtension::CardinalityExtension(SolverState& s, InferenceManager& im)
: d_state(s),
d_im(im),
- d_card_processed(u),
+ d_card_processed(s.getUserContext()),
d_finite_type_constants_processed(false)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_im.assertInference(lem, d_emp_exp, "card", 1);
}
}
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
}
void CardinalityExtension::checkCardCycles()
Trace("sets-cycle-debug")
<< "CYCLE: " << fact << " from " << exp << std::endl;
d_im.assertInference(fact, exp, "card_cycle");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
}
else
{
}
}
d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
return;
Trace("sets-debug") << " it is empty..." << std::endl;
Assert(!d_state.areEqual(n, emp_set));
d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
return;
Trace("sets-debug")
<< "...derived " << conc.size() << " conclusions" << std::endl;
d_im.assertInference(conc, n.eqNode(p), "cg_eqpar");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
return;
{
Node conc = n.eqNode(cpk);
d_im.assertInference(conc, exps, "cg_par_sing");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
}
else
{
}
}
d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq");
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
return;
}
}
// flush the lemmas
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
}
bool CardinalityExtension::isModelValueBasic(Node eqc)
* Constructs a new instance of the cardinality solver w.r.t. the provided
* contexts.
*/
- CardinalityExtension(SolverState& s,
- InferenceManager& im,
- context::Context* c,
- context::UserContext* u);
+ CardinalityExtension(SolverState& s, InferenceManager& im);
~CardinalityExtension() {}
/** reset
#include "theory/sets/inference_manager.h"
#include "options/sets_options.h"
-#include "theory/sets/theory_sets.h"
-#include "theory/sets/theory_sets_private.h"
using namespace std;
using namespace CVC4::kind;
namespace theory {
namespace sets {
-InferenceManager::InferenceManager(TheorySetsPrivate& p,
+InferenceManager::InferenceManager(Theory& t,
SolverState& s,
- context::Context* c,
- context::UserContext* u)
- : d_parent(p),
- d_state(s),
- d_sentLemma(false),
- d_addedFact(false),
- d_lemmas_produced(u),
- d_keep(c)
+ ProofNodeManager* pnm)
+ : InferenceManagerBuffered(t, s, pnm), d_state(s)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
-void InferenceManager::reset()
-{
- d_sentLemma = false;
- d_addedFact = false;
- d_pendingLemmas.clear();
-}
-
bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
{
// should we send this fact out as a lemma?
{
lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
}
- d_pendingLemmas.push_back(lem);
+ addPendingLemma(lem);
return true;
}
Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
}
bool polarity = fact.getKind() != NOT;
TNode atom = polarity ? fact : fact[0];
+ if (d_state.isEntailed(atom, polarity))
+ {
+ return false;
+ }
// things we can assert to equality engine
if (atom.getKind() == MEMBER
|| (atom.getKind() == EQUAL && atom[0].getType().isSet()))
{
// send to equality engine
- if (d_parent.assertFact(fact, exp))
+ if (assertInternalFact(atom, polarity, exp))
{
- d_addedFact = true;
+ // return true if this wasn't redundant
return true;
}
}
- else if (!d_state.isEntailed(fact, true))
+ else
{
// must send as lemma
Node lem = fact;
{
lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
}
- d_pendingLemmas.push_back(lem);
+ addPendingLemma(lem);
return true;
}
return false;
const char* c,
int inferType)
{
- d_keep.insert(exp);
- d_keep.insert(fact);
if (assertFactRec(fact, exp, inferType))
{
Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
{
n = Rewriter::rewrite(n);
Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
- flushLemma(lem);
+ // send the lemma
+ lemma(lem);
Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
if (reqPol != 0)
{
Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
<< std::endl;
- d_parent.getOutputChannel()->requirePhase(n, reqPol > 0);
- }
-}
-void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess)
-{
- if (!d_state.isInConflict())
- {
- for (const Node& l : lemmas)
- {
- flushLemma(l, preprocess);
- }
+ requirePhase(n, reqPol > 0);
}
- lemmas.clear();
-}
-
-void InferenceManager::flushLemma(Node lem, bool preprocess)
-{
- if (d_state.isInConflict())
- {
- return;
- }
- if (d_lemmas_produced.find(lem) != d_lemmas_produced.end())
- {
- Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
- return;
- }
- Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
- d_lemmas_produced.insert(lem);
- LemmaProperty p =
- preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
- d_parent.getOutputChannel()->lemma(lem, p);
- d_sentLemma = true;
-}
-
-void InferenceManager::flushPendingLemmas(bool preprocess)
-{
- flushLemmas(d_pendingLemmas, preprocess);
-}
-
-bool InferenceManager::hasLemmaCached(Node lem) const
-{
- return d_lemmas_produced.find(lem) != d_lemmas_produced.end();
-}
-
-bool InferenceManager::hasProcessed() const
-{
- return d_state.isInConflict() || d_sentLemma || d_addedFact;
-}
-bool InferenceManager::hasSentLemma() const { return d_sentLemma; }
-bool InferenceManager::hasAddedFact() const { return d_addedFact; }
-
-void InferenceManager::conflict(Node conf)
-{
- d_parent.getOutputChannel()->conflict(conf);
- d_state.notifyInConflict();
}
} // namespace sets
#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+#include "theory/inference_manager_buffered.h"
#include "theory/sets/solver_state.h"
-#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
* of theory of sets or internally as literals asserted to the equality engine
* of theory of sets. The latter literals are referred to as "facts".
*/
-class InferenceManager
+class InferenceManager : public InferenceManagerBuffered
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- InferenceManager(TheorySetsPrivate& p,
- SolverState& s,
- context::Context* c,
- context::UserContext* u);
- /** reset
- *
- * Called at the beginning of a full effort check. Resets the information
- * related to this class regarding whether facts and lemmas have been
- * processed.
- */
- void reset();
+ InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
/**
* Add facts corresponding to ( exp => fact ) via calls to the assertFact
* method of TheorySetsPrivate.
const char* c,
int inferType = 0);
- /** Flush lemmas
- *
- * This sends lemmas on the output channel of the theory of sets.
- *
- * The argument preprocess indicates whether preprocessing should be applied
- * (by TheoryEngine) on each of lemmas.
- */
- void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
- /** singular version of above */
- void flushLemma(Node lem, bool preprocess = false);
- /** Do we have pending lemmas? */
- bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); }
- /** Applies flushLemmas on d_pendingLemmas */
- void flushPendingLemmas(bool preprocess = false);
/** flush the splitting lemma ( n OR (NOT n) )
*
* If reqPol is not 0, then a phase requirement for n is requested with
* polarity ( reqPol>0 ).
*/
void split(Node n, int reqPol = 0);
- /** Have we sent a lemma during the current call to a full effort check? */
- bool hasSentLemma() const;
- /** Have we added a fact during the current call to a full effort check? */
- bool hasAddedFact() const;
- /** Have we processed an inference (fact, lemma, or conflict)? */
- bool hasProcessed() const;
- /** Have we sent lem as a lemma in the current user context? */
- bool hasLemmaCached(Node lem) const;
-
- /**
- * Send conflict.
- * @param conf The conflict node to be sent on the output channel
- */
- void conflict(Node conf);
private:
/** constants */
Node d_true;
Node d_false;
- /** the theory of sets which owns this */
- TheorySetsPrivate& d_parent;
- /** Reference to the state object for the theory of sets */
- SolverState& d_state;
- /** pending lemmas */
- std::vector<Node> d_pendingLemmas;
- /** sent lemma
- *
- * This flag is set to true during a full effort check if this theory
- * called d_out->lemma(...).
- */
- bool d_sentLemma;
- /** added fact
- *
- * This flag is set to true during a full effort check if this theory
- * added an internal fact to its equality engine.
- */
- bool d_addedFact;
- /** A user-context-dependent cache of all lemmas produced */
- NodeSet d_lemmas_produced;
/**
- * A set of nodes to ref-count. Nodes that are facts or are explanations of
- * facts must be added to this set since the equality engine does not
- * ref count nodes.
+ * Reference to the state object for the theory of sets. We store the
+ * (derived) state here, since it has additional methods required in this
+ * class.
*/
- NodeSet d_keep;
+ SolverState& d_state;
/** Assert fact recursive
*
* This is a helper function for assertInference, which calls assertFact
namespace theory {
namespace sets {
-SolverState::SolverState(TheorySetsPrivate& p,
- context::Context* c,
+SolverState::SolverState(context::Context* c,
context::UserContext* u,
Valuation val)
- : TheoryState(c, u, val), d_parent(p), d_proxy(u), d_proxy_to_term(u)
+ : TheoryState(c, u, val), d_parent(nullptr), d_proxy(u), d_proxy_to_term(u)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
+void SolverState::setParent(TheorySetsPrivate* p) { d_parent = p; }
+
void SolverState::reset()
{
d_set_eqc.clear();
if (polarity && d_ee->hasTerm(n[1]))
{
Node r = d_ee->getRepresentative(n[1]);
- if (d_parent.isMember(n[0], r))
+ if (d_parent->isMember(n[0], r))
{
return true;
}
d_proxy_to_term[k] = n;
Node eq = k.eqNode(n);
Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
- d_parent.getOutputChannel()->lemma(eq);
+ d_parent->getOutputChannel()->lemma(eq);
if (nk == SINGLETON)
{
Node slem = nm->mkNode(MEMBER, n[0], k);
Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
<< std::endl;
- d_parent.getOutputChannel()->lemma(slem);
+ d_parent->getOutputChannel()->lemma(slem);
}
return k;
}
Node ulem = nm->mkNode(SUBSET, n1, n2);
Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
<< std::endl;
- d_parent.getOutputChannel()->lemma(ulem);
+ d_parent->getOutputChannel()->lemma(ulem);
}
}
d_univset[tn] = n;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
public:
- SolverState(TheorySetsPrivate& p,
- context::Context* c,
- context::UserContext* u,
- Valuation val);
+ SolverState(context::Context* c, context::UserContext* u, Valuation val);
+ /** Set parent */
+ void setParent(TheorySetsPrivate* p);
//-------------------------------- initialize per check
/** reset, clears the data structures maintained by this class. */
void reset();
/** the empty vector and map */
std::vector<Node> d_emptyVec;
std::map<Node, Node> d_emptyMap;
- /** Reference to the parent theory of sets */
- TheorySetsPrivate& d_parent;
+ /** Pointer to the parent theory of sets */
+ TheorySetsPrivate* d_parent;
/** The list of all equivalence classes of type set in the current context */
std::vector<Node> d_set_eqc;
/** Maps types to the equivalence class containing empty set of that type */
const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
- d_internal(new TheorySetsPrivate(*this, c, u, valuation)),
+ d_state(c, u, valuation),
+ d_im(*this, d_state, pnm),
+ d_internal(new TheorySetsPrivate(*this, d_state, d_im)),
d_notify(*d_internal.get())
{
- // use the state object as the official theory state
- d_theoryState = d_internal->getSolverState();
+ // use the official theory state and inference manager objects
+ d_theoryState = &d_state;
+ d_inferManager = &d_im;
+
+ // TODO: remove this
+ d_state.setParent(d_internal.get());
}
TheorySets::~TheorySets()
{
- // Do not move me to the header. See explanation in the constructor.
}
TheoryRewriter* TheorySets::getTheoryRewriter()
void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
-bool TheorySets::preNotifyFact(
- TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
-{
- return d_internal->preNotifyFact(atom, polarity, fact);
-}
-
void TheorySets::notifyFact(TNode atom,
bool polarity,
TNode fact,
#include <memory>
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
//--------------------------------- standard check
/** Post-check, called after the fact queue of the theory is processed. */
void postCheck(Effort level) override;
- /** Pre-notify fact, return true if processed. */
- bool preNotifyFact(TNode atom,
- bool pol,
- TNode fact,
- bool isPrereg,
- bool isInternal) override;
/** Notify fact */
void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
//--------------------------------- end standard check
private:
TheorySetsPrivate& d_theory;
};
+ /** The state of the sets solver at full effort */
+ SolverState d_state;
+ /** The inference manager */
+ InferenceManager d_im;
/** The internal theory */
std::unique_ptr<TheorySetsPrivate> d_internal;
/** Instance of the above class */
namespace sets {
TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
- context::Context* c,
- context::UserContext* u,
- Valuation valuation)
- : d_members(c),
- d_deq(c),
- d_termProcessed(u),
- d_keep(c),
+ SolverState& state,
+ InferenceManager& im)
+ : d_members(state.getSatContext()),
+ d_deq(state.getSatContext()),
+ d_termProcessed(state.getUserContext()),
d_full_check_incomplete(false),
d_external(external),
- d_state(*this, c, u, valuation),
- d_im(*this, d_state, c, u),
- d_rels(new TheorySetsRels(d_state, d_im, u)),
- d_cardSolver(new CardinalityExtension(d_state, d_im, c, u)),
+ d_state(state),
+ d_im(im),
+ d_rels(new TheorySetsRels(d_state, d_im)),
+ d_cardSolver(new CardinalityExtension(d_state, d_im)),
d_rels_enabled(false),
d_card_enabled(false)
{
// infer equality between elements of singleton
Node exp = s1.eqNode(s2);
Node eq = s1[0].eqNode(s2[0]);
- d_keep.insert(exp);
- d_keep.insert(eq);
- assertFact(eq, exp);
+ d_im.assertInternalFact(eq, true, exp);
}
else
{
if (s1[0] != m2[0])
{
Node eq = s1[0].eqNode(m2[0]);
- d_keep.insert(exp);
- d_keep.insert(eq);
Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
<< " => " << eq << std::endl;
- assertFact(eq, exp);
+ d_im.assertInternalFact(eq, true, exp);
}
}
else
return false;
}
-bool TheorySetsPrivate::assertFact(Node fact, Node exp)
-{
- Trace("sets-assert") << "TheorySets::assertFact : " << fact
- << ", exp = " << exp << std::endl;
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
- if (d_state.isEntailed(atom, polarity))
- {
- return false;
- }
- if (atom.getKind() == kind::EQUAL)
- {
- d_equalityEngine->assertEquality(atom, polarity, exp);
- }
- else
- {
- d_equalityEngine->assertPredicate(atom, polarity, exp);
- }
- // call the notify new fact method
- notifyFact(atom, polarity, exp);
- return true;
-}
-
void TheorySetsPrivate::fullEffortReset()
{
Assert(d_equalityEngine->consistent());
d_state.reset();
// reset the inference manager
d_im.reset();
+ d_im.clearPendingLemmas();
// reset the cardinality solver
d_cardSolver->reset();
}
Trace("sets") << "----- Full effort check ------" << std::endl;
do
{
- Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+ Assert(!d_im.hasPendingLemma() || d_im.hasProcessed());
Trace("sets") << "...iterate full effort check..." << std::endl;
fullEffortReset();
}
// check subtypes
checkSubtypes();
- d_im.flushPendingLemmas(true);
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
continue;
}
// check downwards closure
checkDownwardsClosure();
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
continue;
}
// check upwards closure
checkUpwardsClosure();
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
continue;
}
// check disequalities
checkDisequalities();
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
continue;
}
// check reduce comprehensions
checkReduceComprehensions();
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
continue;
d_rels->check(Theory::EFFORT_FULL);
}
} while (!d_im.hasSentLemma() && !d_state.isInConflict()
- && d_im.hasAddedFact());
- Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+ && d_im.hasSentFact());
+ Assert(!d_im.hasPendingLemma() || d_im.hasProcessed());
Trace("sets") << "----- End full effort check, conflict="
<< d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
<< std::endl;
Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
lem = Rewriter::rewrite(lem);
d_im.assertInference(lem, d_true, "diseq", 1);
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
if (d_im.hasProcessed())
{
return;
nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
Trace("sets-comprehension")
<< "Comprehension reduction: " << lem << std::endl;
- d_im.flushLemma(lem);
+ d_im.lemma(lem);
}
}
Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
}
-bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact)
-{
- // use entailment check (is this necessary?)
- return d_state.isEntailed(atom, polarity);
-}
-
void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
{
if (d_state.isInConflict())
{
Node pexp = NodeManager::currentNM()->mkNode(
kind::AND, atom, atom[1].eqNode(s));
- d_keep.insert(pexp);
if (s.getKind() == kind::SINGLETON)
{
if (s[0] != atom[0])
{
Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
Node eq = s[0].eqNode(atom[0]);
- d_keep.insert(eq);
// triggers an internal inference
- assertFact(eq, pexp);
+ d_im.assertInternalFact(eq, true, pexp);
}
}
else
void eqNotifyNewClass(TNode t);
void eqNotifyMerge(TNode t1, TNode t2);
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- /** Assert fact holds in the current context with explanation exp.
- *
- * exp should be explainable by the equality engine of this class, and fact
- * should be a literal.
- */
- bool assertFact(Node fact, Node exp);
private:
/** Are a and b trigger terms in the equality engine that may be disequal? */
* context.
*/
NodeSet d_termProcessed;
- NodeSet d_keep;
//propagation
class EqcInfo
* contexts.
*/
TheorySetsPrivate(TheorySets& external,
- context::Context* c,
- context::UserContext* u,
- Valuation valuation);
+ SolverState& state,
+ InferenceManager& im);
~TheorySetsPrivate();
//--------------------------------- standard check
/** Post-check, called after the fact queue of the theory is processed. */
void postCheck(Theory::Effort level);
- /** Preprocess fact, return true if processed. */
- bool preNotifyFact(TNode atom, bool polarity, TNode fact);
/** Notify new fact */
void notifyFact(TNode atom, bool polarity, TNode fact);
//--------------------------------- end standard check
private:
TheorySets& d_external;
+ /** The state of the sets solver at full effort */
+ SolverState& d_state;
+ /** The inference manager of the sets solver */
+ InferenceManager& d_im;
/** Pointer to the equality engine of theory of sets */
eq::EqualityEngine* d_equalityEngine;
* given set type, or creates a new one if it does not exist.
*/
Node getChooseFunction(const TypeNode& setType);
- /** The state of the sets solver at full effort */
- SolverState d_state;
- /** The inference manager of the sets solver */
- InferenceManager d_im;
/** subtheory solver for the theory of relations */
std::unique_ptr<TheorySetsRels> d_rels;
/** subtheory solver for the theory of sets with cardinality */
typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT;
typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT;
-TheorySetsRels::TheorySetsRels(SolverState& s,
- InferenceManager& im,
- context::UserContext* u)
- : d_state(s), d_im(im), d_shared_terms(u)
+TheorySetsRels::TheorySetsRels(SolverState& s, InferenceManager& im)
+ : d_state(s), d_im(im), d_shared_terms(s.getUserContext())
{
d_trueNode = NodeManager::currentNM()->mkConst(true);
d_falseNode = NodeManager::currentNM()->mkConst(false);
// if we are still not in conflict, send lemmas
if (!d_state.isInConflict())
{
- d_im.flushPendingLemmas();
+ d_im.doPendingLemmas();
}
}
d_pending.clear();
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
public:
- TheorySetsRels(SolverState& s,
- InferenceManager& im,
- context::UserContext* u);
+ TheorySetsRels(SolverState& s, InferenceManager& im);
~TheorySetsRels();
/**
d_numCurrentFacts = 0;
}
+bool TheoryInferenceManager::hasProcessed() const
+{
+ return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
+ || d_numCurrentFacts > 0;
+}
+
void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
{
if (!d_theoryState.isInConflict())
* beginning of this loop and repeat its strategy while hasAddedFact is true.
*/
void reset();
+ /**
+ * Returns true if we are in conflict, or if we have sent a lemma or fact
+ * since the last call to reset.
+ */
+ bool hasProcessed() const;
//--------------------------------------- propagations
/**
* T-propagate literal lit, possibly encountered by equality engine,
projects / cvc5.git / commitdiff