(proof-new) Support proofs of quantifier instantiation (#5001)

This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.

6 files changed, 181 insertions, 39 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index c156cbdf8..a771309f0 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -42,10 +42,10 @@ InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
 {
 }
 
-Node InstRewriterCegqi::rewriteInstantiation(Node q,
-                                             std::vector<Node>& terms,
-                                             Node inst,
-                                             bool doVts)
+TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
+                                                  std::vector<Node>& terms,
+                                                  Node inst,
+                                                  bool doVts)
 {
   return d_parent->rewriteInstantiation(q, terms, inst, doVts);
 }
@@ -453,11 +453,12 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q)
     }
   }
 }
-Node InstStrategyCegqi::rewriteInstantiation(Node q,
-                                             std::vector<Node>& terms,
-                                             Node inst,
-                                             bool doVts)
+TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
+                                                  std::vector<Node>& terms,
+                                                  Node inst,
+                                                  bool doVts)
 {
+  Node prevInst = inst;
   if (doVts)
   {
     // do virtual term substitution
@@ -470,7 +471,12 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q,
   {
     inst = doNestedQE(q, terms, inst, doVts);
   }
-  return inst;
+  if (prevInst != inst)
+  {
+    // not proof producing yet
+    return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
+  }
+  return TrustNode::null();
 }
 
 InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index dac5a198c..c767b8a4e 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -43,12 +43,13 @@ class InstRewriterCegqi : public InstantiationRewriter
   ~InstRewriterCegqi() {}
   /**
    * Rewrite the instantiation via d_parent, based on virtual term substitution
-   * and nested quantifier elimination.
+   * and nested quantifier elimination. Returns a TrustNode of kind REWRITE,
+   * corresponding to the rewrite and its proof generator.
    */
-  Node rewriteInstantiation(Node q,
-                            std::vector<Node>& terms,
-                            Node inst,
-                            bool doVts) override;
+  TrustNode rewriteInstantiation(Node q,
+                                 std::vector<Node>& terms,
+                                 Node inst,
+                                 bool doVts) override;
 
  private:
   /** pointer to the parent of this class */
@@ -106,11 +107,14 @@ class InstStrategyCegqi : public QuantifiersModule
    * We rewrite inst based on virtual term substitution and nested quantifier
    * elimination. For details, see "Solving Quantified Linear Arithmetic via
    * Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
+   *
+   * Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its
+   * proof generator.
    */
-  Node rewriteInstantiation(Node q,
-                            std::vector<Node>& terms,
-                            Node inst,
-                            bool doVts);
+  TrustNode rewriteInstantiation(Node q,
+                                 std::vector<Node>& terms,
+                                 Node inst,
+                                 bool doVts);
   /** get the instantiation rewriter object */
   InstantiationRewriter* getInstRewriter() const;
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 04b6e0dda..abf2ecdbe 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -35,12 +35,16 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
+Instantiate::Instantiate(QuantifiersEngine* qe,
+                         context::UserContext* u,
+                         ProofNodeManager* pnm)
     : d_qe(qe),
+      d_pnm(pnm),
       d_term_db(nullptr),
       d_term_util(nullptr),
       d_total_inst_debug(u),
-      d_c_inst_match_trie_dom(u)
+      d_c_inst_match_trie_dom(u),
+      d_pfInst(pnm ? new CDProof(pnm) : nullptr)
 {
 }
 
@@ -231,24 +235,101 @@ bool Instantiate::addInstantiation(
     return false;
   }
 
+  // Set up a proof if proofs are enabled. This proof stores a proof of
+  // the instantiation body with q as a free assumption.
+  std::shared_ptr<LazyCDProof> pfTmp;
+  if (isProofEnabled())
+  {
+    pfTmp.reset(new LazyCDProof(
+        d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
+  }
+
   // construct the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
   Assert(d_term_util->d_vars[q].size() == terms.size());
   // get the instantiation
-  Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+  Node body =
+      getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get());
   Node orig_body = body;
-  // now preprocess
-  body = quantifiers::QuantifiersRewriter::preprocess(body, true);
+  // now preprocess, storing the trust node for the rewrite
+  TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
+  if (!tpBody.isNull())
+  {
+    Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
+    body = tpBody.getNode();
+    // do a tranformation step
+    if (pfTmp != nullptr)
+    {
+      //              ----------------- from preprocess
+      // orig_body    orig_body = body
+      // ------------------------------ EQ_RESOLVE
+      // body
+      Node proven = tpBody.getProven();
+      // add the transformation proof, or THEORY_PREPROCESS if none provided
+      pfTmp->addLazyStep(proven,
+                         tpBody.getGenerator(),
+                         true,
+                         "Instantiate::getInstantiation:qpreprocess",
+                         false,
+                         PfRule::THEORY_PREPROCESS);
+      pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {body});
+    }
+  }
   Trace("inst-debug") << "...preprocess to " << body << std::endl;
 
   // construct the lemma
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
 
-  Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
-  lem = Rewriter::rewrite(lem);
+  // construct the instantiation, and rewrite the lemma
+  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, q, body);
+
+  // If proofs are enabled, construct the proof, which is of the form:
+  // ... free assumption q ...
+  // ------------------------- from pfTmp
+  // body
+  // ------------------------- SCOPE
+  // (=> q body)
+  // -------------------------- MACRO_SR_PRED_ELIM
+  // lem
+  bool hasProof = false;
+  if (isProofEnabled())
+  {
+    // make the proof of body
+    std::shared_ptr<ProofNode> pfn = pfTmp->getProofFor(body);
+    // make the scope proof to get (=> q body)
+    std::vector<Node> assumps;
+    assumps.push_back(q);
+    std::shared_ptr<ProofNode> pfns = d_pnm->mkScope({pfn}, assumps);
+    Assert(assumps.size() == 1 && assumps[0] == q);
+    // store in the main proof
+    d_pfInst->addProof(pfns);
+    Node prevLem = lem;
+    lem = Rewriter::rewrite(lem);
+    if (prevLem != lem)
+    {
+      d_pfInst->addStep(lem, PfRule::MACRO_SR_PRED_ELIM, {prevLem}, {});
+    }
+    hasProof = true;
+  }
+  else
+  {
+    lem = Rewriter::rewrite(lem);
+  }
 
-  // check for lemma duplication
-  if (!d_qe->addLemma(lem, true, false))
+  // added lemma, which checks for lemma duplication
+  bool addedLem = false;
+  if (hasProof)
+  {
+    // use trust interface
+    TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get());
+    addedLem = d_qe->addTrustedLemma(tlem, true, false);
+  }
+  else
+  {
+    addedLem = d_qe->addLemma(lem, true, false);
+  }
+
+  if (!addedLem)
   {
     Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate);
@@ -367,7 +448,8 @@ bool Instantiate::existsInstantiation(Node q,
 Node Instantiate::getInstantiation(Node q,
                                    std::vector<Node>& vars,
                                    std::vector<Node>& terms,
-                                   bool doVts)
+                                   bool doVts,
+                                   LazyCDProof* pf)
 {
   Node body;
   Assert(vars.size() == terms.size());
@@ -375,10 +457,34 @@ Node Instantiate::getInstantiation(Node q,
   // Notice that this could be optimized, but no significant performance
   // improvements were observed with alternative implementations (see #1386).
   body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
+
+  // store the proof of the instantiated body, with (open) assumption q
+  if (pf != nullptr)
+  {
+    pf->addStep(body, PfRule::INSTANTIATE, {q}, terms);
+  }
+
   // run rewriters to rewrite the instantiation in sequence.
   for (InstantiationRewriter*& ir : d_instRewrite)
   {
-    body = ir->rewriteInstantiation(q, terms, body, doVts);
+    TrustNode trn = ir->rewriteInstantiation(q, terms, body, doVts);
+    if (!trn.isNull())
+    {
+      Node newBody = trn.getNode();
+      // if using proofs, we store a preprocess + transformation step.
+      if (pf != nullptr)
+      {
+        Node proven = trn.getProven();
+        pf->addLazyStep(proven,
+                        trn.getGenerator(),
+                        true,
+                        "Instantiate::getInstantiation:rewrite_inst",
+                        false,
+                        PfRule::THEORY_PREPROCESS);
+        pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {});
+      }
+      body = newBody;
+    }
   }
   return body;
 }
