diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-26 11:47:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-26 11:47:22 -0500 |
| commit | 72f70f1573651bcbf5f327c7a3411ece0e607e3f (patch) | |
| tree | d2e57f33fdbb6a260b0f523aa4cf2b621474e374 /src/theory/quantifiers/sygus_inst.cpp | |
| parent | fa6c3db414d27f47e0bee55480df939e78c14eb3 (diff) | |
Pass term registry to quantifiers modules (#6216)
Diffstat (limited to 'src/theory/quantifiers/sygus_inst.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 52a2787f7..c5f9b44b0 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -186,8 +186,9 @@ void addSpecialValues( SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_ce_lemma_added(qs.getUserContext()), d_global_terms(qs.getUserContext()), d_notified_assertions(qs.getUserContext()) @@ -209,7 +210,7 @@ void SygusInst::reset_round(Theory::Effort e) d_active_quant.clear(); d_inactive_quant.clear(); - FirstOrderModel* model = d_quantEngine->getModel(); + FirstOrderModel* model = d_treg.getModel(); uint32_t nasserted = model->getNumAssertedQuantifiers(); for (uint32_t i = 0; i < nasserted; ++i) @@ -245,9 +246,9 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) if (quant_e != QEFFORT_STANDARD) return; - FirstOrderModel* model = d_quantEngine->getModel(); + FirstOrderModel* model = d_treg.getModel(); Instantiate* inst = d_qim.getInstantiate(); - TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); + TermDbSygus* db = d_treg.getTermDatabaseSygus(); SygusExplain syexplain(db); NodeManager* nm = NodeManager::currentNM(); options::SygusInstMode mode = options::sygusInstMode(); @@ -480,7 +481,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types) /* Generate counterexample lemma for 'q'. */ NodeManager* nm = NodeManager::currentNM(); - TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); + TermDbSygus* db = d_treg.getTermDatabaseSygus(); /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype * instantiation constant ic_i with type types[i] and wrap each ic_i in |