diff options
23 files changed, 163 insertions, 82 deletions
diff --git a/src/options/sep_options b/src/options/sep_options index fecf4401e..ba10cdefb 100644 --- a/src/options/sep_options +++ b/src/options/sep_options @@ -15,4 +15,10 @@ option sepMinimalRefine --sep-min-refine bool :default false option sepDisequalC --sep-deq-c bool :default true assume cardinality elements are distinct +option sepPreSkolemEmp --sep-pre-skolem-emp bool :default false + eliminate emp constraint at preprocess time + +option sepChildRefine --sep-child-refine bool :default false + child-specific refinements of negated star, positive wand + endmodule diff --git a/src/options/sets_options b/src/options/sets_options index 4c019c039..52a8f78ba 100644 --- a/src/options/sets_options +++ b/src/options/sets_options @@ -5,22 +5,8 @@ module SETS "options/sets_options.h" Sets -option setsPropagate --sets-propagate bool :default true - determines whether to propagate learnt facts to Theory Engine / SAT solver - -option setsEagerLemmas --sets-eager-lemmas bool :default true - add lemmas even at regular effort - -expert-option setsCare1 --sets-care1 bool :default false - generate one lemma at a time for care graph - -option setsPropFull --sets-prop-full bool :default true - additional propagation at full effort - -option setsGuessEmpty --sets-guess-empty int :default 0 - when to guess leaf nodes being empty (0...2 : most aggressive..least aggressive) - -option setsSlowLemmas --sets-slow-lemmas bool :default true +option setsProxyLemmas --sets-proxy-lemmas bool :default false + introduce proxy variables eagerly to shorten lemmas option setsInferAsLemmas --sets-infer-as-lemmas bool :default true send inferences as lemmas diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 46469fb0d..d726b836f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -102,6 +102,7 @@ #include "util/hash.h" #include "util/proof.h" #include "util/resource_manager.h" +#include "options/sep_options.h" using namespace std; using namespace CVC4; @@ -3963,6 +3964,17 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } + if(options::sepPreSkolemEmp()) { + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node prev = d_assertions[i]; + Node next = sep::TheorySepRewriter::preprocess( prev ); + if( next!=prev ){ + d_assertions.replace( i, Rewriter::rewrite( next ) ); + Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl; + Trace("sep-preprocess") << " ...got " << d_assertions[i] << endl; + } + } + } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 9c09371c4..1a0faa021 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -231,7 +231,7 @@ int ModelEngine::checkModel(){ } bool ModelEngine::considerQuantifiedFormula( Node q ) { - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q ); + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) || !d_quantEngine->getModel()->isQuantifierActive( q ) ){ return false; }else{ if( options::fmfEmptySorts() ){ @@ -328,7 +328,7 @@ void ModelEngine::debugPrint( const char* c ){ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); Trace( c ) << " "; - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ + if( !considerQuantifiedFormula( q ) ){ Trace( c ) << "*Inactive* "; }else{ Trace( c ) << " "; diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 6c4ad33db..318442ba5 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -21,7 +21,7 @@ constant SEP_NIL_REF \ variable SEP_NIL "separation nil" -operator SEP_EMP 1 "separation empty heap" +operator SEP_EMP 2 "separation empty heap" operator SEP_PTO 2 "points to relation" operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index e2cd4f9dc..680bd8536 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -265,7 +265,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << std::endl; if( sep_children.empty() ){ TypeEnumerator te_domain( it->first ); - m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain ); + TypeEnumerator te_range( d_loc_to_data_type[it->first] ); + m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range ); }else if( sep_children.size()==1 ){ m_heap = sep_children[0]; }else{ @@ -311,6 +312,7 @@ void TheorySep::check(Effort e) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; + /* if( atom.getKind()==kind::SEP_EMP ){ TypeNode tn = atom[0].getType(); if( d_emp_arg.find( tn )==d_emp_arg.end() ){ @@ -319,6 +321,7 @@ void TheorySep::check(Effort e) { //normalize argument TODO } } + */ TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom; TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null(); bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP; @@ -410,7 +413,6 @@ void TheorySep::check(Effort e) { //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate(); //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn ); - /* TODO? }else if( s_atom.getKind()==kind::SEP_EMP ){ //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) ); Node lem; @@ -427,7 +429,7 @@ void TheorySep::check(Effort e) { } Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl; d_out->lemma( lem ); - */ + }else{ //labeled emp should be rewritten Assert( false ); @@ -546,6 +548,12 @@ void TheorySep::check(Effort e) { if( d_pto_model.find( vv )==d_pto_model.end() ){ Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl; d_pto_model[vv] = s_atom[1]; + + //replace this on pto-model since this term is more relevant + TypeNode vtn = vv.getType(); + if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=d_type_references_all[vtn].end() ){ + d_tmodel[vv] = s_atom[0]; + } } } }else{ @@ -991,7 +999,7 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node return tn1; }else if( n.getKind()==kind::SEP_EMP ){ TypeNode tn = n[0].getType(); - TypeNode tnd; + TypeNode tnd = n[1].getType(); registerRefDataTypes( tn, tnd, atom ); card = 1; visited[n] = card; @@ -1110,6 +1118,8 @@ void TheorySep::initializeBounds() { //must include at least one constant n_emp = 1; } + Trace("sep-bound") << "Card maximums : " << d_card_max[tn] << " " << d_card_max[TypeNode::null()] << std::endl; + Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl; Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl; for( unsigned r=0; r<n_emp; r++ ){ Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" ); @@ -1321,6 +1331,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: std::vector< Node > children; children.resize( n.getNumChildren() ); Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() ); + std::map< int, Node > mvals; 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; int sub_index = itl->first; @@ -1339,6 +1350,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: lbl_mval = d_label_model[sub_lbl].getValue( rtn ); } Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval << std::endl; + mvals[sub_index] = lbl_mval; children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 ); if( children[sub_index].isNull() ){ return Node::null(); @@ -1346,14 +1358,18 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: } Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType())); if( n.getKind()==kind::SEP_STAR ){ + //disjoint contraints + std::vector< Node > conj; + std::vector< Node > bchildren; + bchildren.insert( bchildren.end(), children.begin(), children.end() ); 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 ) ); + bchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) ); } vs.push_back( lbl_mval ); if( vsu.isNull() ){ @@ -1362,11 +1378,32 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval ); } } - children.push_back( vsu.eqNode( lbl ) ); + bchildren.push_back( vsu.eqNode( lbl ) ); - //return the lemma - Assert( children.size()>1 ); - return NodeManager::currentNM()->mkNode( kind::AND, children ); + Assert( bchildren.size()>1 ); + conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) ); + + if( options::sepChildRefine() ){ + //child-specific refinements (TODO: use ?) + for( unsigned i=0; i<children.size(); i++ ){ + std::vector< Node > tchildren; + Node mval = mvals[i]; + tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) ); + tchildren.push_back( children[i] ); + std::vector< Node > rem_children; + for( unsigned j=0; j<children.size(); j++ ){ + if( j!=i ){ + rem_children.push_back( n[j] ); + } + } + std::map< Node, Node > rvisited; + Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children ); + rem = applyLabel( rem, NodeManager::currentNM()->mkNode( kind::SETMINUS, lbl, mval ), rvisited ); + tchildren.push_back( rem ); + conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) ); + } + } + return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj ); }else{ std::vector< Node > wchildren; //disjoint constraints diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 3e74bd61e..48523cd06 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -17,6 +17,8 @@ #include "expr/attribute.h" #include "theory/sep/theory_sep_rewriter.h" +#include "theory/quantifiers/quant_util.h" +#include "options/sep_options.h" namespace CVC4 { namespace theory { @@ -160,18 +162,57 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } - -/* -RewriteResponse TheorySepRewriter::preRewrite(TNode node) { - if( node.getKind()==kind::SEP_EMP ){ - Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl; - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::SEP_EMP, NodeManager::currentNM()->mkConst( true ) ) ); +Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) { + std::map< Node, Node >::iterator it = visited[pol].find( n ); + if( it==visited[pol].end() ){ + Trace("ajr-temp") << "Pre-skolem emp " << n << " with pol " << pol << std::endl; + Node ret = n; + if( n.getKind()==kind::SEP_EMP ){ + if( !pol ){ + TypeNode tnx = n[0].getType(); + TypeNode tny = n[1].getType(); + Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" ); + Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" ); + return NodeManager::currentNM()->mkNode( kind::SEP_STAR, + NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ), + NodeManager::currentNM()->mkConst( true ) ).negate(); + } + }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){ + std::vector< Node > children; + bool childChanged = false; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool newPol, newHasPol; + QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol ); + Node nc = n[i]; + if( newHasPol ){ + nc = preSkolemEmp( n[i], newPol, visited ); + childChanged = childChanged || nc!=n[i]; + } + children.push_back( nc ); + } + if( childChanged ){ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[pol][n] = ret; + return n; }else{ - Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl; - return RewriteResponse(REWRITE_DONE, node); + return it->second; + } +} + +Node TheorySepRewriter::preprocess( Node n ) { + if( options::sepPreSkolemEmp() ){ + bool pol = true; + std::map< bool, std::map< Node, Node > > visited; + n = preSkolemEmp( n, pol, visited ); } + return n; } -*/ + }/* CVC4::theory::sep namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index 02adbebe5..58b79c7fd 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -43,7 +43,10 @@ public: static inline void init() {} static inline void shutdown() {} - +private: + static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ); +public: + static Node preprocess( Node n ); };/* class TheorySepRewriter */ }/* CVC4::theory::sep namespace */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index edf250c4d..51e3fe703 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -262,11 +262,11 @@ bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) { bool conj = (n.getKind()==kind::AND)==polarity; for( unsigned i=0; i<n.getNumChildren(); i++ ){ bool isEnt = isEntailed( n[i], polarity ); - if( isEnt==conj ){ - return conj; + if( isEnt!=conj ){ + return !conj; } } - return !conj; + return conj; }else if( n.isConst() ){ return ( polarity && n==d_true ) || ( !polarity && n==d_false ); } @@ -609,36 +609,30 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { Assert( d_equalityEngine.areEqual( mem[1], eq_set ) ); if( mem[1]!=eq_set ){ Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl; - #if 1 - Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set ); - nmem = Rewriter::rewrite( nmem ); - std::vector< Node > exp; - exp.push_back( mem ); - exp.push_back( mem[1].eqNode( eq_set ) ); - assertInference( nmem, exp, lemmas, "downc" ); - if( d_conflict ){ - return; - } - #else - Node k = getProxy( eq_set ); - Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k ); - if( ee_areEqual( mem, pmem ) ){ + if( !options::setsProxyLemmas() ){ Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set ); nmem = Rewriter::rewrite( nmem ); - d_keep.insert( nmem ); - d_keep.insert( pmem ); - assertFactRec( nmem, pmem, lemmas ); + std::vector< Node > exp; + exp.push_back( mem ); + exp.push_back( mem[1].eqNode( eq_set ) ); + assertInference( nmem, exp, lemmas, "downc" ); + if( d_conflict ){ + return; + } }else{ - Trace("sets-debug") << "...infer proxy membership" << std::endl; - Node exp = NodeManager::currentNM()->mkNode( kind::AND, mem, mem[1].eqNode( eq_set ) ); - d_keep.insert( pmem ); - d_keep.insert( exp ); - assertFactRec( pmem, exp, lemmas ); - } - if( d_conflict ){ - return; + //use proxy set + Node k = getProxy( eq_set ); + Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k ); + Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set ); + nmem = Rewriter::rewrite( nmem ); + std::vector< Node > exp; + if( ee_areEqual( mem, pmem ) ){ + exp.push_back( pmem ); + }else{ + nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem ); + } + assertInference( nmem, exp, lemmas, "downc" ); } - #endif } } } diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 index 3c0e7df32..3f908c3be 100644 --- a/test/regress/regress0/sep/dispose-1.smt2 +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -11,7 +11,7 @@ ;----------------- (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)))) +(assert (not (and (sep (and (emp 0 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) (check-sat) ;(get-model) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 98348f617..17750eaa3 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) -(assert (sep (not (emp l)) (not (emp l)))) +(assert (sep (not (emp l l)) (not (emp l l)))) (assert (pto l l)) (check-sat) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 index 52d99d8c0..e89c0fd30 100644 --- a/test/regress/regress0/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2 @@ -5,7 +5,7 @@ (declare-sort U 0) (declare-fun u () U) -(assert (sep (not (emp u)) (not (emp u)))) +(assert (sep (not (emp u u)) (not (emp u u)))) (assert (forall ((x U) (y U)) (= x y))) diff --git a/test/regress/regress0/sep/finite-witness-sat.smt2 b/test/regress/regress0/sep/finite-witness-sat.smt2 index 93413d950..8aedbfd25 100644 --- a/test/regress/regress0/sep/finite-witness-sat.smt2 +++ b/test/regress/regress0/sep/finite-witness-sat.smt2 @@ -4,7 +4,7 @@ (declare-sort Loc 0) (declare-const l Loc) -(assert (not (emp l))) +(assert (not (emp l l))) (assert (forall ((x Loc) (y Loc)) (not (pto x y)))) diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 index 71fe96d71..679b1e363 100644 --- a/test/regress/regress0/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress0/sep/fmf-nemp-2.smt2 @@ -5,6 +5,6 @@ (declare-fun u1 () U) (declare-fun u2 () U) (assert (not (= u1 u2))) -(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1)) (pto x 0))))) +(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1 0)) (pto x 0))))) ; satisfiable with heap of size 2, model of U of size 3 (check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index a0766a7e0..99d7f9c91 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) -(assert (not (emp 0))) +(assert (not (emp 0 0))) (check-sat) diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 index d71b937fc..9c38fb405 100644 --- a/test/regress/regress0/sep/quant_wand.smt2 +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -5,7 +5,7 @@ (declare-const u Int) -(assert (emp 0)) +(assert (emp 0 0)) (assert (forall ((y Int)) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index 9239fb770..42efae553 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -7,6 +7,6 @@ (declare-fun a () U) (declare-fun b () U) -(assert (emp x)) +(assert (emp x x)) (assert (sep (pto x a) (pto y b))) (check-sat) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 8a46d9fdd..3fa0d0555 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -6,6 +6,8 @@ (declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc))))) +(declare-fun data0 () Node) + (declare-const dv Int) (declare-const v Loc) @@ -15,7 +17,7 @@ (declare-const r Loc) (define-fun ten-tree0 ((x Loc) (d Int)) Bool -(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) +(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0 data0) (= l (as sep.nil Loc))) (and (emp loc0 data0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) (declare-const dy Int) (declare-const y Loc) @@ -23,7 +25,7 @@ (declare-const z Loc) (define-fun ord-tree0 ((x Loc) (d Int)) Bool -(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) +(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0 data0) (= y (as sep.nil Loc))) (and (emp loc0 data0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) ;------- f ------- (assert (= y (as sep.nil Loc))) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index fa0aab591..12aa0a67e 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -6,5 +6,5 @@ (declare-fun u () Int) (declare-fun v () Int) (assert (wand (pto x u) (pto y v))) -(assert (emp 0)) +(assert (emp 0 0)) (check-sat) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 1d799c8c9..dad089f8b 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) -(assert (wand (emp 0) (emp 0))) +(assert (wand (emp 0 0) (emp 0 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index 0db7330d1..b59b53b58 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -2,6 +2,6 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) -(assert (wand (emp x) (pto x 3))) +(assert (wand (emp x x) (pto x 3))) (check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 index cce0f79e3..fa6a83143 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) -(assert (wand (pto x 1) (emp x))) +(assert (wand (pto x 1) (emp x x))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index c9851661a..850be7b97 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) -(assert (emp x)) +(assert (emp x x)) (check-sat) |