diff options
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 */ |