diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-16 13:32:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-16 13:32:42 -0500 |
commit | 7c249b3efdeeb51fd3dfc2571bc529c55880cf5c (patch) | |
tree | 220a1c3f2aa53b047c2a52260fce3bd2dce22429 /src/theory/theory_model.h | |
parent | 547df7cd146091674562dfa4812f10bae7765934 (diff) |
Refactor SMT-level model object (#5277)
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.
Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.
This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 9f330ff6c..e8665bb83 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -20,7 +20,6 @@ #include <unordered_map> #include <unordered_set> -#include "smt/model.h" #include "theory/ee_setup_info.h" #include "theory/rep_set.h" #include "theory/substitutions.h" @@ -76,12 +75,12 @@ namespace theory { * above functions such as getRepresentative() when assigning total * interpretations for uninterpreted functions. */ -class TheoryModel : public Model +class TheoryModel { friend class TheoryEngineModelBuilder; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); - ~TheoryModel() override; + virtual ~TheoryModel(); /** * Finish init, where ee is the equality engine the model should use. */ @@ -295,23 +294,21 @@ public: */ Node getValue(TNode n) const; /** get comments */ - void getComments(std::ostream& out) const override; + void getComments(std::ostream& out) const; //---------------------------- separation logic /** set the heap and value sep.nil is equal to */ void setHeapModel(Node h, Node neq); /** get the heap and value sep.nil is equal to */ bool getHeapModel(Node& h, Node& neq) const; - /** get the heap and value sep.nil is equal to */ - bool getHeapModel(Expr& h, Expr& neq) const override; //---------------------------- end separation logic /** is the list of approximations non-empty? */ - bool hasApproximations() const override; + bool hasApproximations() const; /** get approximations */ - std::vector<std::pair<Expr, Expr> > getApproximations() const override; + std::vector<std::pair<Node, Node> > getApproximations() const; /** get domain elements for uninterpreted sort t */ - std::vector<Expr> getDomainElements(Type t) const override; + std::vector<Node> getDomainElements(TypeNode t) const; /** get the representative set object */ const RepSet* getRepSet() const { return &d_rep_set; } /** get the representative set object (FIXME: remove this, see #1199) */ @@ -319,17 +316,15 @@ public: //---------------------------- model cores /** set using model core */ - void setUsingModelCore() override; + void setUsingModelCore(); /** record model core symbol */ - void recordModelCoreSymbol(Expr sym) override; + void recordModelCoreSymbol(Node sym); /** Return whether symbol expr is in the model core. */ - bool isModelCoreSymbol(Expr sym) const override; + bool isModelCoreSymbol(Node sym) const; //---------------------------- end model cores - /** get value function for Exprs. */ - Expr getValue(Expr expr) const override; /** get cardinality for sort */ - Cardinality getCardinality(Type t) const override; + Cardinality getCardinality(TypeNode t) const; //---------------------------- function values /** a map from functions f to a list of all APPLY_UF terms with operator f */ |