summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/inference_manager.cpp8
-rw-r--r--src/theory/sets/inference_manager.h6
-rw-r--r--src/theory/sets/solver_state.cpp57
-rw-r--r--src/theory/sets/solver_state.h37
-rw-r--r--src/theory/sets/theory_sets.cpp8
-rw-r--r--src/theory/sets/theory_sets_private.cpp14
-rw-r--r--src/theory/sets/theory_sets_private.h6
7 files changed, 35 insertions, 101 deletions
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index f99dad91e..8f25f6511 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -72,7 +72,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
if (fact == d_false)
{
Trace("sets-lemma") << "Conflict : " << exp << std::endl;
- d_state.setConflict(exp);
+ conflict(exp);
return true;
}
return false;
@@ -233,6 +233,12 @@ bool InferenceManager::hasProcessed() const
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
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index ba6be9905..3278b848e 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -109,6 +109,12 @@ class InferenceManager
/** 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;
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index f3371cf61..5e5e9d22a 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -27,19 +27,14 @@ namespace sets {
SolverState::SolverState(TheorySetsPrivate& p,
context::Context* c,
- context::UserContext* u)
- : d_conflict(c), d_parent(p), d_ee(nullptr), d_proxy(u), d_proxy_to_term(u)
+ context::UserContext* u,
+ Valuation val)
+ : TheoryState(c, u, val), d_parent(p), d_proxy(u), d_proxy_to_term(u)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
-void SolverState::finishInit(eq::EqualityEngine* ee)
-{
- Assert(ee != nullptr);
- d_ee = ee;
-}
-
void SolverState::reset()
{
d_set_eqc.clear();
@@ -169,52 +164,6 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
}
}
-Node SolverState::getRepresentative(Node a) const
-{
- if (d_ee->hasTerm(a))
- {
- return d_ee->getRepresentative(a);
- }
- return a;
-}
-
-bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); }
-
-bool SolverState::areEqual(Node a, Node b) const
-{
- if (a == b)
- {
- return true;
- }
- if (d_ee->hasTerm(a) && d_ee->hasTerm(b))
- {
- return d_ee->areEqual(a, b);
- }
- return false;
-}
-
-bool SolverState::areDisequal(Node a, Node b) const
-{
- if (a == b)
- {
- return false;
- }
- else if (d_ee->hasTerm(a) && d_ee->hasTerm(b))
- {
- return d_ee->areDisequal(a, b, false);
- }
- return a.isConst() && b.isConst();
-}
-
-eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; }
-
-void SolverState::setConflict() { d_conflict = true; }
-void SolverState::setConflict(Node conf)
-{
- d_parent.getOutputChannel()->conflict(conf);
- d_conflict = true;
-}
-
void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
{
if (a != b)
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index dce90c2d3..3a40befbd 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -22,6 +22,7 @@
#include "context/cdhashset.h"
#include "theory/sets/skolem_cache.h"
+#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
@@ -42,19 +43,15 @@ class TheorySetsPrivate;
* to initialize the information in this class regarding full effort checks.
* Other query calls are then valid for the remainder of the full effort check.
*/
-class SolverState
+class SolverState : public TheoryState
{
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
public:
SolverState(TheorySetsPrivate& p,
context::Context* c,
- context::UserContext* u);
- /**
- * Finish initialize, there ee is a pointer to the official equality engine
- * of theory of strings.
- */
- void finishInit(eq::EqualityEngine* ee);
+ context::UserContext* u,
+ Valuation val);
//-------------------------------- initialize per check
/** reset, clears the data structures maintained by this class. */
void reset();
@@ -63,28 +60,6 @@ class SolverState
/** register term n of type tnn in the equivalence class of r */
void registerTerm(Node r, TypeNode tnn, Node n);
//-------------------------------- end initialize per check
- /** Are we currently in conflict? */
- bool isInConflict() const { return d_conflict; }
- /**
- * Indicate that we are in conflict, without a conflict clause. This is
- * called, for instance, when we have propagated a conflicting literal.
- */
- void setConflict();
- /** Set conf is a conflict node to be sent on the output channel. */
- void setConflict(Node conf);
- /**
- * Get the representative of a in the equality engine of this class, or a
- * itself if it is not registered as a term.
- */
- Node getRepresentative(Node a) const;
- /** Is a registered as a term in the equality engine of this class? */
- bool hasTerm(Node a) const;
- /** Is a=b according to equality reasoning in the current context? */
- bool areEqual(Node a, Node b) const;
- /** Is a!=b according to equality reasoning in the current context? */
- bool areDisequal(Node a, Node b) const;
- /** get equality engine */
- eq::EqualityEngine* getEqualityEngine() const;
/** add equality to explanation
*
* This adds a = b to exp if a and b are syntactically disequal. The equality
@@ -229,12 +204,8 @@ class SolverState
/** the empty vector and map */
std::vector<Node> d_emptyVec;
std::map<Node, Node> d_emptyMap;
- /** Whether or not we are in conflict. This flag is SAT context dependent. */
- context::CDO<bool> d_conflict;
/** Reference to the parent theory of sets */
TheorySetsPrivate& d_parent;
- /** Pointer to the official equality engine of theory of sets */
- eq::EqualityEngine* d_ee;
/** 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 */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index fd9af488f..fc544f46f 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,13 +34,11 @@ TheorySets::TheorySets(context::Context* c,
const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
- d_internal(new TheorySetsPrivate(*this, c, u)),
+ d_internal(new TheorySetsPrivate(*this, c, u, valuation)),
d_notify(*d_internal.get())
{
- // Do not move me to the header.
- // The constructor + destructor are not in the header as d_internal is a
- // unique_ptr<TheorySetsPrivate> and TheorySetsPrivate is an opaque type in
- // the header (Pimpl). See https://herbsutter.com/gotw/_100/ .
+ // use the state object as the official theory state
+ d_theoryState = d_internal->getSolverState();
}
TheorySets::~TheorySets()
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index bb9423570..879862d15 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -36,14 +36,15 @@ namespace sets {
TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
context::Context* c,
- context::UserContext* u)
+ context::UserContext* u,
+ Valuation valuation)
: d_members(c),
d_deq(c),
d_termProcessed(u),
d_keep(c),
d_full_check_incomplete(false),
d_external(external),
- d_state(*this, c, u),
+ 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)),
@@ -67,7 +68,6 @@ void TheorySetsPrivate::finishInit()
{
d_equalityEngine = d_external.getEqualityEngine();
Assert(d_equalityEngine != nullptr);
- d_state.finishInit(d_equalityEngine);
}
void TheorySetsPrivate::eqNotifyNewClass(TNode t)
@@ -178,7 +178,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
// conflict
Trace("sets-prop")
<< "Propagate eq-mem conflict : " << exp << std::endl;
- d_state.setConflict(exp);
+ d_im.conflict(exp);
return;
}
}
@@ -316,7 +316,7 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp)
{
Trace("sets-prop")
<< "Propagate mem-eq conflict : " << pexp << std::endl;
- d_state.setConflict(pexp);
+ d_im.conflict(pexp);
}
}
}
@@ -1410,7 +1410,7 @@ bool TheorySetsPrivate::propagate(TNode literal)
bool ok = d_external.d_out->propagate(literal);
if (!ok)
{
- d_state.setConflict();
+ d_state.notifyInConflict();
}
return ok;
@@ -1426,7 +1426,7 @@ Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
void TheorySetsPrivate::conflict(TNode a, TNode b)
{
Node conf = explain(a.eqNode(b));
- d_state.setConflict(conf);
+ d_im.conflict(conf);
Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation "
<< conf << std::endl;
Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 27ea6a9b8..9a786598c 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -156,12 +156,16 @@ class TheorySetsPrivate {
*/
TheorySetsPrivate(TheorySets& external,
context::Context* c,
- context::UserContext* u);
+ context::UserContext* u,
+ Valuation valuation);
~TheorySetsPrivate();
TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+ /** Get the solver state */
+ SolverState* getSolverState() { return &d_state; }
+
/**
* Finish initialize, called after the equality engine of theory sets has
* been determined.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback