diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/arrays/inference_manager.cpp | 128 | ||||
| -rw-r--r-- | src/theory/arrays/inference_manager.h | 77 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 123 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 |
5 files changed, 269 insertions, 67 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c0f53e455..7c22b880a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -400,6 +400,8 @@ libcvc4_add_sources( theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h + theory/arrays/inference_manager.cpp + theory/arrays/inference_manager.h theory/arrays/proof_checker.cpp theory/arrays/proof_checker.h theory/arrays/skolem_cache.cpp diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp new file mode 100644 index 000000000..f429140be --- /dev/null +++ b/src/theory/arrays/inference_manager.cpp @@ -0,0 +1,128 @@ +/********************* */ +/*! \file inference_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Arrays inference manager + **/ + +#include "theory/arrays/inference_manager.h" + +#include "options/smt_options.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arrays { + +InferenceManager::InferenceManager(Theory& t, + TheoryState& state, + ProofNodeManager* pnm) + : TheoryInferenceManager(t, state, pnm), + d_lemmaPg(pnm ? new EagerProofGenerator(pnm, + state.getUserContext(), + "ArrayLemmaProofGenerator") + : nullptr) +{ +} + +bool InferenceManager::assertInference(TNode atom, + bool polarity, + TNode reason, + PfRule id) +{ + Trace("arrays-infer") << "TheoryArrays::assertInference: " + << (polarity ? Node(atom) : atom.notNode()) << " by " + << reason << "; " << id << std::endl; + Assert(atom.getKind() == EQUAL); + // if proofs are enabled, we determine which proof rule to add, otherwise + // we simply assert the internal fact + if (isProofEnabled()) + { + Node fact = polarity ? Node(atom) : atom.notNode(); + std::vector<Node> children; + std::vector<Node> args; + // convert to proof rule application + convert(id, fact, reason, children, args); + return assertInternalFact(atom, polarity, id, children, args); + } + return assertInternalFact(atom, polarity, reason); +} + +bool InferenceManager::arrayLemma( + Node conc, Node exp, PfRule id, LemmaProperty p, bool doCache) +{ + Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp + << "; " << id << std::endl; + NodeManager* nm = NodeManager::currentNM(); + if (isProofEnabled()) + { + std::vector<Node> children; + std::vector<Node> args; + // convert to proof rule application + convert(id, conc, exp, children, args); + // make the trusted lemma based on the eager proof generator and send + TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args); + return trustedLemma(tlem, p, doCache); + } + // send lemma without proofs + Node lem = nm->mkNode(IMPLIES, exp, conc); + return lemma(lem, p, doCache); +} + +void InferenceManager::convert(PfRule& id, + Node conc, + Node exp, + std::vector<Node>& children, + std::vector<Node>& args) +{ + // note that children must contain something equivalent to exp, + // regardless of the PfRule. + switch (id) + { + case PfRule::MACRO_SR_PRED_INTRO: + Assert(exp.isConst()); + args.push_back(conc); + break; + case PfRule::ARRAYS_READ_OVER_WRITE: + if (exp.isConst()) + { + // Premise can be shown by rewriting, use standard predicate intro rule. + // This is the case where we have 2 constant indices. + id = PfRule::MACRO_SR_PRED_INTRO; + args.push_back(conc); + } + else + { + children.push_back(exp); + args.push_back(conc[0]); + } + break; + case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: children.push_back(exp); break; + case PfRule::ARRAYS_READ_OVER_WRITE_1: + Assert(exp.isConst()); + args.push_back(conc[0]); + break; + case PfRule::ARRAYS_EXT: children.push_back(exp); break; + default: + // unknown rule, should never happen + Assert(false); + children.push_back(exp); + args.push_back(conc); + id = PfRule::ARRAYS_TRUST; + break; + } +} + +} // namespace arrays +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h new file mode 100644 index 000000000..2073fac6a --- /dev/null +++ b/src/theory/arrays/inference_manager.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \file inference_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Arrays inference manager + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H +#define CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H + +#include "expr/node.h" +#include "expr/proof_rule.h" +#include "theory/eager_proof_generator.h" +#include "theory/theory_inference_manager.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** + * The arrays inference manager. + */ +class InferenceManager : public TheoryInferenceManager +{ + public: + InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm); + ~InferenceManager() {} + + /** + * Assert inference. This sends an internal fact to the equality engine + * immediately, possibly with proof support. The identifier id which + * rule to apply when proofs are enabled. The order of children + * and arguments to use in the proof step are determined internally in + * this method. + * + * @return true if the fact was successfully asserted, and false if the + * fact was redundant. + */ + bool assertInference(TNode atom, bool polarity, TNode reason, PfRule id); + /** + * Send lemma (exp => conc) based on proof rule id with properties p. Cache + * the lemma if doCache is true. + */ + bool arrayLemma(Node conc, + Node exp, + PfRule id, + LemmaProperty p = LemmaProperty::NONE, + bool doCache = false); + + private: + /** + * Converts a conclusion, explanation and proof rule id used by the array + * theory to the set of arguments required for a proof rule application. + */ + void convert(PfRule& id, + Node conc, + Node exp, + std::vector<Node>& children, + std::vector<Node>& args); + /** Eager proof generator for lemmas from the above method */ + std::unique_ptr<EagerProofGenerator> d_lemmaPg; +}; + +} // namespace arrays +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index c0a3af8f3..5dee75a6c 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,10 +21,12 @@ #include "expr/kind.h" #include "expr/node_algorithm.h" +#include "expr/proof_checker.h" #include "options/arrays_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" +#include "theory/arrays/skolem_cache.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -78,6 +80,7 @@ TheoryArrays::TheoryArrays(context::Context* c, d_ppEqualityEngine(u, name + "theory::arrays::pp", true), d_ppFacts(u), d_state(c, u, valuation), + d_im(*this, d_state, pnm), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), @@ -131,9 +134,10 @@ TheoryArrays::TheoryArrays(context::Context* c, { d_pchecker.registerTo(pc); } - - // indicate we are using the default theory state object + // indicate we are using the default theory state object, and the arrays + // inference manager d_theoryState = &d_state; + d_inferManager = &d_im; } TheoryArrays::~TheoryArrays() { @@ -758,10 +762,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node) { preRegisterTermInternal(ni); } - // Apply RIntro1 Rule - d_equalityEngine->assertEquality( - ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1); + d_im.assertInference( + ni.eqNode(v), true, d_true, PfRule::ARRAYS_READ_OVER_WRITE_1); d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); @@ -837,9 +840,7 @@ void TheoryArrays::explain(TNode literal, Node& explanation) TrustNode TheoryArrays::explain(TNode literal) { - Node explanation; - explain(literal, explanation); - return TrustNode::mkTrustPropExp(literal, explanation, nullptr); + return d_im.explainLit(literal); } ///////////////////////////////////////////////////////////////////////////// @@ -1179,38 +1180,26 @@ void TheoryArrays::presolve() // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// - -Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual) +Node TheoryArrays::getSkolem(TNode ref) { + // the call to SkolemCache::getExtIndexSkolem should be deterministic, but use + // cache anyways for now Node skolem; std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); if (it == d_skolemCache.end()) { - NodeManager* nm = NodeManager::currentNM(); - skolem = nm->mkSkolem(name, type, comment); + Assert(ref.getKind() == kind::NOT && ref[0].getKind() == kind::EQUAL); + // make the skolem using the skolem cache utility + skolem = SkolemCache::getExtIndexSkolem(ref); d_skolemCache[ref] = skolem; } else { skolem = (*it).second; - if (d_equalityEngine->hasTerm(ref) && d_equalityEngine->hasTerm(skolem) - && d_equalityEngine->areEqual(ref, skolem)) - { - 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; - d_equalityEngine->assertEquality(d, true, d_true); - Assert(!d_state.isInConflict()); - d_skolemAssertions.push_back(d); - d_skolemIndex = d_skolemIndex + 1; - } - Debug("pf::array") << "getSkolem DONE" << std::endl; return skolem; } @@ -1294,7 +1283,8 @@ void TheoryArrays::postCheck(Effort level) 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"; + Trace("arrays-lem") + << "Arrays::addExtLemma (weak-eq) " << lemma << "\n"; d_out->lemma(lemma, LemmaProperty::SEND_ATOMS); d_readTableContext->pop(); Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; @@ -1325,7 +1315,7 @@ void TheoryArrays::postCheck(Effort level) bool TheoryArrays::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) { - if (!isPrereg) + if (!isInternal && !isPrereg) { if (atom.getKind() == kind::EQUAL) { @@ -1347,13 +1337,14 @@ bool TheoryArrays::preNotifyFact( void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { // if a disequality - if (atom.getKind() == kind::EQUAL && !pol) + if (atom.getKind() == kind::EQUAL && !pol && !isInternal) { + // Notice that this should be an external assertion, since we do not + // internally infer disequalities. // Apply ArrDiseq Rule if diseq is between arrays if (fact[0][0].getType().isArray() && !d_state.isInConflict()) { NodeManager* nm = NodeManager::currentNM(); - TypeNode indexType = fact[0][0].getType()[0]; TNode k; // k is the skolem for this disequality. @@ -1361,12 +1352,7 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) << 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); + k = getSkolem(fact); Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); @@ -1377,19 +1363,17 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) && d_equalityEngine->hasTerm(bk)) { // Propagate witness disequality - might produce a conflict - d_permRef.push_back(lemma); Debug("pf::array") << "Asserting to the equality engine:" << std::endl << "\teq = " << eq << std::endl << "\treason = " << fact << std::endl; - - d_equalityEngine->assertEquality(eq, false, fact); + d_im.assertInference(eq, false, fact, PfRule::ARRAYS_EXT); ++d_numProp; } // 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_im.arrayLemma(eq.notNode(), fact, PfRule::ARRAYS_EXT); ++d_numExt; } else @@ -1669,7 +1653,8 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { preRegisterTermInternal(selConst); } - d_equalityEngine->assertEquality(selConst.eqNode(defValue), true, d_true); + d_im.assertInference( + selConst.eqNode(defValue), true, d_true, PfRule::ARRAYS_TRUST); } const CTNodeList* stores = d_infoMap.getStores(a); @@ -1805,8 +1790,8 @@ void TheoryArrays::propagate(RowLemmaType lem) if (!bjExists) { preRegisterTermInternal(bj); } - d_equalityEngine->assertEquality( - aj_eq_bj, true, reason, theory::eq::MERGED_THROUGH_ROW); + d_im.assertInference( + aj_eq_bj, true, reason, PfRule::ARRAYS_READ_OVER_WRITE); ++d_numProp; return; } @@ -1815,10 +1800,9 @@ void TheoryArrays::propagate(RowLemmaType lem) Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; Node reason = (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode(); - Node i_eq_j = i.eqNode(j); - d_permRef.push_back(reason); - d_equalityEngine->assertEquality( - i_eq_j, true, reason, theory::eq::MERGED_THROUGH_ROW); + Node j_eq_i = j.eqNode(i); + d_im.assertInference( + j_eq_i, true, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA); ++d_numProp; return; } @@ -1884,7 +1868,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(aj2); } - d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true); + d_im.assertInference( + aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -1895,7 +1880,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(bj2); } - d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true); + d_im.assertInference( + bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { return; @@ -1913,22 +1899,24 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(bj2); } - d_equalityEngine->assertEquality(eq1, true, d_true); + d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO); return; } Node eq2 = i.eqNode(j); Node eq2_r = Rewriter::rewrite(eq2); if (eq2_r == d_true) { - d_equalityEngine->assertEquality(eq2, true, d_true); + d_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO); return; } Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r); - Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n"; + Trace("arrays-lem") << "Arrays::addRowLemma (1) adding " << lemma << "\n"; d_RowAlreadyAdded.insert(lem); - d_out->lemma(lemma); + // use non-rewritten nodes + d_im.arrayLemma( + aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); ++d_numRow; } else { @@ -1997,7 +1985,8 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(aj2); } - d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true); + d_im.assertInference( + aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -2008,7 +1997,8 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(bj2); } - d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true); + d_im.assertInference( + bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { continue; @@ -2026,22 +2016,24 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(bj2); } - d_equalityEngine->assertEquality(eq1, true, d_true); + d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO); continue; } Node eq2 = i.eqNode(j); Node eq2_r = Rewriter::rewrite(eq2); if (eq2_r == d_true) { - d_equalityEngine->assertEquality(eq2, true, d_true); + d_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO); continue; } Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r); - Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; + Trace("arrays-lem") << "Arrays::addRowLemma (2) adding " << lem << "\n"; d_RowAlreadyAdded.insert(l); - d_out->lemma(lem); + // use non-rewritten nodes, theory preprocessing will rewrite + d_im.arrayLemma( + aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); ++d_numRow; lemmasAdded = true; if (options::arraysReduceSharing()) { @@ -2053,14 +2045,13 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; - - explain(a.eqNode(b), d_conflictNode); - - if (!d_inCheckModel) { - d_out->conflict(d_conflictNode); + if (d_inCheckModel) + { + // if in check model, don't send the conflict + d_state.notifyInConflict(); + return; } - - d_state.notifyInConflict(); + d_im.conflictEqConstantMerge(a, b); } TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy( diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 8c15a50bf..0dd95795b 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -26,10 +26,12 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "theory/arrays/array_info.h" +#include "theory/arrays/inference_manager.h" #include "theory/arrays/proof_checker.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_equality_engine.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -187,6 +189,8 @@ class TheoryArrays : public Theory { TheoryArraysRewriter d_rewriter; /** A (default) theory state object */ TheoryState d_state; + /** The arrays inference manager */ + InferenceManager d_im; public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; @@ -428,7 +432,7 @@ class TheoryArrays : public Theory { context::CDList<Node> d_arrayMerges; std::vector<CTNodeList*> d_readBucketAllocations; - Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); + Node getSkolem(TNode ref); Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); Node removeRepLoops(TNode a, TNode rep); |