Track instantiation reasons in proofs (#6935)

This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.

Also simplifies an old argument modEq which was unused.

FYI @MikolasJanota

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 4b95b47da8ba51eafda4c1b1baf6a6b8bd7d5469..173e4df9abda59aecc0e0c72af1dcf01ab8e210f 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -827,10 +827,16 @@ enum class PfRule : uint32_t
   SKOLEMIZE,
   // ======== Instantiate
   // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
-  // Arguments: (t1 ... tn)
+  // Arguments: (t1 ... tn, (id (t)?)? )
   // ----------------------------------------
   // Conclusion: F*sigma
-  // sigma maps x1 ... xn to t1 ... tn.
+  // where sigma maps x1 ... xn to t1 ... tn.
+  //
+  // The optional argument id indicates the inference id that caused the
+  // instantiation. The term t indicates an additional term (e.g. the trigger)
+  // associated with the instantiation, which depends on the id. If the id
+  // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that
+  // generated the instantiation.
   INSTANTIATE,
   // ======== (Trusted) quantifiers preprocess
   // Children: ?

diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp
index ba2c07326295ce5006a62f0bc6d926cd24df3d0f..22304f9e84f09650d03fa5e71b05c00fc3f12ae2 100644 (file)
--- a/src/smt/unsat_core_manager.cpp
+++ b/src/smt/unsat_core_manager.cpp
@@ -80,7 +80,10 @@ void UnsatCoreManager::getRelevantInstantiations(
       const std::vector<Node>& instTerms = cur->getArguments();
       Assert(cs.size() == 1);
       Node q = cs[0]->getResult();
-      insts[q].push_back({instTerms.begin(), instTerms.end()});
+      // the instantiation is a prefix of the arguments up to the number of
+      // variables
+      insts[q].push_back(
+          {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()});
     }
     for (const std::shared_ptr<ProofNode>& cp : cs)
     {

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 9fbe37254b4a2e1c400bcd8e7c06795242f33fe8..c0700c06ef1657e421463ffbdcc04e85afbb6e3d 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -16,6 +16,7 @@
 #include "theory/inference_id.h"
 
 #include <iostream>
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
@@ -395,5 +396,10 @@ std::ostream& operator<<(std::ostream& out, InferenceId i)
   return out;
 }
 
+Node mkInferenceIdNode(InferenceId i)
+{
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i)));
+}
+
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 9ba324675998bb9eed3a16bcc0f98ab669a5523b..b3be59c5c754c635909c8e94f7aa60ad349701a8 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -20,6 +20,8 @@
 
 #include <iosfwd>
 
+#include "expr/node.h"
+
 namespace cvc5 {
 namespace theory {
 
@@ -786,6 +788,9 @@ const char* toString(InferenceId i);
  */
 std::ostream& operator<<(std::ostream& out, InferenceId i);
 
+/** Make node from inference id */
+Node mkInferenceIdNode(InferenceId i);
+
 }  // namespace theory
 }  // namespace cvc5
 

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index f059767a6c29644941545785801af6327f4dd5c4..f65828d2f58c471067f773666e24c8abb6a5b56e 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -491,7 +491,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   else if (inst->addInstantiation(d_curr_quant,
                                   subs,
                                   InferenceId::QUANTIFIERS_INST_CEGQI,
-                                  false,
+                                  Node::null(),
                                   false,
                                   usedVts))
   {

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 62558e2c65c916edc859a72bcd53b40be01d656d..5291259787c0ffb3685fcb0eab4258c39419b23b 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -59,6 +59,7 @@ Trigger::Trigger(QuantifiersState& qs,
     Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
     d_nodes.push_back(np);
   }
+  d_trNode = NodeManager::currentNM()->mkNode(SEXPR, d_nodes);
   if (Trace.isOn("trigger"))
   {
     QuantAttributes& qa = d_qreg.getQuantAttributes();
@@ -163,7 +164,7 @@ uint64_t Trigger::addInstantiations()
 
 bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
-  return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
+  return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode);
 }
 
 bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)

diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 172e93c120c1fad9ff213f066f5f93753babcecc..944a082c086de51307ee5b094a211595c209d5bb 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -181,6 +181,8 @@ class Trigger {
                                            std::vector<Node>& gts);
   /** The nodes comprising this trigger. */
   std::vector<Node> d_nodes;
