diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-15 12:56:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-15 14:56:05 -0300 |
| commit | 56a30b7ae82b82606fe9e46e3a2c47b963e6a8e6 (patch) | |
| tree | aa360445f77b0da19a93e1973a26603951ab29b4 | |
| parent | 31b053a52258bd4697409b92d042a8bebb64f7b2 (diff) | |
Distinguish quantifiers preprocess as its own proof rule (#6897)
| -rw-r--r-- | src/proof/proof_rule.cpp | 1 | ||||
| -rw-r--r-- | src/proof/proof_rule.h | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/proof_checker.cpp | 8 |
4 files changed, 18 insertions, 2 deletions
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index def57532d..7be07f7f5 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -135,6 +135,7 @@ const char* toString(PfRule id) case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; case PfRule::SKOLEMIZE: return "SKOLEMIZE"; case PfRule::INSTANTIATE: return "INSTANTIATE"; + case PfRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS"; //================================================= String rules case PfRule::CONCAT_EQ: return "CONCAT_EQ"; case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index d20c3ecc0..9625e1d28 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -830,6 +830,13 @@ enum class PfRule : uint32_t // Conclusion: F*sigma // sigma maps x1 ... xn to t1 ... tn. INSTANTIATE, + // ======== (Trusted) quantifiers preprocess + // Children: ? + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // where F is an equality of the form t = QuantifiersRewriter::preprocess(t) + QUANTIFIERS_PREPROCESS, //================================================= String rules //======================== Core solver diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 17fd089d6..f4cd8cb69 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -264,10 +264,10 @@ bool Instantiate::addInstantiation(Node q, // ------------------------------ EQ_RESOLVE // body Node proven = tpBody.getProven(); - // add the transformation proof, or THEORY_PREPROCESS if none provided + // add the transformation proof, or the trusted rule if none provided pfTmp->addLazyStep(proven, tpBody.getGenerator(), - PfRule::THEORY_PREPROCESS, + PfRule::QUANTIFIERS_PREPROCESS, true, "Instantiate::getInstantiation:qpreprocess"); pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {}); diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index fae160aa8..f44f2f291 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -32,6 +32,8 @@ void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::EXISTS_INTRO, this); pc->registerChecker(PfRule::SKOLEMIZE, this); pc->registerChecker(PfRule::INSTANTIATE, this); + // trusted rules + pc->registerTrustedChecker(PfRule::QUANTIFIERS_PREPROCESS, this, 3); } Node QuantifiersProofRuleChecker::checkInternal( @@ -117,6 +119,12 @@ Node QuantifiersProofRuleChecker::checkInternal( body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); return inst; } + else if (id == PfRule::QUANTIFIERS_PREPROCESS) + { + Assert(!args.empty()); + Assert(args[0].getType().isBoolean()); + return args[0]; + } // no rule return Node::null(); |