From a97944b850f201fd692aa870e830b8fa0369c541 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 9 Sep 2016 14:14:09 -0500 Subject: [PATCH] Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions. --- src/options/quantifiers_options | 2 +- src/options/sep_options | 2 - src/smt/smt_engine.cpp | 1 + src/theory/quantifiers_engine.cpp | 11 +- src/theory/sep/theory_sep.cpp | 214 ++++++++++-------- src/theory/sep/theory_sep.h | 12 +- test/regress/regress0/sep/Makefile.am | 3 +- test/regress/regress0/sep/chain-int.smt2 | 2 +- test/regress/regress0/sep/crash1220.smt2 | 2 +- .../regress0/sep/dispose-list-4-init.smt2 | 2 +- test/regress/regress0/sep/dup-nemp.smt2 | 2 +- .../regress0/sep/emp2-quant-unsat.smt2 | 12 + test/regress/regress0/sep/loop-1220.smt2 | 2 +- test/regress/regress0/sep/nemp.smt2 | 2 +- test/regress/regress0/sep/nspatial-simp.smt2 | 2 +- test/regress/regress0/sep/pto-01.smt2 | 2 +- test/regress/regress0/sep/pto-02.smt2 | 2 +- test/regress/regress0/sep/pto-04.smt2 | 2 +- test/regress/regress0/sep/sep-01.smt2 | 2 +- test/regress/regress0/sep/sep-02.smt2 | 2 +- test/regress/regress0/sep/sep-03.smt2 | 2 +- test/regress/regress0/sep/sep-find2.smt2 | 2 +- .../regress/regress0/sep/sep-neg-1refine.smt2 | 2 +- .../regress/regress0/sep/sep-neg-nstrict.smt2 | 2 +- .../regress0/sep/sep-neg-nstrict2.smt2 | 2 +- test/regress/regress0/sep/sep-neg-simple.smt2 | 2 +- test/regress/regress0/sep/sep-neg-swap.smt2 | 2 +- .../regress/regress0/sep/sep-nterm-again.smt2 | 2 +- .../regress0/sep/sep-nterm-val-model.smt2 | 2 +- test/regress/regress0/sep/sep-plus1.smt2 | 2 +- test/regress/regress0/sep/sep-simp-unc.smt2 | 2 +- .../regress0/sep/sep-simp-unsat-emp.smt2 | 2 +- test/regress/regress0/sep/simple-neg-sat.smt2 | 2 +- .../regress0/sep/split-find-unsat-w-emp.smt2 | 2 +- .../regress0/sep/split-find-unsat.smt2 | 2 +- test/regress/regress0/sep/wand-0526-sat.smt2 | 2 +- test/regress/regress0/sep/wand-crash.smt2 | 2 +- test/regress/regress0/sep/wand-false.smt2 | 2 +- .../regress/regress0/sep/wand-nterm-simp.smt2 | 2 +- .../regress0/sep/wand-nterm-simp2.smt2 | 2 +- test/regress/regress0/sep/wand-simp-sat.smt2 | 2 +- test/regress/regress0/sep/wand-simp-sat2.smt2 | 2 +- .../regress/regress0/sep/wand-simp-unsat.smt2 | 2 +- 43 files changed, 179 insertions(+), 148 deletions(-) create mode 100644 test/regress/regress0/sep/emp2-quant-unsat.smt2 diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 462995bec..606e33d75 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -310,7 +310,7 @@ option cbqiInnermost --cbqi-innermost bool :read-write :default true option cbqiNestedQE --cbqi-nested-qe bool :default false process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation -option quantEpr --quant-epr bool :default false +option quantEpr --quant-epr bool :default false :read-write infer whether in effectively propositional fragment, use for cbqi ### local theory extensions options diff --git a/src/options/sep_options b/src/options/sep_options index 043355bda..fecf4401e 100644 --- a/src/options/sep_options +++ b/src/options/sep_options @@ -12,8 +12,6 @@ option sepExp --sep-exp bool :default false experimental flag for sep option sepMinimalRefine --sep-min-refine bool :default false only add refinement lemmas for minimal (innermost) assertions -option sepPreciseBound --sep-prec-bound bool :default false - calculate precise bounds for labels option sepDisequalC --sep-deq-c bool :default true assume cardinality elements are distinct diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9c8838113..93e62f79d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1690,6 +1690,7 @@ void SmtEngine::setDefaults() { //disable modes not supported by incremental options::sortInference.set( false ); options::ufssFairnessMonotone.set( false ); + options::quantEpr.set( false ); } if( d_logic.hasCardinalityConstraints() ){ //must have finite model finding on diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 316357ef2..7c1fd82d3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -19,6 +19,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" +#include "theory/sep/theory_sep.h" #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/bounded_integers.h" @@ -113,11 +114,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* } if( options::quantEpr() ){ - if( !options::incrementalSolving() ){ - d_qepr = new QuantEPR; - }else{ - d_qepr = NULL; - } + Assert( !options::incrementalSolving() ); + d_qepr = new QuantEPR; }else{ d_qepr = NULL; } @@ -367,6 +365,9 @@ void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) { } } if( d_qepr!=NULL ){ + //must handle sources of other new constants e.g. separation logic + //FIXME: cleanup + ((sep::TheorySep*)getTheoryEngine()->theoryOf( THEORY_SEP ))->initializeBounds(); d_qepr->finishInit(); } } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 8ab92368a..eefc0e779 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -26,6 +26,7 @@ #include "smt/logic_exception.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" +#include "options/quantifiers_options.h" using namespace std; @@ -45,6 +46,7 @@ TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + d_bounds_init = false; // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::SEP_PTO); @@ -126,43 +128,6 @@ void TheorySep::explain(TNode literal, std::vector& assumptions) { } } -void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) { - if( visited.find( t )==visited.end() ){ - visited[t] = true; - Trace("sep-prereg-debug") << "Preregister : " << t << std::endl; - if( t.getKind()==kind::SEP_NIL ){ - Trace("sep-prereg") << "Preregister nil : " << t << std::endl; - //per type, all nil variable references are equal - TypeNode tn = t.getType(); - std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); - if( it==d_nil_ref.end() ){ - Trace("sep-prereg") << "...set as reference." << std::endl; - setNilRef( tn, t ); - }else{ - Node nr = it->second; - Trace("sep-prereg") << "...reference is " << nr << "." << std::endl; - if( t!=nr ){ - if( d_reduce.find( t )==d_reduce.end() ){ - d_reduce.insert( t ); - Node lem = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, t, nr ); - Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl; - d_out->lemma( lem ); - } - } - } - }else{ - for( unsigned i=0; i visited; - preRegisterTermRec( term, visited ); -} - void TheorySep::propagate(Effort e){ @@ -234,14 +199,12 @@ void TheorySep::computeCareGraph() { ///////////////////////////////////////////////////////////////////////////// -void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) -{ +void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){ // Send the equality engine information to the model m->assertEqualityEngine( &d_equalityEngine ); - } -void TheorySep::postProcessModel(TheoryModel* m) { +void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "Printing model for TheorySep..." << std::endl; std::vector< Node > sep_children; @@ -253,11 +216,9 @@ void TheorySep::postProcessModel(TheoryModel* m) { Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() ); Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl; TypeEnumerator te_range( d_loc_to_data_type[it->first] ); - //m->d_comment_str << "Model for heap, type = " << it->first << " : " << std::endl; computeLabelModel( it->second, d_tmodel ); if( d_label_model[it->second].d_heap_locs_model.empty() ){ Trace("sep-model") << " [empty]" << std::endl; - //m->d_comment_str << " [empty]" << std::endl; }else{ for( unsigned j=0; jsecond].d_heap_locs_model.size(); j++ ){ Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON ); @@ -266,20 +227,17 @@ void TheorySep::postProcessModel(TheoryModel* m) { Assert( l.isConst() ); pto_children.push_back( l ); Trace("sep-model") << " " << l << " -> "; - //m->d_comment_str << " " << l << " -> "; if( d_pto_model[l].isNull() ){ Trace("sep-model") << "_"; //m->d_comment_str << "_"; pto_children.push_back( *te_range ); }else{ Trace("sep-model") << d_pto_model[l]; - //m->d_comment_str << d_pto_model[l]; Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] ); Assert( vpto.isConst() ); pto_children.push_back( vpto ); } Trace("sep-model") << std::endl; - //m->d_comment_str << std::endl; sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) ); } } @@ -288,8 +246,6 @@ void TheorySep::postProcessModel(TheoryModel* m) { m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil ); Trace("sep-model") << "sep.nil = " << vnil << std::endl; Trace("sep-model") << std::endl; - //m->d_comment_str << "sep.nil = " << vnil << std::endl; - //m->d_comment_str << std::endl; if( sep_children.empty() ){ TypeEnumerator te_domain( it->first ); m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain ); @@ -299,8 +255,6 @@ void TheorySep::postProcessModel(TheoryModel* m) { m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children ); } m->setHeapModel( m_heap, m_neq ); - //m->d_comment_str << m->d_sep_heap << std::endl; - //m->d_comment_str << m->d_sep_nil_eq << std::endl; } Trace("sep-model") << "Finished printing model for TheorySep." << std::endl; } @@ -314,10 +268,17 @@ void TheorySep::presolve() { Trace("sep-pp") << "Presolving" << std::endl; //TODO: cleanup if incremental? - //we must preregister all instances of sep.nil to ensure they are made equal - for( unsigned i=0; i visited; - preRegisterTermRec( d_pp_nils[i], visited ); + 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; isecond.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(); } @@ -392,28 +353,6 @@ void TheorySep::check(Effort e) { TypeNode tn = getReferenceType( s_atom ); Assert( d_reference_bound.find( tn )!=d_reference_bound.end() ); c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound[tn] ) ); - if( options::sepPreciseBound() ){ - //more precise bound - Trace("sep-bound") << "Propagate Bound(" << s_lbl << ") = "; - Assert( d_lbl_reference_bound.find( s_lbl )!=d_lbl_reference_bound.end() ); - for( unsigned j=0; j bound_loc; - bound_loc.insert( bound_loc.end(), d_references[s_atom][j].begin(), d_references[s_atom][j].end() ); - //carry all locations for now - bound_loc.insert( bound_loc.end(), d_lbl_reference_bound[s_lbl].begin(), d_lbl_reference_bound[s_lbl].end() ); - //Trace("sep-bound") << std::endl; - Node bound_v = mkUnion( tn, bound_loc ); - Trace("sep-bound") << " ...bound value : " << bound_v << std::endl; - children.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, c_lbl, bound_v ) ); - } - Trace("sep-bound") << "Done propagate Bound(" << s_lbl << ")" << std::endl; - } std::vector< Node > labels; getLabelChildren( s_atom, s_lbl, children, labels ); Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())); @@ -845,10 +784,10 @@ TypeNode TheorySep::getDataType( Node n ) { //must process assertions at preprocess so that quantified assertions are processed properly void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - //dummy sort in case heap loc/data is unconstrained d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; if( n.getKind()==kind::SEP_NIL ){ - if( std::find( d_pp_nils.begin(), d_pp_nils.end(), n )==d_pp_nils.end() ){ - d_pp_nils.push_back( n ); + 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 ){ //get the reference type (will compute d_type_references) @@ -887,7 +827,7 @@ TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index ); if( it==d_reference_type[atom].end() ){ card = 0; - TypeNode tn; + TypeNode tn; if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){ for( unsigned i=0; i::iterator itt = d_loc_to_data_type.find( tn1 ); if( itt==d_loc_to_data_type.end() ){ if( !d_loc_to_data_type.empty() ){ @@ -1035,9 +995,55 @@ void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){ } } +void TheorySep::initializeBounds() { + if( !d_bounds_init ){ + Trace("sep-bound") << "Initialize sep bounds..." << std::endl; + d_bounds_init = true; + for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ + TypeNode tn = it->first; + Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; + QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL; + //if pto had free variable reference + if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ + if( d_reference_bound_fv.find( tn )!=d_reference_bound_fv.end() ){ + //include Herbrand universe of tn + if( qepr && qepr->isEPR( tn ) ){ + for( unsigned j=0; jd_consts[tn].size(); j++ ){ + Node k = qepr->d_consts[tn][j]; + if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){ + d_type_references[tn].push_back( k ); + } + } + }else{ + d_reference_bound_invalid[tn] = true; + Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl; + } + } + } + unsigned n_emp = 0; + if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ + n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()]; + }else if( d_type_references[tn].empty() ){ + //must include at least one constant + n_emp = 1; + } + Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl; + for( unsigned r=0; rmkSkolem( "e", tn, "cardinality bound element for seplog" ); + d_type_references_card[tn].push_back( e ); + //must include this constant back into EPR handling + if( qepr && qepr->isEPR( tn ) ){ + qepr->d_consts[tn].push_back( e ); + } + } + } + } +} + Node TheorySep::getBaseLabel( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_base_label.find( tn ); if( it==d_base_label.end() ){ + initializeBounds(); Trace("sep") << "Make base label for " << tn << std::endl; std::stringstream ss; ss << "__Lb"; @@ -1051,35 +1057,45 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { ss2 << "__Lu"; d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" ); d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() ); + + //check whether monotonic (elements can be added to tn without effecting satisfiability) + bool tn_is_monotonic = true; + if( tn.isSort() ){ + //TODO: use monotonicity inference + tn_is_monotonic = !getLogicInfo().isQuantified(); + }else{ + tn_is_monotonic = tn.getCardinality().isInfinite(); + } //add a reference type for maximum occurrences of empty in a constraint - unsigned n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()]; - for( unsigned r=0; rmkSkolem( "e", tn, "cardinality bound element for seplog" ); - //d_type_references_all[tn].push_back( NodeManager::currentNM()->mkSkolem( "e", NodeManager::currentNM()->mkRefType(tn) ) ); - if( options::sepDisequalC() ){ + if( options::sepDisequalC() && tn_is_monotonic ){ + for( unsigned r=0; rmkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] ); d_out->lemma( eq.negate() ); } + d_type_references_all[tn].push_back( e ); } - d_type_references_all[tn].push_back( e ); - d_lbl_reference_bound[d_base_label[tn]].push_back( e ); + }else{ + //break symmetries TODO + + d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() ); } - //construct bound - d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] ); - Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl; + Assert( !d_type_references_all[tn].empty() ); + + if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ + //construct bound + d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] ); + Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl; - if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_reference_bound[tn], d_reference_bound_max[tn] ); Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl; d_out->lemma( slem ); - }else{ - Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl; + //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 ); } - //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 ); //assert that nil ref is not in base label Node nr = getNilRef( tn ); @@ -1373,7 +1389,6 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) { Assert( false ); } } - //end hack for( unsigned j=0; j& tmodel ) { //TypeNode tn = u.getType().getRefConstituentType(); TypeNode tn = u.getType(); Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl; - Assert( d_type_references_all.find( tn )!=d_type_references_all.end() && !d_type_references_all[tn].empty() ); + Assert( d_type_references_all.find( tn )!=d_type_references_all.end() ); + Assert( !d_type_references_all[tn].empty() ); tt = d_type_references_all[tn][0]; }else{ tt = itm->second; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 32aa065b7..4f60c5781 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -51,7 +51,10 @@ class TheorySep : public Theory { /** True node for predicates = false */ Node d_false; - std::vector< Node > d_pp_nils; + //whether bounds have been initialized + bool d_bounds_init; + + std::map< TypeNode, std::vector< Node > > d_pp_nils; Node mkAnd( std::vector< TNode >& assumptions ); @@ -88,10 +91,8 @@ class TheorySep : public Theory { /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector& assumptions); - void preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ); public: - void preRegisterTerm(TNode t); void propagate(Effort e); Node explain(TNode n); @@ -220,11 +221,11 @@ class TheorySep : public Theory { std::map< TypeNode, Node > d_reference_bound; std::map< TypeNode, Node > d_reference_bound_max; std::map< TypeNode, bool > d_reference_bound_invalid; + std::map< TypeNode, bool > d_reference_bound_fv; std::map< TypeNode, std::vector< Node > > d_type_references; + std::map< TypeNode, std::vector< Node > > d_type_references_card; std::map< TypeNode, std::vector< Node > > d_type_references_all; std::map< TypeNode, unsigned > d_card_max; - //bounds for labels - std::map< Node, std::vector< Node > > d_lbl_reference_bound; //for empty argument std::map< TypeNode, Node > d_emp_arg; //map from ( atom, label, child index ) -> label @@ -299,6 +300,7 @@ public: return &d_equalityEngine; } + void initializeBounds(); };/* class TheorySep */ }/* CVC4::theory::sep namespace */ diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 6078bfa19..7bcd700bd 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ fmf-nemp-2.smt2 \ trees-1.smt2 \ wand-false.smt2 \ - dup-nemp.smt2 + dup-nemp.smt2 \ + emp2-quant-unsat.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 index d3245e33f..ebe52fa46 100644 --- a/test/regress/regress0/sep/chain-int.smt2 +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 index a0fc5a187..f68434f33 100755 --- a/test/regress/regress0/sep/crash1220.smt2 +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 index 766354cd9..b3e2088b1 100644 --- a/test/regress/regress0/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 009561128..98348f617 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 new file mode 100644 index 000000000..52d99d8c0 --- /dev/null +++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --quant-epr +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun u () U) + +(assert (sep (not (emp u)) (not (emp u)))) + +(assert (forall ((x U) (y U)) (= x y))) + +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 index 2981606d8..b857aec2a 100644 --- a/test/regress/regress0/sep/loop-1220.smt2 +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index e1e21dd10..a0766a7e0 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 ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (not (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 index 0c93719c9..c807757d1 100755 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index b0dece248..28ed5c47b 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index f0b6d2dee..ab1cea0c8 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 index 1734c93bb..9b0afda7a 100644 --- a/test/regress/regress0/sep/pto-04.smt2 +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index c3330f036..a93fc4db8 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 index 403bcf077..6f190d964 100644 --- a/test/regress/regress0/sep/sep-02.smt2 +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 index 427c44b50..8dce5acc7 100644 --- a/test/regress/regress0/sep/sep-03.smt2 +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 index 26a27eb22..356f866c1 100644 --- a/test/regress/regress0/sep/sep-find2.smt2 +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 index 8ddbdd05f..ab12c6461 100644 --- a/test/regress/regress0/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 index 1a69336a8..425e5ce3c 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 index e71e6a51a..7ada6ff06 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 index 191e7527f..7b6fc69e9 100644 --- a/test/regress/regress0/sep/sep-neg-simple.smt2 +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 index f89a9c0ac..53f890b0d 100644 --- a/test/regress/regress0/sep/sep-neg-swap.smt2 +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 index 9b4afe36a..3e595b5e9 100644 --- a/test/regress/regress0/sep/sep-nterm-again.smt2 +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 index 0178134cb..d4fb0fd52 100644 --- a/test/regress/regress0/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index 772acd981..9522e2420 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 index 6cdf51294..cedbb53eb 100755 --- a/test/regress/regress0/sep/sep-simp-unc.smt2 +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) (declare-fun x () U) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index fb58b9d10..9239fb770 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 index 0c0b6a9a3..70927ad82 100644 --- a/test/regress/regress0/sep/simple-neg-sat.smt2 +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 index ed3187a96..10e509e05 100644 --- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 index 1731174fa..1a9e76a8a 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index 0c0ee72ad..fa0aab591 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (declare-fun y () Int) (declare-fun u () Int) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 9b4871323..1d799c8c9 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 ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (wand (emp 0) (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 index 642c0a8aa..65500f775 100644 --- a/test/regress/regress0/sep/wand-false.smt2 +++ b/test/regress/regress0/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x x) false)) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index e8ee4252c..0db7330d1 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (emp 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 c317e8736..cce0f79e3 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (emp x))) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 index df4bfa6d8..120683f74 100755 --- a/test/regress/regress0/sep/wand-simp-sat.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 index 059e91317..c684d16ad 100755 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index 95bc85537..c9851661a 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (assert (emp x)) -- 2.30.2