diff options
Diffstat (limited to 'src/theory/valuation.h')
-rw-r--r-- | src/theory/valuation.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 4ecdecad0..54af14fdd 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -32,6 +32,7 @@ namespace theory { class EntailmentCheckParameters; class EntailmentCheckSideEffects; +class TheoryModel; /** * The status of an equality in the current context. @@ -106,6 +107,11 @@ public: Node getModelValue(TNode var); /** + * Returns pointer to model. + */ + TheoryModel* getModel(); + + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function * is a Node that can be queried via getSatValue(). |