diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-06 17:12:29 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-06 15:12:29 -0800 |
commit | cbd86eb4ed8bafc17f28244b746a376a019462f1 (patch) | |
tree | 69abc6102e61036f9e60c8276f350d68eaecb931 /src/theory/strings/solver_state.h | |
parent | bef9df667e2788cab327b0c8c6590ba833297670 (diff) |
Move more string utility functions (#3398)
This is work towards splitting a "core solver" object from TheoryStrings.
This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.
It also corrects an issue where we were maintaining two `d_conflict` fields.
Diffstat (limited to 'src/theory/strings/solver_state.h')
-rw-r--r-- | src/theory/strings/solver_state.h | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index f14b4b4af..a2001bb3b 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -23,6 +23,7 @@ #include "context/context.h" #include "expr/node.h" #include "theory/uf/equality_engine.h" +#include "theory/valuation.h" namespace CVC4 { namespace theory { @@ -87,7 +88,7 @@ class EqcInfo class SolverState { public: - SolverState(context::Context* c, eq::EqualityEngine& ee); + SolverState(context::Context* c, eq::EqualityEngine& ee, Valuation& v); ~SolverState(); //-------------------------------------- equality information /** @@ -166,12 +167,28 @@ class SolverState * for some eqc that is currently equal to z. */ void addEndpointsToEqcInfo(Node t, Node concat, Node eqc); + /** Entailment check + * + * This calls entailmentCheck on the Valuation object of theory of strings. + */ + std::pair<bool, Node> entailmentCheck(TheoryOfMode mode, TNode lit); + /** Separate by length + * + * Separate the string representatives in argument n into a partition cols + * whose collections have equal length. The i^th vector in cols has length + * lts[i] for all elements in col. + */ + void separateByLength(const std::vector<Node>& n, + std::vector<std::vector<Node> >& cols, + std::vector<Node>& lts); private: /** Pointer to the SAT context object used by the theory of strings. */ context::Context* d_context; /** Reference to equality engine of the theory of strings. */ eq::EqualityEngine& d_ee; + /** Reference to the valuation of the theory of strings */ + Valuation& d_valuation; /** Are we in conflict? */ context::CDO<bool> d_conflict; /** The pending conflict if one exists */ |