Distinguish quantifiers preprocess as its own proof rule (#6897)

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index def57532d10b4021978e9ff0847c662deea7da9f..7be07f7f5306dccf8df167c3c622833049733f17 100644 (file)
--- 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 d20c3ecc06d5ccc099636bb58634c860639ccc3b..9625e1d28b78a0ca96d2bcd0b34813ec8217fab1 100644 (file)
--- 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 17fd089d63b7df8a7362e6cfa1cdc4c855368c2c..f4cd8cb6927ce859b8dfce5693ce97deaf6bd5c2 100644 (file)
--- 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 fae160aa87fd7fbdb1983287da65fa584569d456..f44f2f291ca0a6c8a1a08ecffca657e2020553bd 100644 (file)
--- 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();