Introduce inference ids for quantifier instantiation (#6119)

This makes quantifiers use standard inference ids.

This eliminates the need to track ad-hoc statistics, per instantiation type.

This makes minor modifications to a few interfaces in quantifiers to enable this.

1 files changed, 13 insertions, 6 deletions

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index e55e677df..abdee69ef 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "expr/proof.h"
+#include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
@@ -126,12 +127,16 @@ class Instantiate : public QuantifiersUtil
    * This function returns true if the instantiation lemma for quantified
    * formula q for the substitution specified by terms is successfully enqueued
    * via a call to QuantifiersInferenceManager::addPendingLemma.
-   *   mkRep : whether to take the representatives of the terms in the range of
-   *           the substitution m,
-   *   modEq : whether to check for duplication modulo equality in instantiation
-   *           tries (for performance),
-   *   doVts : whether we must apply virtual term substitution to the
-   *           instantiation lemma.
+   * @param q the quantified formula to instantiate
+   * @param terms the terms to instantiate with
+   * @param id the identifier of the instantiation lemma sent via the inference
+   * manager
+   * @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.
    *
    * This call may fail if it can be determined that the instantiation is not
    * relevant or legal in the current context. This happens if:
@@ -147,6 +152,7 @@ class Instantiate : public QuantifiersUtil
    */
   bool addInstantiation(Node q,
                         std::vector<Node>& terms,
+                        InferenceId id,
                         bool mkRep = false,
                         bool modEq = false,
                         bool doVts = false);
@@ -176,6 +182,7 @@ class Instantiate : public QuantifiersUtil
   bool addInstantiationExpFail(Node q,
                                std::vector<Node>& terms,
                                std::vector<bool>& failMask,
+                               InferenceId id,
                                bool mkRep = false,
                                bool modEq = false,
                                bool doVts = false,