diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 13:43:02 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 13:43:02 -0500 |
commit | 442c809911bcc45ae45dc97650146c459a841ea3 (patch) | |
tree | 1a08cc6448314cc494d63414d8b47713afa5ebf0 /src/expr/node_manager.h | |
parent | 14fb8fac59e368a36e936a2d0497745eda72c637 (diff) |
Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index dcd7005f8..79c7320f7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -157,6 +157,9 @@ class NodeManager { * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; + + /** sep nil per type */ + std::map< TypeNode, Node > d_sep_nils; /** * A list of subscribers for NodeManager events. @@ -487,9 +490,8 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - /** Create nil reference for separation logic with the given type. */ + /** Create nil reference for separation logic with the given type (unique per type). */ Node mkSepNil(const TypeNode& type); - Node* mkSepNilPtr(const TypeNode& type); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); |