From e97f9447ed646d4a15ba1c107fa8a0f94165353b Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Thu, 17 Feb 2022 10:08:46 -0800 Subject: [PATCH] [proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100) Instead of printing "trust" in the case of a simplification rule that cannot be translated to an Alethe simplify rule print "all_simplify". This also replaces the heuristic in THEORY_REWRITE to determine which simplify rule is needed. --- src/proof/alethe/alethe_post_processor.cpp | 170 +-------------------- src/proof/alethe/alethe_proof_rule.cpp | 1 + src/proof/alethe/alethe_proof_rule.h | 1 + 3 files changed, 9 insertions(+), 163 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 759974687..24d17676f 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -324,170 +324,14 @@ bool AletheProofPostprocessCallback::update(Node res, return success; } - // The rule is translated according to the theory id tid and the outermost - // connective of the first term in the conclusion F, since F always has the - // form (= t1 t2) where t1 is the term being rewritten. This is not an exact - // translation but should work in most cases. - // - // E.g. if F is (= (* 0 d) 0) and tid = THEORY_ARITH, then prod_simplify - // is correctly guessed as the rule. case PfRule::THEORY_REWRITE: - { - AletheRule vrule = AletheRule::UNDEFINED; - Node t = res[0]; - - theory::TheoryId tid; - if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid)) - { - return addAletheStep( - vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp); - } - switch (tid) - { - case theory::TheoryId::THEORY_BUILTIN: - { - switch (t.getKind()) - { - case kind::ITE: - { - vrule = AletheRule::ITE_SIMPLIFY; - break; - } - case kind::EQUAL: - { - vrule = AletheRule::EQ_SIMPLIFY; - break; - } - case kind::AND: - { - vrule = AletheRule::AND_SIMPLIFY; - break; - } - case kind::OR: - { - vrule = AletheRule::OR_SIMPLIFY; - break; - } - case kind::NOT: - { - vrule = AletheRule::NOT_SIMPLIFY; - break; - } - case kind::IMPLIES: - { - vrule = AletheRule::IMPLIES_SIMPLIFY; - break; - } - case kind::WITNESS: - { - vrule = AletheRule::QNT_SIMPLIFY; - break; - } - default: - { - // In this case the rule is undefined - } - } - break; - } - case theory::TheoryId::THEORY_BOOL: - { - vrule = AletheRule::BOOL_SIMPLIFY; - break; - } - case theory::TheoryId::THEORY_UF: - { - if (t.getKind() == kind::EQUAL) - { - // A lot of these seem to be symmetry rules but not all... - vrule = AletheRule::EQUIV_SIMPLIFY; - } - break; - } - case theory::TheoryId::THEORY_ARITH: - { - switch (t.getKind()) - { - case kind::DIVISION: - { - vrule = AletheRule::DIV_SIMPLIFY; - break; - } - case kind::RELATION_PRODUCT: - { - vrule = AletheRule::PROD_SIMPLIFY; - break; - } - case kind::SUB: - { - vrule = AletheRule::MINUS_SIMPLIFY; - break; - } - case kind::NEG: - { - vrule = AletheRule::UNARY_MINUS_SIMPLIFY; - break; - } - case kind::ADD: - { - vrule = AletheRule::SUM_SIMPLIFY; - break; - } - case kind::MULT: - { - vrule = AletheRule::PROD_SIMPLIFY; - break; - } - case kind::EQUAL: - { - vrule = AletheRule::EQUIV_SIMPLIFY; - break; - } - case kind::LT: - { - [[fallthrough]]; - } - case kind::GT: - { - [[fallthrough]]; - } - case kind::GEQ: - { - [[fallthrough]]; - } - case kind::LEQ: - { - vrule = AletheRule::COMP_SIMPLIFY; - break; - } - case kind::CAST_TO_REAL: - { - return addAletheStep(AletheRule::LA_GENERIC, - res, - nm->mkNode(kind::SEXPR, d_cl, res), - children, - {nm->mkConstInt(Rational(1))}, - *cdp); - } - default: - { - // In this case the rule is undefined - } - } - break; - } - case theory::TheoryId::THEORY_QUANTIFIERS: - { - vrule = AletheRule::QUANTIFIER_SIMPLIFY; - break; - } - default: - { - // In this case the rule is undefined - }; - } - return addAletheStep( - vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp); + { + return addAletheStep(AletheRule::ALL_SIMPLIFY, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + {}, + *cdp); } // ======== Resolution and N-ary Resolution // See proof_rule.h for documentation on the RESOLUTION and CHAIN_RESOLUTION diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp index 52a47fe37..313839dec 100644 --- a/src/proof/alethe/alethe_proof_rule.cpp +++ b/src/proof/alethe/alethe_proof_rule.cpp @@ -114,6 +114,7 @@ const char* aletheRuleToString(AletheRule id) case AletheRule::QNT_SIMPLIFY: return "qnt_simplify"; case AletheRule::SKO_EX: return "sko_ex"; case AletheRule::SKO_FORALL: return "sko_forall"; + case AletheRule::ALL_SIMPLIFY: return "all_simplify"; case AletheRule::SYMM: return "symm"; case AletheRule::NOT_SYMM: return "not_symm"; case AletheRule::REORDERING: return "reordering"; diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h index 331e38ac6..d9515bd44 100644 --- a/src/proof/alethe/alethe_proof_rule.h +++ b/src/proof/alethe/alethe_proof_rule.h @@ -368,6 +368,7 @@ enum class AletheRule : uint32_t COMP_SIMPLIFY, NARY_ELIM, QNT_SIMPLIFY, + ALL_SIMPLIFY, // ======== let // G,x1->F1,...,xn->Fn > j. (= G G') // --------------------------------- -- 2.30.2