Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.

7 files changed, 59 insertions, 43 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 2dc3aebe5..aa5634e7a 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -943,7 +943,9 @@ Expr ExprManager::mkBoundVar(Type type) {
 
 Expr ExprManager::mkSepNil(Type type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
+  Node n = d_nodeManager->mkSepNil(*type.d_typeNode); 
+  return n.toExpr();
+  //return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
 }
 
 Expr ExprManager::mkAssociative(Kind kind,
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d2ac7e2a1..94b136c46 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -169,6 +169,8 @@ NodeManager::~NodeManager() {
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
     d_operators[i] = Node::null();
   }
+  
+  d_sep_nils.clear();
 
   //d_tupleAndRecordTypes.clear();
   d_tt_cache.d_children.clear();
@@ -682,17 +684,16 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
 }
 
 Node NodeManager::mkSepNil(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::SEP_NIL);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
-  return n;
-}
-
-Node* NodeManager::mkSepNilPtr(const TypeNode& type) {
-  Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  return n;
+  std::map< TypeNode, Node >::iterator it = d_sep_nils.find( type );
+  if( it==d_sep_nils.end() ){
+    Node n = NodeBuilder<0>(this, kind::SEP_NIL);
+    n.setAttribute(TypeAttr(), type);
+    n.setAttribute(TypeCheckedAttr(), true);
+    d_sep_nils[type] = n;
+    return n;
+  }else{
+    return it->second;
+  }
 }
 
 Node NodeManager::mkAbstractValue(const TypeNode& type) {
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);
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index eefc0e779..fcf5ec88d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -267,20 +267,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){
 void TheorySep::presolve() {
   Trace("sep-pp") << "Presolving" << std::endl;
   //TODO: cleanup if incremental?
-  
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_pp_nils.begin(); it != d_pp_nils.end(); ++it ){
-    Trace("sep-pp") << it->second.size() << " nil references of type " << it->first << std::endl;
-    if( !it->second.empty() ){
-      setNilRef( it->first, it->second[0] );
-      //ensure all instances of sep.nil are made equal
-      for( unsigned i=1; i<it->second.size(); i++ ){
-        Node lem = NodeManager::currentNM()->mkNode( it->first.isBoolean() ? kind::IFF : kind::EQUAL, it->second[i], it->second[0] );
-        Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl;
-        d_out->lemma( lem );
-      }
-    }
-  }
-  d_pp_nils.clear();
 }
 
 
@@ -784,7 +770,6 @@ TypeNode TheorySep::getDataType( Node n ) {
 
 //must process assertions at preprocess so that quantified assertions are processed properly
 void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) {
-  d_pp_nils.clear();
   std::map< Node, bool > visited;
   for( unsigned i=0; i<assertions.size(); i++ ){
     Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl;
@@ -803,12 +788,8 @@ void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) {
 void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()==kind::SEP_NIL ){
-      TypeNode tn = n.getType();
-      if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){
-        d_pp_nils[tn].push_back( n );
-      }
-    }else if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
+    Trace("sep-pp-debug") << "process assertion : " << n << std::endl;
+    if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
       //get the reference type (will compute d_type_references)
       int card = 0;
       TypeNode tn = computeReferenceType( n, card );
@@ -822,7 +803,7 @@ void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
 }
 
 TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) {
-  Trace("sep-type") << "getReference type " << atom << " " << index << std::endl;
+  Trace("sep-pp-debug") << "getReference type " << atom << " " << index << std::endl;
   Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 );
   std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
   if( it==d_reference_type[atom].end() ){
@@ -878,7 +859,7 @@ TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) {
 
 TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) {
   if( visited.find( n )==visited.end() ){
-    Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl;
+    Trace("sep-pp-debug") << "visit : " << n << " : " << atom << " " << index << std::endl;
     visited[n] = -1;
     if( n.getKind()==kind::SEP_PTO ){
       //TODO: when THEORY_SETS supports mixed Int/Real sets
@@ -926,9 +907,6 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
       TypeNode tn = n.getType();
       TypeNode tnd;
       registerRefDataTypes( tn, tnd, n );
-      if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){
-        d_pp_nils[tn].push_back( n );
-      }
       return tn;
     }else{
       card = 0;
@@ -1095,6 +1073,23 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
       //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
       //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
       //d_out->lemma( slem );
+      
+      //symmetry breaking
+      std::map< unsigned, Node > lit_mem_map;
+      for( unsigned i=0; i<d_type_references_card[tn].size(); i++ ){
+        lit_mem_map[i] = NodeManager::currentNM()->mkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound[tn]);
+      }
+      for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){
+        std::vector< Node > children;
+        for( unsigned j=(i+1); j<d_type_references_card[tn].size(); j++ ){
+          children.push_back( lit_mem_map[j].negate() );
+        }
+        Assert( !children.empty() );
+        Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children );
+        sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem );
+        Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl;
+        d_out->lemma( sym_lem );
+      }
     }
     
     //assert that nil ref is not in base label
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 4f60c5781..a7ca3aff3 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -53,8 +53,6 @@ class TheorySep : public Theory {
   
   //whether bounds have been initialized
   bool d_bounds_init;
-  
-  std::map< TypeNode, std::vector< Node > > d_pp_nils;
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 7bcd700bd..b43a9a570 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -57,7 +57,8 @@ TESTS =	\
   trees-1.smt2 \
   wand-false.smt2 \
   dup-nemp.smt2 \
-  emp2-quant-unsat.smt2
+  emp2-quant-unsat.smt2 \
+  dispose-1.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
new file mode 100644
index 000000000..3c0e7df32
--- /dev/null
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -0,0 +1,17 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const w Int)
+(declare-const w1 Int)
+(declare-const w2 Int)
+
+;------- f -------
+(assert (= w1 (as sep.nil Int)))
+(assert (= w2 (as sep.nil Int)))
+;-----------------
+
+(assert (pto w (as sep.nil Int)))
+(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+
+(check-sat)
+;(get-model)