diff options
Diffstat (limited to 'src/theory/model.h')
| -rw-r--r-- | src/theory/model.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 19415ae7b..7ccbe2fc3 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -22,10 +22,13 @@ #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" +#include "theory/ite_simplifier.h" namespace CVC4 { + namespace theory { + /** Theory Model class * For Model m, should call m.initialize() before using */ @@ -35,8 +38,9 @@ class TheoryModel : public Model protected: /** substitution map for this model */ SubstitutionMap d_substitutions; + ITESimplifier d_iteSimp; public: - TheoryModel( context::Context* c, std::string name, bool enableFuncModels ); + TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine d_equalityEngine; @@ -55,7 +59,7 @@ protected: /** * Get model value function. This function is called by getValue */ - Node getModelValue( TNode n ) const; + Node getModelValue(TNode n, bool hasBoundVars = false) const; public: /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) |