Ensure heap disjointness in sep refinements.

6 files changed, 46 insertions, 8 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index be0af4929..d9416fbc6 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -747,8 +747,7 @@ void TheorySep::check(Effort e) {
                   pol_atom = atom.negate();
                 }
                 lemc.push_back( pol_atom );
-                //TODO: add disjointness assumption
-                
+
                 //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() );
                 //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() );
                 lemc.insert( lemc.end(), conc.begin(), conc.end() );
@@ -1165,11 +1164,40 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             return Node::null();
           }
         }
+        Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
         if( n.getKind()==kind::SEP_STAR ){
+          //disjoint contraints
+          Node vsu;
+          std::vector< Node > vs;
+          for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
+            Node sub_lbl = itl->second;
+            Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
+            for( unsigned j=0; j<vs.size(); j++ ){
+              children.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
+            }
+            vs.push_back( lbl_mval );
+            if( vsu.isNull() ){
+              vsu = lbl_mval;
+            }else{
+              vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval );
+            }
+          }
+          children.push_back( vsu.eqNode( lbl ) );
+          
+          //return the lemma
           Assert( children.size()>1 );
           return NodeManager::currentNM()->mkNode( kind::AND, children );      
         }else{
-          return NodeManager::currentNM()->mkNode( kind::OR, children[0].negate(), children[1] );
+          std::vector< Node > wchildren;
+          //disjoint constraints
+          Node sub_lbl_0 = d_label_map[n][lbl][0];
+          Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
+          wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() );
+          
+          //return the lemma
+          wchildren.push_back( children[0].negate() );
+          wchildren.push_back( children[1] );
+          return NodeManager::currentNM()->mkNode( kind::OR, wchildren );
         }
       }else{
         //nested star/wand, label it and return
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 9744cae99..d72e02d97 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -54,7 +54,8 @@ TESTS =	\
   wand-0526-sat.smt2 \
   quant_wand.smt2 \
   fmf-nemp-2.smt2 \
-  trees-1.smt2
+  trees-1.smt2 \
+  wand-false.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2
index 54530cbf4..1731174fa 100644
--- a/test/regress/regress0/sep/split-find-unsat.smt2
+++ b/test/regress/regress0/sep/split-find-unsat.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --no-check-models
-; EXPECT: sat
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
-(set-info :status sat)
+(set-info :status unsat)
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2
new file mode 100644
index 000000000..642c0a8aa
--- /dev/null
+++ b/test/regress/regress0/sep/wand-false.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun x () Int)
+(assert (wand (pto x x) false))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2
index 69305e95c..c317e8736 100644
--- a/test/regress/regress0/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --no-check-models
-; EXPECT: unsat
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
+(set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (emp x)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2
index ebc115fdd..059e91317 100755
--- a/test/regress/regress0/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat2.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --no-check-models
-; EXPECT: unsat
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
+(set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
 (check-sat)