From 730e277a542602f36fc548e8face6b8209b2bb94 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 7 Jul 2016 17:14:56 -0500 Subject: [PATCH] Ensure heap disjointness in sep refinements. --- src/theory/sep/theory_sep.cpp | 34 +++++++++++++++++-- test/regress/regress0/sep/Makefile.am | 3 +- .../regress0/sep/split-find-unsat.smt2 | 4 +-- test/regress/regress0/sep/wand-false.smt2 | 7 ++++ .../regress0/sep/wand-nterm-simp2.smt2 | 3 +- test/regress/regress0/sep/wand-simp-sat2.smt2 | 3 +- 6 files changed, 46 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/sep/wand-false.smt2 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; jmkNode( 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) -- 2.30.2