summaryrefslogtreecommitdiff
path: root/src/theory/model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/model.h')
-rw-r--r--src/theory/model.h10
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback