(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.

9 files changed, 328 insertions, 137 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 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2e69080e7..da60561ad 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -174,7 +174,8 @@ class QuantifiersEnginePrivate
 
 QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      context::UserContext* u,
-                                     TheoryEngine* te)
+                                     TheoryEngine* te,
+                                     ProofNodeManager* pnm)
     : d_te(te),
       d_masterEqualityEngine(nullptr),
       d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
@@ -187,7 +188,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_term_db(new quantifiers::TermDb(c, u, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
-      d_instantiate(new quantifiers::Instantiate(this, u)),
+      d_instantiate(new quantifiers::Instantiate(this, u, pnm)),
       d_skolemize(new quantifiers::Skolemize(this, u)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_conflict_c(c, false),
@@ -1021,6 +1022,19 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   }
 }
 
+bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
+                                        bool doCache,
+                                        bool doRewrite)
+{
+  Node lem = tlem.getProven();
+  if (!addLemma(lem, doCache, doRewrite))
+  {
+    return false;
+  }
+  d_lemmasWaitingPg[lem] = tlem.getGenerator();
+  return true;
+}
+
 bool QuantifiersEngine::removeLemma( Node lem ) {
   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
   if( it!=d_lemmas_waiting.end() ){
@@ -1102,19 +1116,31 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode()
 }
 
 void QuantifiersEngine::flushLemmas(){
+  OutputChannel& out = getOutputChannel();
   if( !d_lemmas_waiting.empty() ){
     //take default output channel if none is provided
     d_hasAddedLemma = true;
-    for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
-      Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
-      getOutputChannel().lemma(d_lemmas_waiting[i], LemmaProperty::PREPROCESS);
+    std::map<Node, ProofGenerator*>::iterator itp;
+    for (const Node& lemw : d_lemmas_waiting)
+    {
+      Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
+      itp = d_lemmasWaitingPg.find(lemw);
+      if (itp != d_lemmasWaitingPg.end())
+      {
+        TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
+        out.trustedLemma(tlemw, LemmaProperty::PREPROCESS);
+      }
+      else
+      {
+        out.lemma(lemw, LemmaProperty::PREPROCESS);
+      }
     }
     d_lemmas_waiting.clear();
   }
   if( !d_phase_req_waiting.empty() ){
     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
-      getOutputChannel().requirePhase( it->first, it->second );
+      out.requirePhase(it->first, it->second);
     }
     d_phase_req_waiting.clear();
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 6afc4f925..bd88034cb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -55,8 +55,11 @@ class QuantifiersEngine {
   typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
-public:
-  QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
+ public:
+  QuantifiersEngine(context::Context* c,
+                    context::UserContext* u,
+                    TheoryEngine* te,
+                    ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
   /** get theory engine */
@@ -196,100 +199,117 @@ private:
  void flushLemmas();
 
 public:
-  /** add lemma lem */
-  bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
-  /** remove pending lemma */
-  bool removeLemma( Node lem );
-  /** add require phase */
-  void addRequirePhase( Node lit, bool req );
-  /** mark relevant quantified formula, this will indicate it should be checked before the others */
-  void markRelevant( Node q );
-  /** has added lemma */
-  bool hasAddedLemma() const;
-  /** theory engine needs check
-   *
-   * This is true if the theory engine has more constraints to process. When
-   * it is false, we are tentatively going to terminate solving with
-   * sat/unknown. For details, see TheoryEngine::needCheck.
-   */
-  bool theoryEngineNeedsCheck() const;
-  /** is in conflict */
-  bool inConflict() { return d_conflict; }
-  /** set conflict */
-  void setConflict();
-  /** get current q effort */
-  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
-  /** get number of waiting lemmas */
-  unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
-  /** get needs check */
-  bool getInstWhenNeedsCheck( Theory::Effort e );
-  /** get user pat mode */
-  options::UserPatMode getInstUserPatMode();
+ /**
+  * Add lemma to the lemma buffer of this quantifiers engine.
+  * @param lem The lemma to send
+  * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
+  * @param doRewrite Whether to rewrite the lemma
+  * @return true if the lemma was successfully added to the buffer
+  */
+ bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
+ /**
+  * Add trusted lemma lem, same as above, but where a proof generator may be
+  * provided along with the lemma.
+  */
+ bool addTrustedLemma(TrustNode tlem,
+                      bool doCache = true,
+                      bool doRewrite = true);
+ /** remove pending lemma */
+ bool removeLemma(Node lem);
+ /** add require phase */
+ void addRequirePhase(Node lit, bool req);
+ /** mark relevant quantified formula, this will indicate it should be checked
+  * before the others */
+ void markRelevant(Node q);
+ /** has added lemma */
+ bool hasAddedLemma() const;
+ /** theory engine needs check
+  *
+  * This is true if the theory engine has more constraints to process. When
+  * it is false, we are tentatively going to terminate solving with
+  * sat/unknown. For details, see TheoryEngine::needCheck.
+  */
+ bool theoryEngineNeedsCheck() const;
+ /** is in conflict */
+ bool inConflict() { return d_conflict; }
+ /** set conflict */
+ void setConflict();
+ /** get current q effort */
+ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
+ /** get number of waiting lemmas */
+ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
+ /** get needs check */
+ bool getInstWhenNeedsCheck(Theory::Effort e);
+ /** get user pat mode */
+ options::UserPatMode getInstUserPatMode();
 
- public:
-  /** add term to database */
-  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
-  /** notification when master equality engine is updated */
-  void eqNotifyNewClass(TNode t);
-  /** debug print equality engine */
-  void debugPrintEqualityEngine( const char * c );
-  /** get internal representative
-   *
-   * Choose a term that is equivalent to a in the current context that is the
-   * best term for instantiating the index^th variable of quantified formula q.
-   * If no legal term can be found, we return null. This can occur if:
-   * - a's type is not a subtype of the type of the index^th variable of q,
-   * - a is in an equivalent class with all terms that are restricted not to
-   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
-   * guided instantiation.
-   */
-  Node getInternalRepresentative( Node a, Node q, int index );
+public:
+ /** add term to database */
+ void addTermToDatabase(Node n,
+                        bool withinQuant = false,
+                        bool withinInstClosure = false);
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ /** debug print equality engine */
+ void debugPrintEqualityEngine(const char* c);
+ /** get internal representative
+  *
+  * Choose a term that is equivalent to a in the current context that is the
+  * best term for instantiating the index^th variable of quantified formula q.
+  * If no legal term can be found, we return null. This can occur if:
+  * - a's type is not a subtype of the type of the index^th variable of q,
+  * - a is in an equivalent class with all terms that are restricted not to
+  * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
+  * guided instantiation.
+  */
+ Node getInternalRepresentative(Node a, Node q, int index);
 
- public:
-  //----------user interface for instantiations (see quantifiers/instantiate.h)
-  /** print instantiations */
-  void printInstantiations(std::ostream& out);
-  /** print solution for synthesis conjectures */
-  void printSynthSolution(std::ostream& out);
-  /** get list of quantified formulas that were instantiated */
-  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
-  /** get instantiations */
-  void getInstantiations(Node q, std::vector<Node>& insts);
-  void getInstantiations(std::map<Node, std::vector<Node> >& insts);
-  /** get instantiation term vectors */
-  void getInstantiationTermVectors(Node q,
-                                   std::vector<std::vector<Node> >& tvecs);
-  void getInstantiationTermVectors(
-      std::map<Node, std::vector<std::vector<Node> > >& insts);
-  /** get instantiated conjunction */
-  Node getInstantiatedConjunction(Node q);
-  /** get unsat core lemmas */
-  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
-  /** get explanation for instantiation lemmas */
-  void getExplanationForInstLemmas(const std::vector<Node>& lems,
-                                   std::map<Node, Node>& quant,
-                                   std::map<Node, std::vector<Node> >& tvec);
+public:
+ //----------user interface for instantiations (see quantifiers/instantiate.h)
+ /** print instantiations */
+ void printInstantiations(std::ostream& out);
+ /** print solution for synthesis conjectures */
+ void printSynthSolution(std::ostream& out);
+ /** get list of quantified formulas that were instantiated */
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ /** get instantiations */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ void getInstantiations(std::map<Node, std::vector<Node> >& insts);
+ /** get instantiation term vectors */
+ void getInstantiationTermVectors(Node q,
+                                  std::vector<std::vector<Node> >& tvecs);
+ void getInstantiationTermVectors(
+     std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /** get instantiated conjunction */
+ Node getInstantiatedConjunction(Node q);
+ /** get unsat core lemmas */
+ bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+ /** get explanation for instantiation lemmas */
+ void getExplanationForInstLemmas(const std::vector<Node>& lems,
+                                  std::map<Node, Node>& quant,
+                                  std::map<Node, std::vector<Node> >& tvec);
 
-  /** get synth solutions
-   *
-   * This method returns true if there is a synthesis solution available. This
-   * is the case if the last call to check satisfiability originated in a
-   * check-synth call, and the synthesis engine module of this class
-   * successfully found a solution for all active synthesis conjectures.
-   *
-   * This method adds entries to sol_map that map functions-to-synthesize with
-   * their solutions, for all active conjectures. This should be called
-   * immediately after the solver answers unsat for sygus input.
-   *
-   * For details on what is added to sol_map, see
-   * SynthConjecture::getSynthSolutions.
-   */
-  bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
+ /** get synth solutions
+  *
+  * This method returns true if there is a synthesis solution available. This
+  * is the case if the last call to check satisfiability originated in a
+  * check-synth call, and the synthesis engine module of this class
+  * successfully found a solution for all active synthesis conjectures.
+  *
+  * This method adds entries to sol_map that map functions-to-synthesize with
+  * their solutions, for all active conjectures. This should be called
+  * immediately after the solver answers unsat for sygus input.
+  *
+  * For details on what is added to sol_map, see
+  * SynthConjecture::getSynthSolutions.
+  */
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 
-  //----------end user interface for instantiations
+ //----------end user interface for instantiations
 
-  /** statistics class */
-  class Statistics {
+ /** statistics class */
+ class Statistics
+ {
   public:
     TimerStat d_time;
     TimerStat d_qcf_time;
@@ -379,6 +399,8 @@ public:
   BoolMap d_lemmas_produced_c;
   /** lemmas waiting */
   std::vector<Node> d_lemmas_waiting;
+  /** map from waiting lemmas to their proof generators */
+  std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
   /** phase requirements waiting */
   std::map<Node, bool> d_phase_req_waiting;
   /** inst round counters TODO: make context-dependent? */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6837d4be5..6a548e5b6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -165,7 +165,8 @@ void TheoryEngine::finishInit() {
   if (d_logicInfo.isQuantified())
   {
     // initialize the quantifiers engine
-    d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+    d_quantEngine =
+        new QuantifiersEngine(d_context, d_userContext, this, d_pnm);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.