diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-21 10:55:04 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-21 10:55:04 -0600 |
| commit | 25a2af86e7beaa46a8159f87263f605818d14157 (patch) | |
| tree | db007bbf560722287a484327a49d21ed953eb2ff /src/theory/strings/solver_state.h | |
| parent | ba91b6a2dabe7d153b78e6a04e0ef594f033e945 (diff) | |
Split extended functions solver in strings (#3768)
Diffstat (limited to 'src/theory/strings/solver_state.h')
| -rw-r--r-- | src/theory/strings/solver_state.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index cb17e6d1b..28dfbfd09 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 "options/theory_options.h" +#include "theory/theory_model.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" @@ -169,6 +170,8 @@ class SolverState * should currently be a representative of the equality engine of this class. */ EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true); + /** Get pointer to the model object of the Valuation object */ + TheoryModel* getModel() const; /** add endpoints to eqc info * @@ -195,7 +198,6 @@ class SolverState 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; |