From: Andrew Reynolds Date: Tue, 24 Aug 2021 00:33:18 +0000 (-0500) Subject: Uniform treatment of trusted theory inferences in proofs (#7044) X-Git-Tag: cvc5-1.0.0~1343 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b76dcf208986709fefbd0978982de3fe8ecc626;p=cvc5.git Uniform treatment of trusted theory inferences in proofs (#7044) Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE. --- diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 008b0dc6f..286396523 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -79,7 +79,6 @@ const char* toString(PfRule id) case PfRule::ITE_ELIM2: return "ITE_ELIM2"; case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; - //================================================= De Morgan rules case PfRule::NOT_AND: return "NOT_AND"; //================================================= CNF rules case PfRule::CNF_AND_POS: return "CNF_AND_POS"; @@ -120,7 +119,6 @@ const char* toString(PfRule id) return "ARRAYS_READ_OVER_WRITE_CONTRA"; case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; - case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; @@ -132,7 +130,6 @@ const char* toString(PfRule id) case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; case PfRule::DT_SPLIT: return "DT_SPLIT"; case PfRule::DT_CLASH: return "DT_CLASH"; - case PfRule::DT_TRUST: return "DT_TRUST"; //================================================= Quantifiers rules case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; @@ -160,7 +157,6 @@ const char* toString(PfRule id) case PfRule::RE_ELIM: return "RE_ELIM"; case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ"; case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; - case PfRule::STRING_TRUST: return "STRING_TRUST"; //================================================= Arith rules case PfRule::MACRO_ARITH_SCALE_SUM_UB: return "ARITH_SCALE_SUM_UPPER_BOUNDS"; @@ -168,7 +164,6 @@ const char* toString(PfRule id) case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; - case PfRule::INT_TRUST: return "INT_TRUST"; case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN"; case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 78e773bdc..7a3ce6882 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -722,12 +722,6 @@ enum class PfRule : uint32_t // (forall ((x T)) // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) ARRAYS_EQ_RANGE_EXPAND, - // ======== Array Trust - // Children: (P1 ... Pn) - // Arguments: (F) - // --------------------- - // Conclusion: F - ARRAYS_TRUST, //================================================= Bit-Vector rules // Note: bitblast() represents the result of the bit-blasted term as a @@ -800,12 +794,6 @@ enum class PfRule : uint32_t // Conclusion: false // for i != j. DT_CLASH, - // ======== Datatype Trust - // Children: (P1 ... Pn) - // Arguments: (F) - // --------------------- - // Conclusion: F - DT_TRUST, //================================================= Quantifiers rules // ======== Skolem intro @@ -1082,12 +1070,6 @@ enum class PfRule : uint32_t // Also applies to the case where (seq.unit y) is a constant sequence // of length one. STRING_SEQ_UNIT_INJ, - // ======== String Trust - // Children: none - // Arguments: (Q) - // --------------------- - // Conclusion: (Q) - STRING_TRUST, //================================================= Arithmetic rules // ======== Adding Inequalities @@ -1152,12 +1134,6 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: arith::OperatorElim::getAxiomFor(t) ARITH_OP_ELIM_AXIOM, - // ======== Int Trust - // Children: (P1 ... Pn) - // Arguments: (Q) - // --------------------- - // Conclusion: (Q) - INT_TRUST, //======== Multiplication sign inference // Children: none diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d8fc1c578..03db36bb5 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -29,6 +29,7 @@ #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" using namespace std; @@ -1820,9 +1821,11 @@ std::shared_ptr Constraint::externalExplain( } case ArithProofType::IntHoleAP: { - pf = pnm->mkNode(PfRule::INT_TRUST, + Node t = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); + pf = pnm->mkNode(PfRule::THEORY_INFERENCE, children, - {getProofLiteral()}, + {getProofLiteral(), t}, getProofLiteral()); break; } diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index 45f972038..0f4d97b4d 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -16,6 +16,7 @@ #include "theory/arith/pp_rewrite_eq.h" #include "options/arith_options.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" namespace cvc5 { @@ -44,10 +45,12 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) // don't need to rewrite terms since rewritten is not a non-standard op if (proofsEnabled()) { + Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); return d_ppPfGen.mkTrustedRewrite( atom, rewritten, - d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)})); + d_pnm->mkNode( + PfRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t})); } return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); } diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 4e25ae76b..58de8e391 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -36,11 +36,8 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::INT_TIGHT_UB, this); pc->registerChecker(PfRule::INT_TIGHT_LB, this); pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this); - pc->registerChecker(PfRule::ARITH_MULT_POS, this); pc->registerChecker(PfRule::ARITH_MULT_NEG, this); - // trusted rules - pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2); } Node ArithProofRuleChecker::checkInternal(PfRule id, @@ -340,25 +337,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } // Check that all have the same constant: } - case PfRule::INT_TRUST: - { - if (Debug.isOn("arith::pf::check::trust")) - { - Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl; - Debug("arith::pf::check::trust") << " children: " << std::endl; - for (const auto& c : children) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - Debug("arith::pf::check::trust") << " args:" << std::endl; - for (const auto& c : args) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - } - Assert(args.size() == 1); - return args[0]; - } case PfRule::ARITH_OP_ELIM_AXIOM: { Assert(children.empty()); diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index fc3f67cf0..2949cf105 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -16,6 +16,7 @@ #include "theory/arrays/inference_manager.h" #include "options/smt_options.h" +#include "theory/builtin/proof_checker.h" #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -116,13 +117,15 @@ void InferenceManager::convert(PfRule& id, break; case PfRule::ARRAYS_EXT: children.push_back(exp); break; default: - if (id != PfRule::ARRAYS_TRUST) + if (id != PfRule::THEORY_INFERENCE) { Assert(false) << "Unknown rule " << id << "\n"; } children.push_back(exp); args.push_back(conc); - id = PfRule::ARRAYS_TRUST; + args.push_back( + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS)); + id = PfRule::THEORY_INFERENCE; break; } } diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp index 6d546d746..557a43a02 100644 --- a/src/theory/arrays/proof_checker.cpp +++ b/src/theory/arrays/proof_checker.cpp @@ -31,8 +31,6 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this); pc->registerChecker(PfRule::ARRAYS_EXT, this); pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this); - // trusted rules - pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2); } Node ArraysProofRuleChecker::checkInternal(PfRule id, @@ -111,13 +109,6 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id, Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]); return args[0].eqNode(expandedEqRange); } - if (id == PfRule::ARRAYS_TRUST) - { - // "trusted" rules - Assert(!args.empty()); - Assert(args[0].getType().isBoolean()); - return args[0]; - } // no rule return Node::null(); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 1a6dfedbb..0f0d24cde 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1671,11 +1671,12 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { preRegisterTermInternal(selConst); } + // not currently supported in proofs, use THEORY_INFERENCE d_im.assertInference(selConst.eqNode(defValue), true, InferenceId::ARRAYS_CONST_ARRAY_DEFAULT, d_true, - PfRule::ARRAYS_TRUST); + PfRule::THEORY_INFERENCE); } const CTNodeList* stores = d_infoMap.getStores(a); diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index a4323a1d0..afbfd16c1 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -17,6 +17,7 @@ #include "proof/proof.h" #include "proof/proof_checker.h" +#include "theory/builtin/proof_checker.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" @@ -243,7 +244,8 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* { // failed to reconstruct, add trust Trace("dt-ipc") << "...failed " << infer << std::endl; - cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc}); + Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES); + cdp->addStep(conc, PfRule::THEORY_INFERENCE, expv, {conc, t}); } else { diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 77f9a4c27..23ca26a1f 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -30,8 +30,6 @@ void DatatypesProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::DT_COLLAPSE, this); pc->registerChecker(PfRule::DT_SPLIT, this); pc->registerChecker(PfRule::DT_CLASH, this); - // trusted rules - pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2); } Node DatatypesProofRuleChecker::checkInternal(PfRule id, @@ -122,12 +120,6 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id, } return nm->mkConst(false); } - else if (id == PfRule::DT_TRUST) - { - Assert(!args.empty()); - Assert(args[0].getType().isBoolean()); - return args[0]; - } // no rule return Node::null(); } diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index b8c0a851c..f48d29416 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -541,7 +541,7 @@ void InferProofCons::convert(InferenceId infer, if (conc.getKind() != OR) { // This should never happen. If it does, we resort to using - // STRING_TRUST below (in production mode). + // THEORY_INFERENCE below (in production mode). Assert(false) << "Expected OR conclusion for " << infer; } else @@ -876,7 +876,7 @@ void InferProofCons::convert(InferenceId infer, case InferenceId::STRINGS_CTN_TRANS: case InferenceId::STRINGS_CTN_DECOMPOSE: default: - // do nothing, these will be converted to STRING_TRUST below since the + // do nothing, these will be converted to THEORY_INFERENCE below since the // rule is unknown. break; } @@ -925,11 +925,14 @@ void InferProofCons::convert(InferenceId infer, Trace("strings-ipc-fail") << " e: " << ec << std::endl; } } - // untrustworthy conversion, the argument of STRING_TRUST is its conclusion + // untrustworthy conversion, the argument of THEORY_INFERENCE is its + // conclusion ps.d_args.clear(); ps.d_args.push_back(conc); + Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_STRINGS); + ps.d_args.push_back(t); // use the trust rule - ps.d_rule = PfRule::STRING_TRUST; + ps.d_rule = PfRule::THEORY_INFERENCE; // add to stats d_statistics.d_inferencesNoPf << infer; } diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 36b42f296..5a4008724 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -53,8 +53,6 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::RE_ELIM, this); pc->registerChecker(PfRule::STRING_CODE_INJ, this); pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this); - // trusted rules - pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2); } Node StringProofRuleChecker::checkInternal(PfRule id, @@ -506,13 +504,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id, AlwaysAssert(t[0].getType() == t[1].getType()); return t[0].eqNode(t[1]); } - else if (id == PfRule::STRING_TRUST) - { - // "trusted" rules - Assert(!args.empty()); - Assert(args[0].getType().isBoolean()); - return args[0]; - } return Node::null(); }