From a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Oct 2012 21:59:58 +0000 Subject: fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const. --- src/theory/model.h | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) (limited to 'src/theory/model.h') 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& constantReps, bool evalOnly); public: -- cgit v1.2.3