From d01d291be3213368985f28d0072905c4f033d5ff Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 11 Apr 2012 16:31:03 +0000 Subject: [PATCH] merge from arrays-clark branch --- configure.ac | 2 +- src/parser/smt/Smt.g | 8 +- src/parser/smt/smt.cpp | 15 +- src/parser/smt/smt.h | 1 + src/parser/smt2/smt2.cpp | 12 +- src/prop/bvminisat/core/Solver.cc | 15 +- src/prop/bvminisat/core/Solver.h | 2 + src/prop/prop_engine.cpp | 4 + src/prop/prop_engine.h | 5 + src/smt/smt_engine.cpp | 2 + src/theory/arith/theory_arith.cpp | 5 + src/theory/arrays/array_info.cpp | 23 + src/theory/arrays/array_info.h | 13 +- src/theory/arrays/kinds | 6 +- src/theory/arrays/theory_arrays.cpp | 1577 ++++++++--------- src/theory/arrays/theory_arrays.h | 515 ++---- src/theory/arrays/theory_arrays_rewriter.h | 43 +- src/theory/arrays/theory_arrays_type_rules.h | 26 + src/theory/bv/bitblast_strategies.cpp | 2 +- src/theory/bv/bv_sat.cpp | 9 +- src/theory/bv/bv_sat.h | 5 +- src/theory/bv/theory_bv.cpp | 315 +++- src/theory/bv/theory_bv.h | 69 +- .../theory_bv_rewrite_rules_simplification.h | 3 + src/theory/bv/theory_bv_utils.h | 23 + src/theory/shared_terms_database.cpp | 226 ++- src/theory/shared_terms_database.h | 93 +- src/theory/theory.cpp | 2 +- src/theory/theory.h | 4 +- src/theory/theory_engine.cpp | 488 +++-- src/theory/theory_engine.h | 127 +- src/theory/uf/equality_engine.h | 17 + src/theory/uf/equality_engine_impl.h | 65 +- src/theory/uf/theory_uf.cpp | 47 +- src/theory/valuation.cpp | 6 +- src/util/bitvector.h | 8 + src/util/ntuple.h | 2 + test/Makefile.am | 1 + test/regress/regress0/Makefile.am | 2 +- test/regress/regress0/arrays/Makefile.am | 4 +- test/regress/regress0/arrays/x2.smt | 17 + test/regress/regress0/arrays/x3.smt | 46 + test/regress/regress0/aufbv/Makefile.am | 31 + test/regress/regress0/aufbv/bug00.smt | 35 + 44 files changed, 2433 insertions(+), 1488 deletions(-) create mode 100644 test/regress/regress0/arrays/x2.smt create mode 100644 test/regress/regress0/arrays/x3.smt create mode 100644 test/regress/regress0/aufbv/Makefile.am create mode 100644 test/regress/regress0/aufbv/bug00.smt diff --git a/configure.ac b/configure.ac index 47df960d5..bd31b9824 100644 --- a/configure.ac +++ b/configure.ac @@ -882,7 +882,7 @@ if test $cvc4_has_threads = maybe; then LDFLAGS="$cvc4_save_LDFLAGS" fi if test $cvc4_has_threads = no; then - if test $with_portfolio = yes; then + if test x$with_portfolio = xyes; then AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?]) fi with_portfolio=no diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 5a80083b3..6dd4e78f3 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -511,7 +511,13 @@ sortSymbol returns [CVC4::parser::smt::myType t] { $t = PARSER_STATE->getSort(name); } | BITVECTOR_TOK '[' NUMERAL_TOK ']' { $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); - } + } + /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in + * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */ + | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' { + $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)), + EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2))); + } ; /** diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 508bfe352..58495c650 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -44,6 +44,9 @@ std::hash_map Smt::newL logicMap["QF_UFLIRA"] = QF_UFLIRA; logicMap["QF_UFNIA"] = QF_UFNIA; logicMap["QF_UFNIRA"] = QF_UFNIRA; + logicMap["QF_ABV"] = QF_ABV; + logicMap["QF_AUFBV"] = QF_AUFBV; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -188,6 +191,17 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case QF_ABV: + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + + case QF_AUFBV: + addUf(); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + case QF_AUFLIA: addTheory(THEORY_ARRAYS_EX); addUf(); @@ -206,7 +220,6 @@ void Smt::setLogic(const std::string& name) { case AUFNIRA: case LRA: case UFNIA: - case QF_AUFBV: Unhandled(name); } } diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 62bb24336..3a089641f 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -40,6 +40,7 @@ public: AUFLIRA, AUFNIRA, LRA, + QF_ABV, QF_AUFBV, QF_AUFLIA, QF_AUFLIRA, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 39eaf5b95..a4b8647a9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -149,6 +149,17 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case Smt::QF_ABV: + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + break; + + case Smt::QF_AUFBV: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + break; + case Smt::QF_AUFLIA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); @@ -167,7 +178,6 @@ void Smt2::setLogic(const std::string& name) { case Smt::AUFNIRA: case Smt::LRA: case Smt::UFNIA: - case Smt::QF_AUFBV: Unhandled(name); } } diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 238a9cbf7..7e6f4fd93 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -153,7 +153,10 @@ Var Solver::newVar(bool sign, bool dvar) bool Solver::addClause_(vec& ps) { - assert(decisionLevel() == 0); + if (decisionLevel() > 0) { + cancelUntil(0); + } + if (!ok) return false; // Check if clause is satisfied and remove false/duplicate literals: @@ -500,6 +503,7 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { only_bcp = true; ccmin_mode = 0; lbool result = search(-1, UIP_FIRST); + return result; } else { return l_True; } @@ -842,14 +846,7 @@ lbool Solver::solve_() model.clear(); conflict.clear(); - ccmin_mode = 2; - - // reduce the database - reduceDB(); - - // this is a new search, reset the parameters - restart_first = opt_restart_first; - restart_inc = opt_restart_inc; + ccmin_mode = 0; if (!ok) return l_False; diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 33d1900c9..c7346d7f7 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -148,6 +148,8 @@ public: // void addMarkerLiteral(Var var) { + // make sure it wasn't already marked + Assert(marker[var] == 0); marker[var] = 1; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7d4cb7b1c..abe22cb48 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -86,6 +86,10 @@ PropEngine::~PropEngine() { delete d_satSolver; } +void PropEngine::processAssertionsStart() { + d_theoryEngine->preprocessStart(); +} + void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 91b9a61e6..93c35bbf3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -169,6 +169,11 @@ public: */ void shutdown() { } + /** + * Signal that a new round of assertions is ready so we can notify the theory engine + */ + void processAssertionsStart(); + /** * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b6eb3915..e73af60e9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1013,6 +1013,8 @@ void SmtEnginePrivate::processAssertions() { } } + d_smt.d_propEngine->processAssertionsStart(); + // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1c6287c4a..3b29cbcd1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -345,6 +345,11 @@ void TheoryArith::addSharedTerm(TNode n){ } Node TheoryArith::ppRewrite(TNode atom) { + + if (!atom.getType().isBoolean()) { + return atom; + } + Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; Node a = d_pbSubstitutions.apply(atom); diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 50ded8758..cd6c38a7f 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -139,6 +139,20 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){ }; +void ArrayInfo::setNonLinear(const TNode a) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->isNonLinear = true; + info_map[a] = temp_info; + } else { + (*it).second->isNonLinear = true; + } + +} + /** * Returns the information associated with TNode a @@ -152,6 +166,15 @@ const Info* ArrayInfo::getInfo(const TNode a) const{ return emptyInfo; } +const bool ArrayInfo::isNonLinear(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) + return (*it).second->isNonLinear; + return false; +} + List* ArrayInfo::getIndices(const TNode a) const{ CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index d1c435b48..3eae369ca 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -55,9 +55,10 @@ namespace theory { namespace arrays { typedef context::CDList CTNodeList; +typedef quad RowLemmaType; -struct TNodeQuadHashFunction { - size_t operator()(const quad& q ) const { +struct RowLemmaTypeHashFunction { + size_t operator()(const RowLemmaType& q ) const { TNode n1 = q.first; TNode n2 = q.second; TNode n3 = q.third; @@ -66,7 +67,7 @@ struct TNodeQuadHashFunction { n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF); } -};/* struct TNodeQuadHashFunction */ +};/* struct RowLemmaTypeHashFunction */ void printList (CTNodeList* list); void printList( List* list); @@ -81,11 +82,12 @@ bool inList(const CTNodeList* l, const TNode el); class Info { public: + context::CDO isNonLinear; List* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck) { + Info(context::Context* c, Backtracker* bck) : isNonLinear(c, false) { indices = new List(bck); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -228,6 +230,7 @@ public: void addStore(const Node a, const TNode st); void addInStore(const TNode a, const TNode st); + void setNonLinear(const TNode a); /** * Returns the information associated with TNode a @@ -235,6 +238,8 @@ public: const Info* getInfo(const TNode a) const; + const bool isNonLinear(const TNode a) const; + List* getIndices(const TNode a) const; const CTNodeList* getStores(const TNode a) const; diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 2f4bc7313..06240a315 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -7,7 +7,7 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" typechecker "theory/arrays/theory_arrays_type_rules.h" -properties polite stable-infinite +properties polite stable-infinite parametric properties check propagate presolve rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" @@ -24,7 +24,11 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" +# used internally by array theory +operator ARR_TABLE_FUN 4 "array table function" + typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule +typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule endtheory diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 03a9d7a4c..718483143 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,45 +23,87 @@ #include #include "theory/rewriter.h" #include "expr/command.h" +#include "theory/uf/equality_engine_impl.h" + using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::arrays; -TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : +namespace CVC4 { +namespace theory { +namespace arrays { + + +// These are the options that produce the best empirical results on QF_AX benchmarks. +// Use static configuration of options for now +const bool d_ccStore = false; +const bool d_useArrTable = false; +const bool d_eagerLemmas = true; +const bool d_propagateLemmas = false; +const bool d_preprocess = true; +const bool d_solveWrite = true; +const bool d_useNonLinearOpt = true; + + +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARRAY, c, u, out, valuation), - d_ccChannel(this), - d_cc(c, &d_ccChannel), - d_unionFind(c), - d_backtracker(c), - d_infoMap(c,&d_backtracker), - d_disequalities(c), - d_equalities(c), - d_prop_queue(c), - d_atoms(), - d_explanations(c), - d_conflict(), d_numRow("theory::arrays::number of Row lemmas", 0), d_numExt("theory::arrays::number of Ext lemmas", 0), d_numProp("theory::arrays::number of propagations", 0), d_numExplain("theory::arrays::number of explanations", 0), + d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), + d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), d_checkTimer("theory::arrays::checkTime"), - d_donePreregister(false) + d_ppNotify(), + d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"), + d_ppFacts(u), + // d_ppCache(u), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_mayEqualNotify(), + d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"), + d_conflict(c, false), + d_backtracker(c), + d_infoMap(c, &d_backtracker), + d_mergeQueue(c), + d_mergeInProgress(false), + d_RowQueue(u), + d_RowAlreadyAdded(u), + d_sharedArrays(c), + d_sharedTerms(c, false), + d_reads(c), + d_permRef(c) { - //d_backtracker = new Backtracker(c); - //d_infoMap = ArrayInfo(c, d_backtracker); - StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); StatisticsRegistry::registerStat(&d_numProp); StatisticsRegistry::registerStat(&d_numExplain); + StatisticsRegistry::registerStat(&d_numNonLinear); + StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); StatisticsRegistry::registerStat(&d_checkTimer); + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + + d_ppEqualityEngine.addTerm(d_true); + d_ppEqualityEngine.addTerm(d_false); + d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false); + + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::SELECT); + if (d_ccStore) { + d_equalityEngine.addFunctionKind(kind::STORE); + } + d_equalityEngine.addFunctionKind(kind::EQUAL); + if (d_useArrTable) { + d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN); + } } @@ -71,159 +113,27 @@ TheoryArrays::~TheoryArrays() { StatisticsRegistry::unregisterStat(&d_numExt); StatisticsRegistry::unregisterStat(&d_numProp); StatisticsRegistry::unregisterStat(&d_numExplain); + StatisticsRegistry::unregisterStat(&d_numNonLinear); + StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits); StatisticsRegistry::unregisterStat(&d_checkTimer); } -void TheoryArrays::addSharedTerm(TNode t) { - Trace("arrays") << "Arrays::addSharedTerm(): " - << t << endl; -} - - -void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { -} - -void TheoryArrays::notifyCongruent(TNode a, TNode b) { - Trace("arrays") << "Arrays::notifyCongruent(): " - << a << " = " << b << endl; - if(!d_conflict.isNull()) { - return; - } - merge(a,b); -} - - -void TheoryArrays::check(Effort e) { - TimerStat::CodeTimer codeTimer(d_checkTimer); - - if(!d_donePreregister ) { - // only start looking for lemmas after preregister on all input terms - // has been called - return; - } - - Trace("arrays") <<"Arrays::start check "; - while(!done()) { - Node assertion = get(); - Trace("arrays") << "Arrays::check(): " << assertion << endl; - - switch(assertion.getKind()) { - case kind::EQUAL: - case kind::IFF: - d_cc.addEquality(assertion); - if(!d_conflict.isNull()) { - // addEquality can cause a notify congruent which calls merge - // which can lead to a conflict - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - merge(assertion[0], assertion[1]); - break; - case kind::NOT: - { - Assert(assertion[0].getKind() == kind::EQUAL || - assertion[0].getKind() == kind::IFF ); - Node a = assertion[0][0]; - Node b = assertion[0][1]; - addDiseq(assertion[0]); - - d_cc.addTerm(a); - d_cc.addTerm(b); - - if(!d_conflict.isNull()) { - // we got notified through notifyCongruent which called merge - // after addTerm since we weren't watching a or b before - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - else if(find(a) == find(b)) { - Node conflict = constructConflict(assertion[0]); - d_conflict = Node::null(); - d_out->conflict(conflict); - return; - } - Assert(!d_cc.areCongruent(a,b)); - if(a.getType().isArray()) { - queueExtLemma(a, b); - } - break; - } - default: - Unhandled(assertion.getKind()); - } - - } - - if(fullEffort(e)) { - // generate the lemmas on the worklist - //while(!d_RowQueue.empty() || ! d_extQueue.empty()) { - dischargeLemmas(); - Trace("arrays-lem")<<"Arrays::discharged lemmas "< - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - - default: - Unhandled(n.getKind()); - } -} - -Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - switch(in.getKind()) { - case kind::EQUAL: - { - d_staticFactManager.addEq(in); - if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { - outSubstitutions.addSubstitution(in[0], in[1]); - return PP_ASSERT_STATUS_SOLVED; - } - if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { - outSubstitutions.addSubstitution(in[1], in[0]); - return PP_ASSERT_STATUS_SOLVED; - } - break; - } - case kind::NOT: - { - Assert(in[0].getKind() == kind::EQUAL || - in[0].getKind() == kind::IFF ); - Node a = in[0][0]; - Node b = in[0][1]; - d_staticFactManager.addDiseq(in[0]); - break; - } - default: - break; - } - return PP_ASSERT_STATUS_UNSOLVED; -} -Node TheoryArrays::preprocessTerm(TNode term) { +Node TheoryArrays::ppRewrite(TNode term) { + if (!d_preprocess) return term; switch (term.getKind()) { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j if (term[0].getKind() == kind::STORE && - d_staticFactManager.areDiseq(term[0][1], term[1])) { + (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) || + (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; } break; @@ -233,7 +143,8 @@ Node TheoryArrays::preprocessTerm(TNode term) { // IF i != j and j comes before i in the ordering if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && - d_staticFactManager.areDiseq(term[1], term[0][1])) { + (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) || + (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) { Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2]; Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2]; return outer; @@ -241,6 +152,7 @@ Node TheoryArrays::preprocessTerm(TNode term) { break; } case kind::EQUAL: { + if (!d_solveWrite) break; if (term[0].getKind() == kind::STORE || term[1].getKind() == kind::STORE) { TNode left = term[0]; @@ -295,7 +207,8 @@ Node TheoryArrays::preprocessTerm(TNode term) { NodeBuilder<> hyp(kind::AND); for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; - if (d_staticFactManager.areDiseq(index_i, index_j)) { + if (d_ppEqualityEngine.areDisequal(index_i, index_j) || + (index_i.isConst() && index_j.isConst() && index_i != index_j)) { continue; } Node hyp2(index_i.getType() == nm->booleanType()? @@ -338,7 +251,7 @@ Node TheoryArrays::preprocessTerm(TNode term) { Node l = left; Node tmp; NodeBuilder<> nb(kind::AND); - while (right.getKind() == STORE) { + while (right.getKind() == kind::STORE) { tmp = nm->mkNode(kind::SELECT, l, right[1]); nb << tmp.eqNode(right[2]); tmp = nm->mkNode(kind::SELECT, right[0], right[1]); @@ -357,699 +270,683 @@ Node TheoryArrays::preprocessTerm(TNode term) { return term; } -Node TheoryArrays::recursivePreprocessTerm(TNode term) { - unsigned nc = term.getNumChildren(); - if (nc == 0 || - (theoryOf(term) != theory::THEORY_ARRAY && - term.getType() != NodeManager::currentNM()->booleanType())) { - return term; - } - NodeMap::iterator find = d_ppCache.find(term); - if (find != d_ppCache.end()) { - return (*find).second; - } - NodeBuilder<> newNode(term.getKind()); - unsigned i; - for (i = 0; i < nc; ++i) { - newNode << recursivePreprocessTerm(term[i]); - } - Node newTerm = Rewriter::rewrite(newNode); - Node newTerm2 = preprocessTerm(newTerm); - if (newTerm != newTerm2) { - newTerm = recursivePreprocessTerm(Rewriter::rewrite(newTerm2)); - } - d_ppCache[term] = newTerm; - return newTerm; -} -Node TheoryArrays::ppRewrite(TNode atom) { - if (d_donePreregister) return atom; - Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str()); - return recursivePreprocessTerm(atom); +Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { + switch(in.getKind()) { + case kind::EQUAL: + { + d_ppFacts.push_back(in); + d_ppEqualityEngine.addEquality(in[0], in[1], in); + if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + outSubstitutions.addSubstitution(in[0], in[1]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + outSubstitutions.addSubstitution(in[1], in[0]); + return PP_ASSERT_STATUS_SOLVED; + } + break; + } + case kind::NOT: + { + d_ppFacts.push_back(in); + Assert(in[0].getKind() == kind::EQUAL || + in[0].getKind() == kind::IFF ); + Node a = in[0][0]; + Node b = in[0][1]; + d_ppEqualityEngine.addDisequality(a, b, in); + break; + } + default: + break; + } + return PP_ASSERT_STATUS_UNSOLVED; } -void TheoryArrays::merge(TNode a, TNode b) { - Assert(d_conflict.isNull()); +///////////////////////////////////////////////////////////////////////////// +// T-PROPAGATION / REGISTRATION +///////////////////////////////////////////////////////////////////////////// - Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl; - // make "a" the one with shorter diseqList - CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a); - CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); + // If already in conflict, no more propagation + if (d_conflict) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl; + return false; + } - if(deq_ia != d_disequalities.end()) { - if(deq_ib == d_disequalities.end() || - (*deq_ia).second->size() > (*deq_ib).second->size()) { - TNode tmp = a; - a = b; - b = tmp; + // See if the literal has been asserted already + Node normalized = Rewriter::rewrite(literal); + bool satValue = false; + bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); + + // If asserted, we're done or in conflict + if (isAsserted) { + if (!satValue) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + std::vector assumptions; + Node negatedLiteral; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return false; } + // Propagate even if already known in SAT - could be a new equation between shared terms + // (terms that weren't shared when the literal was asserted!) } - a = find(a); - b = find(b); - if( a == b) { - return; - } + // Nothing, just enqueue it for propagation and mark it as asserted already + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + d_literalsToPropagate.push_back(literal); + return true; +}/* TheoryArrays::propagate(TNode) */ - // b becomes the canon of a - setCanon(a, b); - - deq_ia = d_disequalities.find(a); - map alreadyDiseqs; - if(deq_ia != d_disequalities.end()) { - /* - * Collecting the disequalities of b, no need to check for conflicts - * since the representative of b does not change and we check all the things - * in a's class when we look at the diseq list of find(a) - */ - - CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b); - if(deq_ib != d_disequalities.end()) { - CTNodeListAlloc* deq = (*deq_ib).second; - for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) { - TNode deqn = *j; - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - Assert(sp == b || tp == b); - if(sp == b) { - alreadyDiseqs[tp] = deqn; - } else { - alreadyDiseqs[sp] = deqn; - } - } - } - /* - * Looking for conflicts in the a disequality list. Note - * that at this point a and b are already merged. Also has - * the side effect that it adds them to the list of b (which - * became the canonical representative) - */ - - CTNodeListAlloc* deqa = (*deq_ia).second; - for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) { - TNode deqn = (*i); - Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - - if(find(s) == find(t)) { - d_conflict = deqn; +void TheoryArrays::explain(TNode literal, std::vector& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::SELECT: + lhs = literal; + rhs = d_true; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); return; - } - Assert( sp == b || tp == b); - - // make sure not to add duplicates - - if(sp == b) { - if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[tp] = deqn; - } } else { - if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[sp] = deqn; - } + // Predicates + lhs = literal[0]; + rhs = d_false; + break; } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} + + /** + * Stores in d_infoMap the following information for each term a of type array: + * + * - all i, such that there exists a term a[i] or a = store(b i v) + * (i.e. all indices it is being read atl; store(b i v) is implicitly read at + * position i due to the implicit axiom store(b i v)[i] = v ) + * + * - all the stores a is congruent to (this information is context dependent) + * + * - all store terms of the form store (a i v) (i.e. in which a appears + * directly; this is invariant because no new store terms are created) + * + * Note: completeness depends on having pre-register called on all the input + * terms before starting to instantiate lemmas. + */ +void TheoryArrays::preRegisterTerm(TNode node) +{ + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; + + switch (node.getKind()) { + case kind::EQUAL: + // Add the terms + // d_equalityEngine.addTerm(node[0]); + // d_equalityEngine.addTerm(node[1]); + d_equalityEngine.addTerm(node); + // Add the trigger for equality + d_equalityEngine.addTriggerEquality(node[0], node[1], node); + d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); + break; + case kind::SELECT: + // Reads + d_equalityEngine.addTerm(node); + // Maybe it's a predicate + // TODO: remove this or keep it if we allow Boolean elements in arrays. + if (node.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerEquality(node, d_true, node); + d_equalityEngine.addTriggerEquality(node, d_false, node.notNode()); } - } - // TODO: check for equality propagations - // a and b are find(a) and find(b) here - checkPropagations(a,b); + d_infoMap.addIndex(node[0], node[1]); + checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0])); + d_reads.push_back(node); + break; - if(a.getType().isArray()) { - checkRowLemmas(a,b); - checkRowLemmas(b,a); - // note the change in order, merge info adds the list of - // the 2nd argument to the first - d_infoMap.mergeInfo(b, a); - } + case kind::STORE: { + d_equalityEngine.addTriggerTerm(node); + TNode a = node[0]; + TNode i = node[1]; + TNode v = node[2]; -} + d_mayEqualEqualityEngine.addEquality(node, node[0], d_true); + NodeManager* nm = NodeManager::currentNM(); + Node ni = nm->mkNode(kind::SELECT, node, i); + if (!d_equalityEngine.hasTerm(ni)) { + preRegisterTerm(ni); + } -void TheoryArrays::checkPropagations(TNode a, TNode b) { - EqLists::const_iterator ita = d_equalities.find(a); - EqLists::const_iterator itb = d_equalities.find(b); + // Apply RIntro1 Rule + d_equalityEngine.addEquality(ni, v, d_true); - if(ita != d_equalities.end()) { - if(itb!= d_equalities.end()) { - // because b is the canonical representative - List* eqsa = (*ita).second; - List* eqsb = (*itb).second; + d_infoMap.addStore(node, node); + d_infoMap.addInStore(a, node); - for(List::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) { - Node eq = *it; - Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); - if(find(eq[0])== find(eq[1])) { - d_prop_queue.push_back(eq); - } - } - eqsb->concat(eqsa); + checkStore(node); + break; + } + default: + // Variables etc + if (node.getType().isArray()) { + d_equalityEngine.addTriggerTerm(node); } else { - List* eqsb = new List(&d_backtracker); - List* eqsa = (*ita).second; - d_equalities.insert(b, eqsb); - eqsb->concat(eqsa); + d_equalityEngine.addTerm(node); } - } else { - List* eqsb = new List(&d_backtracker); - d_equalities.insert(b, eqsb); - List* eqsa = new List(&d_backtracker); - d_equalities.insert(a, eqsa); - eqsb->concat(eqsa); + break; } } -bool TheoryArrays::isNonLinear(TNode a) { - Assert(a.getType().isArray()); - const CTNodeList* inst = d_infoMap.getInStores(find(a)); - if(inst->size()<=1) { - return false; - } - return true; -} - -bool TheoryArrays::isAxiom(TNode t1, TNode t2) { - Trace("arrays-axiom")<<"Arrays::isAxiom start "<getLevel()) << "TheoryArrays::propagate()" << std::endl; + if (!d_conflict) { + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; + bool satValue; + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + d_out->propagate(literal); + } else { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; + Node negatedLiteral; + std::vector assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; } } } - return false; + } -Node TheoryArrays::constructConflict(TNode diseq) { - Trace("arrays") << "arrays: begin constructConflict()" << endl; - Trace("arrays") << "arrays: using diseq == " << diseq << endl; +Node TheoryArrays::explain(TNode literal) +{ + ++d_numExplain; + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; + std::vector assumptions; + explain(literal, assumptions); + return mkAnd(assumptions); +} + - // returns the reason the two terms are equal - Node explanation = d_cc.explain(diseq[0], diseq[1]); +///////////////////////////////////////////////////////////////////////////// +// SHARING +///////////////////////////////////////////////////////////////////////////// - NodeBuilder<> nb(kind::AND); - if(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF) { - // if the explanation is only one literal - if(!isAxiom(explanation[0], explanation[1]) && - !isAxiom(explanation[1], explanation[0])) { - nb<getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; + d_equalityEngine.addTriggerTerm(t); + if (t.getType().isArray()) { + d_sharedArrays.insert(t,true); } else { - Assert(explanation.getKind() == kind::AND); - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); i++) { - if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) { - nb<<*i; - } - } + d_sharedTerms = true; } - - nb<push_back(b); +EqualityStatus TheoryArrays::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 { - CTNodeList* list = new (true)CTNodeList(getContext()); - list->push_back(b); - d_atoms[a] = list; + if (d_equalityEngine.areDisequal(a, b)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; } - + //TODO: can we be more precise sometimes? + return EQUALITY_UNKNOWN; } -*/ -void TheoryArrays::addEq(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - TNode a = eq[0]; - TNode b = eq[1]; - - // don't need to say find(a) because due to the structure of the lists it gets - // automatically added - appendToEqList(a, eq); - appendToEqList(b, eq); - -} -void TheoryArrays::appendToEqList(TNode n, TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - EqLists::const_iterator it = d_equalities.find(n); - if(it == d_equalities.end()) { - List* eqs = new List(&d_backtracker); - eqs->append(eq); - d_equalities.insert(n, eqs); - } else { - List* eqs = (*it).second; - eqs->append(eq); +void TheoryArrays::computeCareGraph() +{ + if (d_sharedArrays.size() > 0) { + context::CDHashMap::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); + for (; it1 != iend; ++it1) { + for (it2 = it1, ++it2; it2 != iend; ++it2) { + EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first); + if (eqStatusArr != EQUALITY_UNKNOWN) { + continue; + } + Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN); + addCarePair((*it1).first, (*it2).first); + ++d_numSharedArrayVarSplits; + return; + } + } } -} + if (d_sharedTerms) { -void TheoryArrays::addDiseq(TNode diseq) { - Assert(diseq.getKind() == kind::EQUAL || - diseq.getKind() == kind::IFF); - TNode a = diseq[0]; - TNode b = diseq[1]; + vector< pair > currentPairs; - appendToDiseqList(find(a), diseq); - appendToDiseqList(find(b), diseq); + // Go through the read terms and see if there are any to split on + unsigned size = d_reads.size(); + for (unsigned i = 0; i < size; ++ i) { + TNode r1 = d_reads[i]; -} + for (unsigned j = i + 1; j < size; ++ j) { + TNode r2 = d_reads[j]; -void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { - Trace("arrays") << "appending " << eq << endl - << " to diseq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - CNodeTNodesMap::iterator deq_i = d_disequalities.find(of); - CTNodeListAlloc* deq; - if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false, - ContextMemoryAllocator(getContext()->getCMM())); - d_disequalities.insertDataFromContextMemory(of, deq); - } else { - deq = (*deq_i).second; - } + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl; - deq->push_back(eq); -} + // If the terms are already known to be equal, we are also in good shape + if (d_equalityEngine.areEqual(r1, r2)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl; + continue; + } + if (r1[0] != r2[0]) { + // If arrays are known to be disequal, or cannot become equal, we can continue + if (d_equalityEngine.areDisequal(r1[0], r2[0]) || + (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl; + continue; + } + } -/** - * Iterates through the indices of a and stores of b and checks if any new - * Row lemmas need to be instantiated. - */ -bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); + TNode x = r1[1]; + TNode y = r2[1]; - if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 || - d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) { - return true; - } + EqualityStatus eqStatus = getEqualityStatus(x, y); - return false; -} + if (eqStatus != EQUALITY_UNKNOWN) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl; + continue; + } -bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { - NodeManager* nm = NodeManager::currentNM(); - Node aj = nm->mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); + if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; + continue; + } - if(find(i) == find(j) || find(aj) == find(bj)) { - Trace("arrays") << "isRedundantInContext valid " - << a << " " << b << " " << i << " " << j << endl; - checkRowForIndex(j, b); // why am i doing this? - checkRowForIndex(i, a); - return true; - } - Trace("arrays") << "isRedundantInContext " << a << endl - << "isRedundantInContext " << b << endl - << "isRedundantInContext " << i << endl - << "isRedundantInContext " << j << endl; - Node ieqj = i.eqNode(j); - Node literal1 = Rewriter::rewrite(ieqj); - bool hasValue1, satValue1; - Node ff = nm->mkConst(false); - Node tt = nm->mkConst(true); - if (literal1 == ff) { - hasValue1 = true; - satValue1 = false; - } else if (literal1 == tt) { - hasValue1 = true; - satValue1 = true; - } else { - hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); - } - if (hasValue1) { - if (satValue1) { - Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl; - return true; - } - Node ajeqbj = aj.eqNode(bj); - Node literal2 = Rewriter::rewrite(ajeqbj); - bool hasValue2, satValue2; - if (literal2 == ff) { - hasValue2 = true; - satValue2 = false; - } else if (literal2 == tt) { - hasValue2 = true; - satValue2 = true; - } else { - hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); - } - if (hasValue2) { - if (satValue2) { - Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl; - return true; + // Get representative trigger terms + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y); + + EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); + switch (eqStatusDomain) { + case EQUALITY_FALSE_AND_PROPAGATED: + case EQUALITY_FALSE: + continue; + break; + case EQUALITY_TRUE_AND_PROPAGATED: + case EQUALITY_TRUE: + // Should have been propagated to us + Assert(false); + continue; + break; + case EQUALITY_FALSE_IN_MODEL: + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl; + continue; + break; + default: + break; + } + + // Otherwise, add this pair + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl; + addCarePair(x_shared, y_shared); } - // conflict - Assert(!satValue1 && !satValue2); - Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL); - NodeBuilder<2> nb(kind::AND); - //literal1 = areDisequal(literal1[0], literal1[1]); - //literal2 = areDisequal(literal2[0], literal2[1]); - Assert(!literal1.isNull() && !literal2.isNull()); - nb << literal1.notNode() << literal2.notNode(); - literal1 = nb; - d_conflict = Node::null(); - d_out->conflict(literal1); - Trace("arrays") << "TheoryArrays::isRedundantInContext() " - << "conflict via lemma: " << literal1 << endl; - return true; } } - if(alreadyAddedRow(a, b, i, j)) { - Trace("arrays") << "isRedundantInContext already added " - << a << " " << b << " " << i << " " << j << endl; - return true; - } - return false; } -TNode TheoryArrays::areDisequal(TNode a, TNode b) { - Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n"; - - a = find(a); - b = find(b); - - CNodeTNodesMap::const_iterator it = d_disequalities.find(a); - if(it!= d_disequalities.end()) { - CTNodeListAlloc::const_iterator i = (*it).second->begin(); - for( ; i!= (*it).second->end(); i++) { - Trace("arrays-prop") << " " << *i << "\n"; - TNode s = (*i)[0]; - TNode t = (*i)[1]; - - Assert(find(s) == a || find(t) == a); - TNode sp, tp; - if(find(t) == a) { - sp = find(t); - tp = find(s); - } - else { - sp = find(s); - tp = find(t); - } - if(tp == b) { - return *i; - } +///////////////////////////////////////////////////////////////////////////// +// MODEL GENERATION +///////////////////////////////////////////////////////////////////////////// - } - } - Trace("arrays-prop") << " not disequal \n"; - return TNode::null(); -} -bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { - Trace("arrays-prop")<<"Arrays::propagateFromRow "<mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); + switch(n.getKind()) { - Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj); - Node eq_ij = nm->mkNode(kind::EQUAL, i, j); - - // first check if the current context implies NOT (i = j) - // in which case we can propagate a[j] = b[j] - // FIXME: does i = j need to be a SAT literal or can we propagate anyway? - - // if it does not have an atom we must add the lemma (do we?!) - if(d_atoms.count(eq_aj_bj) != 0 || - d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) { - Node diseq = areDisequal(i, j); - // check if the current context implies that (NOT i = j) - if(diseq != TNode::null()) { - // if it's unassigned - Trace("arrays-prop")<<"satValue "<propagate(eq_aj_bj); - ++d_numProp; - // save explanation - d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq)); - return true; - } + case kind::VARIABLE: + Unhandled(kind::VARIABLE); - } - } + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - // now check if the current context implies NOT a[j] = b[j] - // in which case we propagate i = j + default: + Unhandled(n.getKind()); + } +} - // we can't propagate if it does not have an atom - if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) { - Node diseq = areDisequal(aj, bj); - Assert(TNode::null() == Node::null()); +///////////////////////////////////////////////////////////////////////////// +// NOTIFICATIONS +///////////////////////////////////////////////////////////////////////////// - if(diseq != TNode::null()) { - if(d_valuation.getSatValue(eq_ij) == Node::null()) { - d_out->propagate(eq_ij); - ++d_numProp; - // save explanation - d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq)); - return true; - } - } - } - Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; - return false; +void TheoryArrays::presolve() +{ + Trace("arrays")<<"Presolving \n"; } -Node TheoryArrays::explain(TNode n) { +///////////////////////////////////////////////////////////////////////////// +// MAIN SOLVER +///////////////////////////////////////////////////////////////////////////// - Trace("arrays")<<"Arrays::explain start for "< nb(kind::AND); + while (!done() && !d_conflict) + { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; + + // If the assertion doesn't have a literal, it's a shared equality + Assert(assertion.isPreregistered || + ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || + (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && + d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); + + // Do the work + switch (fact.getKind()) { + case kind::EQUAL: + d_equalityEngine.addEquality(fact[0], fact[1], fact); + break; + case kind::SELECT: + d_equalityEngine.addPredicate(fact, true, fact); + break; + case kind::NOT: + if (fact[0].getKind() == kind::SELECT) { + d_equalityEngine.addPredicate(fact[0], false, fact); + } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) { + // Assert the dis-equality + d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); + + // Apply ArrDiseq Rule if diseq is between arrays + if(fact[0][0].getType().isArray()) { + NodeManager* nm = NodeManager::currentNM(); + TypeNode indexType = fact[0][0].getType()[0]; + TNode k; + std::hash_map::iterator it = d_diseqCache.find(fact); + if (it == d_diseqCache.end()) { + Node newk = nm->mkVar(indexType); + Dump.declareVar(newk.toExpr(), + "an extensional lemma index variable from the theory of arrays"); + d_diseqCache[fact] = newk; + k = newk; + } + else { + k = (*it).second; + } - if(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF) { - // if the explanation is only one literal - if(!isAxiom(explanation[0], explanation[1]) && - !isAxiom(explanation[1], explanation[0])) { - nb<mkNode(kind::SELECT, fact[0][0], k); + Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); + if (!d_equalityEngine.hasTerm(ak)) { + preRegisterTerm(ak); + } + if (!d_equalityEngine.hasTerm(bk)) { + preRegisterTerm(bk); + } + d_equalityEngine.addDisequality(ak, bk, fact); + Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n"; + ++d_numExt; + } + } + break; + default: + Unreachable(); } } + + // If in conflict, output the conflict + if (d_conflict) { + Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; + d_out->conflict(d_conflictNode); + } else { - Assert(explanation.getKind() == kind::AND); - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); i++) { - if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) { - nb<<*i; - } + // Otherwise we propagate + propagate(e); + + if(!d_eagerLemmas && fullEffort(e)) { + // generate the lemmas on the worklist + Trace("arrays-lem")<<"Arrays::discharging lemmas: "<, TNodeHashFunction>::const_iterator - it = d_explanations.find(n); - Assert(it!= d_explanations.end()); - TNode diseq = (*it).second.second; - TNode s = diseq[0]; - TNode t = diseq[1]; - TNode eq = (*it).second.first; - TNode a = eq[0]; - TNode b = eq[1]; + Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl; +} - Assert ((find(a) == find(s) && find(b) == find(t)) || - (find(a) == find(t) && find(b) == find(s))); +Node TheoryArrays::mkAnd(std::vector& conjunctions) +{ + Assert(conjunctions.size() > 0); - if(find(a) == find(t)) { - TNode temp = t; - t = s; - s = temp; - } + std::set all; + std::set explained; - // construct the explanation + unsigned i = 0; + TNode t; + for (; i < conjunctions.size(); ++i) { + t = conjunctions[i]; - NodeBuilder<> nb(kind::AND); - Node explanation1 = d_cc.explain(a, s); - Node explanation2 = d_cc.explain(b, t); + // Remove true node - represents axiomatically true assertion + if (t == d_true) continue; - if(explanation1.getKind() == kind::AND) { - for(TNode::iterator i= TNode(explanation1).begin(); - i!=TNode(explanation1).end(); ++i) { - nb << *i; + // Expand explanation resulting from propagating a ROW lemma + if (t.getKind() == kind::OR) { + if ((explained.find(t) == explained.end())) { + Assert(t[1].getKind() == kind::EQUAL); + d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions); + explained.insert(t); + } + continue; } - } else { - Assert(explanation1.getKind() == kind::EQUAL || - explanation1.getKind() == kind::IFF); - nb << explanation1; + all.insert(t); } - if(explanation2.getKind() == kind::AND) { - for(TNode::iterator i= TNode(explanation2).begin(); - i!=TNode(explanation2).end(); ++i) { - nb << *i; - } - } else { - Assert(explanation2.getKind() == kind::EQUAL || - explanation2.getKind() == kind::IFF); - nb << explanation2; + Assert(all.size() > 0); + if (all.size() == 1) { + // All the same, or just one + return *(all.begin()); + } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; } - nb << diseq; - Node reason = nb; - d_out->explanation(reason); - Trace("arrays")<<"explanation "<< reason<<" done \n"; - */ + return conjunction; } -void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<print(); - Trace("arrays-crl")<<" ------------ and "<print(); +void TheoryArrays::setNonLinear(TNode a) +{ + if (d_infoMap.isNonLinear(a)) return; + + Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; + d_infoMap.setNonLinear(a); + ++d_numNonLinear; List* i_a = d_infoMap.getIndices(a); - const CTNodeList* st_b = d_infoMap.getStores(b); - const CTNodeList* inst_b = d_infoMap.getInStores(b); + const CTNodeList* st_a = d_infoMap.getStores(a); + const CTNodeList* inst_a = d_infoMap.getInStores(a); - List::const_iterator it = i_a->begin(); - CTNodeList::const_iterator its; + CTNodeList::const_iterator it = st_a->begin(); - for( ; it != i_a->end(); it++ ) { - TNode i = *it; - its = st_b->begin(); - for ( ; its != st_b->end(); its++) { - TNode store = *its; + // Propagate non-linearity down chain of stores + for(; it!= st_a->end(); ++it) { + TNode store = *it; + Assert(store.getKind()==kind::STORE); + setNonLinear(store[0]); + } + + // Instantiate ROW lemmas that were ignored before + List::const_iterator itl = i_a->begin(); + RowLemmaType lem; + for(; itl != i_a->end(); ++itl ) { + TNode i = *itl; + it = inst_a->begin(); + for ( ; it !=inst_a->end(); ++it) { + TNode store = *it; Assert(store.getKind() == kind::STORE); TNode j = store[1]; TNode c = store[0]; - - if( !isRedundantRowLemma(store, c, j, i)){ - //&&!propagateFromRow(store, c, j, i)) { - queueRowLemma(store, c, j, i); - } + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<begin(); +} - for( ; it != i_a->end(); it++ ) { - TNode i = *it; - its = inst_b->begin(); - for ( ; its !=inst_b->end(); its++) { - TNode store = *its; - Assert(store.getKind() == kind::STORE); - TNode j = store[1]; - TNode c = store[0]; - if ( isNonLinear(c) - &&!isRedundantRowLemma(store, c, j, i)){ - //&&!propagateFromRow(store, c, j, i)) { - queueRowLemma(store, c, j, i); +void TheoryArrays::mergeArrays(TNode a, TNode b) +{ + // Note: a is the new representative + Assert(a.getType().isArray() && b.getType().isArray()); + + if (d_mergeInProgress) { + // Nested call to mergeArrays, just push on the queue and return + d_mergeQueue.push(a.eqNode(b)); + return; + } + + d_mergeInProgress = true; + + Node n; + while (true) { + if (d_useNonLinearOpt) { + bool aNL = d_infoMap.isNonLinear(a); + bool bNL = d_infoMap.isNonLinear(b); + if (aNL) { + if (bNL) { + // already both marked as non-linear - no need to do anything + } + else { + // Set b to be non-linear + setNonLinear(b); + } } + else { + if (bNL) { + // Set a to be non-linear + setNonLinear(a); + } + else { + // Check for new non-linear arrays + const CTNodeList* astores = d_infoMap.getStores(a); + const CTNodeList* bstores = d_infoMap.getStores(a); + Assert(astores->size() <= 1 && bstores->size() <= 1); + if (astores->size() > 0 && bstores->size() > 0) { + setNonLinear(a); + setNonLinear(b); + } + } + } + } + + d_mayEqualEqualityEngine.addEquality(a, b, d_true); + checkRowLemmas(a,b); + checkRowLemmas(b,a); + + // merge info adds the list of the 2nd argument to the first + d_infoMap.mergeInfo(a, b); + + // If no more to do, break + if (d_conflict || d_mergeQueue.empty()) { + break; } - } - Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; + // Otherwise, prepare for next iteration + n = d_mergeQueue.front(); + a = n[0]; + b = n[1]; + d_mergeQueue.pop(); + } + d_mergeInProgress = false; } -/** - * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the - * same and a and b are also not identical. - * - */ - -inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); - // construct lemma - NodeManager* nm = NodeManager::currentNM(); - Node aj = nm->mkNode(kind::SELECT, a, j); - Node bj = nm->mkNode(kind::SELECT, b, j); - Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); - Node eq2 = nm->mkNode(kind::EQUAL, i, j); - Node lem = nm->mkNode(kind::OR, eq2, eq1); +void TheoryArrays::checkStore(TNode a) { + Trace("arrays-cri")<<"Arrays::checkStore "<print(); + } + Assert(a.getType().isArray()); + Assert(a.getKind()==kind::STORE); + TNode b = a[0]; + TNode i = a[1]; + TNode brep = d_equalityEngine.getRepresentative(b); - Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lem); - ++d_numRow; + if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) { + List* js = d_infoMap.getIndices(brep); + List::const_iterator it = js->begin(); + RowLemmaType lem; + for(; it!= js->end(); ++it) { + TNode j = *it; + if (i == j) continue; + lem = make_quad(a,b,i,j); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<print(); } Assert(a.getType().isArray()); + Assert(d_equalityEngine.getRepresentative(a) == a); const CTNodeList* stores = d_infoMap.getStores(a); const CTNodeList* instores = d_infoMap.getInStores(a); CTNodeList::const_iterator it = stores->begin(); + RowLemmaType lem; - for(; it!= stores->end(); it++) { + for(; it!= stores->end(); ++it) { TNode store = *it; Assert(store.getKind()==kind::STORE); TNode j = store[1]; - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<getLevel()) <<"Arrays::checkRowForIndex ("<begin(); - for(; it!= instores->end(); it++) { - TNode instore = *it; - Assert(instore.getKind()==kind::STORE); - TNode j = instore[1]; - //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<begin(); + for(; it!= instores->end(); ++it) { + TNode instore = *it; + Assert(instore.getKind()==kind::STORE); + TNode j = instore[1]; + if (i == j) continue; + lem = make_quad(instore, instore[0], j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<print(); - } - Assert(a.getType().isArray()); - Assert(a.getKind()==kind::STORE); - TNode b = a[0]; - TNode i = a[1]; + Trace("arrays-crl")<<" ------------ and "<print(); - List* js = d_infoMap.getIndices(b); - List::const_iterator it = js->begin(); + List* i_a = d_infoMap.getIndices(a); + const CTNodeList* st_b = d_infoMap.getStores(b); + const CTNodeList* inst_b = d_infoMap.getInStores(b); + + List::const_iterator it = i_a->begin(); + CTNodeList::const_iterator its; - for(; it!= js->end(); it++) { - TNode j = *it; + RowLemmaType lem; - if(!isRedundantRowLemma(a, b, i, j)) { - //Trace("arrays-lem")<<"Arrays::checkRowStore ("<end(); ++it ) { + TNode i = *it; + its = st_b->begin(); + for ( ; its != st_b->end(); ++its) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<begin() ; it != i_a->end(); ++it ) { + TNode i = *it; + its = inst_b->begin(); + for ( ; its !=inst_b->end(); ++its) { + TNode store = *its; + Assert(store.getKind() == kind::STORE); + TNode j = store[1]; + TNode c = store[0]; + lem = make_quad(store, c, j, i); + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + if (!d_equalityEngine.hasTerm(aj)) { + preRegisterTerm(aj); + } + if (!d_equalityEngine.hasTerm(bj)) { + preRegisterTerm(bj); + } + + if (d_equalityEngine.areEqual(aj,bj)) { + return; + } + + if (d_useArrTable) { + Node tableEntry = nm->mkNode(kind::ARR_TABLE_FUN, a, b, i, j); + if (d_equalityEngine.getSize(tableEntry) != 1) { + return; + } + } -/** -* Adds a new Ext lemma of the form -* a = b OR a[k]!=b[k], for a new variable k -*/ + //Propagation + if (d_propagateLemmas) { + if (d_equalityEngine.areDisequal(i,j)) { + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j)); + d_permRef.push_back(reason); + d_equalityEngine.addEquality(aj, bj, reason); + ++d_numProp; + return; + } + if (d_equalityEngine.areDisequal(aj,bj)) { + Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); + d_permRef.push_back(reason); + d_equalityEngine.addEquality(i, j, reason); + ++d_numProp; + return; + } + } -inline void TheoryArrays::addExtLemma(TNode a, TNode b) { - Assert(a.getType().isArray()); - Assert(b.getType().isArray()); + // TODO: maybe add triggers here - Trace("arrays-cle")<<"Arrays::checkExtLemmas "<mkNode(kind::EQUAL, aj, bj); + Node eq2 = nm->mkNode(kind::EQUAL, i, j); + Node lemma = nm->mkNode(kind::OR, eq2, eq1); + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lemma); + ++d_numRow; + } + else { + d_RowQueue.push(lem); + } +} - if( d_extAlreadyAdded.count(make_pair(a, b)) == 0 - && d_extAlreadyAdded.count(make_pair(b, a)) == 0) { +void TheoryArrays::dischargeLemmas() +{ + size_t sz = d_RowQueue.size(); + for (unsigned count = 0; count < sz; ++count) { + RowLemmaType l = d_RowQueue.front(); + d_RowQueue.pop(); + if (d_RowAlreadyAdded.count(l) != 0) { + continue; + } - NodeManager* nm = NodeManager::currentNM(); - TypeNode ixType = a.getType()[0]; - Node k = nm->mkVar(ixType); - Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays"); - Node eq = nm->mkNode(kind::EQUAL, a, b); - Node ak = nm->mkNode(kind::SELECT, a, k); - Node bk = nm->mkNode(kind::SELECT, b, k); - Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk)); - Node lem = nm->mkNode(kind::OR, eq, neq); + TNode a = l.first; + TNode b = l.second; + TNode i = l.third; + TNode j = l.fourth; + Assert(a.getType().isArray() && b.getType().isArray()); + + NodeManager* nm = NodeManager::currentNM(); + Node aj = nm->mkNode(kind::SELECT, a, j); + Node bj = nm->mkNode(kind::SELECT, b, j); + + // Check for redundant lemma + // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context) + if (d_equalityEngine.areEqual(i,j) || + d_equalityEngine.areEqual(a,b) || + d_equalityEngine.areEqual(aj,bj)) { + d_RowQueue.push(l); + continue; + } - Trace("arrays-lem")<<"Arrays::addExtLemma "<lemma(lem); - ++d_numExt; - return; - } + // construct lemma + Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); + Node eq2 = nm->mkNode(kind::EQUAL, i, j); + Node lem = nm->mkNode(kind::OR, eq2, eq1); - Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lem); + ++d_numRow; + } } + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index dcae47dc7..12dbd771d 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,7 +2,7 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: lianah ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -22,17 +22,12 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #include "theory/theory.h" -#include "theory/arrays/union_find.h" -#include "util/congruence_closure.h" #include "theory/arrays/array_info.h" -#include "util/hash.h" -#include "util/ntuple.h" #include "util/stats.h" -#include "util/backtrackable.h" -#include "theory/arrays/static_fact_manager.h" - -#include -#include +#include "theory/uf/equality_engine.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdqueue.h" namespace CVC4 { namespace theory { @@ -87,417 +82,237 @@ namespace arrays { * check. Ext lemmas are stored in a cache to prevent instantiating essentially * the same lemma multiple times. */ -class TheoryArrays : public Theory { -private: +static inline std::string spaces(int level) +{ + std::string indentStr(level, ' '); + return indentStr; +} +class TheoryArrays : public Theory { - class CongruenceChannel { - TheoryArrays* d_arrays; + ///////////////////////////////////////////////////////////////////////////// + // MISC + ///////////////////////////////////////////////////////////////////////////// - public: - CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {} - void notifyCongruent(TNode a, TNode b) { - d_arrays->notifyCongruent(a, b); - } - }; /* class CongruenceChannel*/ - friend class CongruenceChannel; + private: - /** - * Output channel connected to the congruence closure module. - */ - CongruenceChannel d_ccChannel; + /** True node for predicates = true */ + Node d_true; - /** - * Instance of the congruence closure module. - */ - CongruenceClosure d_cc; + /** True node for predicates = false */ + Node d_false; - /** - * (Temporary) fact manager for preprocessing - eventually handle this with - * something more standard (like congruence closure module) - */ - StaticFactManager d_staticFactManager; + // Statistics - /** - * Cache for proprocessing of atoms. - */ - typedef std::hash_map NodeMap; - NodeMap d_ppCache; + /** number of Row lemmas */ + IntStat d_numRow; + /** number of Ext lemmas */ + IntStat d_numExt; + /** number of propagations */ + IntStat d_numProp; + /** number of explanations */ + IntStat d_numExplain; + /** calls to non-linear */ + IntStat d_numNonLinear; + /** splits on array variables */ + IntStat d_numSharedArrayVarSplits; + /** time spent in check() */ + TimerStat d_checkTimer; - /** - * Union find for storing the equalities. - */ + public: - UnionFind d_unionFind; + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + ~TheoryArrays(); - Backtracker d_backtracker; + std::string identify() const { return std::string("TheoryArrays"); } + ///////////////////////////////////////////////////////////////////////////// + // PREPROCESSING + ///////////////////////////////////////////////////////////////////////////// - /** - * Context dependent map from a congruence class canonical representative of - * type array to an Info pointer that keeps track of information useful to axiom - * instantiation - */ + private: - ArrayInfo d_infoMap; + // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used + class PPNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; - /** - * Received a notification from the congruence closure algorithm that the two - * nodes a and b have become congruent. - */ + /** The notify class for d_ppEqualityEngine */ + PPNotifyClass d_ppNotify; - void notifyCongruent(TNode a, TNode b); + /** Equaltity engine */ + uf::EqualityEngine d_ppEqualityEngine; + // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine + context::CDList d_ppFacts; - typedef context::CDChunkList CTNodeListAlloc; - typedef context::CDHashMap CNodeTNodesMap; - typedef context::CDHashMap*, TNodeHashFunction > EqLists; + Node preprocessTerm(TNode term); + Node recursivePreprocessTerm(TNode term); + public: - typedef __gnu_cxx::hash_map NodeTNodesMap; - /** - * List of all disequalities this theory has seen. Maintains the invariant that - * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map - * */ - CNodeTNodesMap d_disequalities; - EqLists d_equalities; - context::CDList d_prop_queue; + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); - void checkPropagations(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // T-PROPAGATION / REGISTRATION + ///////////////////////////////////////////////////////////////////////////// - /** List of all atoms the SAT solver knows about and are candidates for - * propagation. */ - __gnu_cxx::hash_set d_atoms; + private: - /** List of disequalities needed to construct explanations for propagated - * row lemmas */ + /** Literals to propagate */ + context::CDList d_literalsToPropagate; - context::CDHashMap, TNodeHashFunction> d_explanations; + /** Index of the next literal to propagate */ + context::CDO d_literalsToPropagateIndex; - /** - * stores the conflicting disequality (still need to call construct - * conflict to get the actual explanation) - */ - Node d_conflict; + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); - typedef context::CDList< quad > QuadCDList; + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector& assumptions); + public: - /** - * Ext lemma workslist that stores extensionality lemmas that still need to be added - */ - std::hash_set, TNodePairHashFunction> d_extQueue; + void preRegisterTerm(TNode n); + void propagate(Effort e); + Node explain(TNode n); - /** - * Row Lemma worklist, stores lemmas that can still be added to the SAT solver - * to be emptied during full effort check - */ - std::hash_set, TNodeQuadHashFunction > d_RowQueue; + ///////////////////////////////////////////////////////////////////////////// + // SHARING + ///////////////////////////////////////////////////////////////////////////// - /** - * Extensionality lemma cache which stores the array pair (a,b) for which - * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver. - */ - std::hash_set, TNodePairHashFunction> d_extAlreadyAdded; + private: - /** - * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a - * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed - * to prevent infinite recursion in addRowLemma. - */ - std::hash_set, TNodeQuadHashFunction > d_RowAlreadyAdded; + class MayEqualNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; - /* - * Congruence helper methods - */ + /** The notify class for d_mayEqualEqualityEngine */ + MayEqualNotifyClass d_mayEqualNotify; - void addDiseq(TNode diseq); - void addEq(TNode eq); + /** Equaltity engine for determining if two arrays might be equal */ + uf::EqualityEngine d_mayEqualEqualityEngine; - void appendToDiseqList(TNode of, TNode eq); - void appendToEqList(TNode a, TNode b); - Node constructConflict(TNode diseq); + public: - /** - * Merges two congruence classes in the internal union-find and checks for a - * conflict. - */ + void addSharedTerm(TNode t); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void computeCareGraph(); + bool isShared(TNode t) + { return (d_sharedArrays.find(t) != d_sharedArrays.end()); } - void merge(TNode a, TNode b); - inline TNode find(TNode a); - inline TNode debugFind(TNode a) const; - inline void setCanon(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// - void queueRowLemma(TNode a, TNode b, TNode i, TNode j); - inline void queueExtLemma(TNode a, TNode b); + private: + public: - /** - * Adds a Row lemma of the form: - * i = j OR a[j] = b[j] - */ - void addRowLemma(TNode a, TNode b, TNode i, TNode j); + Node getValue(TNode n); - /** - * Adds a new Ext lemma of the form - * a = b OR a[k]!=b[k], for a new variable k - */ - void addExtLemma(TNode a, TNode b); + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// - /** - * Because Row1 axioms of the form (store a i v) [i] = v are not added as - * explicitly but are kept track of internally, is axiom recognizez an axiom - * of the above form given the two terms in the equality. - */ - bool isAxiom(TNode lhs, TNode rhs); + private: + public: + void presolve(); + void shutdown() { } - bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j); - bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j); + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// + public: + void check(Effort e); - bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) { - //Trace("arrays-lem")<<"alreadyAddedRow check for "<, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin(); - a = find(a); - b = find(b); - i = find(i); - j = find(j); + private: - for( ; it!= d_RowAlreadyAdded.end(); it++) { + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass { + TheoryArrays& d_arrays; + public: + NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} - TNode a_ = find((*it).first); - TNode b_ = find((*it).second); - TNode i_ = find((*it).third); - TNode j_ = find((*it).fourth); - if( a == a_ && b == b_ && i==i_ && j==j_) { - //Trace("arrays-lem")<<"alreadyAddedRow found "<getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to arrays + return d_arrays.propagate(propagation); } - return false; - } - - - bool isNonLinear(TNode n); - - /** - * Checks if any new Row lemmas need to be generated after merging arrays a - * and b; called after setCanon. - */ - void checkRowLemmas(TNode a, TNode b); - - /** - * Called after a new select term a[i] is created to check whether new Row - * lemmas need to be instantiated. - */ - void checkRowForIndex(TNode i, TNode a); - - void checkStore(TNode a); - /** - * Lemma helper functions to prevent changing the list we are iterating through. - */ - void insertInQuadQueue(std::set >& queue, TNode a, TNode b, TNode i, TNode j){ - if(i != j) { - queue.insert(make_quad(a,b,i,j)); - } - } - - void dischargeLemmas() { - // we need to swap the temporary lists because adding a lemma calls preregister - // which might modify the d_RowQueue we would be iterating through - std::hash_set, TNodeQuadHashFunction > temp_Row; - temp_Row.swap(d_RowQueue); - - std::hash_set, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin(); - for( ; it1!= temp_Row.end(); it1++) { - if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) { - addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth); - } - else { - // add it to queue may be needed later - queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth); + void notify(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + if (t1.getType().isArray()) { + d_arrays.mergeArrays(t1, t2); + if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { + return; + } } + // Propagate equality between shared terms + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + d_arrays.propagate(equality); } + }; - std::hash_set, TNodePairHashFunction> temp_ext; - temp_ext.swap(d_extQueue); - std::hash_set, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin(); - for(; it2 != temp_ext.end(); it2++) { - addExtLemma((*it2).first, (*it2).second); - } - } + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; - /** Checks if instead of adding a lemma of the form i = j OR a[j] = b[j] - * we can propagate either i = j or NOT a[j] = b[j] and does the propagation. - * Returns whether it did propagate. - */ - bool propagateFromRow(TNode a, TNode b, TNode i, TNode j); + /** Equaltity engine */ + uf::EqualityEngine d_equalityEngine; - TNode areDisequal(TNode a, TNode b); - - - - /* - * === STATISTICS === - */ + // Are we in conflict? + context::CDO d_conflict; - /** number of Row lemmas */ - IntStat d_numRow; - /** number of Ext lemmas */ - IntStat d_numExt; - - /** number of propagations */ - IntStat d_numProp; - IntStat d_numExplain; - /** time spent in check() */ - TimerStat d_checkTimer; - - bool d_donePreregister; - - Node preprocessTerm(TNode term); - Node recursivePreprocessTerm(TNode term); - -public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); - ~TheoryArrays(); + /** The conflict node */ + Node d_conflictNode; /** - * Stores in d_infoMap the following information for each term a of type array: - * - * - all i, such that there exists a term a[i] or a = store(b i v) - * (i.e. all indices it is being read atl; store(b i v) is implicitly read at - * position i due to the implicit axiom store(b i v)[i] = v ) - * - * - all the stores a is congruent to (this information is context dependent) - * - * - all store terms of the form store (a i v) (i.e. in which a appears - * directly; this is invariant because no new store terms are created) - * - * Note: completeness depends on having pre-register called on all the input - * terms before starting to instantiate lemmas. + * Context dependent map from a congruence class canonical representative of + * type array to an Info pointer that keeps track of information useful to axiom + * instantiation */ - void preRegisterTerm(TNode n) { - //TimerStat::CodeTimer codeTimer(d_preregisterTimer); - Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<getLevel()<<"\n"; - d_infoMap.addIndex(n[0], n[1]); - checkRowForIndex(n[1], find(n[0])); - //Trace("arrays-preregister")<<"n[0] \n"; - //d_infoMap.getInfo(n[0])->print(); - //Trace("arrays-preregister")<<"find(n[0]) \n"; - //d_infoMap.getInfo(find(n[0]))->print(); - break; - - case kind::STORE: - { - // this should always be called at level0 since we do not create new store terms - TNode a = n[0]; - TNode i = n[1]; - TNode v = n[2]; - - NodeManager* nm = NodeManager::currentNM(); - Node ni = nm->mkNode(kind::SELECT, n, i); - Node eq = nm->mkNode(kind::EQUAL, ni, v); - - d_cc.addEquality(eq); - - d_infoMap.addIndex(n, i); - d_infoMap.addStore(n, n); - d_infoMap.addInStore(a, n); - - checkStore(n); - - break; - } - default: - Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; - } - } - //void registerTerm(TNode n) { - // Trace("arrays-register")<<"Arrays::registerTerm "< d_backtracker; + ArrayInfo d_infoMap; - void presolve() { - Trace("arrays")<<"Presolving \n"; - d_donePreregister = true; - } + context::CDQueue d_mergeQueue; - void addSharedTerm(TNode t); - void notifyEq(TNode lhs, TNode rhs); - void check(Effort e); + bool d_mergeInProgress; - void propagate(Effort e) { + typedef quad RowLemmaType; - // Trace("arrays-prop")<<"Propagating \n"; + context::CDQueue d_RowQueue; + context::CDHashSet d_RowAlreadyAdded; - // context::CDList::const_iterator it = d_prop_queue.begin(); - /* - for(; it!= d_prop_queue.end(); it++) { - TNode eq = *it; - if(d_valuation.getSatValue(eq).isNull()) { - //FIXME remove already propagated literals? - d_out->propagate(eq); - ++d_numProp; - } - }*/ - //d_prop_queue.deleteSelf(); - /* - __gnu_cxx::hash_set::const_iterator it = d_atoms.begin(); - - for(; it!= d_atoms.end(); it++) { - TNode eq = *it; - Assert(eq.getKind()==kind::EQUAL); - Trace("arrays-prop")<<"value of "< d_sharedArrays; + context::CDO d_sharedTerms; + context::CDList d_reads; + std::hash_map d_diseqCache; - } - Node explain(TNode n); + // List of nodes that need permanent references in this context + context::CDList d_permRef; - Node getValue(TNode n); - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); - void shutdown() { } - std::string identify() const { return std::string("TheoryArrays"); } + Node mkAnd(std::vector& conjunctions); + void setNonLinear(TNode a); + void mergeArrays(TNode a, TNode b); + void checkStore(TNode a); + void checkRowForIndex(TNode i, TNode a); + void checkRowLemmas(TNode a, TNode b); + void queueRowLemma(RowLemmaType lem); + void dischargeLemmas(); };/* class TheoryArrays */ -inline void TheoryArrays::setCanon(TNode a, TNode b) { - d_unionFind.setCanon(a, b); -} - -inline TNode TheoryArrays::find(TNode a) { - return d_unionFind.find(a); -} - -inline TNode TheoryArrays::debugFind(TNode a) const { - return d_unionFind.debugFind(a); -} - }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index f3a19ff02..627f34a30 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -36,11 +36,22 @@ public: Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl; switch (node.getKind()) { case kind::SELECT: { - // select(store(a,i,v),i) = v TNode store = node[0]; - if (store.getKind() == kind::STORE && - store[1] == node[1]) { - return RewriteResponse(REWRITE_DONE, store[2]); + if (store.getKind() == kind::STORE) { + // select(store(a,i,v),j) + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1])); + if (eqRewritten.getKind() == kind::CONST_BOOLEAN) { + bool value = eqRewritten.getConst(); + if (value) { + // select(store(a,i,v),i) = v + return RewriteResponse(REWRITE_DONE, store[2]); + } + else { + // select(store(a,i,v),j) = select(a,j) if i /= j + Node newNode = NodeManager::currentNM()->mkNode(kind::SELECT, store[0], node[1]); + return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + } + } } break; } @@ -53,11 +64,25 @@ public: value[1] == node[1]) { return RewriteResponse(REWRITE_DONE, store); } - // store(store(a,i,v),i,w) = store(a,i,w) - if (store.getKind() == kind::STORE && - store[1] == node[1]) { - Node newNode = NodeManager::currentNM()->mkNode(kind::STORE, store[0], store[1], value); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + if (store.getKind() == kind::STORE) { + // store(store(a,i,v),j,w) + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1])); + if (eqRewritten.getKind() == kind::CONST_BOOLEAN) { + bool val = eqRewritten.getConst(); + NodeManager* nm = NodeManager::currentNM(); + if (val) { + // store(store(a,i,v),i,w) = store(a,i,w) + Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value); + return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + } + else if (node[1] < store[1]) { + // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) + // IF i != j and j comes before i in the ordering + Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value); + newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]); + return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + } + } } break; } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index fd9e7cb2f..fabff0aab 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -65,6 +65,32 @@ struct ArrayStoreTypeRule { } };/* struct ArrayStoreTypeRule */ +struct ArrayTableFunTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::ARR_TABLE_FUN); + TypeNode arrayType = n[0].getType(check); + if( check ) { + if(!arrayType.isArray()) { + throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array"); + } + TypeNode arrType2 = n[1].getType(check); + if(!arrayType.isArray()) { + throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array"); + } + TypeNode indexType = n[2].getType(check); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array"); + } + indexType = n[3].getType(check); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array"); + } + } + return arrayType.getArrayIndexType(); + } +};/* struct ArrayStoreTypeRule */ + struct CardinalityComputer { inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::ARRAY_TYPE); diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index edaf8c154..b579122e5 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -338,7 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { } void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { - Assert (node.getKind() == kind::VARIABLE); + // Assert (node.getKind() == kind::VARIABLE); Assert(bits.size() == 0); for (unsigned i = 0; i < utils::getSize(node); ++i) { diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index f5c43688a..2f4ac1324 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -83,6 +83,9 @@ void Bitblaster::bbAtom(TNode node) { return; } + // make sure it is marked as an atom + addAtom(node); + BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numAtoms; // the bitblasted definition of the atom @@ -298,12 +301,14 @@ void Bitblaster::initAtomBBStrategies() { } void Bitblaster::initTermBBStrategies() { + // Changed this to DefaultVarBB because any foreign kind should be treated as a variable + // TODO: check this is OK for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_termBBStrategies[i] = UndefinedTermBBStrategy; + d_termBBStrategies[i] = DefaultVarBB; } /// setting default bb strategies for terms: - d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; + // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB; d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB; diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 647e4fe9f..2422da0b7 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -82,7 +82,9 @@ class Bitblaster { currently asserted by the DPLL SAT solver. */ /// helper methods + public: bool hasBBAtom(TNode node); + private: bool hasBBTerm(TNode node); void getBBTerm(TNode node, Bits& bits); @@ -101,6 +103,7 @@ class Bitblaster { Node bbOptimize(TNode node); void bbAtom(TNode node); + void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); @@ -116,7 +119,7 @@ public: bool solve(bool quick_solve = false); void bitblast(TNode node); void getConflict(std::vector& conflict); - void addAtom(TNode atom); + bool getPropagations(std::vector& propagations); void explainPropagation(TNode atom, std::vector& explanation); private: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 429e5ff19..a3f4364ba 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,8 +20,8 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/valuation.h" - #include "theory/bv/bv_sat.h" +#include "theory/uf/equality_engine_impl.h" using namespace CVC4; using namespace CVC4::theory; @@ -31,16 +31,67 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; + +const bool d_useEqualityEngine = true; +const bool d_useSatPropagation = true; + + TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_BV, c, u, out, valuation), d_context(c), d_assertions(c), d_bitblaster(new Bitblaster(c) ), d_statistics(), - d_alreadyPropagatedSet(c) - { + d_alreadyPropagatedSet(c), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_conflict(c, false), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_toBitBlast(c) + { d_true = utils::mkTrue(); + d_false = utils::mkFalse(); + + if (d_useEqualityEngine) { + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + + } } + TheoryBV::~TheoryBV() { delete d_bitblaster; } @@ -68,32 +119,99 @@ void TheoryBV::preRegisterTerm(TNode node) { node.getKind() == kind::BITVECTOR_SLT || node.getKind() == kind::BITVECTOR_SLE) { d_bitblaster->bitblast(node); - d_bitblaster->addAtom(node); } + + if (d_useEqualityEngine) { + switch (node.getKind()) { + case kind::EQUAL: + // Add the terms + d_equalityEngine.addTerm(node); + // Add the trigger for equality + d_equalityEngine.addTriggerEquality(node[0], node[1], node); + d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); + break; + default: + d_equalityEngine.addTerm(node); + break; + } + } + } -void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; +void TheoryBV::check(Effort e) +{ + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; - while (!done()) { - TNode assertion = get(); - // make sure we do not assert things we propagated - if (!hasBeenPropagated(assertion)) { - BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; - bool ok = d_bitblaster->assertToSat(assertion, true); + while (!done() && !d_conflict) { + Assertion assertion = get(); + TNode fact = assertion.assertion; + + BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; + + // If the assertion doesn't have a literal, it's a shared equality + bool shared = !assertion.isPreregistered; + Assert(!d_useEqualityEngine || !shared || + ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || + (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && + d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); + + // Notify the Equality Engine + switch (fact.getKind()) { + case kind::EQUAL: + if (d_useEqualityEngine) { + d_equalityEngine.addEquality(fact[0], fact[1], fact); + } + if (shared && !d_bitblaster->hasBBAtom(fact)) { + d_bitblaster->bitblast(fact); + } + break; + case kind::NOT: + if (fact[0].getKind() == kind::EQUAL) { + // Assert the dis-equality + if (d_useEqualityEngine) { + d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); + } + if (shared && !d_bitblaster->hasBBAtom(fact[0])) { + d_bitblaster->bitblast(fact[0]); + } + } else { + if (d_useEqualityEngine) { + d_equalityEngine.addPredicate(fact[0], false, fact); + } + break; + } + break; + default: + if (d_useEqualityEngine) { + d_equalityEngine.addPredicate(fact, true, fact); + } + break; + } + + // make sure we do not assert things we propagated + if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) { + bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation); if (!ok) { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - Node conflict = mkConjunction(conflictAtoms); - d_out->conflict(conflict); - BVDebug("bitvector") << "TheoryBV::check returns conflict: " <getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + d_out->conflict(d_conflictNode); + return; + } + if (e == EFFORT_FULL) { + + Assert(done() && !d_conflict); BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; // in standard effort we only do boolean constraint propagation bool ok = d_bitblaster->solve(false); @@ -127,12 +245,36 @@ Node TheoryBV::getValue(TNode n) { } } -bool TheoryBV::hasBeenPropagated(TNode node) { - return d_alreadyPropagatedSet.count(node); -} void TheoryBV::propagate(Effort e) { - BVDebug("bitvector") << "TheoryBV::propagate() \n"; + BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl; + + if (d_conflict) { + return; + } + + // get new propagations from the equality engine + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; + bool satValue; + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + d_out->propagate(literal); + } else { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + Node negatedLiteral; + std::vector assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return; + } + } // get new propagations from the sat solver std::vector propagations; @@ -142,6 +284,10 @@ void TheoryBV::propagate(Effort e) { for (unsigned i = 0; i < propagations.size(); ++ i) { TNode node = propagations[i]; BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; + if (!d_valuation.isSatLiteral(node)) { + // TODO: maybe propagate shared terms too? + continue; + } if (d_valuation.getSatValue(node) == Node::null()) { vector explanation; d_bitblaster->explainPropagation(node, explanation); @@ -162,21 +308,21 @@ void TheoryBV::propagate(Effort e) { } -Node TheoryBV::explain(TNode n) { - BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; - std::vector explanation; - d_bitblaster->explainPropagation(n, explanation); - Node exp; +// Node TheoryBV::explain(TNode n) { +// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; +// std::vector explanation; +// d_bitblaster->explainPropagation(n, explanation); +// Node exp; - if (explanation.size() == 0) { - return utils::mkTrue(); - } +// if (explanation.size() == 0) { +// return utils::mkTrue(); +// } - exp = utils::mkAnd(explanation); +// exp = utils::mkAnd(explanation); - BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; - return exp; -} +// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; +// return exp; +// } Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { @@ -203,3 +349,108 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu } return PP_ASSERT_STATUS_UNSOLVED; } + + +bool TheoryBV::propagate(TNode literal) +{ + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; + + // If already in conflict, no more propagation + if (d_conflict) { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; + return false; + } + + // See if the literal has been asserted already + Node normalized = Rewriter::rewrite(literal); + bool satValue = false; + bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); + + // If asserted, we might be in conflict + if (isAsserted) { + if (!satValue) { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + std::vector assumptions; + Node negatedLiteral; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return false; + } + // Propagate even if already known in SAT - could be a new equation between shared terms + // (terms that weren't shared when the literal was asserted!) + } + + // Nothing, just enqueue it for propagation and mark it as asserted already + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + d_literalsToPropagate.push_back(literal); + + return true; +}/* TheoryBV::propagate(TNode) */ + + +void TheoryBV::explain(TNode literal, std::vector& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } else { + // Predicates + lhs = literal[0]; + rhs = d_false; + break; + } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} + + +Node TheoryBV::explain(TNode node) { + BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + std::vector assumptions; + explain(node, assumptions); + return mkAnd(assumptions); +} + + +void TheoryBV::addSharedTerm(TNode t) { + Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; + if (d_useEqualityEngine) { + d_equalityEngine.addTriggerTerm(t); + } +} + + +EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) +{ + if (d_useEqualityEngine) { + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + } + return EQUALITY_UNKNOWN; +} + diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d147c8bb5..940eaef56 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -27,6 +27,8 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" +#include "theory/uf/equality_engine.h" +#include "context/cdqueue.h" namespace BVMinisat { class SimpSolver; @@ -40,6 +42,12 @@ namespace bv { /// forward declarations class Bitblaster; +static inline std::string spaces(int level) +{ + std::string indentStr(level, ' '); + return indentStr; +} + class TheoryBV : public Theory { @@ -54,11 +62,11 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; Node d_true; - + Node d_false; + /** Context dependent set of atoms we already propagated */ context::CDHashSet d_alreadyPropagatedSet; - bool hasBeenPropagated(TNode node); public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); @@ -70,8 +78,6 @@ public: void check(Effort e); - void propagate(Effort e); - Node explain(TNode n); Node getValue(TNode n); @@ -93,6 +99,61 @@ private: Statistics d_statistics; + // Added by Clark + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass { + TheoryBV& d_bv; + public: + NotifyClass(TheoryBV& uf): d_bv(uf) {} + + bool notify(TNode propagation) { + Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to bv + return d_bv.propagate(propagation); + } + + void notify(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + // Propagate equality between shared terms + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + d_bv.propagate(t1.eqNode(t2)); + } + }; + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equaltity engine */ + uf::EqualityEngine d_equalityEngine; + + // Are we in conflict? + context::CDO d_conflict; + + /** The conflict node */ + Node d_conflictNode; + + /** Literals to propagate */ + context::CDList d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO d_literalsToPropagateIndex; + + context::CDQueue d_toBitBlast; + + /** 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); + + void addSharedTerm(TNode t); + + EqualityStatus getEqualityStatus(TNode a, TNode b); + +public: + + void propagate(Effort e); + };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index cf8310e5a..530949de2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -866,6 +866,9 @@ Node RewriteRule::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned power = utils::isPow2Const(node[1]) - 1; + if (power == 0) { + return utils::mkConst(utils::getSize(node), 0); + } Node extract = utils::mkExtract(a, power - 1, 0); Node zeros = utils::mkConst(utils::getSize(node) - power, 0); return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 8b5dd0499..38547ad99 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -344,6 +344,29 @@ inline Node mkConjunction(const std::vector& nodes) { } +inline Node mkAnd(const std::vector& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +}/* mkAnd() */ + + // Turn a set into a string inline std::string setToString(const std::set& nodeSet) { std::stringstream out; diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 1687f3480..24cbc165c 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -16,9 +16,43 @@ **/ #include "theory/shared_terms_database.h" +#include "theory/uf/equality_engine_impl.h" using namespace CVC4; -using namespace CVC4::theory; +using namespace theory; + +SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context) + : ContextNotifyObj(context), + d_context(context), + d_statSharedTerms("theory::shared_terms", 0), + d_addedSharedTermsSize(context, 0), + d_termsToTheories(context), + d_alreadyNotifiedMap(context), + d_sharedNotify(notify), + d_termToNotifyList(context), + d_allocatedNLSize(0), + d_allocatedNLNext(context, 0), + d_EENotify(*this), + d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +{ + StatisticsRegistry::registerStat(&d_statSharedTerms); + NodeManager* nm = NodeManager::currentNM(); + d_true = nm->mkConst(true); + d_false = nm->mkConst(false); + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); +} + + +SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) +{ + StatisticsRegistry::unregisterStat(&d_statSharedTerms); + for (unsigned i = 0; i < d_allocatedNLSize; ++i) { + d_allocatedNL[i]->deleteSelf(); + } +} + void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; @@ -30,6 +64,9 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_addedSharedTerms.push_back(atom); d_addedSharedTermsSize = d_addedSharedTermsSize + 1; d_termsToTheories[search_pair] = theories; + if (!d_equalityEngine.hasTerm(term)) { + d_equalityEngine.addTriggerTerm(term); + } } else { Assert(theories != (*find).second); d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); @@ -79,6 +116,7 @@ Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) con return Theory::setDifference((*find).second, alreadyNotified); } + Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { // Get the theories that were already notified AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); @@ -89,7 +127,191 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { } } + +SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList() +{ + NotifyList* retval; + if (d_allocatedNLSize == d_allocatedNLNext) { + retval = new (true) NotifyList(d_context); + d_allocatedNL.push_back(retval); + d_allocatedNLNext = ++d_allocatedNLSize; + } + else { + retval = d_allocatedNL[d_allocatedNLNext]; + d_allocatedNLNext = d_allocatedNLNext + 1; + } + Assert(retval->empty()); + return retval; +} + + +void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) +{ + // Note: a is the new representative + + NotifyList* pnlLeft = NULL; + NotifyList* pnlRight = NULL; + + TermToNotifyList::iterator it = d_termToNotifyList.find(a); + if (it == d_termToNotifyList.end()) { + pnlLeft = getNewNotifyList(); + d_termToNotifyList[a] = pnlLeft; + } + else { + pnlLeft = (*it).second; + } + it = d_termToNotifyList.find(b); + if (it != d_termToNotifyList.end()) { + pnlRight = (*it).second; + } + + // Get theories interested in EC for lhs + Theory::Set lhsSet = getNotifiedTheories(a); + Theory::Set rhsSet = getNotifiedTheories(b); + NotifyList::iterator nit; + TNode left, right; + + for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { + + if (Theory::setContains(currentTheory, rhsSet)) { + right = b; + } + else if (pnlRight != NULL && + ((nit = pnlRight->end()) != pnlRight->end())) { + right = (*nit).second; + } + else { + // no match for right: continue + continue; + } + + if (Theory::setContains(currentTheory, lhsSet)) { + left = a; + } + else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) { + left = (*nit).second; + } + else { + // no match for left: insert right into left + (*pnlLeft)[currentTheory] = right; + continue; + } + + // New shared equality: notify the client + + // TODO: add propagation of disequalities? + + // Normalize the equality + Node equality = left.eqNode(right); + Node normalized = Rewriter::rewriteEquality(currentTheory, equality); + if (normalized.getKind() != kind::CONST_BOOLEAN) { + // Notify client + d_sharedNotify.notify(normalized, equality, currentTheory); + } else { + Assert(equality.getConst()); + } + } + +} + + void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { - d_alreadyNotifiedMap[term] = Theory::setUnion(theories, d_alreadyNotifiedMap[term]); + Theory::Set alreadyNotified = d_alreadyNotifiedMap[term]; + Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified); + if (newlyNotified != 0) { + TNode rep = d_equalityEngine.getRepresentative(term); + if (rep != term) { + TermToNotifyList::iterator it = d_termToNotifyList.find(rep); + Assert(it != d_termToNotifyList.end()); + NotifyList* pnl = (*it).second; + for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { + if (Theory::setContains(theory, newlyNotified) && + pnl->find(theory) == pnl->end()) { + (*pnl)[theory] = term; + } + } + } + } + d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); +} + + +bool SharedTermsDatabase::areEqual(TNode a, TNode b) { + return d_equalityEngine.areEqual(a,b); +} + + +bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { + return d_equalityEngine.areDisequal(a,b); +} + + +void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) +{ + bool negated = literal.getKind() == kind::NOT; + TNode atom = negated ? literal[0] : literal; + if (negated) { + Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); + d_equalityEngine.addDisequality(atom[0], atom[1], reason); + } + else { + Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); + d_equalityEngine.addEquality(atom[0], atom[1], reason); + } } + +static Node mkAnd(const std::vector& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +}/* mkAnd() */ + + +Node SharedTermsDatabase::explain(TNode literal) +{ + std::vector assumptions; + explain(literal, assumptions); + return mkAnd(assumptions); +} + + +void SharedTermsDatabase::explain(TNode literal, std::vector& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 2efd121a0..6af7fd41f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -20,6 +20,7 @@ #include "theory/theory.h" #include "context/context.h" #include "util/stats.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { @@ -34,6 +35,10 @@ public: private: + Node d_true; + + Node d_false; + /** The context */ context::Context* d_context; @@ -59,26 +64,72 @@ private: /** Map from term to theories that have already been notified about the shared term */ AlreadyNotifiedMap d_alreadyNotifiedMap; +public: + /** Class for notifications about new shared term equalities */ + class SharedTermsNotifyClass { + public: + SharedTermsNotifyClass() {} + virtual ~SharedTermsNotifyClass() {} + virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0; + }; + +private: + // Instance of class to send shared term notifications to + SharedTermsNotifyClass& d_sharedNotify; + + // Type for list of theory, node pairs: theory is theory to be notified, + // node is the representative for this equivalence class known to the + // theory that will be notified + typedef context::CDHashMap > NotifyList; + typedef context::CDHashMap TermToNotifyList; + + // Map from terms (only valid for reps) to their notify lists + // Note that theory, term pairs only need to be in the notify list if the + // representative term is not a valid shared term for the theory. + TermToNotifyList d_termToNotifyList; + + // List of allocated NotifyList* objects + std::vector d_allocatedNL; + + // Total number of allocated NotifyList* objects + unsigned d_allocatedNLSize; + + // Size of portion of d_allocatedNL that is currently in use + context::CDO d_allocatedNLNext; + /** This method removes all the un-necessary stuff from the maps */ void backtrack(); -public: + // EENotifyClass: template helper class for d_equalityEngine - handles call-backs + class EENotifyClass { + SharedTermsDatabase& d_sharedTerms; + public: + EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} + bool notify(TNode propagation) { return true; } // Not used + void notify(TNode t1, TNode t2) { + d_sharedTerms.mergeSharedTerms(t1, t2); + } + }; - SharedTermsDatabase(context::Context* context) - : ContextNotifyObj(context), - d_context(context), - d_statSharedTerms("theory::shared_terms", 0), - d_addedSharedTermsSize(context, 0), - d_termsToTheories(context), - d_alreadyNotifiedMap(context) - { - StatisticsRegistry::registerStat(&d_statSharedTerms); - } + /** The notify class for d_equalityEngine */ + EENotifyClass d_EENotify; - ~SharedTermsDatabase() throw(AssertionException) - { - StatisticsRegistry::unregisterStat(&d_statSharedTerms); - } + /** Equaltity engine */ + theory::uf::EqualityEngine d_equalityEngine; + + /** Attach a new notify list to an equivalence class representative */ + NotifyList* getNewNotifyList(); + + /** Method called by equalityEngine when a becomes equal to b */ + void mergeSharedTerms(TNode a, TNode b); + + /** Internal explanation method */ + void explain(TNode literal, std::vector& assumptions); + +public: + + SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context); + ~SharedTermsDatabase() throw(AssertionException); /** * Add a shared term to the database. The shared term is a subterm of the atom and @@ -116,6 +167,18 @@ public: */ void markNotified(TNode term, theory::Theory::Set theories); + bool isShared(TNode term) const { + return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); + } + + bool areEqual(TNode a, TNode b); + + bool areDisequal(TNode a, TNode b); + + void processSharedLiteral(TNode literal, TNode reason); + + Node explain(TNode literal); + /** * This method gets called on backtracks from the context manager. */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 6460533e2..afd311bf2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -60,7 +60,7 @@ void Theory::computeCareGraph() { // We don't care about the terms of different types continue; } - switch (getEqualityStatus(a, b)) { + 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 diff --git a/src/theory/theory.h b/src/theory/theory.h index a8d34eab3..28fdc8cbe 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -281,7 +281,7 @@ public: id = kindToTheoryId(typeNode.getKind()); } if (id == THEORY_BUILTIN) { - Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl; + Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl; return s_uninterpretedSortOwner; } return id; @@ -637,7 +637,7 @@ public: /** a - b */ static inline Set setDifference(Set a, Set b) { - return ((~b) & AllTheories) & a; + return (~b) & a; } static inline std::string setToString(theory::Theory::Set theorySet) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a3ff4d90b..1bb830aa8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -43,15 +43,17 @@ TheoryEngine::TheoryEngine(context::Context* context, d_context(context), d_userContext(userContext), d_activeTheories(context, 0), - d_sharedTerms(context), - d_atomPreprocessingCache(), + d_notify(*this), + d_sharedTerms(d_notify, context), + d_ppCache(), d_possiblePropagations(), d_hasPropagated(context), d_inConflict(context, false), d_sharedTermsExist(context, false), d_hasShutDown(false), d_incomplete(context, false), - d_sharedAssertions(context), + d_sharedLiteralsIn(context), + d_assertedLiteralsOut(context), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), @@ -118,8 +120,8 @@ void TheoryEngine::check(Theory::Effort effort) { // Do the checking try { - // Clear any leftover propagated equalities - d_propagatedEqualities.clear(); + // Clear any leftover propagated shared literals + d_propagatedSharedLiterals.clear(); // Mark the output channel unused (if this is FULL_EFFORT, and nothing // is done by the theories, no additional check will be needed) @@ -173,10 +175,10 @@ void TheoryEngine::check(Theory::Effort effort) { // We are still satisfiable, propagate as much as possible propagate(effort); - // If we have any propagated equalities, we enqueue them to the theories and re-check - if (d_propagatedEqualities.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl; - assertSharedEqualities(); + // If we have any propagated shared literals, we enqueue them to the theories and re-check + if (d_propagatedSharedLiterals.size() > 0) { + Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; + outputSharedLiterals(); continue; } @@ -191,12 +193,12 @@ void TheoryEngine::check(Theory::Effort effort) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl; combineTheories(); - // If we have any propagated equalities, we enqueue them to the theories and re-check - if (d_propagatedEqualities.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl; - assertSharedEqualities(); + // If we have any propagated shared literals, we enqueue them to the theories and re-check + if (d_propagatedSharedLiterals.size() > 0) { + Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; + outputSharedLiterals(); } else { - // No propagated equalities, we're either sat, or there are lemmas added + // No propagated shared literals, we're either sat, or there are lemmas added break; } } else { @@ -204,8 +206,8 @@ void TheoryEngine::check(Theory::Effort effort) { } } - // Clear any leftover propagated equalities - d_propagatedEqualities.clear(); + // Clear any leftover propagated shared literals + d_propagatedSharedLiterals.clear(); Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl; @@ -214,15 +216,15 @@ void TheoryEngine::check(Theory::Effort effort) { } } -void TheoryEngine::assertSharedEqualities() { - // Assert all the shared equalities - for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) { - const SharedEquality& eq = d_propagatedEqualities[i]; +void TheoryEngine::outputSharedLiterals() { + // Assert all the shared literals + for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) { + const SharedLiteral& eq = d_propagatedSharedLiterals[i]; // Check if the theory already got this one - if (d_sharedAssertions.find(eq.toAssert) == d_sharedAssertions.end()) { - Debug("sharing") << "TheoryEngine::assertSharedEqualities(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl; - Debug("sharing") << "TheoryEngine::assertSharedEqualities(): orignal " << eq.toExplain.node << " from " << eq.toExplain.theory << std::endl; - d_sharedAssertions[eq.toAssert] = eq.toExplain; + if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) { + Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl; + Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl; + d_assertedLiteralsOut[eq.toAssert] = eq.toExplain; if (eq.toAssert.theory == theory::THEORY_LAST) { d_propagatedLiterals.push_back(eq.toAssert.node); } else { @@ -231,7 +233,7 @@ void TheoryEngine::assertSharedEqualities() { } } // Clear the equalities - d_propagatedEqualities.clear(); + d_propagatedSharedLiterals.clear(); } @@ -260,40 +262,44 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; + if (d_sharedTerms.areEqual(carePair.a, carePair.b) || + d_sharedTerms.areDisequal(carePair.a, carePair.b)) { + continue; + } + + if (carePair.a.isConst() && carePair.b.isConst()) { + // TODO: equality engine should auto-detect these as disequal + d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst(true)); + continue; + } + Node equality = carePair.a.eqNode(carePair.b); Node normalizedEquality = Rewriter::rewrite(equality); bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN; - - // If the node has a literal, it has been asserted so we should just check it bool value; if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) { + // Missed propagation! Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl; - + if (isTrivial) { - // if the equality is trivial, we assert it back to the theory saying the sat solver should explain value = normalizedEquality.getConst(); + normalizedEquality = NodeManager::currentNM()->mkConst(true); } - - // Normalize the equality to the theory that requested it - Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality); - - if (value) { - SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory); - if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) { - d_propagatedEqualities.push_back(sharedEquality); - } - } else { - SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory); - if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) { - d_propagatedEqualities.push_back(sharedEquality); - } + else { + d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST; + if (!value) normalizedEquality = normalizedEquality.notNode(); } - } else { - Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; - - // There is no value, so we need to split on it - lemma(equality.orNode(equality.notNode()), false, false); + if (!value) { + equality = equality.notNode(); + } + d_sharedTerms.processSharedLiteral(equality, normalizedEquality); + continue; } + + // There is no value, so we need to split on it + Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; + lemma(equality.orNode(equality.notNode()), false, false); + } } @@ -493,6 +499,43 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa return solveStatus; } +// Recursively traverse a term and call the theory rewriter on its sub-terms +Node TheoryEngine::ppTheoryRewrite(TNode term) +{ + NodeMap::iterator find = d_ppCache.find(term); + if (find != d_ppCache.end()) { + return (*find).second; + } + unsigned nc = term.getNumChildren(); + if (nc == 0) { + return theoryOf(term)->ppRewrite(term); + } + Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; + NodeBuilder<> newNode(term.getKind()); + if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { + newNode << term.getOperator(); + } + unsigned i; + for (i = 0; i < nc; ++i) { + newNode << ppTheoryRewrite(term[i]); + } + Node newTerm = Rewriter::rewrite(newNode); + Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm); + if (newTerm != newTerm2) { + newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2)); + } + d_ppCache[term] = newTerm; + Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl; + return newTerm; +} + + +void TheoryEngine::preprocessStart() +{ + d_ppCache.clear(); +} + + struct preprocess_stack_element { TNode node; bool children_added; @@ -518,15 +561,15 @@ Node TheoryEngine::preprocess(TNode assertion) { Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl; // If node already in the cache we're done, pop from the stack - NodeMap::iterator find = d_atomPreprocessingCache.find(current); - if (find != d_atomPreprocessingCache.end()) { + NodeMap::iterator find = d_ppCache.find(current); + if (find != d_ppCache.end()) { toVisit.pop_back(); continue; } - // If this is an atom, we preprocess it with the theory + // If this is an atom, we preprocess its terms with the theory ppRewriter if (Theory::theoryOf(current) != THEORY_BOOL) { - d_atomPreprocessingCache[current] = theoryOf(current)->ppRewrite(current); + d_ppCache[current] = ppTheoryRewrite(current); continue; } @@ -538,13 +581,13 @@ Node TheoryEngine::preprocess(TNode assertion) { builder << current.getOperator(); } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { - Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end()); - builder << d_atomPreprocessingCache[current[i]]; + Assert(d_ppCache.find(current[i]) != d_ppCache.end()); + builder << d_ppCache[current[i]]; } // Mark the substitution and continue Node result = builder; Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl; - d_atomPreprocessingCache[current] = result; + d_ppCache[current] = result; toVisit.pop_back(); } else { // Mark that we have added the children if any @@ -553,59 +596,94 @@ Node TheoryEngine::preprocess(TNode assertion) { // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; - NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode); - if (childFind == d_atomPreprocessingCache.end()) { + NodeMap::iterator childFind = d_ppCache.find(childNode); + if (childFind == d_ppCache.end()) { toVisit.push_back(childNode); } } } else { // No children, so we're done Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl; - d_atomPreprocessingCache[current] = current; + d_ppCache[current] = current; toVisit.pop_back(); } } } // Return the substituted version - return d_atomPreprocessingCache[assertion]; + return d_ppCache[assertion]; } void TheoryEngine::assertFact(TNode node) { Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + Trace("theory::assertFact") << "TheoryEngine::assertFact(" << node << ")" << std::endl; d_propEngine->checkTime(); // Get the atom - TNode atom = node.getKind() == kind::NOT ? node[0] : node; - - // Assert the fact to the appropriate theory and mark it active + bool negated = node.getKind() == kind::NOT; + TNode atom = negated ? node[0] : node; Theory* theory = theoryOf(atom); - theory->assertFact(node, true); - markActive(Theory::setInsert(theory->getId())); - // If any shared terms, notify the theories - if (d_sharedTerms.hasSharedTerms(atom)) { - SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); - SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); - for (; it != it_end; ++ it) { - TNode term = *it; - Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); - for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { - if (Theory::setContains(theory, theories)) { - theoryOf(theory)->addSharedTermInternal(term); + //TODO: there is probably a bug here if shared terms start to exist after some asseritons have been processed + if (d_sharedTermsExist) { + + // If any shared terms, notify the theories + if (d_sharedTerms.hasSharedTerms(atom)) { + SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); + SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); + for (; it != it_end; ++ it) { + TNode term = *it; + Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); + for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) { + if (Theory::setContains(id, theories)) { + theoryOf(id)->addSharedTermInternal(term); + } } + d_sharedTerms.markNotified(term, theories); + markActive(theories); + } + } + + if (atom.getKind() == kind::EQUAL && + d_sharedTerms.isShared(atom[0]) && + d_sharedTerms.isShared(atom[1])) { + Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl; + // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain + if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || + ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { + Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl; + return; + } + d_sharedLiteralsIn[node] = THEORY_LAST; + d_sharedTerms.processSharedLiteral(node, node); + if (d_propagatedSharedLiterals.size() > 0) { + Debug("theory") << "TheoryEngine::assertFact: distributing shared literals" << std::endl; + outputSharedLiterals(); + } + // TODO: have processSharedLiteral propagate disequalities? + if (node.getKind() == kind::EQUAL) { + // Don't have to assert it - this will be taken care of by processSharedLiteral + Assert(isActive(theory->getId())); + return; } - d_sharedTerms.markNotified(term, theories); - markActive(theories); + } + // If theory didn't already get this literal, add to the map + NodeTheoryPair ntp(node, theory->getId()); + if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) { + d_assertedLiteralsOut[ntp] = Node(); } } + + // Assert the fact to the appropriate theory and mark it active + theory->assertFact(node, true); + markActive(Theory::setInsert(theory->getId())); } void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { - Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl; + Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl; d_propEngine->checkTime(); @@ -617,58 +695,51 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { d_hasPropagated.insert(literal); } - TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + bool negated = (literal.getKind() == kind::NOT); + TNode atom = negated ? literal[0] : literal; + bool value; - if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) { - // If not an equality it must be a SAT literal so we enlist it, and it can only - // be propagated by the theory that owns it, as it is the only one that got - // a preregister call with it. + if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL || + !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) { + // If not an equality or if an equality between terms that are not both shared, + // it must be a SAT literal so we enqueue it Assert(d_propEngine->isSatLiteral(literal)); - d_propagatedLiterals.push_back(literal); + if (d_propEngine->hasValue(literal, value)) { + // if we are propagting something that already has a sat value we better be the same + Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; + Assert(value); + } else { + d_propagatedLiterals.push_back(literal); + } } else { - // Otherwise it might be a shared-term (dis-)equality + // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain + if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || + ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { + Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl; + return; + } + + // Otherwise it is a shared-term (dis-)equality Node normalizedLiteral = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedLiteral)) { - // If there is a literal, just enqueue it, same as above - bool value; + // If there is a literal, propagate it to SAT if (d_propEngine->hasValue(normalizedLiteral, value)) { // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; + Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; Assert(value); } else { - SharedEquality sharedEquality(normalizedLiteral, literal, theory, theory::THEORY_LAST); - d_propagatedEqualities.push_back(sharedEquality); - } - } - // Otherwise, we assert it to all interested theories - Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]); - Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]); - // Now notify the theories - if (Theory::setIntersection(lhsNotified, rhsNotified) != 0) { - bool negated = literal.getKind() == kind::NOT; - for (TheoryId currentTheory = theory::THEORY_FIRST; currentTheory != theory::THEORY_LAST; ++ currentTheory) { - if (currentTheory == theory) { - // Don't reassert to the same theory - continue; - } - // Assert if theory is interested in both terms - if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) { - // Normalize the equality - Node equality = Rewriter::rewriteEquality(currentTheory, atom); - if (equality.getKind() != kind::CONST_BOOLEAN) { - // The assertion - Node assertion = negated ? equality.notNode() : equality; - // Remember it to assert later - d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); - } else { - Assert(negated || equality.getConst()); - } - } + SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); + d_propagatedSharedLiterals.push_back(sharedLiteral); } } + // Assert to interested theories + Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; + d_sharedLiteralsIn[literal] = theory; + d_sharedTerms.processSharedLiteral(literal, literal); } } + void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) { Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl; @@ -681,6 +752,14 @@ void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) { theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType() == b.getType()); + if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) { + if (d_sharedTerms.areEqual(a,b)) { + return EQUALITY_TRUE_AND_PROPAGATED; + } + else if (d_sharedTerms.areDisequal(a,b)) { + return EQUALITY_FALSE_AND_PROPAGATED; + } + } return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } @@ -695,29 +774,26 @@ Node TheoryEngine::getExplanation(TNode node) { Theory* theory; //This is true if atom is a shared assertion - bool sharedAssertion = false; + bool sharedLiteral = false; - SharedAssertionsMap::iterator find; + AssertedLiteralsOutMap::iterator find; // "find" will have a value when sharedAssertion is true if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) { - find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST)); - sharedAssertion = (find != d_sharedAssertions.end()); + find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST)); + sharedLiteral = (find != d_assertedLiteralsOut.end()); } // Get the explanation - if(sharedAssertion){ - theory = theoryOf((*find).second.theory); - explanation = theory->explain((*find).second.node); + if(sharedLiteral) { + explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT)); } else { theory = theoryOf(atom); explanation = theory->explain(node); - } - // Explain any shared equalities that might be in the explanation - if (d_sharedTermsExist) { - NodeBuilder<> nb(kind::AND); - explainEqualities(theory->getId(), explanation, nb); - explanation = nb; + // Explain any shared equalities that might be in the explanation + if (d_sharedTermsExist) { + explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId())); + } } Assert(!explanation.isNull()); @@ -730,6 +806,114 @@ Node TheoryEngine::getExplanation(TNode node) { return explanation; } +Node TheoryEngine::explain(ExplainTask toExplain) +{ + Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; + + std::set satAssertions; + std::deque explainQueue; + // TODO: benchmark whether this helps + std::hash_set explained; + bool value; + + // No need to explain "true" + explained.insert(ExplainTask(NodeManager::currentNM()->mkConst(true), SHARED_DATABASE_EXPLANATION)); + + while (true) { + + Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; + + if (explained.find(toExplain) == explained.end()) { + + explained.insert(toExplain); + + if (toExplain.node.getKind() == kind::AND) { + for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) { + explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory)); + } + } + else { + + switch (toExplain.kind) { + + // toExplain.node contains a shared literal sent out from theory engine (before being rewritten) + case SHARED_LITERAL_OUT: { + // Shortcut - see if this came directly from a theory + SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node); + if (it != d_sharedLiteralsIn.end()) { + TheoryId id = (*it).second; + if (id == theory::THEORY_LAST) { + Assert(d_propEngine->isSatLiteral(toExplain.node)); + Assert(d_propEngine->hasValue(toExplain.node, value) && value); + satAssertions.insert(toExplain.node); + break; + } + explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second)); + } + // Otherwise, get explanation from shared terms database + else { + explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION)); + } + break; + } + + // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation + case THEORY_EXPLANATION: { + AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory)); + if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) { + Assert(d_propEngine->isSatLiteral(toExplain.node)); + Assert(d_propEngine->hasValue(toExplain.node, value) && value); + satAssertions.insert(toExplain.node); + } + else { + explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT)); + } + break; + } + + // toExplain.node contains an explanation from the shared terms database + // Each literal in the explanation should be in the d_sharedLiteralsIn map + case SHARED_DATABASE_EXPLANATION: { + Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end()); + TheoryId id = d_sharedLiteralsIn[toExplain.node]; + if (id == theory::THEORY_LAST) { + Assert(d_propEngine->isSatLiteral(toExplain.node)); + Assert(d_propEngine->hasValue(toExplain.node, value) && value); + satAssertions.insert(toExplain.node); + } + else { + explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id)); + } + break; + } + default: + Unreachable(); + } + } + } + + if (explainQueue.empty()) break; + + toExplain = explainQueue.front(); + explainQueue.pop_front(); + } + + Assert(satAssertions.size() > 0); + if (satAssertions.size() == 1) { + return *(satAssertions.begin()); + } + + // Now build the explanation + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = satAssertions.begin(); + std::set::const_iterator it_end = satAssertions.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + return conjunction; +} + void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Mark that we are in conflict @@ -742,9 +926,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { if (d_sharedTermsExist) { // In the multiple-theories case, we need to reconstruct the conflict - NodeBuilder<> nb(kind::AND); - explainEqualities(theoryId, conflict, nb); - Node fullConflict = nb; + Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId)); Assert(properConflict(fullConflict)); Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl; lemma(fullConflict, true, false); @@ -754,47 +936,3 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { lemma(conflict, true, false); } } - -void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) { - Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl; - if (literals.getKind() == kind::AND) { - for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) { - TNode literal = literals[i]; - TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - if (atom.getKind() == kind::EQUAL) { - explainEquality(theoryId, literal, builder); - } else if(literal.getKind() == kind::AND){ - explainEqualities(theoryId, literal, builder); - } else { - builder << literal; - } - } - } else { - TNode atom = literals.getKind() == kind::NOT ? literals[0] : literals; - if (atom.getKind() == kind::EQUAL) { - explainEquality(theoryId, literals, builder); - } else { - builder << literals; - } - } -} - -void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder) { - Assert(eqLiteral.getKind() == kind::EQUAL || (eqLiteral.getKind() == kind::NOT && eqLiteral[0].getKind() == kind::EQUAL)); - - SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId)); - if (find == d_sharedAssertions.end()) { - // Not a shared assertion, just add it since it must be SAT literal - builder << Rewriter::rewrite(eqLiteral); - } else { - TheoryId explainingTheory = (*find).second.theory; - if (explainingTheory == theory::THEORY_LAST) { - // If the theory is from the SAT solver, just take the normalized one - builder << (*find).second.node; - } else { - // Explain it using the theory that propagated it - Node explanation = theoryOf(explainingTheory)->explain((*find).second.node); - explainEqualities(explainingTheory, explanation, builder); - } - } -} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5712b1502..dd642a865 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -98,6 +98,21 @@ class TheoryEngine { */ context::CDO d_activeTheories; + // NotifyClass: template helper class for Shared Terms Database + class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass { + TheoryEngine& d_theoryEngine; + public: + NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {} + ~NotifyClass() {} + + void notify(TNode literal, TNode original, theory::TheoryId theory) { + d_theoryEngine.propagateSharedLiteral(literal, original, theory); + } + }; + + // Instance of NotifyClass + NotifyClass d_notify; + /** * The database of shared terms. */ @@ -106,9 +121,9 @@ class TheoryEngine { typedef std::hash_map NodeMap; /** - * Cache from proprocessing of atoms. + * Cache for theory-preprocessing of assertions */ - NodeMap d_atomPreprocessingCache; + NodeMap d_ppCache; /** * Used for "missed-t-propagations" dumping mode only. A set of all @@ -296,32 +311,55 @@ class TheoryEngine { return theory::Theory::setContains(theory, d_activeTheories); } - struct SharedEquality { + struct SharedLiteral { /** The node/theory pair for the assertion */ + /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */ NodeTheoryPair toAssert; - /** This is the node/theory pair that we will use to explain it */ - NodeTheoryPair toExplain; + /** This is the node that we will use to explain it */ + Node toExplain; - SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory) + SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory) : toAssert(assertion, receivingTheory), - toExplain(original, sendingTheory) + toExplain(original) { } - };/* struct SharedEquality */ + };/* struct SharedLiteral */ /** - * Map from equalities asserted to a theory, to the theory that can explain them. + * Map from nodes to theories. */ - typedef context::CDHashMap SharedAssertionsMap; + typedef context::CDHashMap SharedLiteralsInMap; /** - * A map from asserted facts to where they came from (for explanations). + * All shared literals asserted to theory engine. + * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT). */ - SharedAssertionsMap d_sharedAssertions; + SharedLiteralsInMap d_sharedLiteralsIn; /** - * Assert a shared equalities propagated by theories. + * Map from literals asserted by theory engine to literal that can explain */ - void assertSharedEqualities(); + typedef context::CDHashMap AssertedLiteralsOutMap; + + /** + * All literals asserted to theories from theory engine. + * Maps from literal/theory pair to literal that can explain this assertion. + */ + AssertedLiteralsOutMap d_assertedLiteralsOut; + + /** + * Shared literals queud up to be asserted to the individual theories. + */ + std::vector d_propagatedSharedLiterals; + + void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory) + { + d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory)); + } + + /** + * Assert the shared literals that are queued up to the theories. + */ + void outputSharedLiterals(); /** * Literals that are propagated by the theory. Note that these are TNodes. @@ -335,11 +373,6 @@ class TheoryEngine { */ context::CDO d_propagatedLiteralsIndex; - /** - * Shared term equalities that should be asserted to the individual theories. - */ - std::vector d_propagatedEqualities; - /** * Decisions that are requested via propagateAsDecision(). The theory * can only request decisions on nodes that have an assigned litearl in @@ -466,6 +499,20 @@ public: return d_propEngine; } +private: + + /** + * Helper for preprocess + */ + Node ppTheoryRewrite(TNode term); + +public: + + /** + * Signal the start of a new round of assertion preprocessing + */ + void preprocessStart(); + /** * Runs theory specific preprocesssing on the non-Boolean parts of * the formula. This is only called on input assertions, after ITEs @@ -518,15 +565,6 @@ public: */ void preRegister(TNode preprocessed); - /** - * Call the theories to perform one last rewrite on the theory atoms - * if they wish. This last rewrite is only performed on the input atoms. - * At this point it is ensured that atoms do not contain any Boolean - * strucure, i.e. there is no ITE nodes in them. - * - */ - Node preCheckRewrite(TNode node); - /** * Assert the formula to the appropriate theory. * @param node the assertion @@ -568,6 +606,7 @@ public: void getPropagatedLiterals(std::vector& literals) { for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { + Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); } } @@ -589,8 +628,40 @@ public: bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; + enum ExplainTaskKind { + // Literal sent out from the theory engine + SHARED_LITERAL_OUT, + // Explanation produced by a theory + THEORY_EXPLANATION, + // Explanation produced by the shared terms database + SHARED_DATABASE_EXPLANATION + }; + + struct ExplainTask { + Node node; + ExplainTaskKind kind; + theory::TheoryId theory; + ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) : + node(n), kind(k), theory(tid) {} + bool operator == (const ExplainTask& other) const { + return node == other.node && kind == other.kind && theory == other.theory; + } + }; + + struct ExplainTaskHashFunction { + size_t operator () (const ExplainTask& task) const { + size_t hash = 0; + hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node); + hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2); + hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2); + return hash; + } + }; + Node getExplanation(TNode node); + Node explain(ExplainTask toExplain); + Node getValue(TNode node); /** diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index d8757926a..4eabf63de 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -558,6 +558,11 @@ private: /** The false node */ Node d_false; + /** + * Adds an equality of terms t1 and t2 to the database. + */ + void addEqualityInternal(TNode t1, TNode t2, TNode reason); + public: /** @@ -616,6 +621,11 @@ public: */ bool hasTerm(TNode t) const; + /** + * Adds aa predicate t with given polarity + */ + void addPredicate(TNode t, bool polarity, TNode reason); + /** * Adds an equality t1 = t2 to the database. */ @@ -693,6 +703,13 @@ public: * Check whether the two term are dis-equal. */ bool areDisequal(TNode t1, TNode t2); + + /** + * Return the number of nodes in the equivalence class contianing t + * Adds t if not already there. + */ + size_t getSize(TNode t); + }; } // Namespace uf diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index dd1bf0cbc..be12e5f19 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -188,9 +188,9 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId } template -void EqualityEngine::addEquality(TNode t1, TNode t2, TNode reason) { +void EqualityEngine::addEqualityInternal(TNode t1, TNode t2, TNode reason) { - Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl; // Add the terms if they are not already in the database addTerm(t1); @@ -200,19 +200,39 @@ void EqualityEngine::addEquality(TNode t1, TNode t2, TNode reason) EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t2Id = getNodeId(t2); enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason)); + propagate(); } +template +void EqualityEngine::addPredicate(TNode t, bool polarity, TNode reason) { + + Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; + + addEqualityInternal(t, polarity ? d_true : d_false, reason); +} + +template +void EqualityEngine::addEquality(TNode t1, TNode t2, TNode reason) { + + Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; + + addEqualityInternal(t1, t2, reason); + + Node equality = t1.eqNode(t2); + addEqualityInternal(equality, d_true, reason); +} + template void EqualityEngine::addDisequality(TNode t1, TNode t2, TNode reason) { Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl; Node equality1 = t1.eqNode(t2); - addEquality(equality1, d_false, reason); - + addEqualityInternal(equality1, d_false, reason); + Node equality2 = t2.eqNode(t1); - addEquality(equality2, d_false, reason); + addEqualityInternal(equality2, d_false, reason); } @@ -516,9 +536,6 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, std::vecto // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms (they might not be there) addTerm(t1); addTerm(t2); @@ -537,8 +554,6 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, std::vecto EqualityNodeId t2Id = getNodeId(t2); getExplanation(t1Id, t2Id, equalities); - // Pop the possible extra information - d_context->pop(); } template @@ -548,9 +563,6 @@ void EqualityEngine::explainDisequality(TNode t1, TNode t2, std::ve // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); @@ -573,8 +585,6 @@ void EqualityEngine::explainDisequality(TNode t1, TNode t2, std::ve EqualityNodeId falseId = getNodeId(d_false); getExplanation(equalityId, falseId, equalities); - // Pop the possible extra information - d_context->pop(); } @@ -722,6 +732,10 @@ void EqualityEngine::addTriggerEquality(TNode t1, TNode t2, TNode t } } + if (Debug.isOn("equality::internal")) { + debugPrintGraph(); + } + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl; } @@ -809,17 +823,11 @@ bool EqualityEngine::areEqual(TNode t1, TNode t2) // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); - // Pop the context (triggers new term removal) - d_context->pop(); - // Return whether the two terms are equal return equal; } @@ -830,9 +838,6 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2) // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); @@ -841,17 +846,21 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2) Node equality = t1.eqNode(t2); addTerm(equality); if (getEqualityNode(equality).getFind() == getEqualityNode(d_false).getFind()) { - d_context->pop(); return true; } - // Pop the context (triggers new term removal) - d_context->pop(); - // Return whether the terms are disequal return false; } +template +size_t EqualityEngine::getSize(TNode t) +{ + // Add the term + addTerm(t); + return getEqualityNode(getEqualityNode(t).getFind()).getSize(); +} + template void EqualityEngine::addTriggerTerm(TNode t) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4ac81bc74..f53918683 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -96,11 +96,11 @@ void TheoryUF::check(Effort level) { d_equalityEngine.addEquality(fact[0], fact[1], fact); break; case kind::APPLY_UF: - d_equalityEngine.addEquality(fact, d_true, fact); + d_equalityEngine.addPredicate(fact, true, fact); break; case kind::NOT: if (fact[0].getKind() == kind::APPLY_UF) { - d_equalityEngine.addEquality(fact[0], d_false, fact); + d_equalityEngine.addPredicate(fact[0], false, fact); } else { // Assert the dis-equality d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); @@ -132,24 +132,21 @@ void TheoryUF::propagate(Effort level) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; bool satValue; - if (!d_valuation.hasSatValue(literal, satValue)) { + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { d_out->propagate(literal); } else { - if (!satValue) { - Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl; - Node negatedLiteral; - std::vector assumptions; - if (literal != d_false) { - negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); - assumptions.push_back(negatedLiteral); - } - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; - } else { - Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl; + Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl; + Node negatedLiteral; + std::vector assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; } } } @@ -196,20 +193,18 @@ bool TheoryUF::propagate(TNode literal) { } // See if the literal has been asserted already + Node normalized = Rewriter::rewrite(literal); bool satValue = false; - bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue); + bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); // If asserted, we're done or in conflict if (isAsserted) { - if (satValue) { - Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl; - return true; - } else { - Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl; + if (!satValue) { + Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; std::vector assumptions; Node negatedLiteral; - if (literal != d_false) { - negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); assumptions.push_back(negatedLiteral); } explain(literal, assumptions); @@ -217,6 +212,8 @@ bool TheoryUF::propagate(TNode literal) { d_conflict = true; return false; } + // Propagate even if already known in SAT - could be a new equation between shared terms + // (terms that weren't shared when the literal was asserted!) } // Nothing, just enqueue it for propagation and mark it as asserted already diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 627125a27..5eb4f0dc7 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -79,9 +79,9 @@ Node Valuation::getSatValue(TNode n) const { } bool Valuation::hasSatValue(TNode n, bool& value) const { - Node normalized = Rewriter::rewrite(n); - if (d_engine->getPropEngine()->isSatLiteral(normalized)) { - return d_engine->getPropEngine()->hasValue(normalized, value); + // Node normalized = Rewriter::rewrite(n); + if (d_engine->getPropEngine()->isSatLiteral(n)) { + return d_engine->getPropEngine()->hasValue(n, value); } else { return false; } diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 512f23136..5d0c301d4 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -188,12 +188,20 @@ public: BitVector unsignedDiv (const BitVector& y) const { Assert (d_size == y.d_size); + // TODO: decide whether we really want these semantics + if (y.d_value == 0) { + return BitVector(d_size, Integer(0)); + } Assert (d_value >= 0 && y.d_value > 0); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } BitVector unsignedRem(const BitVector& y) const { Assert (d_size == y.d_size); + // TODO: decide whether we really want these semantics + if (y.d_value == 0) { + return BitVector(d_size, Integer(0)); + } Assert (d_value >= 0 && y.d_value > 0); return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } diff --git a/src/util/ntuple.h b/src/util/ntuple.h index 4f8b73945..a3d28977f 100644 --- a/src/util/ntuple.h +++ b/src/util/ntuple.h @@ -30,6 +30,7 @@ public: T1 first; T2 second; T3 third; + triple() {} triple(const T1& t1, const T2& t2, const T3& t3) : first(t1), second(t2), @@ -50,6 +51,7 @@ public: T2 second; T3 third; T4 fourth; + quad() {} quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) : first(t1), second(t2), diff --git a/test/Makefile.am b/test/Makefile.am index 2bcb283d7..a870ac44a 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -39,6 +39,7 @@ subdirs_to_check = \ regress/regress0/bv \ regress/regress0/bv/core \ regress/regress0/arrays \ + regress/regress0/aufbv \ regress/regress0/datatypes \ regress/regress0/lemmas \ regress/regress0/push-pop \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9245bb0af..3d68b73cb 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 datatypes lemmas push-pop preprocess +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv datatypes lemmas push-pop preprocess BINARY = cvc4 if PROOF_REGRESSIONS diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index b112d1129..5a18658d5 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -25,7 +25,9 @@ TESTS = \ incorrect8.minimized.smt \ incorrect9.smt \ incorrect10.smt \ - incorrect11.smt + incorrect11.smt \ + x2.smt \ + x3.smt EXTRA_DIST = $(TESTS) \ bug272.smt \ diff --git a/test/regress/regress0/arrays/x2.smt b/test/regress/regress0/arrays/x2.smt new file mode 100644 index 000000000..c043e88b9 --- /dev/null +++ b/test/regress/regress0/arrays/x2.smt @@ -0,0 +1,17 @@ +(benchmark read5.smt +:logic QF_AX +:status unsat +:extrafuns ((a Index)) +:extrafuns ((S Array)) +:extrafuns ((SS Array)) +:status unknown +:formula +(flet ($n1 (= S SS)) +(let (?n2 (select S a)) +(let (?n3 (store SS a ?n2)) +(flet ($n4 (= S ?n3)) +(flet ($n5 true) +(flet ($n6 (if_then_else $n1 $n4 $n5)) +(flet ($n7 (not $n6)) +$n7 +)))))))) diff --git a/test/regress/regress0/arrays/x3.smt b/test/regress/regress0/arrays/x3.smt new file mode 100644 index 000000000..ff070f142 --- /dev/null +++ b/test/regress/regress0/arrays/x3.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_AX +:status sat +:extrafuns ((v4 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v1 Array)) +:extrafuns ((v6 Element)) +:extrafuns ((v0 Array)) +:extrafuns ((v5 Element)) +:status unknown +:formula +(let (?n1 (store v1 v3 v6)) +(flet ($n2 (distinct ?n1 v0)) +(flet ($n3 (= v4 v2)) +(flet ($n4 true) +(let (?n5 (store v1 v4 v6)) +(let (?n6 (select ?n5 v2)) +(let (?n7 (ite $n4 ?n6 v6)) +(let (?n8 (select v1 v3)) +(let (?n9 (ite $n3 ?n7 ?n8)) +(flet ($n10 (distinct ?n8 ?n8)) +(let (?n11 (ite $n10 v6 ?n6)) +(let (?n12 (ite $n2 ?n9 ?n11)) +(flet ($n13 (= v6 ?n12)) +(flet ($n14 (distinct ?n8 v5)) +(let (?n15 (ite $n2 v1 v0)) +(let (?n16 (ite $n14 v1 ?n15)) +(flet ($n17 (distinct ?n5 ?n16)) +(flet ($n18 (and $n13 $n17)) +(flet ($n19 (distinct v0 ?n5)) +(let (?n20 (ite $n19 v2 v4)) +(flet ($n21 (= v3 v2)) +(flet ($n22 (= v0 v0)) +(flet ($n23 (= v6 ?n8)) +(flet ($n24 false) +(flet ($n25 (= ?n6 ?n8)) +(let (?n26 (ite $n25 v3 v2)) +(let (?n27 (ite $n24 v4 ?n26)) +(let (?n28 (ite $n23 v3 ?n27)) +(let (?n29 (ite $n22 ?n28 v4)) +(let (?n30 (ite $n21 v3 ?n29)) +(flet ($n31 (distinct ?n20 ?n30)) +(flet ($n32 (or $n18 $n31)) +$n32 +))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am new file mode 100644 index 000000000..9afa37e46 --- /dev/null +++ b/test/regress/regress0/aufbv/Makefile.am @@ -0,0 +1,31 @@ +if PROOF_REGRESSIONS +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4 +else +TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4 +endif + +# 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 = \ + bug00.smt + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# 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/aufbv/bug00.smt b/test/regress/regress0/aufbv/bug00.smt new file mode 100644 index 000000000..d662207dd --- /dev/null +++ b/test/regress/regress0/aufbv/bug00.smt @@ -0,0 +1,35 @@ +(benchmark no_init_multi_member7.smt +:logic QF_AUFBV +:status unsat +:extrafuns ((member_6_curr_2 BitVec[32])) +:extrafuns ((arr_next_15 Array[32:32])) +:extrafuns ((member_3_curr_4 BitVec[32])) +:extrafuns ((main_0_x_3 BitVec[32])) +:extrafuns ((member_3_curr_5 BitVec[32])) +:extrafuns ((arr_val_8 Array[32:32])) +:status unknown +:formula +(flet ($n1 true) +(let (?n2 bv0[32]) +(let (?n3 bv1[32]) +(let (?n4 (select arr_val_8 member_6_curr_2)) +(flet ($n5 (= ?n3 ?n4)) +(let (?n6 (ite $n5 ?n3 ?n2)) +(flet ($n7 (= ?n2 ?n6)) +(let (?n8 (select arr_next_15 member_3_curr_5)) +(flet ($n9 (= ?n2 ?n8)) +(let (?n10 (select arr_next_15 ?n3)) +(flet ($n11 (= ?n10 member_3_curr_4)) +(let (?n12 (select arr_next_15 ?n2)) +(flet ($n13 (= ?n3 ?n12)) +(flet ($n14 (= ?n2 main_0_x_3)) +(flet ($n15 (= ?n3 member_3_curr_4)) +(flet ($n16 (and $n14 $n15)) +(let (?n17 (ite $n16 ?n2 member_3_curr_4)) +(flet ($n18 (= member_3_curr_5 ?n17)) +(flet ($n19 (= member_6_curr_2 ?n12)) +(let (?n20 (select arr_next_15 member_6_curr_2)) +(flet ($n21 (= ?n2 ?n20)) +(flet ($n22 (and $n7 $n9 $n11 $n13 $n18 $n19 $n1 $n21)) +$n22 +))))))))))))))))))))))) -- 2.30.2