diff options
author | Tim King <taking@cs.nyu.edu> | 2012-09-11 00:20:51 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-09-11 00:20:51 +0000 |
commit | d8883776ce80199096f99d1088910d478fd0cd6e (patch) | |
tree | 1425084ba75c36b00656c74d59dd8ebf5bf88a1a /src/theory/model.h | |
parent | 680af6f4dc9e5d6616918e8fde18cd64774d0df5 (diff) |
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 06618e07c..ea1fa0fed 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -70,6 +70,12 @@ 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 */ @@ -108,8 +114,10 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); public: - /** get value function */ + /** get value function for Exprs. */ Expr getValue( const Expr& expr ); + + /** to stream function */ void toStream( std::ostream& out ); public: |