diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-10 22:29:17 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-10 22:29:17 +0000 |
commit | 680af6f4dc9e5d6616918e8fde18cd64774d0df5 (patch) | |
tree | 5ec89cf302d5bc93ff1da80efa2125152d1c71b6 /src/theory/model.h | |
parent | 586b07613702027fc685e55994e2a325961ca5b7 (diff) |
modified getValue to return Expr instead of Node
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 086e39f3e..06618e07c 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -70,11 +70,6 @@ protected: */ Node getModelValue( TNode n ); public: - /** - * Get value function. This should be called only after a ModelBuilder has called buildModel(...) - * on this model. - */ - Node getValue( TNode n ); /** 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,12 +108,15 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); public: + /** get value function */ + Expr getValue( const Expr& expr ); + /** to stream function */ + void toStream( std::ostream& out ); +public: /** print representative debug function */ void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ void printRepresentative( std::ostream& out, Node r ); - /** to stream function */ - void toStream( std::ostream& out ); }; /** Default model class |