diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 137 |
1 files changed, 111 insertions, 26 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 631785437..fcde18b66 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,13 +21,14 @@ #include "expr/kind.h" #include "options/arrays_options.h" #include "options/smt_options.h" +#include "proof/array_proof.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" #include "smt/command.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_model.h" -#include "proof/theory_proof.h" -#include "proof/proof_manager.h" #include "theory/valuation.h" using namespace std; @@ -78,7 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true), d_conflict(c, false), d_backtracker(c), - d_infoMap(c, &d_backtracker), + d_infoMap(c, &d_backtracker, name), d_mergeQueue(c), d_mergeInProgress(false), d_RowQueue(c), @@ -383,21 +384,27 @@ bool TheoryArrays::propagate(TNode literal) }/* TheoryArrays::propagate(TNode) */ -void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { +void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; //eq::EqProof * eqp = new eq::EqProof; - eq::EqProof * eqp = NULL; + // eq::EqProof * eqp = NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); + d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof); } - if( eqp ){ - Debug("array-pf") << " Proof is : " << std::endl; - eqp->debug_print("array-pf"); + if(proof){ + Debug("pf::array") << " Proof is : " << std::endl; + proof->debug_print("pf::array"); } + + Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl << "\t"; + for (unsigned i = 0; i < assumptions.size(); ++i) { + Debug("pf::array") << assumptions[i] << " "; + } + Debug("pf::array") << std::endl; } TNode TheoryArrays::weakEquivGetRep(TNode node) { @@ -597,7 +604,7 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) { } } } - } + } } /** @@ -787,6 +794,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) else { d_equalityEngine.addTerm(node); } + break; } // Invariant: preregistered terms are exactly the terms in the equality engine @@ -807,12 +815,16 @@ void TheoryArrays::propagate(Effort e) } -Node TheoryArrays::explain(TNode literal) +Node TheoryArrays::explain(TNode literal) { + return explain(literal, NULL); +} + +Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) { ++d_numExplain; Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; - explain(literal, assumptions); + explain(literal, assumptions, proof); return mkAnd(assumptions); } @@ -1230,7 +1242,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type makeEqual = false; } } + + Debug("pf::array") << "Pregistering a Skolem" << std::endl; preRegisterTermInternal(skolem); + Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl; + if (makeEqual) { Node d = skolem.eqNode(ref); Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; @@ -1239,6 +1255,8 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type d_skolemAssertions.push_back(d); d_skolemIndex = d_skolemIndex + 1; } + + Debug("pf::array") << "getSkolem DONE" << std::endl; return skolem; } @@ -1293,28 +1311,76 @@ void TheoryArrays::check(Effort e) { // Apply ArrDiseq Rule if diseq is between arrays if(fact[0][0].getType().isArray() && !d_conflict) { + if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; } + NodeManager* nm = NodeManager::currentNM(); TypeNode indexType = fact[0][0].getType()[0]; - TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false); + + TNode k; + // k is the skolem for this disequality. + if (!d_proofsEnabled) { + Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl; + + // If not in replay mode, generate a fresh skolem variable + k = getSkolem(fact, + "array_ext_index", + indexType, + "an extensional lemma index variable from the theory of arrays", + false); + + // Register this skolem for the proof replay phase + PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k)); + } else { + if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) { + // In the solution pass we didn't need this skolem. Therefore, we don't need it + // in this reply pass, either. + break; + } + + // Reuse the same skolem as in the solution pass + k = ProofManager::getSkolemizationManager()->getSkolem(fact); + Debug("pf::array") << "Skolem = " << k << std::endl; + } Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); Node eq = ak.eqNode(bk); Node lemma = fact[0].orNode(eq.notNode()); + + // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered + // when we output the lemma. However, in replay need the lemma to be propagated, and so we + // preregister manually. + if (d_proofsEnabled) { + if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); } + if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); } + } + if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) { // Propagate witness disequality - might produce a conflict d_permRef.push_back(lemma); - d_equalityEngine.assertEquality(eq, false, lemma, eq::MERGED_ARRAYS_EXT); + Debug("pf::array") << "Asserting to the equality engine:" << std::endl + << "\teq = " << eq << std::endl + << "\treason = " << fact << std::endl; + + d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT); ++d_numProp; } - Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n"; - d_out->lemma(lemma); - ++d_numExt; + + if (!d_proofsEnabled) { + // If this is the solution pass, generate the lemma. Otherwise, don't generate it - + // as this is the lemma that we're reproving... + Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n"; + d_out->lemma(lemma); + ++d_numExt; + } + } else { + Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl; + d_modelConstraints.push_back(fact); } } break; - default: - Unreachable(); + default: + Unreachable(); } } @@ -1389,8 +1455,10 @@ void TheoryArrays::check(Effort e) { weakEquivBuildCond(r2[0], r[1], conjunctions); lemma = mkAnd(conjunctions, true); // LSH FIXME: which kind of arrays lemma is this + Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n"; d_out->lemma(lemma, RULE_INVALID, false, false, true); d_readTableContext->pop(); + Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; return; } } @@ -1401,7 +1469,7 @@ void TheoryArrays::check(Effort e) { if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) { // generate the lemmas on the worklist - Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; + Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n"; while (d_RowQueue.size() > 0 && !d_conflict) { if (dischargeLemmas()) { break; @@ -1865,6 +1933,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) void TheoryArrays::propagate(RowLemmaType lem) { + Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = " + << options::arraysPropagate() << std::endl; + TNode a = lem.first; TNode b = lem.second; TNode i = lem.third; @@ -1919,6 +1990,8 @@ void TheoryArrays::propagate(RowLemmaType lem) void TheoryArrays::queueRowLemma(RowLemmaType lem) { + Debug("pf::array") << "Array solver: queue row lemma called" << std::endl; + if (d_conflict || d_RowAlreadyAdded.contains(lem)) { return; } @@ -1958,14 +2031,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // Prefer equality between indexes so as not to introduce new read terms if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { - Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); + Node i_eq_j; + if (!d_proofsEnabled) { + i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this + } else { + i_eq_j = i.eqNode(j); + } + getOutputChannel().requirePhase(i_eq_j, true); d_decisionRequests.push(i_eq_j); } // TODO: maybe add triggers here - if (options::arraysEagerLemmas() || bothExist) { + if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) { // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); @@ -2137,14 +2216,20 @@ bool TheoryArrays::dischargeLemmas() } void TheoryArrays::conflict(TNode a, TNode b) { + Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; + eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b)); + d_conflictNode = explain(a.iffNode(b), proof); } else { - d_conflictNode = explain(a.eqNode(b)); + d_conflictNode = explain(a.eqNode(b), proof); } + if (!d_inCheckModel) { - d_out->conflict(d_conflictNode); + if (proof) { proof->debug_print("pf::array"); } + ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL; + d_out->conflict(d_conflictNode, proof_array); } + d_conflict = true; } |