(proof-new) Miscellaneous sync to master (#6129)

Towards having proofs working on master.

diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index a14247dced6e67ae97f19ace8c0bac79f7d3e67d..21ffd63b82116a696cabbfd411e7c2268ca3c907 100644 (file)
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -148,8 +148,8 @@ class ProofChecker
   Node checkDebug(PfRule id,
                   const std::vector<Node>& cchildren,
                   const std::vector<Node>& args,
-                  Node expected,
-                  const char* traceTag);
+                  Node expected = Node::null(),
+                  const char* traceTag = "");
   /** Indicate that psc is the checker for proof rule id */
   void registerChecker(PfRule id, ProofRuleChecker* psc);
   /**

diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 5996cd7479138e3421ce5deba58a3c00b1c38965..acff2ded16c3d96dc4cb9f994bb0433c505311a3 100644 (file)
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -80,12 +80,9 @@ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol);
  * [***] This class traverses the left hand side of a given equality-to-prove
  * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
  * steps to obtain its rewritten form. To do so, it applies any available
- * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
- * (post-order traversal). It thus does not require the user of this class to
- * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
- * addRewriteStep. In particular, notice that in the above example, we realize
- * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
- * ending with f(a)=f(b).
+ * rewrite step at pre-rewrite (pre-order traversal) and post-rewrite
+ * (post-order traversal) based on whether the user specified pre-rewrite or a
+ * post-rewrite during addRewriteStep.
  *
  * This class may additionally be used for term-context-sensitive rewrite
  * systems. An example is the term formula removal pass which rewrites

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index bc701ebc871ab94704900d04c814489bc79da6ff..ff437e7e6a98e870f9b255f23376eef7a6c55349 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -997,7 +997,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
 
 Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
 {
-  Node tw = SkolemManager::getWitnessForm(t);
+  Node tw = SkolemManager::getOriginalForm(t);
   Node eq = t.eqNode(tw);
   if (t == tw)
   {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 94e53a0939272899f0a2130aa57097172674c134..3fdf67ed7465ffed738120384adf5cdf5933d16c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1523,6 +1523,19 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
+void SmtEngine::getRelevantInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+  Assert(d_state->getMode() == SmtMode::UNSAT);
+  // generate with new proofs
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
+      pe->getProof(), *d_asserts, *d_definedFunctions);
+  d_ucManager->getRelevantInstantiations(pfn, insts);
+}
+
 std::string SmtEngine::getProof()
 {
   Trace("smt") << "SMT getProof()\n";
@@ -1636,7 +1649,8 @@ void SmtEngine::getInstantiationTermVectors(
   finishInit();
   if (options::proof() && getSmtMode() == SmtMode::UNSAT)
   {
-    // TODO (project #37): minimize instantiations based on proof manager
+    // minimize instantiations based on proof manager
+    getRelevantInstantiationTermVectors(insts);
   }
   else
   {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 94c11be5b7db2ccb7c4889b5fd0fefbf3789a9b0..56f3ffbb863740ed1c35ae3fd160edc3651d33ba 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -527,7 +527,12 @@ class CVC4_PUBLIC SmtEngine
    */
   std::vector<Node> getValues(const std::vector<Node>& exprs);
 
-  /** Print all instantiations made by the quantifiers module.  */
+  /** print instantiations
+   *
+   * Print all instantiations for all quantified formulas on out,
+   * returns true if at least one instantiation was printed. The type of output
+   * (list, num, etc.) is determined by printInstMode.
+   */
   void printInstantiations(std::ostream& out);
   /**
    * Print the current proof. This method should be called after an UNSAT
@@ -664,6 +669,12 @@ class CVC4_PUBLIC SmtEngine
    */
   void getInstantiationTermVectors(Node q,
                                    std::vector<std::vector<Node>>& tvecs);
+  /**
+   * As above but only the instantiations that were relevant for the
+   * refutation.
+   */
+  void getRelevantInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node>>>& insts);
   /**
    * Get instantiation term vectors, which maps each instantiated quantified
    * formula to the list of instantiations for that quantified formula. This