diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-23 15:41:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-23 20:41:13 +0000 |
| commit | d5d526730d11d08c65aa17ea53d0dffb0a72e692 (patch) | |
| tree | 13ce2001785e168ea82cbd0bce0c1750f987a338 /src/theory/quantifiers/instantiate.h | |
| parent | 8fc8793f4337663f7250846dd6acae167a7f27ec (diff) | |
Passing term registry to ematching utilities (#6190)
Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 8e556b648..be410c2c8 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -97,7 +97,6 @@ class Instantiate : public QuantifiersUtil QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, - FirstOrderModel* m, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -224,17 +223,6 @@ class Instantiate : public QuantifiersUtil * Same as above but with vars equal to the bound variables of q. */ Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false); - /** get term for type - * - * This returns an arbitrary term for type tn. - * This term is chosen heuristically to be the best - * term for instantiation. Currently, this - * heuristic enumerates the first term of the - * type if the type is closed enumerable, otherwise - * an existing ground term from the term database if - * one exists, or otherwise a fresh variable. - */ - Node getTermForType(TypeNode tn); //--------------------------------------end general utilities /** @@ -318,8 +306,6 @@ class Instantiate : public QuantifiersUtil QuantifiersRegistry& d_qreg; /** Reference to the term registry */ TermRegistry& d_treg; - /** Pointer to the model */ - FirstOrderModel* d_model; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** instantiation rewriter classes */ @@ -335,8 +321,8 @@ class Instantiate : public QuantifiersUtil * We store context (dependent, independent) versions. If incremental solving * is disabled, we use d_inst_match_trie for performance reasons. */ - std::map<Node, inst::InstMatchTrie> d_inst_match_trie; - std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie; + std::map<Node, InstMatchTrie> d_inst_match_trie; + std::map<Node, CDInstMatchTrie*> d_c_inst_match_trie; /** * The list of quantified formulas for which the domain of d_c_inst_match_trie * is valid. |