diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-26 21:44:22 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-26 21:44:22 +0000 |
commit | c6d2a808e4981f81e4a638d25582e8542e89b716 (patch) | |
tree | c2b7222a92fd1bf967e9074a97643d3bbd80a1e2 /src/theory/model.h | |
parent | c1e936b9cec3d731778b95504770e48c28fd1a65 (diff) |
updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 32 |
1 files changed, 8 insertions, 24 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index adf97df9e..de4d57d2e 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -40,7 +40,7 @@ protected: /** substitution map for this model */ SubstitutionMap d_substitutions; public: - TheoryModel( context::Context* c, std::string name ); + TheoryModel( context::Context* c, std::string name, bool enableFuncModels ); virtual ~TheoryModel(){} /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine d_equalityEngine; @@ -54,15 +54,15 @@ public: protected: /** reset the model */ virtual void reset(); - /** get interpreted value - * This function is called when the value of the node cannot be determined by the theory rewriter - * This should function should return a representative in d_reps - */ - virtual Node getInterpretedValue( TNode n ) = 0; /** * Get model value function. This function is called by getValue */ Node getModelValue( TNode n ); + /** get interpreted value + * This function is called when the value of the node cannot be determined by the theory rewriter + * This should function should return a representative in d_reps + */ + virtual Node getInterpretedValue( TNode n ); public: /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) @@ -125,28 +125,12 @@ public: void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ void printRepresentative( std::ostream& out, Node r ); -}; - -/** Default model class - * The getInterpretedValue function will choose an existing value arbitrarily. - * If none are found, then it will create a new value. - */ -class DefaultModel : public TheoryModel -{ -protected: +public: /** whether function models are enabled */ bool d_enableFuncModels; - /** add term */ - void addTerm( Node n ); -public: - DefaultModel( context::Context* c, std::string name, bool enableFuncModels ); - virtual ~DefaultModel(){} //necessary information for function models std::map< Node, std::vector< Node > > d_uf_terms; std::map< Node, Node > d_uf_models; -public: - void reset(); - Node getInterpretedValue( TNode n ); }; /** TheoryEngineModelBuilder class @@ -159,7 +143,7 @@ protected: /** pointer to theory engine */ TheoryEngine* d_te; /** process build model */ - virtual void processBuildModel( TheoryModel* m, bool fullModel ){} + virtual void processBuildModel( TheoryModel* m, bool fullModel ); /** choose representative for unconstrained equivalence class */ virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); /** normalize representative */ |