Support for separation logic. Enable cbqi by default for pure BV.

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().