From aa9aa46b77f048f2865c29e40ed946371fd115ef Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 23 Mar 2016 12:07:59 -0700 Subject: squash-merge from proof branch --- src/theory/arrays/array_info.cpp | 24 ++--- src/theory/arrays/array_info.h | 3 +- src/theory/arrays/kinds | 5 + src/theory/arrays/theory_arrays.cpp | 137 ++++++++++++++++++++++----- src/theory/arrays/theory_arrays.h | 5 +- src/theory/arrays/theory_arrays_type_rules.h | 9 ++ 6 files changed, 142 insertions(+), 41 deletions(-) (limited to 'src/theory/arrays') diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 55f013f8c..16412c05b 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -44,16 +44,16 @@ Info::~Info() { in_stores->deleteSelf(); } -ArrayInfo::ArrayInfo(context::Context* c, Backtracker* b) +ArrayInfo::ArrayInfo(context::Context* c, Backtracker* b, std::string statisticsPrefix) : ct(c), bck(b), info_map(), - d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), - d_avgIndexListLength("theory::arrays::avgIndexListLength"), - d_avgStoresListLength("theory::arrays::avgStoresListLength"), - d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), - d_listsCount("theory::arrays::listsCount",0), - d_callsMergeInfo("theory::arrays::callsMergeInfo",0), - d_maxList("theory::arrays::maxList",0), - d_tableSize("theory::arrays::infoTableSize", info_map) { + d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"), + d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"), + d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"), + d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"), + d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0), + d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0), + d_maxList(statisticsPrefix + "theory::arrays::maxList",0), + d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) { emptyList = new(true) CTNodeList(ct); emptyInfo = new Info(ct, bck); smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer); @@ -208,7 +208,7 @@ void ArrayInfo::setNonLinear(const TNode a) { } else { (*it).second->isNonLinear = true; } - + } void ArrayInfo::setRIntro1Applied(const TNode a) { @@ -222,7 +222,7 @@ void ArrayInfo::setRIntro1Applied(const TNode a) { } else { (*it).second->rIntro1Applied = true; } - + } void ArrayInfo::setModelRep(const TNode a, const TNode b) { @@ -236,7 +236,7 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) { } else { (*it).second->modelRep = b; } - + } void ArrayInfo::setConstArr(const TNode a, const TNode constArr) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 319864c34..04b9cffb1 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -155,7 +155,8 @@ public: currentStatisticsRegistry()->registerStat(&d_maxList); currentStatisticsRegistry()->registerStat(&d_tableSize); }*/ - ArrayInfo(context::Context* c, Backtracker* b); + + ArrayInfo(context::Context* c, Backtracker* b, std::string statisticsPrefix = ""); ~ArrayInfo(); diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index d5f313ca1..be16d684d 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -54,6 +54,11 @@ typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule +operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only" +operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only" +typerule PARTIAL_SELECT_0 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule +typerule PARTIAL_SELECT_1 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule + # store operations that are ordered (by index) over a store-all are constant construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule 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& assumptions) { +void TheoryArrays::explain(TNode literal, std::vector& 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 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: "< 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; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index eba6c000e..2f69c52f9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -128,7 +128,7 @@ class TheoryArrays : public Theory { TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - std::string instanceName = ""); + std::string name = ""); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -183,7 +183,7 @@ class TheoryArrays : public Theory { bool propagate(TNode literal); /** Explain why this literal is true by adding assumptions */ - void explain(TNode literal, std::vector& assumptions); + void explain(TNode literal, std::vector& assumptions, eq::EqProof *proof); /** For debugging only- checks invariants about when things are preregistered*/ context::CDHashSet d_isPreRegistered; @@ -195,6 +195,7 @@ class TheoryArrays : public Theory { void preRegisterTerm(TNode n); void propagate(Effort e); + Node explain(TNode n, eq::EqProof *proof); Node explain(TNode n); ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 70e1c1a5b..a5d0eac69 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -214,6 +214,15 @@ struct ArraysProperties { } };/* struct ArraysProperties */ + +struct ArrayPartialSelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1); + return nodeManager->integerType(); + } +};/* struct ArrayPartialSelectTypeRule */ + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -- cgit v1.2.3