@@ -675,6 +781,8 @@ void Instantiate::getExplanationForInstLemmas(
 #endif
 }
 
+bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
+
 void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
 {
   if (!options::trackInstLemmas())
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 8b1e0f7fc..7e984b116 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -20,6 +20,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
@@ -53,11 +54,14 @@ class InstantiationRewriter
    *
    * The flag doVts is whether we must apply virtual term substitution to the
    * instantiation.
+   *
+   * Returns a TrustNode of kind REWRITE, corresponding to the rewrite of inst
+   * and its proof generator.
    */
-  virtual Node rewriteInstantiation(Node q,
-                                    std::vector<Node>& terms,
-                                    Node inst,
-                                    bool doVts) = 0;
+  virtual TrustNode rewriteInstantiation(Node q,
+                                         std::vector<Node>& terms,
+                                         Node inst,
+                                         bool doVts) = 0;
 };
 
 /** Instantiate
@@ -84,7 +88,9 @@ class Instantiate : public QuantifiersUtil
   typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
 
  public:
-  Instantiate(QuantifiersEngine* qe, context::UserContext* u);
+  Instantiate(QuantifiersEngine* qe,
+              context::UserContext* u,
+              ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
   /** reset */
@@ -174,11 +180,16 @@ class Instantiate : public QuantifiersUtil
    *
    * Returns the instantiation lemma for q under substitution { vars -> terms }.
    * doVts is whether to apply virtual term substitution to its body.
+   *
+   * If provided, pf is a lazy proof for which we store a proof of the
+   * returned formula with free assumption q. This typically stores a
+   * single INSTANTIATE step concluding the instantiated body of q from q.
    */
   Node getInstantiation(Node q,
                         std::vector<Node>& vars,
                         std::vector<Node>& terms,
-                        bool doVts = false);
+                        bool doVts = false,
+                        LazyCDProof* pf = nullptr);
   /** get instantiation
    *
    * Same as above, but with vars/terms specified by InstMatch m.
@@ -277,6 +288,9 @@ class Instantiate : public QuantifiersUtil
                                    std::map<Node, std::vector<Node> >& tvec);
   //--------------------------------------end user-level interface utilities
 
+  /** Are proofs enabled for this object? */
+  bool isProofEnabled() const;
+
   /** statistics class
    *
    * This tracks statistics on the number of instantiations successfully
@@ -327,6 +341,8 @@ class Instantiate : public QuantifiersUtil
 
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
+  /** pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
   /** cache of term database for quantifiers engine */
   TermDb* d_term_db;
   /** cache of term util for quantifiers engine */
@@ -359,6 +375,10 @@ class Instantiate : public QuantifiersUtil
    * of these instantiations, for each quantified formula.
    */
   std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
+  /**
+   * A CDProof storing instantiation steps.
+   */
+  std::unique_ptr<CDProof> d_pfInst;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0848032f8..e34c1c823 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -2052,8 +2052,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   return n;
 }
 
-
-Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst)
+{
   Node prev = n;
 
   if( options::preSkolemQuant() ){
@@ -2078,8 +2078,9 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   if( n!=prev ){       
     Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
     Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
+    return TrustNode::mkTrustRewrite(prev, n, nullptr);
   }
-  return n;
+  return TrustNode::null();
 }
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index da3bd2212..196e4b108 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
 
 #include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -284,8 +285,10 @@ public:
    * registered quantified formula. If this flag is true, we do not apply
    * certain steps like pre-skolemization since we know they will have no
    * effect.
+   *
+   * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
    */
-  static Node preprocess( Node n, bool isInst = false );
+  static TrustNode preprocess(Node n, bool isInst = false);
   static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
   static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );