diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 14:59:40 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-11 20:59:40 +0000 |
commit | 3d9daccc198844c24c8014f1fff31a64714b3dff (patch) | |
tree | d60ce10253aab175b004f7ae1576bd3b5a31c56a /src/theory/quantifiers/instantiate.h | |
parent | 42d5d8950d849aa4b855aa62834cd5fdee1a91a8 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 19 |
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, |