diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-03 09:18:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-03 09:18:59 -0600 |
commit | 0cd812af4a6db43a7d6c2c95fff7e58f86e90a78 (patch) | |
tree | ab35d8c8dd7ee7c7c8ba085d42ef834fe17e2dbd /src/theory/quantifiers/sygus/synth_engine.cpp | |
parent | 1d44edf91762b837adf3db5ed40af9383e883b28 (diff) |
Standardize the interface for SMT engine subsolvers (#3836)
This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index c9ed16a5f..a77d3681b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -16,12 +16,11 @@ #include "theory/quantifiers/sygus/synth_engine.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -169,9 +168,8 @@ void SynthEngine::assignConjecture(Node q) if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) { // create new smt engine to do quantifier elimination - SmtEngine smt_qe(nm->toExprManager()); - smt_qe.setIsInternalSubsolver(); - smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); + std::unique_ptr<SmtEngine> smt_qe; + initializeSubsolver(smt_qe); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; @@ -234,7 +232,7 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( + Expr qe_res = smt_qe->doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false); Trace("cegqi-qep") << "Result : " << qe_res << std::endl; |