Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 3ee1be530..7157433f9 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -53,10 +53,18 @@ public:
   Node d_true;
   Node d_false;
   mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
+public:  
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
   /** get comments */
   void getComments(std::ostream& out) const;
+private:
+  /** information for separation logic */
+  Node d_sep_heap;
+  Node d_sep_nil_eq;
+public:
+  void setHeapModel( Node h, Node neq );
+  bool getHeapModel( Expr& h, Expr& neq ) const;
 protected:
   /** reset the model */
   virtual void reset();