diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
| commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
| tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/sygus | |
| parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) | |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f93260f0c..066bcd769 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -348,7 +349,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) ptn = ptn.getRangeType(); } Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; - s = d_qe->getTermEnumeration()->getEnumerateTerm(ptn, 0); + s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0); } else { diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 831216445..a0058f2d8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -178,7 +178,7 @@ void SynthConjecture::assign(Node q) Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; // construct base instantiation - d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( + d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); if (!d_embedSideCondition.isNull()) { |