+  /** The nodes as a single s-expression */
+  Node d_trNode;
   /**
    * The preprocessed ground terms in the nodes of the trigger, which as an
    * optimization omits variables and constant subterms. These terms are

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index c3fa664d9f39b5ce0d18dbad9cf59bc64d871798..c4f83191b255ae3ea5d5d85d34a37c68842ac9fa 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -725,8 +725,11 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       }
       // just add the instance
       d_triedLemmas++;
-      if (instq->addInstantiation(
-              f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true))
+      if (instq->addInstantiation(f,
+                                  inst,
+                                  InferenceId::QUANTIFIERS_INST_FMF_FMC,
+                                  Node::null(),
+                                  true))
       {
         Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
         d_addedLemmas++;
@@ -875,8 +878,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if (ie->addInstantiation(
-                f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
+        if (ie->addInstantiation(f,
+                                 inst,
+                                 InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH,
+                                 Node::null(),
+                                 true))
         {
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index cfccd4d937dcf0834b5ed165728c85458b1ecb48..a767af47aa2216fe8767af010e45406d754c86f8 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -56,8 +56,6 @@ class QModelBuilder : public TheoryEngineModelBuilder
   virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
-  /** exist instantiation ? */
-  virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
   //debug model
   void debugModel(TheoryModel* m) override;
   //statistics 

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 747b0621fe7d3a87794d2e88e91b6c47e721ac8a..e58f66d0b368f10548da2a2a142b1561f9224d57 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -301,8 +301,11 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if (inst->addInstantiation(
-                  f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true))
+          if (inst->addInstantiation(f,
+                                     m.d_vals,
+                                     InferenceId::QUANTIFIERS_INST_FMF_EXH,
+                                     Node::null(),
+                                     true))
           {
             addedLemmas++;
             if (d_qstate.isInConflict())

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 268d1371f59fcf6fe5b8b8252ed5e867a069e3b8..05361eaa11a3dd2ad71a0f871e75029e89f6d0c0 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -101,8 +101,8 @@ void Instantiate::addRewriter(InstantiationRewriter* ir)
 bool Instantiate::addInstantiation(Node q,
                                    std::vector<Node>& terms,
                                    InferenceId id,
+                                   Node pfArg,
                                    bool mkRep,
-                                   bool modEq,
                                    bool doVts)
 {
   // For resource-limiting (also does a time check).
@@ -229,7 +229,7 @@ bool Instantiate::addInstantiation(Node q,
   }
 
   // record the instantiation
-  bool recorded = recordInstantiationInternal(q, terms, modEq);
+  bool recorded = recordInstantiationInternal(q, terms);
   if (!recorded)
   {
     Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
@@ -250,7 +250,8 @@ bool Instantiate::addInstantiation(Node q,
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
   Assert(d_qreg.d_vars[q].size() == terms.size());
   // get the instantiation
-  Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
+  Node body = getInstantiation(
+      q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get());
   Node orig_body = body;
   // now preprocess, storing the trust node for the rewrite
   TrustNode tpBody = QuantifiersRewriter::preprocess(body, true);
@@ -394,12 +395,12 @@ bool Instantiate::addInstantiationExpFail(Node q,
                                           std::vector<Node>& terms,
                                           std::vector<bool>& failMask,
                                           InferenceId id,
+                                          Node pfArg,
                                           bool mkRep,
-                                          bool modEq,
                                           bool doVts,
                                           bool expFull)
 {
-  if (addInstantiation(q, terms, id, mkRep, modEq, doVts))
+  if (addInstantiation(q, terms, id, pfArg, mkRep, doVts))
   {
     return true;
   }
@@ -421,7 +422,9 @@ bool Instantiate::addInstantiationExpFail(Node q,
     subs[vars[i]] = terms[i];
   }
   // get the instantiation body
-  Node ibody = getInstantiation(q, vars, terms, doVts);
+  InferenceId idNone = InferenceId::UNKNOWN;
+  Node nulln;
+  Node ibody = getInstantiation(q, vars, terms, idNone, nulln, doVts);
   ibody = Rewriter::rewrite(ibody);
   for (size_t i = 0; i < tsize; i++)
   {
@@ -450,7 +453,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     // check whether the instantiation rewrites to the same thing
     if (!success)
     {
-      Node ibodyc = getInstantiation(q, vars, terms, doVts);
+      Node ibodyc = getInstantiation(q, vars, terms, idNone, nulln, doVts);
       ibodyc = Rewriter::rewrite(ibodyc);
       success = (ibodyc == ibody);
       Trace("inst-exp-fail") << "  rewrite invariant: " << success << std::endl;
@@ -521,6 +524,8 @@ bool Instantiate::existsInstantiation(Node q,
 Node Instantiate::getInstantiation(Node q,
                                    std::vector<Node>& vars,
                                    std::vector<Node>& terms,
+                                   InferenceId id,
+                                   Node pfArg,
                                    bool doVts,
                                    LazyCDProof* pf)
 {
@@ -534,7 +539,19 @@ Node Instantiate::getInstantiation(Node q,
   // store the proof of the instantiated body, with (open) assumption q
   if (pf != nullptr)
   {
-    pf->addStep(body, PfRule::INSTANTIATE, {q}, terms);
+    // additional arguments: if the inference id is not unknown, include it,
+    // followed by the proof argument if non-null. The latter is used e.g.
+    // to track which trigger caused an instantiation.
+    std::vector<Node> pfTerms = terms;
+    if (id != InferenceId::UNKNOWN)
+    {
+      pfTerms.push_back(mkInferenceIdNode(id));
+      if (!pfArg.isNull())
+      {
+        pfTerms.push_back(pfArg);
+      }
+    }
+    pf->addStep(body, PfRule::INSTANTIATE, {q}, pfTerms);
   }
 
   // run rewriters to rewrite the instantiation in sequence.
@@ -564,18 +581,16 @@ Node Instantiate::getInstantiation(Node q,
 Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
 {
   Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
-  return getInstantiation(q, d_qreg.d_vars[q], terms, doVts);
+  return getInstantiation(
+      q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts);
 }
 
-bool Instantiate::recordInstantiationInternal(Node q,
-                                              std::vector<Node>& terms,
-                                              bool modEq)
+bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms)
 {
   if (options::incrementalSolving())
   {
     Trace("inst-add-debug")
-        << "Adding into context-dependent inst trie, modEq = " << modEq
-        << std::endl;
+        << "Adding into context-dependent inst trie" << std::endl;
     CDInstMatchTrie* imt;
     std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
@@ -588,10 +603,10 @@ bool Instantiate::recordInstantiationInternal(Node q,
       d_c_inst_match_trie[q] = imt;
     }
     d_c_inst_match_trie_dom.insert(q);
-    return imt->addInstMatch(d_qstate, q, terms, modEq);
+    return imt->addInstMatch(d_qstate, q, terms);
   }
   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-  return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq);
+  return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
 }
 
 bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index eddc7470b90b443a346f73cb9acfb034069b9996..1f380350f4850d47f5d2b13f1af4d6d4724454f3 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -139,10 +139,10 @@ class Instantiate : public QuantifiersUtil
    * @param terms the terms to instantiate with
    * @param id the identifier of the instantiation lemma sent via the inference
    * manager
+   * @param pfArg an additional node to add to the arguments of the INSTANTIATE
+   * step
    * @param mkRep whether to take the representatives of the terms in the
    * range of the substitution m,
-   * @param modEq whether to check for duplication modulo equality in
-   * instantiation tries (for performance),
    * @param doVts whether we must apply virtual term substitution to the
    * instantiation lemma.
    *
@@ -161,8 +161,8 @@ class Instantiate : public QuantifiersUtil
   bool addInstantiation(Node q,
                         std::vector<Node>& terms,
                         InferenceId id,
+                        Node pfArg = Node::null(),
                         bool mkRep = false,
-                        bool modEq = false,
                         bool doVts = false);
   /**
    * Same as above, but we also compute a vector failMask indicating which
@@ -191,8 +191,8 @@ class Instantiate : public QuantifiersUtil
                                std::vector<Node>& terms,
                                std::vector<bool>& failMask,
                                InferenceId id,
+                               Node pfArg = Node::null(),
                                bool mkRep = false,
-                               bool modEq = false,
                                bool doVts = false,
                                bool expFull = true);
   /** record instantiation
@@ -226,6 +226,8 @@ class Instantiate : public QuantifiersUtil
   Node getInstantiation(Node q,
                         std::vector<Node>& vars,
                         std::vector<Node>& terms,
+                        InferenceId id = InferenceId::UNKNOWN,
+                        Node pfArg = Node::null(),
                         bool doVts = false,
                         LazyCDProof* pf = nullptr);
   /** get instantiation
@@ -293,14 +295,8 @@ class Instantiate : public QuantifiersUtil
   Statistics d_statistics;
 
  private:
-  /** record instantiation, return true if it was not a duplicate
-   *
-   * modEq : whether to check for duplication modulo equality in instantiation
-   *         tries (for performance),
-   */
-  bool recordInstantiationInternal(Node q,
-                                   std::vector<Node>& terms,
-                                   bool modEq = false);
+  /** record instantiation, return true if it was not a duplicate */
+  bool recordInstantiationInternal(Node q, std::vector<Node>& terms);
   /** remove instantiation from the cache */
   bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
   /**

diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index f44f2f291ca0a6c8a1a08ecffca657e2020553bd..5e02e16a540600a534a39884c1230da580025dfa 100644 (file)
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -102,15 +102,16 @@ Node QuantifiersProofRuleChecker::checkInternal(
   else if (id == PfRule::INSTANTIATE)
   {
     Assert(children.size() == 1);
+    // note we may have more arguments than just the term vector
     if (children[0].getKind() != FORALL
-        || args.size() != children[0][0].getNumChildren())
+        || args.size() < children[0][0].getNumChildren())
     {
       return Node::null();
     }
     Node body = children[0][1];
     std::vector<Node> vars;
     std::vector<Node> subs;
-    for (unsigned i = 0, nargs = args.size(); i < nargs; i++)
+    for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++)
     {
       vars.push_back(children[0][0][i]);
       subs.push_back(args[i]);