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