diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
commit | a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 (patch) | |
tree | 8b95b65fad71aab9b0baee4b6bfc976b731f9502 /src/theory/model.h | |
parent | dba60e91f02ae9ca3c3126c76d79a09c95f95a45 (diff) |
fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const.
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 3c6d8e116..8498b55e1 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -55,18 +55,13 @@ protected: /** * 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 ); + Node getModelValue( TNode n ) const; public: /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) * on this model. */ - Node getValue( TNode n ); + Node getValue( TNode n ) const; /** get existing domain value, with possible exclusions * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude @@ -113,9 +108,9 @@ public: bool areDisequal( Node a, Node b ); public: /** get value function for Exprs. */ - Expr getValue( Expr expr ); + Expr getValue( Expr expr ) const; /** get cardinality for sort */ - Cardinality getCardinality( Type t ); + Cardinality getCardinality( Type t ) const; public: /** print representative debug function */ void printRepresentativeDebug( const char* c, Node r ); @@ -238,7 +233,7 @@ private: return *(*it).second; } -}; +}; /** TheoryEngineModelBuilder class * This model builder will consult all theories in a theory engine for @@ -254,8 +249,6 @@ protected: /** process build model */ virtual void processBuildModel(TheoryModel* m, bool fullModel); - /** choose representative for unconstrained equivalence class */ - virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel); /** normalize representative */ Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); public: |