summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-19 13:36:59 -0500
committerGitHub <noreply@github.com>2020-08-19 13:36:59 -0500
commit31717bf7c014bf1971cabcc9b871de5818278126 (patch)
treed7331da2db605b16b67920990ae6def5db03dfd9 /src/theory/sets
parent466520464a8ed862c3a323bb2fbcc92332d9384b (diff)
Make sets and strings solver states inherit from TheoryState (#4918)
This is towards the new standard for theory solvers. This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager. Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).
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