From: ajreynol Date: Fri, 17 Jun 2016 20:55:56 +0000 (-0500) Subject: Support for separation logic. Enable cbqi by default for pure BV. X-Git-Tag: cvc5-1.0.0~6049^2~6^2~2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a2547995acc5a98c8969e628ac5e1c45b0efe94;p=cvc5.git Support for separation logic. Enable cbqi by default for pure BV. --- diff --git a/src/Makefile.am b/src/Makefile.am index cfa4982ca..046b84f3a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -446,7 +446,12 @@ libcvc4_la_SOURCES = \ theory/fp/theory_fp.cpp \ theory/fp/theory_fp_rewriter.h \ theory/fp/theory_fp_rewriter.cpp \ - theory/fp/theory_fp_type_rules.h + theory/fp/theory_fp_type_rules.h \ + theory/sep/theory_sep.h \ + theory/sep/theory_sep.cpp \ + theory/sep/theory_sep_rewriter.h \ + theory/sep/theory_sep_rewriter.cpp \ + theory/sep/theory_sep_type_rules.h nodist_libcvc4_la_SOURCES = \ theory/rewriter_tables.h \ diff --git a/src/Makefile.theories b/src/Makefile.theories index 8b5cef4d5..003128a3c 100644 --- a/src/Makefile.theories +++ b/src/Makefile.theories @@ -1,3 +1,3 @@ -THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl +THEORIES = builtin booleans uf arith bv fp arrays datatypes sets sep strings quantifiers idl diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c04de4421..9dcbc3b4b 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -40,6 +40,8 @@ libexpr_la_SOURCES = \ pickle_data.h \ pickler.cpp \ pickler.h \ + sepconst.cpp \ + sepconst.h \ symbol_table.cpp \ symbol_table.h \ type.cpp \ diff --git a/src/expr/sepconst.cpp b/src/expr/sepconst.cpp new file mode 100644 index 000000000..7646b90d3 --- /dev/null +++ b/src/expr/sepconst.cpp @@ -0,0 +1,29 @@ +/********************* */ +/*! \file sepconst.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/sepconst.h" +#include + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const NilRef& asa) { + return out << "(nil " << asa.getType() << ")"; +} + +}/* CVC4 namespace */ diff --git a/src/expr/sepconst.h b/src/expr/sepconst.h new file mode 100644 index 000000000..9f86c7efc --- /dev/null +++ b/src/expr/sepconst.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file sepconst.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#pragma once + +namespace CVC4 { + // messy; Expr needs NilRef (because it's the payload of a + // CONSTANT-kinded expression), and NilRef needs Expr. + class CVC4_PUBLIC NilRef; + //class CVC4_PUBLIC EmpStar; +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" +#include + +namespace CVC4 { + +class CVC4_PUBLIC NilRef { + const Type d_type; + NilRef() { } +public: + NilRef(Type refType):d_type(refType) { } + + ~NilRef() throw() { + } + Type getType() const { return d_type; } + bool operator==(const NilRef& es) const throw() { + return d_type == es.d_type; + } + bool operator!=(const NilRef& es) const throw() { + return !(*this == es); + } + bool operator<(const NilRef& es) const throw() { + return d_type < es.d_type; + } + bool operator<=(const NilRef& es) const throw() { + return d_type <= es.d_type; + } + bool operator>(const NilRef& es) const throw() { + return !(*this <= es); + } + bool operator>=(const NilRef& es) const throw() { + return !(*this < es); + } +};/* class NilRef */ + +std::ostream& operator<<(std::ostream& out, const NilRef& es) CVC4_PUBLIC; + +struct CVC4_PUBLIC NilRefHashFunction { + inline size_t operator()(const NilRef& es) const { + return TypeHashFunction()(es.getType()); + } +};/* struct NilRefHashFunction */ + +}/* CVC4 namespace */ diff --git a/src/options/Makefile.am b/src/options/Makefile.am index e8a18481b..1eb84b45f 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -30,6 +30,7 @@ OPTIONS_SRC_FILES = \ proof_options \ prop_options \ quantifiers_options \ + sep_options \ sets_options \ smt_options \ strings_options \ @@ -54,6 +55,7 @@ OPTIONS_TEMPS = \ proof_options.tmp \ prop_options.tmp \ quantifiers_options.tmp \ + sep_options.tmp \ sets_options.tmp \ smt_options.tmp \ strings_options.tmp \ @@ -78,6 +80,7 @@ OPTIONS_OPTIONS_FILES = \ proof_options.options \ prop_options.options \ quantifiers_options.options \ + sep_options.options \ sets_options.options \ smt_options.options \ strings_options.options \ @@ -102,6 +105,7 @@ OPTIONS_SEDS = \ proof_options.sed \ prop_options.sed \ quantifiers_options.sed \ + sep_options.sed \ sets_options.sed \ smt_options.sed \ strings_options.sed \ @@ -126,6 +130,7 @@ OPTIONS_HEADS = \ proof_options.h \ prop_options.h \ quantifiers_options.h \ + sep_options.h \ sets_options.h \ smt_options.h \ strings_options.h \ @@ -150,6 +155,7 @@ OPTIONS_CPPS = \ proof_options.cpp \ prop_options.cpp \ quantifiers_options.cpp \ + sep_options.cpp \ sets_options.cpp \ smt_options.cpp \ strings_options.cpp \ @@ -295,14 +301,14 @@ options_holder_template.h options_template.cpp options_get_option_template.cpp o # Make sure the implicit rules never mistake X_options for the -o file for a # CPP file. -arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:; +arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sep_options sets_options smt_options strings_options theory_options uf_options:; # These are phony to force them to be made everytime. -.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp +.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp # Make is happier being listed explictly. Not sure why. -arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp: +arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp: echo "$@" "$(@:.tmp=)" $(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true) #TIM: diff --git a/src/options/sep_options b/src/options/sep_options new file mode 100644 index 000000000..043355bda --- /dev/null +++ b/src/options/sep_options @@ -0,0 +1,20 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module SEP "options/sep_options.h" Sep + +option sepCheckNeg --sep-check-neg bool :default true + check negated spatial assertions + +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 + +endmodule diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 41428ed89..b3fe59b79 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1607,6 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << "Empty set encountered: " << f << " " << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); + } else if(f.getKind() == CVC4::kind::NIL_REF) { + //hack: We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational. + // However, the expression has 0 children. So we convert to (sep_nil tmp) here. + expr = MK_EXPR(CVC4::kind::SEP_NIL, PARSER_STATE->mkBoundVar("__tmp",type) ); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -1911,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet(Type())); } + | NILREF_TOK + { expr = MK_CONST( ::CVC4::NilRef(Type())); } // NOTE: Theory constants go here ; @@ -2646,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val'; INST_CLOSURE_TOK : 'inst-closure'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; +NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; // Other set theory operators are not // tokenized and handled directly when // processing a term diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2da44152a..90fc11803 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -166,6 +166,18 @@ void Smt2::addFloatingPointOperators() { Parser::addOperator(kind::FLOATINGPOINT_TO_SBV); } +void Smt2::addSepOperators() { + //addOperator(kind::SEP_NIL, "sep.nil"); + addOperator(kind::SEP_STAR, "sep"); + addOperator(kind::SEP_PTO, "pto"); + addOperator(kind::SEP_WAND, "wand"); + addOperator(kind::EMP_STAR, "emp"); + //Parser::addOperator(kind::SEP_NIL); + Parser::addOperator(kind::SEP_STAR); + Parser::addOperator(kind::SEP_PTO); + Parser::addOperator(kind::SEP_WAND); + Parser::addOperator(kind::EMP_STAR); +} void Smt2::addTheory(Theory theory) { switch(theory) { @@ -254,7 +266,11 @@ void Smt2::addTheory(Theory theory) { defineType("Float128", getExprManager()->mkFloatingPointType(15, 113)); addFloatingPointOperators(); break; - + + case THEORY_SEP: + addSepOperators(); + break; + default: std::stringstream ss; ss << "internal error: unsupported theory " << theory; @@ -307,6 +323,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const { return d_logic.isTheoryEnabled(theory::THEORY_UF); case THEORY_FP: return d_logic.isTheoryEnabled(theory::THEORY_FP); + case THEORY_SEP: + return d_logic.isTheoryEnabled(theory::THEORY_SEP); default: std::stringstream ss; ss << "internal error: unsupported theory " << theory; @@ -415,6 +433,10 @@ void Smt2::setLogic(std::string name) { addTheory(THEORY_FP); } + if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { + addTheory(THEORY_SEP); + } + }/* Smt2::setLogic() */ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 1ae2c9dd7..b99e142ba 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -51,7 +51,8 @@ public: THEORY_SETS, THEORY_STRINGS, THEORY_UF, - THEORY_FP + THEORY_FP, + THEORY_SEP }; private: @@ -344,6 +345,7 @@ private: void addFloatingPointOperators(); + void addSepOperators(); };/* class Smt2 */ }/* CVC4::parser namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f874074ac..7b6bc8708 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -318,7 +318,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } return; } - + + if( n.getKind() == kind::SEP_NIL ){ + out << "sep.nil"; + return; + } + bool stillNeedToPrintParams = true; bool forceBinary = false; // force N-ary to binary when outputing children // operator @@ -581,6 +586,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; + + //separation + case kind::EMP_STAR: + case kind::SEP_PTO: + case kind::SEP_STAR: + case kind::SEP_WAND:out << smtKindString(k) << " "; break; // quantifiers case kind::FORALL: @@ -853,6 +864,12 @@ static string smtKindString(Kind k) throw() { case kind::REGEXP_RANGE: return "re.range"; case kind::REGEXP_LOOP: return "re.loop"; + //sep theory + case kind::SEP_STAR: return "sep"; + case kind::SEP_PTO: return "pto"; + case kind::SEP_WAND: return "wand"; + case kind::EMP_STAR: return "emp"; + default: ; /* fall through */ } diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 40b757598..8957ad7f7 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -458,7 +458,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa goto next_worklist; } - if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) { + if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) { // still need to rewrite e.g. function applications over boolean Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars); Node n; @@ -682,20 +682,22 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa goto next_worklist; } } else if(!t.isSort() && t.getNumChildren() > 0) { - for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { - if((*i).isBoolean()) { - vector argTypes(t.begin(), t.end()); - replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); - TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), - newType, "a variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - top.setAttribute(BooleanTermAttr(), n); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; + if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){ + for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { + if((*i).isBoolean()) { + vector argTypes(t.begin(), t.end()); + replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); + TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), + newType, "a variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + top.setAttribute(BooleanTermAttr(), n); + d_varCache[top] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; + } } } } @@ -714,6 +716,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa case kind::RR_REWRITE: case kind::RR_DEDUCTION: case kind::RR_REDUCTION: + case kind::SEP_STAR: + case kind::SEP_WAND: // not yet supported result.top() << top; worklist.pop(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d5874c52f..69a150cc9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -94,6 +94,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" +#include "theory/sep/theory_sep.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -1844,8 +1845,8 @@ void SmtEngine::setDefaults() { } } //counterexample-guided instantiation for non-sygus - // enable if any quantifiers with arithmetic or datatypes - if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || + // enable if any possible quantifiers with arithmetic, datatypes or bitvectors + if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || options::cbqiAll() ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); @@ -3985,6 +3986,10 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; dumpAssertions("post-strings-pp", d_assertions); } + if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) { + //separation logic solver needs to register the entire input + ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() ); + } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; //remove rewrite rules diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 00d337395..b7e973928 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -714,7 +714,8 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) { Assert (!value.isNull() || !fullModel); // may be a shared term that did not appear in the current assertions - if (!value.isNull()) { + // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context + if (!value.isNull() && !d_modelMap->hasSubstitution(var)) { Debug("bitvector-model") << " " << var << " => " << value << "\n"; Assert (value.getKind() == kind::CONST_BITVECTOR); d_modelMap->addSubstitution(var, value); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d2637a555..523d868b5 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -190,7 +190,7 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){ for( unsigned i=0; igetTermDatabase()->getCounterexampleLiteral( q ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl; + Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f855154af..5d575969f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,27 +153,23 @@ int ModelEngine::checkModel(){ //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); //for debugging - if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " Reps : "; - for( size_t i=0; isecond.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; - } - Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Term reps : "; - for( size_t i=0; isecond.size(); i++ ){ - Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); - Trace("model-engine-debug") << r << " "; - } - Trace("model-engine-debug") << std::endl; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); - Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; - } + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; isecond.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; + for( size_t i=0; isecond.size(); i++ ){ + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Trace("model-engine-debug") << r << " "; } + Trace("model-engine-debug") << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 437f1bddf..b9aab0236 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -382,7 +382,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { - if( n.getKind()==AND || n.getKind()==OR ){ + if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol; newPol = pol; }else if( n.getKind()==IMPLIES ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c34d86497..9f222431e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) { bool ret = false; if( n.getKind()==UNINTERPRETED_CONSTANT ){ ret = true; - }else{ + }else if( n.getKind()!=SEP_NIL ){ //sep.nil has dummy argument FIXME for( unsigned i=0; i& terms, bo #ifdef CVC4_ASSERTIONS bool bad_inst = false; if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){ + Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl; bad_inst = true; }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){ + Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl; bad_inst = true; }else if( options::cbqi() ){ Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); if( !icf.isNull() ){ if( icf==q ){ + Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl; + bad_inst = true; + }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){ + Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; bad_inst = true; - }else{ - bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ); } } } diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds new file mode 100644 index 000000000..52418aefb --- /dev/null +++ b/src/theory/sep/kinds @@ -0,0 +1,37 @@ +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. +# + +theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h" +typechecker "theory/sep/theory_sep_type_rules.h" + +properties polite stable-infinite parametric +properties check propagate presolve getNextDecisionRequest + +# constants +constant NIL_REF \ + ::CVC4::NilRef \ + ::CVC4::NilRefHashFunction \ + "expr/sepconst.h" \ + "the nil reference constant; payload is an instance of the CVC4::NilRef class" + +rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" + +operator SEP_NIL 1 "separation nil" +operator EMP_STAR 1 "separation empty heap" +operator SEP_PTO 2 "points to relation" +operator SEP_STAR 2: "separation star" +operator SEP_WAND 2 "separation magic wand" +operator SEP_LABEL 2 "separation label" + +typerule NIL_REF ::CVC4::theory::sep::NilRefTypeRule +typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule +typerule EMP_STAR ::CVC4::theory::sep::EmpStarTypeRule +typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule +typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule +typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule +typerule SEP_LABEL ::CVC4::theory::sep::SepLabelTypeRule + +endtheory diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp new file mode 100644 index 000000000..6fec57852 --- /dev/null +++ b/src/theory/sep/theory_sep.cpp @@ -0,0 +1,1502 @@ +/********************* */ +/*! \file theory_sep.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the theory of sep. + ** + ** Implementation of the theory of sep. + **/ + + +#include "theory/sep/theory_sep.h" +#include "theory/valuation.h" +#include "expr/kind.h" +#include +#include "theory/rewriter.h" +#include "theory/theory_model.h" +#include "options/sep_options.h" +#include "options/smt_options.h" +#include "smt/logic_exception.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace sep { + +TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_SEP, c, u, out, valuation, logicInfo), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true), + d_conflict(c, false), + d_reduce(u), + d_infer(c), + d_infer_exp(c), + d_spatial_assertions(c) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::SEP_PTO); + //d_equalityEngine.addFunctionKind(kind::SEP_STAR); +} + +TheorySep::~TheorySep() { + for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ + delete it->second; + } +} + +void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + +Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { + if( assumptions.empty() ){ + return d_true; + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + } +} + +///////////////////////////////////////////////////////////////////////////// +// PREPROCESSING +///////////////////////////////////////////////////////////////////////////// + + + +Node TheorySep::ppRewrite(TNode term) { +/* + Trace("sep-pp") << "ppRewrite : " << term << std::endl; + Node s_atom = term.getKind()==kind::NOT ? term[0] : term; + if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::EMP_STAR ){ + //get the reference type (will compute d_type_references) + int card = 0; + TypeNode tn = getReferenceType( s_atom, card ); + Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl; + } +*/ + return term; +} + +//must process assertions at preprocess so that quantified assertions are processed properly +void TheorySep::processAssertions( std::vector< Node >& assertions ) { + 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_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::EMP_STAR ){ + //get the reference type (will compute d_type_references) + int card = 0; + TypeNode tn = getReferenceType( n, card ); + Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl; + }else{ + for( unsigned i=0; ipropagate(literal); + if (!ok) { + d_conflict = true; + } + return ok; +}/* TheorySep::propagate(TNode) */ + + +void TheorySep::explain(TNode literal, std::vector& assumptions) { + if( literal.getKind()==kind::SEP_LABEL || + ( literal.getKind()==kind::NOT && literal[0].getKind()==kind::SEP_LABEL ) ){ + //labelled assertions are never given to equality engine and should only come from the outside + assumptions.push_back( literal ); + }else{ + // Do the work + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL ); + } else { + d_equalityEngine.explainPredicate( atom, polarity, assumptions ); + } + } +} + +void TheorySep::preRegisterTerm(TNode node){ + +} + + +void TheorySep::propagate(Effort e){ + +} + + +Node TheorySep::explain(TNode literal) +{ + Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl; + std::vector assumptions; + explain(literal, assumptions); + return mkAnd(assumptions); +} + + +///////////////////////////////////////////////////////////////////////////// +// SHARING +///////////////////////////////////////////////////////////////////////////// + + +void TheorySep::addSharedTerm(TNode t) { + Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl; + d_equalityEngine.addTriggerTerm(t, THEORY_SEP); +} + + +EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) { + Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)); + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + else if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + return EQUALITY_UNKNOWN;//FALSE_IN_MODEL; +} + + +void TheorySep::computeCareGraph() { + Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; + for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { + TNode a = d_sharedTerms[i]; + TypeNode aType = a.getType(); + for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { + TNode b = d_sharedTerms[j]; + if (b.getType() != aType) { + // We don't care about the terms of different types + continue; + } + switch (d_valuation.getEqualityStatus(a, b)) { + case EQUALITY_TRUE_AND_PROPAGATED: + case EQUALITY_FALSE_AND_PROPAGATED: + // If we know about it, we should have propagated it, so we can skip + break; + default: + // Let's split on it + addCarePair(a, b); + break; + } + } + } +} + + +///////////////////////////////////////////////////////////////////////////// +// MODEL GENERATION +///////////////////////////////////////////////////////////////////////////// + + +void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) +{ + // Send the equality engine information to the model + m->assertEqualityEngine( &d_equalityEngine ); + + if( fullModel ){ + for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){ + computeLabelModel( it->second, d_tmodel ); + //, (label = " << it->second << ") + Trace("sep-model") << "Model for heap, type = " << it->first << " : " << std::endl; + if( d_label_model[it->second].d_heap_locs_model.empty() ){ + Trace("sep-model") << " [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 ); + Node l = d_label_model[it->second].d_heap_locs_model[j][0]; + Trace("sep-model") << " " << l << " -> "; + if( d_pto_model[l].isNull() ){ + Trace("sep-model") << "_"; + }else{ + Trace("sep-model") << d_pto_model[l]; + } + Trace("sep-model") << std::endl; + } + } + Node nil = getNilRef( it->first ); + Node vnil = d_valuation.getModel()->getRepresentative( nil ); + Trace("sep-model") << "sep.nil = " << vnil << std::endl; + Trace("sep-model") << std::endl; + } + } +} + +///////////////////////////////////////////////////////////////////////////// +// NOTIFICATIONS +///////////////////////////////////////////////////////////////////////////// + + +void TheorySep::presolve() { + Trace("sep-pp") << "Presolving" << std::endl; + //TODO: cleanup if incremental? +} + + +///////////////////////////////////////////////////////////////////////////// +// MAIN SOLVER +///////////////////////////////////////////////////////////////////////////// + + +void TheorySep::check(Effort e) { + if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) { + return; + } + + getOutputChannel().spendResource(options::theoryCheckStep()); + + TimerStat::CodeTimer checkTimer(d_checkTime); + Trace("sep-check") << "Sep::check(): " << e << endl; + + while( !done() && !d_conflict ){ + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl; + + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + if( atom.getKind()==kind::EMP_STAR ){ + TypeNode tn = atom[0].getType(); + if( d_emp_arg.find( tn )==d_emp_arg.end() ){ + d_emp_arg[tn] = atom[0]; + }else{ + //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::EMP_STAR; + if( is_spatial && s_lbl.isNull() ){ + if( d_reduce.find( fact )==d_reduce.end() ){ + Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl; + d_reduce.insert( fact ); + //introduce top-level label, add iff + int card; + TypeNode refType = getReferenceType( s_atom, card ); + Trace("sep-lemma-debug") << "...reference type is : " << refType << ", card is " << card << std::endl; + Node b_lbl = getBaseLabel( refType ); + Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl ); + Node lem; + if( polarity ){ + lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom.negate(), s_atom_new ); + }else{ + lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom, s_atom_new.negate() ); + } + Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem << std::endl; + d_out->lemma( lem ); + } + }else{ + //do reductions + if( is_spatial ){ + if( d_reduce.find( fact )==d_reduce.end() ){ + Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl; + d_reduce.insert( fact ); + Node conc; + std::map< Node, Node >::iterator its = d_red_conc[s_lbl].find( s_atom ); + if( its==d_red_conc[s_lbl].end() ){ + //make conclusion based on type of assertion + if( s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND ){ + std::vector< Node > children; + std::vector< Node > c_lems; + int card; + TypeNode tn = getReferenceType( s_atom, card ); + 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() ); +/* //this is unsound + for( int k=0; kmkNode( 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())); + Assert( children.size()>1 ); + if( s_atom.getKind()==kind::SEP_STAR ){ + //reduction for heap : union, pairwise disjoint + Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, labels[0], labels[1] ); + for( unsigned i=2; imkNode( kind::UNION, ulem, labels[i] ); + } + ulem = s_lbl.eqNode( ulem ); + Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, union : " << ulem << std::endl; + c_lems.push_back( ulem ); + for( unsigned i=0; imkNode( kind::INTERSECTION, labels[i], labels[j] ); + Node ilem = s.eqNode( empSet ); + Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem << std::endl; + c_lems.push_back( ilem ); + } + } + }else{ + Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, s_lbl, labels[0] ); + ulem = ulem.eqNode( labels[1] ); + Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl; + c_lems.push_back( ulem ); + Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, s_lbl, labels[0] ); + Node ilem = s.eqNode( empSet ); + Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; + c_lems.push_back( ilem ); + } + //send out definitional lemmas for introduced sets + for( unsigned j=0; jlemma( c_lems[j] ); + } + //children.insert( children.end(), c_lems.begin(), c_lems.end() ); + conc = NodeManager::currentNM()->mkNode( kind::AND, children ); + }else if( s_atom.getKind()==kind::SEP_PTO ){ + Node ss = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] ); + if( s_lbl!=ss ){ + conc = s_lbl.eqNode( ss ); + } + 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 ); + }else{ + //labeled emp should be rewritten + Assert( false ); + } + d_red_conc[s_lbl][s_atom] = conc; + }else{ + conc = its->second; + } + if( !conc.isNull() ){ + bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; + if( !use_polarity ){ + // introduce guard, assert positive version + Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl; + Node lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + lit = getValuation().ensureLiteral( lit ); + d_neg_guard[s_lbl][s_atom] = lit; + Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl; + AlwaysAssert( !lit.isNull() ); + d_out->requirePhase( lit, true ); + d_neg_guards.push_back( lit ); + d_guard_to_assertion[lit] = s_atom; + //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, lit, conc ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc ); + Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl; + d_out->lemma( lem ); + }else{ + //reduce based on implication + Node ant = atom; + if( polarity ){ + ant = atom.negate(); + } + Node lem = NodeManager::currentNM()->mkNode( kind::OR, ant, conc ); + Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl; + d_out->lemma( lem ); + } + }else{ + Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl; + } + } + } + //assert to equality engine + if( !is_spatial ){ + Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl; + if( s_atom.getKind()==kind::EQUAL ){ + d_equalityEngine.assertEquality(atom, polarity, fact); + }else{ + d_equalityEngine.assertPredicate(atom, polarity, fact); + } + Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl; + }else if( s_atom.getKind()==kind::SEP_PTO ){ + Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] ); + if( polarity && s_lbl!=pto_lbl ){ + //also propagate equality + Node eq = s_lbl.eqNode( pto_lbl ); + Trace("sep-assert") << "Asserting implied equality " << eq << " to EE..." << std::endl; + d_equalityEngine.assertEquality(eq, true, fact); + Trace("sep-assert") << "Done asserting implied equality " << eq << " to EE." << std::endl; + } + //associate the equivalence class of the lhs with this pto + Node r = getRepresentative( s_lbl ); + HeapAssertInfo * ei = getOrMakeEqcInfo( r, true ); + addPto( ei, r, atom, polarity ); + } + //maybe propagate + doPendingFacts(); + //add to spatial assertions + if( !d_conflict && is_spatial ){ + d_spatial_assertions.push_back( fact ); + } + } + } + + if( e == EFFORT_LAST_CALL && !d_conflict && !d_valuation.needCheck() ){ + Trace("sep-process") << "Checking heap at full effort..." << std::endl; + d_label_model.clear(); + d_tmodel.clear(); + d_pto_model.clear(); + Trace("sep-process") << "---Locations---" << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_references_all.end(); ++itt ){ + for( unsigned k=0; ksecond.size(); k++ ){ + Node t = itt->second[k]; + Trace("sep-process") << " " << t << " = "; + if( d_valuation.getModel()->hasTerm( t ) ){ + Node v = d_valuation.getModel()->getRepresentative( t ); + Trace("sep-process") << v << std::endl; + d_tmodel[v] = t; + }else{ + Trace("sep-process") << "?" << std::endl; + } + } + } + Trace("sep-process") << "---" << std::endl; + //build positive/negative assertion lists for labels + std::map< Node, bool > assert_active; + //get the inactive assertions + std::map< Node, std::vector< Node > > lbl_to_assertions; + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + Assert( atom.getKind()==kind::SEP_LABEL ); + TNode s_atom = atom[0]; + TNode s_lbl = atom[1]; + lbl_to_assertions[s_lbl].push_back( fact ); + //check whether assertion is active : either polarity=true, or guard is not asserted false + assert_active[fact] = true; + bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; + if( use_polarity ){ + if( s_atom.getKind()==kind::SEP_PTO ){ + Node vv = d_valuation.getModel()->getRepresentative( s_atom[0] ); + if( d_pto_model.find( vv )==d_pto_model.end() ){ + Trace("sep-inst") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl; + d_pto_model[vv] = s_atom[1]; + } + } + }else{ + if( d_neg_guard[s_lbl].find( s_atom )!=d_neg_guard[s_lbl].end() ){ + //check if the guard is asserted positively + Node guard = d_neg_guard[s_lbl][s_atom]; + bool value; + if( getValuation().hasSatValue( guard, value ) ) { + assert_active[fact] = value; + } + } + } + } + //(recursively) set inactive sub-assertions + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + if( !assert_active[fact] ){ + setInactiveAssertionRec( fact, lbl_to_assertions, assert_active ); + } + } + //set up model information based on active assertions + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + TNode s_atom = atom[0]; + TNode s_lbl = atom[1]; + if( assert_active[fact] ){ + computeLabelModel( s_lbl, d_tmodel ); + } + } + //debug print + if( Trace.isOn("sep-process") ){ + Trace("sep-process") << "--- Current spatial assertions : " << std::endl; + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + Trace("sep-process") << " " << fact; + if( !assert_active[fact] ){ + Trace("sep-process") << " [inactive]"; + } + Trace("sep-process") << std::endl; + } + Trace("sep-process") << "---" << std::endl; + } + if(Trace.isOn("sep-eqc")) { + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); + Trace("sep-eqc") << "EQC:" << std::endl; + while( !eqcs2_i.isFinished() ){ + Node eqc = (*eqcs2_i); + eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + Trace("sep-eqc") << "Eqc( " << eqc << " ) : { "; + while( !eqc2_i.isFinished() ) { + if( (*eqc2_i)!=eqc ){ + Trace("sep-eqc") << (*eqc2_i) << " "; + } + ++eqc2_i; + } + Trace("sep-eqc") << " } " << std::endl; + ++eqcs2_i; + } + Trace("sep-eqc") << std::endl; + } + + if( options::sepCheckNeg() ){ + //get active labels + std::map< Node, bool > active_lbl; + if( options::sepMinimalRefine() ){ + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + TNode s_atom = atom[0]; + bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; + if( !use_polarity ){ + Assert( assert_active.find( fact )!=assert_active.end() ); + if( assert_active[fact] ){ + Assert( atom.getKind()==kind::SEP_LABEL ); + TNode s_lbl = atom[1]; + if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){ + Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl; + active_lbl[s_lbl] = true; + } + } + } + } + } + + //process spatial assertions + bool addedLemma = false; + bool needAddLemma = false; + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + TNode s_atom = atom[0]; + + bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity; + Trace("sep-process-debug") << " check atom : " << s_atom << " use polarity " << use_polarity << std::endl; + if( !use_polarity ){ + Assert( assert_active.find( fact )!=assert_active.end() ); + if( assert_active[fact] ){ + Assert( atom.getKind()==kind::SEP_LABEL ); + TNode s_lbl = atom[1]; + Trace("sep-process") << "--> Active negated atom : " << s_atom << ", lbl = " << s_lbl << std::endl; + //add refinement lemma + if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){ + needAddLemma = true; + int card; + TypeNode tn = getReferenceType( s_atom, card ); + tn = NodeManager::currentNM()->mkSetType(tn); + //tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); + Node o_b_lbl_mval = d_label_model[s_lbl].getValue( tn ); + Trace("sep-process") << " Model for " << s_lbl << " : " << o_b_lbl_mval << std::endl; + + //get model values + std::map< int, Node > mvals; + for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){ + Node sub_lbl = itl->second; + int sub_index = itl->first; + computeLabelModel( sub_lbl, d_tmodel ); + Node lbl_mval = d_label_model[sub_lbl].getValue( tn ); + Trace("sep-process-debug") << " child " << sub_index << " : " << sub_lbl << ", mval = " << lbl_mval << std::endl; + mvals[sub_index] = lbl_mval; + } + + // Now, assert model-instantiated implication based on the negation + Assert( d_label_model.find( s_lbl )!=d_label_model.end() ); + std::vector< Node > conc; + bool inst_success = true; + if( options::sepExp() ){ + //old refinement lemmas + for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){ + int sub_index = itl->first; + std::map< Node, Node > visited; + Node c = applyLabel( s_atom[itl->first], mvals[sub_index], visited ); + Trace("sep-process-debug") << " applied inst : " << c << std::endl; + if( s_atom.getKind()==kind::SEP_STAR || sub_index==0 ){ + conc.push_back( c.negate() ); + }else{ + conc.push_back( c ); + } + } + }else{ + //new refinement + std::map< Node, Node > visited; + Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, tn, active_lbl ); + Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; + if( inst.isNull() ){ + inst_success = false; + }else{ + inst = Rewriter::rewrite( inst ); + if( inst==( polarity ? d_true : d_false ) ){ + inst_success = false; + } + conc.push_back( polarity ? inst : inst.negate() ); + } + } + if( inst_success ){ + std::vector< Node > lemc; + Node pol_atom = atom; + if( polarity ){ + pol_atom = atom.negate(); + } + lemc.push_back( pol_atom ); + //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() ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc ); + if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){ + d_refinement_lem[s_atom][s_lbl].push_back( lem ); + Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl; + Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl; + d_out->lemma( lem ); + addedLemma = true; + }else{ + Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl; + } + } + }else{ + Trace("sep-process-debug") << " no children." << std::endl; + Assert( s_atom.getKind()==kind::SEP_PTO ); + } + }else{ + Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl; + } + } + } + if( !addedLemma ){ + if( needAddLemma ){ + Trace("sep-process") << "WARNING : could not find refinement lemma!!!" << std::endl; + Assert( false ); + d_out->setIncomplete(); + } + } + } + } + Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl; +} + + +Node TheorySep::getNextDecisionRequest() { + for( unsigned i=0; igetTermDatabase()->getCounterexampleLiteral( q ); + bool value; + if( d_valuation.hasSatValue( cel, value ) ){ + success = value; + }else{ + Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl; + success = false; + } + } + } + if( success ){ + bool value; + if( !d_valuation.hasSatValue( g, value ) ) { + Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl; + return g; + } + } + } + Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl; + return Node::null(); +} + +void TheorySep::conflict(TNode a, TNode b) { + Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl; + Node conflictNode; + if (a.getKind() == kind::CONST_BOOLEAN) { + conflictNode = explain(a.iffNode(b)); + } else { + conflictNode = explain(a.eqNode(b)); + } + d_conflict = true; + d_out->conflict( conflictNode ); +} + + +TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) { + +} + +TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { + std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n ); + if( e_i==d_eqc_info.end() ){ + if( doMake ){ + HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() ); + d_eqc_info[n] = ei; + return ei; + }else{ + return NULL; + } + }else{ + return (*e_i).second; + } +} + +TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) { + Trace("sep-type") << "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::EMP_STAR || index!=-1 ); + std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index ); + if( it==d_reference_type[atom].end() ){ + card = 0; + TypeNode tn; + if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){ + for( unsigned i=0; i visited; + tn = getReferenceType2( atom, card, index, n, visited ); + } + if( tn.isNull() && index==-1 ){ + tn = NodeManager::currentNM()->booleanType(); + } + d_reference_type[atom][index] = tn; + d_reference_type_card[atom][index] = card; + Trace("sep-type") << "...ref type return " << card << " for " << atom << " " << index << std::endl; + //add to d_type_references + if( index==-1 ){ + //only contributes if top-level (index=-1) + for( unsigned i=0; i(int)d_card_max[tn] ){ + d_card_max[tn] = card; + } + } + return tn; + }else{ + Assert( d_reference_type_card[atom].find( index )!=d_reference_type_card[atom].end() ); + card = d_reference_type_card[atom][index]; + return it->second; + } +} + +TypeNode TheorySep::getReferenceType2( 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; + visited[n] = -1; + if( n.getKind()==kind::SEP_PTO ){ + TypeNode tn1 = n[0].getType(); + TypeNode tn2 = n[1].getType(); + if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){ + d_reference_bound_invalid[tn1] = true; + }else{ + if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){ + d_references[atom][index].push_back( n[0] ); + } + } + std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 ); + if( itt==d_loc_to_data_type.end() ){ + Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl; + d_loc_to_data_type[tn1] = tn2; + }else{ + if( itt->second!=tn2 ){ + std::stringstream ss; + ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl; + throw LogicException(ss.str()); + Assert( false ); + } + } + card = 1; + visited[n] = card; + return tn1; + //return n[1].getType(); + }else if( n.getKind()==kind::EMP_STAR ){ + card = 1; + visited[n] = card; + return n[0].getType(); + }else if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){ + Assert( n!=atom ); + //get the references + card = 0; + TypeNode tn = getReferenceType( n, card ); + for( unsigned j=0; jcard ? cardc : card; + } + visited[n] = card; + return otn; + } + }else{ + Trace("sep-type-debug") << "already visit : " << n << " : " << atom << " " << index << std::endl; + card = 0; + return TypeNode::null(); + } +} +/* + +int TheorySep::getCardinality( Node n, std::vector< Node >& refs ) { + std::map< Node, int > visited; + return getCardinality2( n, refs, visited ); +} + +int TheorySep::getCardinality2( Node n, std::vector< Node >& refs, std::map< Node, int >& visited ) { + std::map< Node, int >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + + + } +} +*/ + +Node TheorySep::getBaseLabel( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_base_label.find( tn ); + if( it==d_base_label.end() ){ + Trace("sep") << "Make base label for " << tn << std::endl; + std::stringstream ss; + ss << "__Lb"; + TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); + //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + d_base_label[tn] = n_lbl; + //make reference bound + Trace("sep") << "Make reference bound label for " << tn << std::endl; + std::stringstream ss2; + 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() ); + //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() ){ + //ensure that it is distinct from all other references so far + for( unsigned j=0; jmkNode( 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_lbl_reference_bound[d_base_label[tn]].push_back( e ); + } + //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 ); + return n_lbl; + }else{ + return it->second; + } +} + +Node TheorySep::getNilRef( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); + if( it==d_nil_ref.end() ){ + TypeEnumerator te(tn); + Node nil = NodeManager::currentNM()->mkNode( kind::SEP_NIL, *te ); + d_nil_ref[tn] = nil; + return nil; + }else{ + return it->second; + } +} + +Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { + Node u; + if( locs.empty() ){ + TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); + return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType())); + }else{ + for( unsigned i=0; imkNode( kind::SINGLETON, s ); + if( u.isNull() ){ + u = s; + }else{ + u = NodeManager::currentNM()->mkNode( kind::UNION, s, u ); + } + } + return u; + } +} + +Node TheorySep::getLabel( Node atom, int child, Node lbl ) { + std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child ); + if( it==d_label_map[atom][lbl].end() ){ + int card; + TypeNode refType = getReferenceType( atom, card ); + std::stringstream ss; + ss << "__Lc" << child; + TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); + //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType)); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + d_label_map[atom][lbl][child] = n_lbl; + d_label_map_parent[n_lbl] = lbl; + return n_lbl; + }else{ + return (*it).second; + } +} + +Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) { + Assert( n.getKind()!=kind::SEP_LABEL ); + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){ + return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl ); + }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){ + return n; + }else{ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + std::vector< Node > children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + visited[n] = ret; + return ret; + }else{ + return it->second; + } + } +} + +Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel, + TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) { + Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl; + if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){ + Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl; + return Node::null(); + }else{ + if( Trace.isOn("sep-inst") ){ + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){ + for( unsigned j=0; j children; + children.resize( n.getNumChildren() ); + Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() ); + 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; + Assert( sub_index>=0 && sub_index<(int)children.size() ); + Trace("sep-inst-debug") << "Sublabel " << sub_index << " is " << sub_lbl << std::endl; + Node lbl_mval; + if( n.getKind()==kind::SEP_WAND && sub_index==1 ){ + Assert( d_label_map[n][lbl].find( 0 )!=d_label_map[n][lbl].end() ); + Node sub_lbl_0 = d_label_map[n][lbl][0]; + computeLabelModel( sub_lbl_0, tmodel ); + Assert( d_label_model.find( sub_lbl_0 )!=d_label_model.end() ); + lbl_mval = NodeManager::currentNM()->mkNode( kind::UNION, lbl, d_label_model[sub_lbl_0].getValue( rtn ) ); + }else{ + computeLabelModel( sub_lbl, tmodel ); + Assert( d_label_model.find( sub_lbl )!=d_label_model.end() ); + lbl_mval = d_label_model[sub_lbl].getValue( rtn ); + } + Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval << std::endl; + children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, tmodel, rtn, active_lbl, ind+1 ); + if( children[sub_index].isNull() ){ + return Node::null(); + } + } + if( n.getKind()==kind::SEP_STAR ){ + Assert( children.size()>1 ); + return NodeManager::currentNM()->mkNode( kind::AND, children ); + }else{ + return NodeManager::currentNM()->mkNode( kind::OR, children[0].negate(), children[1] ); + } + }else{ + //nested star/wand, label it and return + return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v ); + } + }else if( n.getKind()==kind::SEP_PTO ){ + //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption + Assert( d_label_model.find( o_lbl )!=d_label_model.end() ); + Node vr = d_valuation.getModel()->getRepresentative( n[0] ); + Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr ); + bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end(); + Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl; + std::vector< Node > children; + if( inBaseHeap ){ + Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ); + children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) ); + }else{ + //look up value of data + std::map< Node, Node >::iterator it = pto_model.find( vr ); + if( it!=pto_model.end() ){ + if( n[1]!=it->second ){ + children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) ); + } + }else{ + Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl; + } + } + children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) ); + Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) ); + Trace("sep-inst-debug") << "Return " << ret << std::endl; + return ret; + }else if( n.getKind()==kind::EMP_STAR ){ + //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET ); + return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) ); + }else{ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + std::vector< Node > children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + //careful about caching + //visited[n] = ret; + return ret; + }else{ + return it->second; + } + } + } +} + +void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ) { + Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact << std::endl; + assert_active[fact] = false; + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + TNode s_atom = atom[0]; + TNode s_lbl = atom[1]; + if( s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_STAR ){ + for( unsigned j=0; j& children, std::vector< Node >& labels ) { + for( unsigned i=0; i visited; + Node lc = applyLabel( s_atom[i], lblc, visited ); + Assert( !lc.isNull() ); + if( i==1 && s_atom.getKind()==kind::SEP_WAND ){ + lc = lc.negate(); + } + children.push_back( lc ); + labels.push_back( lblc ); + } + Assert( children.size()>1 ); +} + +void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) { + if( !d_label_model[lbl].d_computed ){ + d_label_model[lbl].d_computed = true; + + //Node v_val = d_valuation.getModelValue( s_lbl ); + //hack FIXME + Node v_val = d_valuation.getModel()->getRepresentative( lbl ); + Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl; + if( v_val.getKind()!=kind::EMPTYSET ){ + while( v_val.getKind()==kind::UNION ){ + Assert( v_val[1].getKind()==kind::SINGLETON ); + d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] ); + v_val = v_val[0]; + } + Assert( v_val.getKind()==kind::SINGLETON ); + d_label_model[lbl].d_heap_locs_model.push_back( v_val ); + } + //end hack + for( unsigned j=0; j::iterator itm = tmodel.find( u ); + if( itm==tmodel.end() ) { + //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl; + //Assert( false ); + //tt = u; + //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() ); + tt = d_type_references_all[tn][0]; + }else{ + tt = itm->second; + } + Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt ); + Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl; + d_label_model[lbl].d_heap_locs.push_back( stt ); + } + } +} + +Node TheorySep::getRepresentative( Node t ) { + if( d_equalityEngine.hasTerm( t ) ){ + return d_equalityEngine.getRepresentative( t ); + }else{ + return t; + } +} + +bool TheorySep::hasTerm( Node a ){ + return d_equalityEngine.hasTerm( a ); +} + +bool TheorySep::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); + }else{ + return false; + } +} + +bool TheorySep::areDisequal( Node a, Node b ){ + if( a==b ){ + return false; + }else if( hasTerm( a ) && hasTerm( b ) ){ + if( d_equalityEngine.areDisequal( a, b, false ) ){ + return true; + } + } + return false; +} + +void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) { + +} + +void TheorySep::eqNotifyPostMerge(TNode t1, TNode t2) { + HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false ); + if( e2 && ( !e2->d_pto.get().isNull() || e2->d_has_neg_pto.get() ) ){ + HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true ); + if( !e2->d_pto.get().isNull() ){ + if( !e1->d_pto.get().isNull() ){ + Trace("sep-pto-debug") << "While merging " << t1 << " " << t2 << ", merge pto." << std::endl; + mergePto( e1->d_pto.get(), e2->d_pto.get() ); + }else{ + e1->d_pto.set( e2->d_pto.get() ); + } + } + e1->d_has_neg_pto.set( e1->d_has_neg_pto.get() || e2->d_has_neg_pto.get() ); + //validate + validatePto( e1, t1 ); + } +} + +void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) { + if( !ei->d_pto.get().isNull() && ei->d_has_neg_pto.get() ){ + for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { + Node fact = (*i); + bool polarity = fact.getKind() != kind::NOT; + if( !polarity ){ + TNode atom = polarity ? fact : fact[0]; + Assert( atom.getKind()==kind::SEP_LABEL ); + TNode s_atom = atom[0]; + if( s_atom.getKind()==kind::SEP_PTO ){ + if( areEqual( atom[1], ei_n ) ){ + addPto( ei, ei_n, atom, false ); + } + } + } + } + //we have now processed all pending negated pto + ei->d_has_neg_pto.set( false ); + } +} + +void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) { + Trace("sep-pto") << "Add pto " << p << ", pol = " << polarity << " to eqc " << ei_n << std::endl; + if( !ei->d_pto.get().isNull() ){ + if( polarity ){ + Trace("sep-pto-debug") << "...eqc " << ei_n << " already has pto " << ei->d_pto.get() << ", merge." << std::endl; + mergePto( ei->d_pto.get(), p ); + }else{ + Node pb = ei->d_pto.get(); + Trace("sep-pto") << "Process positive/negated pto " << " " << pb << " " << p << std::endl; + Assert( pb.getKind()==kind::SEP_LABEL && pb[0].getKind()==kind::SEP_PTO ); + Assert( p.getKind()==kind::SEP_LABEL && p[0].getKind()==kind::SEP_PTO ); + Assert( areEqual( pb[1], p[1] ) ); + std::vector< Node > exp; + if( pb[1]!=p[1] ){ + exp.push_back( pb[1].eqNode( p[1] ) ); + } + exp.push_back( pb ); + exp.push_back( p.negate() ); + std::vector< Node > conc; + if( pb[0][1]!=p[0][1] ){ + conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() ); + } + if( pb[1]!=p[1] ){ + conc.push_back( pb[1].eqNode( p[1] ).negate() ); + } + Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) ); + sendLemma( exp, n_conc, "PTO_NEG_PROP" ); + } + }else{ + if( polarity ){ + ei->d_pto.set( p ); + validatePto( ei, ei_n ); + }else{ + ei->d_has_neg_pto.set( true ); + } + } +} + +void TheorySep::mergePto( Node p1, Node p2 ) { + Trace("sep-lemma-debug") << "Merge pto " << p1 << " " << p2 << std::endl; + Assert( p1.getKind()==kind::SEP_LABEL && p1[0].getKind()==kind::SEP_PTO ); + Assert( p2.getKind()==kind::SEP_LABEL && p2[0].getKind()==kind::SEP_PTO ); + if( !areEqual( p1[0][1], p2[0][1] ) ){ + std::vector< Node > exp; + if( p1[1]!=p2[1] ){ + Assert( areEqual( p1[1], p2[1] ) ); + exp.push_back( p1[1].eqNode( p2[1] ) ); + } + exp.push_back( p1 ); + exp.push_back( p2 ); + sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" ); + } +} + +void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) { + Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl; + conc = Rewriter::rewrite( conc ); + Trace("sep-lemma-debug") << "Got : " << conc << std::endl; + if( conc!=d_true ){ + if( infer && conc!=d_false ){ + Node ant_n; + if( ant.empty() ){ + ant_n = d_true; + }else if( ant.size()==1 ){ + ant_n = ant[0]; + }else{ + ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant ); + } + Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl; + d_pending_exp.push_back( ant_n ); + d_pending.push_back( conc ); + d_infer.push_back( ant_n ); + d_infer_exp.push_back( conc ); + }else{ + std::vector< TNode > ant_e; + for( unsigned i=0; imkNode( kind::AND, ant_e ); + } + if( conc==d_false ){ + Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl; + d_out->conflict( ant_n ); + d_conflict = true; + }else{ + Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl; + d_pending_exp.push_back( ant_n ); + d_pending.push_back( conc ); + d_pending_lem.push_back( d_pending.size()-1 ); + } + } + } +} + +void TheorySep::doPendingFacts() { + if( d_pending_lem.empty() ){ + for( unsigned i=0; imkConst(EmptySet(tn.toType())); + }else if( d_heap_locs.size()==1 ){ + return d_heap_locs[0]; + }else{ + Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] ); + for( unsigned j=2; jmkNode( kind::UNION, curr, d_heap_locs[j] ); + } + return curr; + } +} + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h new file mode 100644 index 000000000..506cb77cd --- /dev/null +++ b/src/theory/sep/theory_sep.h @@ -0,0 +1,294 @@ +/********************* */ +/*! \file theory_sep.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Dejan Jovanovic, Clark Barrett + ** Minor contributors (to current version): Tim King, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory of sep + ** + ** Theory of sep. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H +#define __CVC4__THEORY__SEP__THEORY_SEP_H + +#include "theory/theory.h" +#include "util/statistics_registry.h" +#include "theory/uf/equality_engine.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdqueue.h" + +namespace CVC4 { +namespace theory { + +class TheoryModel; + +namespace sep { + +class TheorySep : public Theory { + typedef context::CDChunkList NodeList; + typedef context::CDHashSet NodeSet; + typedef context::CDHashMap NodeNodeMap; + + ///////////////////////////////////////////////////////////////////////////// + // MISC + ///////////////////////////////////////////////////////////////////////////// + + private: + + /** True node for predicates = true */ + Node d_true; + + /** True node for predicates = false */ + Node d_false; + + Node mkAnd( std::vector< TNode >& assumptions ); + + void processAssertion( Node n, std::map< Node, bool >& visited ); + + public: + + TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + ~TheorySep(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); + + std::string identify() const { return std::string("TheorySep"); } + + ///////////////////////////////////////////////////////////////////////////// + // PREPROCESSING + ///////////////////////////////////////////////////////////////////////////// + + public: + + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); + + void processAssertions( std::vector< Node >& assertions ); + ///////////////////////////////////////////////////////////////////////////// + // T-PROPAGATION / REGISTRATION + ///////////////////////////////////////////////////////////////////////////// + + private: + + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); + + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector& assumptions); + + public: + + void preRegisterTerm(TNode n); + void propagate(Effort e); + Node explain(TNode n); + + public: + + void addSharedTerm(TNode t); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void computeCareGraph(); + + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// + + public: + + void collectModelInfo(TheoryModel* m, bool fullModel); + + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// + + private: + public: + + Node getNextDecisionRequest(); + + void presolve(); + void shutdown() { } + + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// + public: + + void check(Effort e); + + private: + + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass : public eq::EqualityEngineNotify { + TheorySep& d_sep; + public: + NotifyClass(TheorySep& sep): d_sep(sep) {} + + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; + // Just forward to sep + if (value) { + return d_sep.propagate(equality); + } else { + return d_sep.propagate(equality.notNode()); + } + } + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Unreachable(); + } + + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + // Propagate equality between shared terms + return d_sep.propagate(t1.eqNode(t2)); + } else { + return d_sep.propagate(t1.eqNode(t2).notNode()); + } + return true; + } + + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_sep.conflict(t1, t2); + } + + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); } + void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + }; + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equaltity engine */ + eq::EqualityEngine d_equalityEngine; + + /** Are we in conflict? */ + context::CDO d_conflict; + std::vector< Node > d_pending_exp; + std::vector< Node > d_pending; + std::vector< int > d_pending_lem; + + /** list of all refinement lemms */ + std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem; + + /** Conflict when merging constants */ + void conflict(TNode a, TNode b); + + //cache for positive polarity start reduction + NodeSet d_reduce; + std::map< Node, std::map< Node, Node > > d_red_conc; + std::map< Node, std::map< Node, Node > > d_neg_guard; + std::vector< Node > d_neg_guards; + std::map< Node, Node > d_guard_to_assertion; + //cache for references + std::map< Node, std::map< int, TypeNode > > d_reference_type; + std::map< Node, std::map< int, int > > d_reference_type_card; + std::map< Node, std::map< int, std::vector< Node > > > d_references; + /** inferences: maintained to ensure ref count for internally introduced nodes */ + NodeList d_infer; + NodeList d_infer_exp; + NodeList d_spatial_assertions; + + //currently fix one data type for each location type, throw error if using more than one + std::map< TypeNode, TypeNode > d_loc_to_data_type; + //information about types + std::map< TypeNode, Node > d_base_label; + std::map< TypeNode, Node > d_nil_ref; + //reference bound + 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, std::vector< Node > > d_type_references; + 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 + std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map; + std::map< Node, Node > d_label_map_parent; + + //term model + std::map< Node, Node > d_tmodel; + std::map< Node, Node > d_pto_model; + + class HeapAssertInfo { + public: + HeapAssertInfo( context::Context* c ); + ~HeapAssertInfo(){} + context::CDO< Node > d_pto; + context::CDO< bool > d_has_neg_pto; + }; + std::map< Node, HeapAssertInfo * > d_eqc_info; + HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false ); + + //calculate the element type of the heap for spatial assertions + TypeNode getReferenceType( Node atom, int& card, int index = -1 ); + TypeNode getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited); + //get the base label for the spatial assertion + Node getBaseLabel( TypeNode tn ); + Node getNilRef( TypeNode tn ); + Node getLabel( Node atom, int child, Node lbl ); + Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ); + void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ); + + class HeapInfo { + public: + HeapInfo() : d_computed(false) {} + //information about the model + bool d_computed; + std::vector< Node > d_heap_locs; + std::vector< Node > d_heap_locs_model; + //get value + Node getValue( TypeNode tn ); + }; + //heap info ( label -> HeapInfo ) + std::map< Node, HeapInfo > d_label_model; + + void debugPrintHeap( HeapInfo& heap, const char * c ); + void validatePto( HeapAssertInfo * ei, Node ei_n ); + void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ); + void mergePto( Node p1, Node p2 ); + void computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ); + Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel, + TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 ); + void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ); + + Node mkUnion( TypeNode tn, std::vector< Node >& locs ); +private: + Node getRepresentative( Node t ); + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + /** called when two equivalence classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + void eqNotifyPostMerge(TNode t1, TNode t2); + + void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false ); + void doPendingFacts(); +public: + eq::EqualityEngine* getEqualityEngine() { + return &d_equalityEngine; + } + +};/* class TheorySep */ + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */ diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp new file mode 100644 index 000000000..ce0b20cbd --- /dev/null +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -0,0 +1,192 @@ +/********************* */ +/*! \file theory_sep_rewriter.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/attribute.h" +#include "theory/sep/theory_sep_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace sep { + +void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){ + Assert( n.getKind()==kind::SEP_STAR ); + for( unsigned i=0; i temp_s_children; + getAndChildren( n[i], temp_s_children, ns_children ); + Node to_add; + if( temp_s_children.size()==0 ){ + to_add = NodeManager::currentNM()->mkConst( true ); + }else{ + //remove empty star + std::vector< Node > temp_s_children2; + for( unsigned i=0; i1 ){ + to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children2 ); + } + } + if( !to_add.isNull() ){ + //flatten star + if( to_add.getKind()==kind::SEP_STAR ){ + getStarChildren( to_add, s_children, ns_children ); + }else if( std::find( s_children.begin(), s_children.end(), to_add )==s_children.end() ){ + s_children.push_back( to_add ); + } + } + } + } +} + +void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ) { + if( n.getKind()==kind::AND ){ + for( unsigned i=0; i visited; + if( isSpatial( n, visited ) ){ + if( std::find( s_children.begin(), s_children.end(), n )==s_children.end() ){ + s_children.push_back( n ); + } + }else{ + if( std::find( ns_children.begin(), ns_children.end(), n )==ns_children.end() ){ + if( n!=NodeManager::currentNM()->mkConst(true) ){ + ns_children.push_back( n ); + } + } + } + } +} + +bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR || n.getKind()==kind::SEP_LABEL ){ + return true; + }else if( n.getType().isBoolean() ){ + for( unsigned i=0; imkNode( kind::SEP_NIL, n ); + } + break; + } + case kind::SEP_LABEL: { + if( node[0].getKind()==kind::SEP_PTO ){ + Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] ); + if( node[1]!=s ){ + Node c1 = node[1].eqNode( s ); + Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s ); + retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 ); + } + } + if( node[0].getKind()==kind::EMP_STAR ){ + retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) ); + } + break; + } + case kind::SEP_PTO: { + break; + } + case kind::SEP_STAR: { + //flatten + std::vector< Node > s_children; + std::vector< Node > ns_children; + getStarChildren( node, s_children, ns_children ); + if( !s_children.empty() ){ + Node schild; + if( s_children.size()==1 ) { + schild = s_children[0]; + }else{ + schild = NodeManager::currentNM()->mkNode( kind::SEP_STAR, s_children ); + } + ns_children.push_back( schild ); + } + Assert( !ns_children.empty() ); + if( ns_children.size()==1 ){ + retNode = ns_children[0]; + }else{ + retNode = NodeManager::currentNM()->mkNode( kind::AND, ns_children ); + } + break; + } + case kind::EQUAL: + case kind::IFF: { + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + else if (node[0].isConst() && node[1].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + } + if (node[0] > node[1]) { + Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); + return RewriteResponse(REWRITE_DONE, newNode); + } + break; + } + default: + break; + } + if( node!=retNode ){ + Trace("sep-rewrite") << "Sep::rewrite : " << node << " -> " << retNode << std::endl; + } + return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); +} + + +/* +RewriteResponse TheorySepRewriter::preRewrite(TNode node) { + if( node.getKind()==kind::EMP_STAR ){ + Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl; + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::EMP_STAR, NodeManager::currentNM()->mkConst( true ) ) ); + }else{ + Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); + } +} +*/ + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h new file mode 100644 index 000000000..02adbebe5 --- /dev/null +++ b/src/theory/sep/theory_sep_rewriter.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file theory_sep_rewriter.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H +#define __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H + +#include "theory/rewriter.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace sep { + + +class TheorySepRewriter { +private: + static void getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ); + static void getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ); + static bool isSpatial( Node n, std::map< Node, bool >& visited ); +public: + + static RewriteResponse postRewrite(TNode node); + static inline RewriteResponse preRewrite(TNode node) { + Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); + } + + static inline void init() {} + static inline void shutdown() {} + +};/* class TheorySepRewriter */ + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */ diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h new file mode 100644 index 000000000..f47941b03 --- /dev/null +++ b/src/theory/sep/theory_sep_type_rules.h @@ -0,0 +1,136 @@ +/********************* */ +/*! \file theory_sep_type_rules.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Typing and cardinality rules for the theory of sep + ** + ** Typing and cardinality rules for the theory of sep. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H +#define __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H + +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace sep { + +class NilRefTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return TypeNode::fromType( n.getConst().getType() ); + } +}; + +class SepNilTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return n[0].getType(check); + } +}; + +class EmpStarTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return nodeManager->booleanType(); + } +}; + +struct SepPtoTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::SEP_PTO); + if( check ) { + TypeNode refType = n[0].getType(check); + //SEP-POLY + //if(!refType.isRef()) { + // throw TypeCheckingExceptionPrivate(n, "pto applied to non-reference term"); + //} + TypeNode ptType = n[1].getType(check); + //if(!ptType.isComparableTo(refType.getRefConstituentType())){ + // throw TypeCheckingExceptionPrivate(n, "pto maps reference to term of different type"); + //} + } + return nodeManager->booleanType(); + } +};/* struct SepSelectTypeRule */ + +struct SepStarTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TypeNode btype = nodeManager->booleanType(); + Assert(n.getKind() == kind::SEP_STAR); + if( check ){ + for( unsigned i=0; ibooleanType(); + Assert(n.getKind() == kind::SEP_WAND); + if( check ){ + for( unsigned i=0; ibooleanType(); + } +};/* struct EmpStarInternalTypeRule */ + +struct SepLabelTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TypeNode btype = nodeManager->booleanType(); + Assert(n.getKind() == kind::SEP_LABEL); + if( check ){ + TypeNode ctype = n[0].getType( check ); + if( ctype!=btype ){ + throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean"); + } + TypeNode stype = n[1].getType( check ); + if( !stype.isSet() ){ + throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set"); + } + } + return btype; + } +};/* struct SepLabelTypeRule */ + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */ diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 6b268805a..7b9786247 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -37,8 +37,13 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { if( ( parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE /*|| - parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) && + parent.getKind() == kind::REWRITE_RULE || + parent.getKind() == kind::SEP_NIL || + parent.getKind() == kind::SEP_STAR || + parent.getKind() == kind::SEP_WAND || + ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) && current != parent ) { Debug("register::internal") << "quantifier:true" << std::endl; return true; @@ -177,8 +182,13 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { if( ( parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE /*|| - parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) && + parent.getKind() == kind::REWRITE_RULE || + parent.getKind() == kind::SEP_NIL || + parent.getKind() == kind::SEP_STAR || + parent.getKind() == kind::SEP_WAND || + ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) && current != parent ) { Debug("register::internal") << "quantifier:true" << std::endl; return true; diff --git a/src/theory/theory.h b/src/theory/theory.h index 382d4cf65..e8518b1f6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -781,6 +781,14 @@ public: assertions_iterator facts_end() const { return d_facts.end(); } + /** + * Whether facts have been asserted to this theory. + * + * @return true iff facts have been asserted to this theory. + */ + bool hasFacts() { + return !d_facts.empty(); + } typedef context::CDList::const_iterator shared_terms_iterator; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 618fda4c0..78dca299f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -516,18 +516,29 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { - //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL); - if(d_logicInfo.isQuantified()) { - // quantifiers engine must pass effort last call check - d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built - } else if(options::produceModels()) { - // must build model at this point - d_curr_model_builder->buildModel(d_curr_model, true); + //calls to theories requiring the model go here + //FIXME: this should not be theory-specific + if(d_logicInfo.isTheoryEnabled(THEORY_SEP)) { + Assert( d_theoryTable[THEORY_SEP]!=NULL ); + if( d_theoryTable[THEORY_SEP]->hasFacts() ){ + // must build model at this point + d_curr_model_builder->buildModel(getModel(), false); + d_theoryTable[THEORY_SEP]->check(Theory::EFFORT_LAST_CALL); + } } - Trace("theory::assertions-model") << endl; - if (Trace.isOn("theory::assertions-model")) { - printAssertions("theory::assertions-model"); + if( ! d_inConflict && ! needCheck() ){ + if(d_logicInfo.isQuantified()) { + // quantifiers engine must pass effort last call check + d_quantEngine->check(Theory::EFFORT_LAST_CALL); + // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built + } else if(options::produceModels()) { + // must build model at this point + d_curr_model_builder->buildModel(getModel(), true); + } + Trace("theory::assertions-model") << endl; + if (Trace.isOn("theory::assertions-model")) { + printAssertions("theory::assertions-model"); + } } } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6889d1002..a617f9455 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -561,7 +561,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) TheoryModel* tm = (TheoryModel*)m; // buildModel with fullModel = true should only be called once in any context - Assert(!tm->d_modelBuilt); + Assert(!tm->isBuilt()); tm->d_modelBuilt = fullModel; // Reset model @@ -1015,7 +1015,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); if (childrenConst) { retNode = Rewriter::rewrite(retNode); - Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.isConst()); + Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.getKind()==kind::SEP_NIL || retNode.isConst()); } } d_normalizedCache[r] = retNode; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 6e4f77336..833b124eb 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -36,6 +36,7 @@ class TheoryModel : public Model protected: /** substitution map for this model */ SubstitutionMap d_substitutions; + context::CDO d_modelBuilt; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); @@ -51,7 +52,6 @@ public: /** true/false nodes */ Node d_true; Node d_false; - context::CDO d_modelBuilt; mutable std::hash_map d_modelCache; protected: @@ -62,6 +62,8 @@ protected: */ Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; public: + /** is built */ + bool isBuilt() { return d_modelBuilt.get(); } /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) * on this model. diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9c461f57b..ae935798e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -551,9 +551,9 @@ void TheoryUF::eqNotifyNewClass(TNode t) { } void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { - if (getLogicInfo().isQuantified()) { + //if (getLogicInfo().isQuantified()) { //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); - } + //} } void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) { diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 165937c13..7e13668cd 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -87,6 +87,10 @@ Node Valuation::getModelValue(TNode var) { return d_engine->getModelValue(var); } +TheoryModel* Valuation::getModel() { + return d_engine->getModel(); +} + Node Valuation::ensureLiteral(TNode n) { return d_engine->ensureLiteral(n); } diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 4ecdecad0..54af14fdd 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -32,6 +32,7 @@ namespace theory { class EntailmentCheckParameters; class EntailmentCheckSideEffects; +class TheoryModel; /** * The status of an equality in the current context. @@ -105,6 +106,11 @@ public: */ Node getModelValue(TNode var); + /** + * Returns pointer to model. + */ + TheoryModel* getModel(); + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function diff --git a/test/Makefile.am b/test/Makefile.am index dcb58b591..931228f41 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -59,6 +59,7 @@ subdirs_to_check = \ regress/regress0/sets \ regress/regress0/parser \ regress/regress0/sygus \ + regress/regress0/sep \ regress/regress1 \ regress/regress1/arith \ regress/regress2 \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 7d7690d22..45842065f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus sep DIST_SUBDIRS = $(SUBDIRS) # don't override a BINARY imported from a personal.mk diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am new file mode 100644 index 000000000..9d2abaa18 --- /dev/null +++ b/test/regress/regress0/sep/Makefile.am @@ -0,0 +1,76 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + pto-01.smt2 \ + pto-02.smt2 \ + pto-04.smt2 \ + sep-01.smt2 \ + sep-02.smt2 \ + sep-03.smt2 \ + sep-find2.smt2 \ + sep-neg-nstrict.smt2 \ + sep-plus1.smt2 \ + sep-nterm-val-model.smt2 \ + crash1220.smt2 \ + nspatial-simp.smt2 \ + sep-neg-1refine.smt2 \ + sep-neg-simple.smt2 \ + sep-simp-unc.smt2 \ + sep-simp-unsat-emp.smt2 \ + simple-neg-sat.smt2 \ + wand-simp-sat.smt2 \ + wand-simp-sat2.smt2 \ + wand-simp-unsat.smt2 \ + sep-nterm-again.smt2 \ + split-find-unsat.smt2 \ + split-find-unsat-w-emp.smt2 \ + nemp.smt2 \ + wand-crash.smt2 \ + wand-nterm-simp.smt2 \ + wand-nterm-simp2.smt2 \ + loop-1220.smt2 \ + chain-int.smt2 \ + sep-neg-swap.smt2 \ + sep-neg-nstrict2.smt2 \ + dispose-list-4-init.smt2 \ + wand-0526-sat.smt2 \ + quant_wand.smt2 \ + fmf-nemp-2.smt2 + + +FAILING_TESTS = +# loop-1220.smt2 (slow) + +EXTRA_DIST = $(TESTS) + +# slow after changes on Nov 20 : artemis-0512-nonterm.smt2 +# slow after decision engine respects requirePhase: type003.smt2 loop007.smt2 + +# and make sure to distribute it +EXTRA_DIST += + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 new file mode 100644 index 000000000..d3245e33f --- /dev/null +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(assert (sep (pto x y) (pto y z))) +(assert (and (> x 3) (< x 5))) +(assert (and (> y 3) (< y 5))) +(check-sat) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 new file mode 100755 index 000000000..a0fc5a187 --- /dev/null +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) + +(assert (or (pto x a) (sep (pto x a) (pto y b)))) +(assert (or (not (pto x a)) (sep (not (pto x a)) (not (pto y b))))) + +(check-sat) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 new file mode 100644 index 000000000..766354cd9 --- /dev/null +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) + +(declare-sort Loc 0) + +(declare-const w Loc) +(declare-const u1 Loc) +(declare-const u2 Loc) +(declare-const u3 Loc) +(declare-const nil Loc) + +(declare-const w1 Loc) +(declare-const w2 Loc) +(declare-const w3 Loc) +(declare-const w4 Loc) + +; allocated (not nil) +(assert (not (= w nil))) +(assert (not (= u1 nil))) +(assert (not (= u2 nil))) +(assert (not (= u3 nil))) +(assert (not (= w1 nil))) +(assert (not (= w2 nil))) +(assert (not (= w4 nil))) + +; from model +;(assert (= w1 u3)) +;(assert (= w2 u2)) +;(assert (= w3 u1)) +;(assert (= w4 u1)) + +(assert (sep (pto w u1) (pto u1 u2) (pto u2 u3) (pto u3 nil))) +(assert (and (sep (sep (pto w4 w1) (pto w1 w2) (pto w2 nil)) (pto w w3)) (sep (pto w w4) true))) + +(check-sat) diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 new file mode 100644 index 000000000..71fe96d71 --- /dev/null +++ b/test/regress/regress0/sep/fmf-nemp-2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --finite-model-find --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort U 0) +(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))))) +; satisfiable with heap of size 2, model of U of size 3 +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 new file mode 100644 index 000000000..2981606d8 --- /dev/null +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) +(declare-const y0 Int) +(declare-const b0 Int) +(declare-const y00 Int) +(declare-const b00 Int) + +(assert (or false (sep (pto x a) (or false (sep (pto y b) (or false (sep (pto y0 b0) (pto y00 b00) ))))))) +(assert (not (or false (sep (pto x a) (not (or false (sep (pto y b) (not (or false (sep (pto y0 b0) (not (pto y00 b00)) )))))))))) + +(check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 new file mode 100644 index 000000000..e1e21dd10 --- /dev/null +++ b/test/regress/regress0/sep/nemp.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100755 index 000000000..0c93719c9 --- /dev/null +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun x () Int) + +(assert (sep (= x 0) (not (= x 5)))) + +(declare-fun y () Int) +(assert (pto y 0)) +(check-sat) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 new file mode 100644 index 000000000..b0dece248 --- /dev/null +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and (pto x a) (pto x b))) + +(assert (not (= a b))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 new file mode 100644 index 000000000..f0b6d2dee --- /dev/null +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -0,0 +1,25 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + + +(declare-const x Int) + +(declare-const a1 Int) +(declare-const a2 Int) +(declare-const a3 Int) +(declare-const a4 Int) +(declare-const a5 Int) +(declare-const a6 Int) +(declare-const a7 Int) +(declare-const a8 Int) +(declare-const a9 Int) + +(assert (and (pto x a1) (pto x a2) (pto x a3) + (pto x a4) (pto x a5) (pto x a6) + (pto x a7) (pto x a8) (pto x a9) + ) +) + +(assert (not (= a1 a2 a3 a4 a5 a6 a7 a8 a9))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 new file mode 100644 index 000000000..1734c93bb --- /dev/null +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -0,0 +1,36 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const x3 Int) +(declare-const x4 Int) +(declare-const x5 Int) +(declare-const x6 Int) +(declare-const x7 Int) +(declare-const x8 Int) +(declare-const x9 Int) + +(declare-const a1 Int) +(declare-const a2 Int) +(declare-const a3 Int) +(declare-const a4 Int) +(declare-const a5 Int) +(declare-const a6 Int) +(declare-const a7 Int) +(declare-const a8 Int) +(declare-const a9 Int) + +(assert (and (pto x1 a1) (pto x2 a2) (pto x3 a3) + (pto x4 a4) (pto x5 a5) (pto x6 a6) + (pto x7 a7) (pto x8 a8) (pto x9 a9) + ) +) + +(assert (not (and (= x1 x2 x3 x4 x5 x6 x7 x8 x9) + (= a1 a2 a3 a4 a5 a6 a7 a8 a9) + ) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 new file mode 100644 index 000000000..d71b937fc --- /dev/null +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-all +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const u Int) + +(assert (emp 0)) + +(assert +(forall ((y Int)) +(not (wand (pto u 5) (and (= y 42) (pto u 5)))) +)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 new file mode 100644 index 000000000..c3330f036 --- /dev/null +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (sep (pto x a) (pto y b))) + +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 new file mode 100644 index 000000000..403bcf077 --- /dev/null +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (sep (pto x a) (pto y b) (pto z c))) + +(assert (or (= x y) (= y z) (= x z))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 new file mode 100644 index 000000000..427c44b50 --- /dev/null +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and (sep (pto x a) (or (pto x a) (pto y b))) + (sep (pto y b) (or (pto x a) (pto y b))) + ) +) + +(assert (not (sep (pto x a) (pto y b)))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 new file mode 100644 index 000000000..26a27eb22 --- /dev/null +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const x3 Int) +(declare-const x4 Int) +(declare-const x5 Int) +(declare-const x6 Int) +(declare-const x7 Int) + +(declare-const a1 Int) +(declare-const a2 Int) + +(assert (and +(sep (pto x1 a1) (pto x2 a2) (pto x4 a2) (pto x5 a2) (pto x6 a2) (pto x7 a2)) +(sep (pto x1 a1) (pto x3 a2)) +)) + +(assert (distinct x3 x2 x4 x5 x6 x7)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 new file mode 100644 index 000000000..8ddbdd05f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep (pto x a) (pto y b)))) +(assert (sep (pto x a) (pto z b))) + +; sat with model where y != z +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 new file mode 100644 index 000000000..1a69336a8 --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep true (pto x a)))) +(assert (sep (pto x a) (pto z b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 new file mode 100644 index 000000000..e71e6a51a --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (= a b))) +(assert (not (sep true (pto x b)))) +(assert (sep (pto x a) (pto z b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 new file mode 100644 index 000000000..191e7527f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (pto x a))) +(assert (sep (pto x a) (pto z b))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 new file mode 100644 index 000000000..f89a9c0ac --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep (pto y a) (pto x b)))) +(assert (sep (pto x a) (pto y b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 new file mode 100644 index 000000000..9b4afe36a --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (sep (not (pto x a)) (not (pto y b)))) (pto x a) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 new file mode 100644 index 000000000..0178134cb --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) )) + (sep (pto x (+ a 1)) (pto y (+ b 1))) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 new file mode 100644 index 000000000..772acd981 --- /dev/null +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (sep (pto x a) true) + (sep (pto y (+ a 1)) true) +)) +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 new file mode 100755 index 000000000..6cdf51294 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (not (sep (not (pto x a)) (pto y b)))) +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 new file mode 100644 index 000000000..fb58b9d10 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (emp x)) +(assert (sep (pto x a) (pto y b))) +(check-sat) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 new file mode 100644 index 000000000..0c0b6a9a3 --- /dev/null +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (pto y b) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 new file mode 100644 index 000000000..ed3187a96 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x)) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 new file mode 100644 index 000000000..54530cbf4 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 new file mode 100644 index 000000000..0c0ee72ad --- /dev/null +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun u () Int) +(declare-fun v () Int) +(assert (wand (pto x u) (pto y v))) +(assert (emp 0)) +(check-sat) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 new file mode 100644 index 000000000..9b4871323 --- /dev/null +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(assert (wand (emp 0) (emp 0))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 new file mode 100644 index 000000000..e8ee4252c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..69305e95c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (emp x))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 new file mode 100755 index 000000000..df4bfa6d8 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100755 index 000000000..ebc115fdd --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 3))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 new file mode 100755 index 000000000..95bc85537 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 3))) +(assert (emp x)) +(check-sat)