Implement lazy proof checking modes (#7106)

This implements several variants of lazy proof checking in the core proof checker.

Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker.

This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple.

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 071f14dec73d08703979c584f44e53b1a93eb393..b741ec5d545ae64ec594499d8784099f298e6985 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -39,12 +39,25 @@ name   = "Proof"
   help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
 
 [[option]]
-  name       = "proofEagerChecking"
+  name       = "proofCheck"
   category   = "regular"
-  long       = "proof-eager-checking"
-  type       = "bool"
-  default    = "false"
-  help       = "check proofs eagerly with proof for local debugging"
+  long       = "proof-check=MODE"
+  type       = "ProofCheckMode"
+  default    = "LAZY"
+  help       = "select proof checking mode"
+  help_mode  = "Proof checking modes."
+[[option.mode.EAGER]]
+  name       = "eager"
+  help       = "check rule applications and proofs from generators eagerly for local debugging"
+[[option.mode.EAGER_SIMPLE]]
+  name       = "eager-simple"
+  help       = "check rule applications during construction"
+[[option.mode.LAZY]]
+  name       = "lazy"
+  help       = "check rule applications only during final proof construction"
+[[option.mode.NONE]]
+  name       = "none"
+  help       = "do not check rule applications"
 
 [[option]]
   name       = "proofGranularityMode"

diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index c835ca03d2b8c94d813b96a736534d2ccfdc7d6b..4cb39cc404a9ae85de14dbe1bf737fa966f72511 100644 (file)
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -272,8 +272,8 @@ void LazyCDProofChain::addLazyStep(Node expected,
                              << " set to generator " << pg->identify() << "\n";
   // note this will rewrite the generator for expected, if any
   d_gens.insert(expected, pg);
-  // check if chain is closed if options::proofEagerChecking() is on
-  if (options::proofEagerChecking())
+  // check if chain is closed if eager checking is on
+  if (options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     Trace("lazy-cdproofchain")
         << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 1d5aa61b4fb19a47bb2a687bd4346b2cf5193bfe..28a09fc9c8f78a840fea304ca69b09c6a3392bc0 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -85,8 +85,10 @@ ProofCheckerStatistics::ProofCheckerStatistics()
 {
 }
 
-ProofChecker::ProofChecker(uint32_t pclevel, rewriter::RewriteDb* rdb)
-    : d_pclevel(pclevel), d_rdb(rdb)
+ProofChecker::ProofChecker(bool eagerCheck,
+                           uint32_t pclevel,
+                           rewriter::RewriteDb* rdb)
+    : d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb)
 {
 }
 
@@ -245,7 +247,7 @@ Node ProofChecker::checkInternal(PfRule id,
     }
   }
   // fails if pedantic level is not met
-  if (options::proofEagerChecking())
+  if (d_eagerCheck)
   {
     std::stringstream serr;
     if (isPedanticFailure(id, serr, enableOutput))

diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
index 6092a193272427ccdfedf5ac59946249125b01d5..a32f23fe49a07fce1bf59525ac5cb4709acb4019 100644 (file)
--- a/src/proof/proof_checker.h
+++ b/src/proof/proof_checker.h
@@ -105,7 +105,9 @@ class ProofCheckerStatistics
 class ProofChecker
 {
  public:
-  ProofChecker(uint32_t pclevel = 0, rewriter::RewriteDb* rdb = nullptr);
+  ProofChecker(bool eagerCheck,
+               uint32_t pclevel = 0,
+               rewriter::RewriteDb* rdb = nullptr);
   ~ProofChecker() {}
   /**
    * Return the formula that is proven by proof node pn, or null if pn is not
@@ -189,6 +191,8 @@ class ProofChecker
   std::map<PfRule, ProofRuleChecker*> d_checker;
   /** Maps proof trusted rules to their pedantic level */
   std::map<PfRule, uint32_t> d_plevel;
+  /** Whether we check for pedantic failures eagerly */
+  bool d_eagerCheck;
   /** The pedantic level of this checker */
   uint32_t d_pclevel;
   /** Pointer to the rewrite database */

diff --git a/src/proof/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp
index 774b25ef68046207712c6998cf90bac2332905c7..3e91aa799465d92cae482ed49e081b64bb676cf1 100644 (file)
--- a/src/proof/proof_ensure_closed.cpp
+++ b/src/proof/proof_ensure_closed.cpp
@@ -43,7 +43,7 @@ void ensureClosedWrtInternal(Node proven,
     return;
   }
   bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofEagerChecking() && !isTraceDebug)
+  if (options::proofCheck() != options::ProofCheckMode::EAGER && !isTraceDebug)
   {
     // trace is off and proof new eager checking is off, do not do check
     return;

diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp
index e3affb3063c674867d48b76e3ec4750dee19e582..2a141919d38c61b41393525d54ed9686a9c1c33d 100644 (file)
--- a/src/proof/proof_node.cpp
+++ b/src/proof/proof_node.cpp
@@ -23,6 +23,7 @@ namespace cvc5 {
 ProofNode::ProofNode(PfRule id,
                      const std::vector<std::shared_ptr<ProofNode>>& children,
                      const std::vector<Node>& args)
+    : d_provenChecked(false)
 {
   setValue(id, children, args);
 }

diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h
index db82cc63d2bcae9748cdac23cd5b03e0270554a4..f4552ae438c0f6b86112e6c2da3711891d3ecd42 100644 (file)
--- a/src/proof/proof_node.h
+++ b/src/proof/proof_node.h
@@ -123,6 +123,8 @@ class ProofNode
   std::vector<Node> d_args;
   /** The cache of the fact that has been proven, modifiable by ProofChecker */
   Node d_proven;
+  /** Was d_proven actually checked, or is it trusted? */
+  bool d_provenChecked;
 };
 
 inline size_t ProofNodeHashFunction::operator()(

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 7e41a905788ae02c5b35920769f39eb937295577..a3ef944e080e3f1bd5f0cf431ec6987eb2b40f6b 100644 (file)
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -31,6 +31,8 @@ namespace cvc5 {
 ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
+  // we always allocate a proof checker, regardless of the proof checking mode
+  Assert(d_checker != nullptr);
 }
 
 std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
@@ -41,7 +43,8 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
 {
   Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
                << "} " << expected << "\n";
-  Node res = checkInternal(id, children, args, expected);
+  bool didCheck = false;
+  Node res = checkInternal(id, children, args, expected, didCheck);
   if (res.isNull())
   {
     // if it was invalid, then we return the null node
@@ -51,6 +54,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
   std::shared_ptr<ProofNode> pn =
       std::make_shared<ProofNode>(id, children, args);
   pn->d_proven = res;
+  pn->d_provenChecked = didCheck;
   return pn;
 }
 
@@ -291,32 +295,49 @@ bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
   {
     return false;
   }
+  // copy whether we did the check
+  pn->d_provenChecked = pnr->d_provenChecked;
   // can shortcut re-check of rule
   return updateNodeInternal(
       pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
 }
 
+void ProofNodeManager::ensureChecked(ProofNode* pn)
+{
+  if (pn->d_provenChecked)
+  {
+    // already checked
+    return;
+  }
+  // directly call the proof checker
+  Node res = d_checker->check(pn, pn->getResult());
+  pn->d_provenChecked = true;
+  // should have the correct result
+  Assert(res == pn->d_proven);
+}
+
 Node ProofNodeManager::checkInternal(
     PfRule id,
     const std::vector<std::shared_ptr<ProofNode>>& children,
     const std::vector<Node>& args,
-    Node expected)
+    Node expected,
+    bool& didCheck)
 {
-  Node res;
-  if (d_checker)
+  // if the user supplied an expected result, then we trust it if we are in
+  // a proof checking mode that does not eagerly check rule applications
+  if (!expected.isNull())
   {
-    // check with the checker, which takes expected as argument
-    res = d_checker->check(id, children, args, expected);
-    Assert(!res.isNull())
-        << "ProofNodeManager::checkInternal: failed to check proof";
-  }
-  else
-  {
-    // otherwise we trust the expected value, if it exists
-    Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
-                                  "or expected value provided";
-    res = expected;
+    if (options::proofCheck() == options::ProofCheckMode::LAZY
+        || options::proofCheck() == options::ProofCheckMode::NONE)
+    {
+      return expected;
+    }
   }
+  // check with the checker, which takes expected as argument
+  Node res = d_checker->check(id, children, args, expected);
+  didCheck = true;
+  Assert(!res.isNull())
+      << "ProofNodeManager::checkInternal: failed to check proof";
   return res;
 }
 
@@ -371,6 +392,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::clone(
       visited[cur] = cloned;
       // we trust the above cloning does not change what is proven
       cloned->d_proven = cur->d_proven;
+      cloned->d_provenChecked = cur->d_provenChecked;
     }
   }
   Assert(visited.find(orig) != visited.end());
@@ -403,7 +425,7 @@ bool ProofNodeManager::updateNodeInternal(
 {
   Assert(pn != nullptr);
   // ---------------- check for cyclic
-  if (options::proofEagerChecking())
+  if (options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     std::unordered_set<const ProofNode*> visited;
     for (const std::shared_ptr<ProofNode>& cpc : children)
@@ -436,7 +458,8 @@ bool ProofNodeManager::updateNodeInternal(
   if (needsCheck)
   {
     // We expect to prove the same thing as before
-    Node res = checkInternal(id, children, args, pn->d_proven);
+    bool didCheck = false;
+    Node res = checkInternal(id, children, args, pn->d_proven, didCheck);
     if (res.isNull())
     {
       // if it was invalid, then we do not update
@@ -444,6 +467,7 @@ bool ProofNodeManager::updateNodeInternal(
     }
     // proven field should already be the same as the result
     Assert(res == pn->d_proven);
+    pn->d_provenChecked = didCheck;
   }
 
   // we update its value

diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 541686a30643da0314932fe98f7ec003a796b9df..928aabb7678de49b156b3b545f27d897aeccb5ab 100644 (file)
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -163,6 +163,10 @@ class ProofNodeManager
    * unchanged.
    */
   bool updateNode(ProofNode* pn, ProofNode* pnr);
+  /**
+   * Ensure that pn is checked, regardless of the proof check format.
+   */
+  void ensureChecked(ProofNode* pn);
   /** Get the underlying proof checker */
   ProofChecker* getChecker() const;
   /**
@@ -193,11 +197,15 @@ class ProofNodeManager
    * This throws an assertion error if we fail to check such a proof node, or
    * if expected is provided (non-null) and is different what is proven by the
    * other arguments.
+   *
+   * The flag didCheck is set to true if the underlying proof checker was
+   * invoked. This may be false if e.g. the proof checking mode is lazy.
    */
   Node checkInternal(PfRule id,
                      const std::vector<std::shared_ptr<ProofNode>>& children,
                      const std::vector<Node>& args,
-                     Node expected);
+                     Node expected,
+                     bool& didCheck);
   /**
    * Update node internal, return true if successful. This is called by
    * the update node methods above. The argument needsCheck is whether we

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index dd22416dbc1fa9f3baa88c4ec110d0cbc2a174fb..9060c318cb50edcecac74037ac296abe9bf45257 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -220,7 +220,8 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
   Assert(ppSkolems.size() == ppLemmas.size());
 
   // do final checks on the lemmas we are about to send
-  if (isProofEnabled() && options::proofEagerChecking())
+  if (isProofEnabled()
+      && options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 8891016a4b4837cbe28b2c83189552d8502a3692..da49a5990c4fad2283d335d1b543bd662c7d3ef2 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -685,7 +685,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     }
   } while (expanded);
   // now we should be able to close it
-  if (options::proofEagerChecking())
+  if (options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     std::vector<Node> assumptionsVec;
     for (const Node& a : d_assumptions)

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 1eea6286b2606666efb8810d2adfe737b57b9100..1e322ccd323bf006693744672918778608276f74 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -256,7 +256,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
 
 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 {
-  if (options::proofEagerChecking())
+  if (options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation

diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index ae35b346cc4d94f6b96e8d65d134b4aa5b33b787..93b4cae1906b7082a8c24764676608f1cc5c2508 100644 (file)
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -59,7 +59,7 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   PfRule r = pn->getRule();
   // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofEagerChecking())
+  if (options::proofCheck() != options::ProofCheckMode::EAGER)
   {
     if (!d_pedanticFailure)
     {
@@ -70,6 +70,10 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       }
     }
   }
+  if (options::proofCheck() != options::ProofCheckMode::NONE)
+  {
+    d_pnm->ensureChecked(pn.get());
+  }
   uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
   if (plevel != 0)
   {

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 49f67e94c3eda1898896003eed4281fa8744c7d4..ae5de49e9a6069e9b8e5f1cec8d8d435067c485c 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -33,7 +33,9 @@ namespace smt {
 
 PfManager::PfManager(Env& env, SmtEngine* smte)
     : d_env(env),
-      d_pchecker(new ProofChecker(options::proofPedantic())),
+      d_pchecker(new ProofChecker(
+          d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER,
+          d_env.getOptions().proof.proofPedantic)),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c9a82a6176d9c7edf0f0f45f12112cc7276de5c..65762a50bd1c84080529d0ac4feb4305cc969796 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -369,7 +369,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
                << reasonNoProofs.str() << "." << std::endl;
       opts.smt.produceProofs = false;
       opts.smt.checkProofs = false;
-      opts.proof.proofEagerChecking = false;
     }
   }
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27e7b85300fb7174fd16eb85eb7daf1fb9abbfc2..5403928ecefdf7f72c018f6ce0d0724efa080a96 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -876,12 +876,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     }
     // Check that UNSAT results generate a proof correctly.
     if (d_env->getOptions().smt.checkProofs
-        || d_env->getOptions().proof.proofEagerChecking)
+        || d_env->getOptions().proof.proofCheck
+               == options::ProofCheckMode::EAGER)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
         if ((d_env->getOptions().smt.checkProofs
-             || d_env->getOptions().proof.proofEagerChecking)
+             || d_env->getOptions().proof.proofCheck
+                    == options::ProofCheckMode::EAGER)
             && !d_env->getOptions().smt.produceProofs)
         {
           throw ModalException(
@@ -1368,7 +1370,7 @@ void SmtEngine::checkProof()
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  if (d_env->getOptions().proof.proofEagerChecking)
+  if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     pe->checkProof(d_asserts->getAssertionList());
   }
@@ -1439,7 +1441,6 @@ std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
     // disable all proof options
     coreChecker->getOptions().smt.produceProofs = false;
     coreChecker->getOptions().smt.checkProofs = false;
-    coreChecker->getOptions().proof.proofEagerChecking = false;
 
     for (const Node& ucAssertion : core)
     {
@@ -1504,7 +1505,6 @@ void SmtEngine::checkUnsatCore() {
   // disable all proof options
   coreChecker->getOptions().smt.produceProofs = false;
   coreChecker->getOptions().smt.checkProofs = false;
-  coreChecker->getOptions().proof.proofEagerChecking = false;
 
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;

diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2
index ccd0b7634e9b58ca06bf943df8a3e7d303b95692..6744e3a0e8c43395f88a224411c9ea3903027deb 100644 (file)
--- a/test/regress/regress0/arith/non-normal.smt2
+++ b/test/regress/regress0/arith/non-normal.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --proof-eager-checking
+; COMMAND-LINE: --proof-check=eager
 ; EXPECT: sat
 (set-logic QF_UFLRA)
 (declare-fun v1 () Real)