From: Gereon Kremer Date: Wed, 17 Feb 2021 14:39:42 +0000 (+0100) Subject: Add InferenceIds for theory of arrays (#5910) X-Git-Tag: cvc5-1.0.0~2273 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb5e3113312322c21a00062b22c358c30fa27101;p=cvc5.git Add InferenceIds for theory of arrays (#5910) This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN. --- diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index be2972444..afcc9a719 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -37,8 +37,9 @@ InferenceManager::InferenceManager(Theory& t, bool InferenceManager::assertInference(TNode atom, bool polarity, + InferenceId id, TNode reason, - PfRule id) + PfRule pfr) { Trace("arrays-infer") << "TheoryArrays::assertInference: " << (polarity ? Node(atom) : atom.notNode()) << " by " @@ -52,14 +53,14 @@ bool InferenceManager::assertInference(TNode atom, std::vector children; std::vector args; // convert to proof rule application - convert(id, fact, reason, children, args); - return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args); + convert(pfr, fact, reason, children, args); + return assertInternalFact(atom, polarity, id, pfr, children, args); } - return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason); + return assertInternalFact(atom, polarity, id, reason); } bool InferenceManager::arrayLemma( - Node conc, Node exp, PfRule id, LemmaProperty p, bool doCache) + Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p, bool doCache) { Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp << "; " << id << std::endl; @@ -69,14 +70,14 @@ bool InferenceManager::arrayLemma( std::vector children; std::vector args; // convert to proof rule application - convert(id, conc, exp, children, args); + convert(pfr, 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, InferenceId::UNKNOWN, p, doCache); + TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args); + return trustedLemma(tlem, id, p, doCache); } // send lemma without proofs Node lem = nm->mkNode(IMPLIES, exp, conc); - return lemma(lem, InferenceId::UNKNOWN, p, doCache); + return lemma(lem, id, p, doCache); } void InferenceManager::convert(PfRule& id, diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index b4ae228be..96af0b677 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -45,14 +45,15 @@ class InferenceManager : public TheoryInferenceManager * @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); + bool assertInference(TNode atom, bool polarity, InferenceId id, TNode reason, PfRule pfr); /** * Send lemma (exp => conc) based on proof rule id with properties p. Cache * the lemma if doCache is true. */ bool arrayLemma(Node conc, + InferenceId id, Node exp, - PfRule id, + PfRule pfr, LemmaProperty p = LemmaProperty::NONE, bool doCache = false); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b13bd6926..f07140d4e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -771,8 +771,11 @@ void TheoryArrays::preRegisterTermInternal(TNode node) preRegisterTermInternal(ni); } // Apply RIntro1 Rule - d_im.assertInference( - ni.eqNode(v), true, d_true, PfRule::ARRAYS_READ_OVER_WRITE_1); + d_im.assertInference(ni.eqNode(v), + true, + InferenceId::ARRAYS_READ_OVER_WRITE_1, + d_true, + PfRule::ARRAYS_READ_OVER_WRITE_1); d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); @@ -1373,14 +1376,14 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) Debug("pf::array") << "Asserting to the equality engine:" << std::endl << "\teq = " << eq << std::endl << "\treason = " << fact << std::endl; - d_im.assertInference(eq, false, fact, PfRule::ARRAYS_EXT); + d_im.assertInference(eq, false, InferenceId::ARRAYS_EXT, 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_im.arrayLemma(eq.notNode(), fact, PfRule::ARRAYS_EXT); + d_im.arrayLemma(eq.notNode(), InferenceId::ARRAYS_EXT, fact, PfRule::ARRAYS_EXT); ++d_numExt; } else @@ -1660,8 +1663,11 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { preRegisterTermInternal(selConst); } - d_im.assertInference( - selConst.eqNode(defValue), true, d_true, PfRule::ARRAYS_TRUST); + d_im.assertInference(selConst.eqNode(defValue), + true, + InferenceId::UNKNOWN, + d_true, + PfRule::ARRAYS_TRUST); } const CTNodeList* stores = d_infoMap.getStores(a); @@ -1798,7 +1804,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem) preRegisterTermInternal(bj); } d_im.assertInference( - aj_eq_bj, true, reason, PfRule::ARRAYS_READ_OVER_WRITE); + aj_eq_bj, true, InferenceId::ARRAYS_READ_OVER_WRITE, reason, PfRule::ARRAYS_READ_OVER_WRITE); ++d_numProp; return; } @@ -1809,7 +1815,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem) (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode(); Node j_eq_i = j.eqNode(i); d_im.assertInference( - j_eq_i, true, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA); + j_eq_i, true, InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA); ++d_numProp; return; } @@ -1876,7 +1882,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) preRegisterTermInternal(aj2); } d_im.assertInference( - aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); + aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -1888,7 +1894,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) preRegisterTermInternal(bj2); } d_im.assertInference( - bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); + bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { return; @@ -1906,14 +1912,14 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(bj2); } - d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq1, true, InferenceId::UNKNOWN, 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_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); return; } @@ -1923,7 +1929,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) d_RowAlreadyAdded.insert(lem); // use non-rewritten nodes d_im.arrayLemma( - aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); + aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); ++d_numRow; } else { @@ -1993,7 +1999,7 @@ bool TheoryArrays::dischargeLemmas() preRegisterTermInternal(aj2); } d_im.assertInference( - aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); + aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -2005,7 +2011,7 @@ bool TheoryArrays::dischargeLemmas() preRegisterTermInternal(bj2); } d_im.assertInference( - bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO); + bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { continue; @@ -2023,14 +2029,14 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(bj2); } - d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq1, true, InferenceId::UNKNOWN, 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_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); continue; } @@ -2040,7 +2046,7 @@ bool TheoryArrays::dischargeLemmas() d_RowAlreadyAdded.insert(l); // use non-rewritten nodes, theory preprocessing will rewrite d_im.arrayLemma( - aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); + aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE); ++d_numRow; lemmasAdded = true; if (options::arraysReduceSharing()) { diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c037a035a..5a2158d00 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -46,6 +46,11 @@ const char* toString(InferenceId i) case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT"; case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION"; + case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT"; + case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; + case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; + case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA"; + case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT"; case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT"; case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f2192437a..f28faa037 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -96,6 +96,10 @@ enum class InferenceId ARITH_NL_ICP_PROPAGATION, //-------------------- unknown + ARRAYS_EXT, + ARRAYS_READ_OVER_WRITE, + ARRAYS_READ_OVER_WRITE_1, + ARRAYS_READ_OVER_WRITE_CONTRA, BAG_NON_NEGATIVE_COUNT, BAG_MK_BAG_SAME_ELEMENT,