This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
// make a separate smt call
std::unique_ptr<SmtEngine> rrSygus;
- theory::initializeSubsolver(rrSygus);
+ theory::initializeSubsolver(rrSygus,
+ d_preprocContext->getOptions(),
+ d_preprocContext->getLogicInfo());
rrSygus->assertFormula(body);
Trace("sygus-infer") << "*** Check sat..." << std::endl;
Result r = rrSygus->checkSat();
d_symsInAssertions(env.getUserContext())
{
}
-
+const Options& PreprocessingPassContext::getOptions()
+{
+ return d_env.getOptions();
+}
+const LogicInfo& PreprocessingPassContext::getLogicInfo()
+{
+ return d_env.getLogicInfo();
+}
theory::TrustSubstitutionMap&
PreprocessingPassContext::getTopLevelSubstitutions()
{
void spendResource(Resource r);
- /** Get the current logic info of the SmtEngine */
- const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
+ /** Get the options of the environment */
+ const Options& getOptions();
+ /** Get the current logic info of the environment */
+ const LogicInfo& getLogicInfo();
/** Gets a reference to the top-level substitution map */
theory::TrustSubstitutionMap& getTopLevelSubstitutions();
namespace cvc5 {
namespace smt {
-AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {}
+AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent)
+ : d_env(env), d_parent(parent)
+{
+}
AbductionSolver::~AbductionSolver() {}
bool AbductionSolver::getAbduct(const Node& goal,
std::vector<Node> axioms = d_parent->getExpandedAssertions();
std::vector<Node> asserts(axioms.begin(), axioms.end());
// must expand definitions
- Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal);
+ Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
// now negate
conjn = conjn.negate();
d_abdConj = conjn;
Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
<< ", solving for " << d_sssf << std::endl;
// we generate a new smt engine to do the abduction query
- initializeSubsolver(d_subsolver);
+ initializeSubsolver(d_subsolver, d_env);
// get the logic
LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy();
// enable everything needed for sygus
<< ": make new SMT engine" << std::endl;
// Start new SMT engine to check solution
std::unique_ptr<SmtEngine> abdChecker;
- initializeSubsolver(abdChecker);
+ initializeSubsolver(abdChecker, d_env);
Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
<< ": asserting formulas" << std::endl;
for (const Node& e : asserts)
namespace cvc5 {
+class Env;
class SmtEngine;
namespace smt {
class AbductionSolver
{
public:
- AbductionSolver(SmtEngine* parent);
+ AbductionSolver(Env& env, SmtEngine* parent);
~AbductionSolver();
/**
* This method asks this SMT engine to find an abduct with respect to the
* problems.
*/
bool getAbductInternal(Node& abd);
+ /** Reference to the env */
+ Env& d_env;
/** The parent SMT engine */
SmtEngine* d_parent;
/** The SMT engine subsolver
namespace cvc5 {
-Env::Env(NodeManager* nm, Options* opts)
+Env::Env(NodeManager* nm, const Options* opts)
: d_context(new context::Context()),
d_userContext(new context::UserContext()),
d_nodeManager(nm),
/**
* Construct an Env with the given node manager.
*/
- Env(NodeManager* nm, Options* opts);
+ Env(NodeManager* nm, const Options* opts);
/** Destruct the env. */
~Env();
namespace cvc5 {
namespace smt {
-InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
+InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent)
+ : d_env(env), d_parent(parent)
{
}
<< std::endl;
std::vector<Node> axioms = d_parent->getExpandedAssertions();
// must expand definitions
- Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj);
+ Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
std::string name("A");
- quantifiers::SygusInterpol interpolSolver;
+ quantifiers::SygusInterpol interpolSolver(d_env);
if (interpolSolver.solveInterpolation(
name, axioms, conjn, grammarType, interpol))
{
<< ": make new SMT engine" << std::endl;
// Start new SMT engine to check solution
std::unique_ptr<SmtEngine> itpChecker;
- initializeSubsolver(itpChecker);
+ initializeSubsolver(itpChecker, d_env);
Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
<< ": asserting formulas" << std::endl;
if (j == 0)
namespace cvc5 {
+class Env;
class SmtEngine;
namespace smt {
class InterpolationSolver
{
public:
- InterpolationSolver(SmtEngine* parent);
+ InterpolationSolver(Env& env, SmtEngine* parent);
~InterpolationSolver();
/**
const Node& conj);
private:
+ /** Reference to the env */
+ Env& d_env;
/** The parent SMT engine */
SmtEngine* d_parent;
};
#include "options/language.h"
#include "options/smt_options.h"
#include "smt/assertions.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "theory/smt_engine_subsolver.h"
std::unique_ptr<SmtEngine> optChecker;
// initializeSubSolver will copy the options and theories enabled
// from the current solver to optChecker and adds timeout
- theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
+ theory::initializeSubsolver(
+ optChecker, parentSMTSolver->getEnv(), needsTimeout, timeout);
// we need to be in incremental mode for multiple objectives since we need to
// push pop we need to produce models to inrement on our objective
optChecker->setOption("incremental", "true");
Result OptimizationSolver::optimizeParetoNaiveGIA()
{
// initial call to Pareto optimizer, create the checker
- if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
+ if (!d_optChecker)
+ {
+ d_optChecker = createOptCheckerWithTimeout(d_parent);
+ }
NodeManager* nm = d_optChecker->getNodeManager();
// checks whether the current set of assertions are satisfied or not
namespace cvc5 {
+class Env;
class SmtEngine;
namespace smt {
private:
/**
* Initialize an SMT subsolver for offline optimization purpose
+ * @param env the environment, which determines options and logic for the
+ * subsolver
* @param parentSMTSolver the parental solver containing the assertions
* @param needsTimeout specifies whether it needs timeout for each single
* query
namespace cvc5 {
namespace smt {
-QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {}
+QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms)
+ : d_env(env), d_smtSolver(sms)
+{
+}
QuantElimSolver::~QuantElimSolver() {}
// ensure the body is rewritten
q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
// do nested quantifier elimination if necessary
- q = quantifiers::NestedQe::doNestedQe(q, true);
+ q = quantifiers::NestedQe::doNestedQe(d_env, q, true);
Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
<< q << std::endl;
// tag the quantified formula with the quant-elim attribute
#include "smt/assertions.h"
namespace cvc5 {
+class Env;
+
namespace smt {
class SmtSolver;
class QuantElimSolver
{
public:
- QuantElimSolver(SmtSolver& sms);
+ QuantElimSolver(Env& env, SmtSolver& sms);
~QuantElimSolver();
/**
bool isInternalSubsolver);
private:
+ /** Reference to the env */
+ Env& d_env;
/** The SMT solver, which is used during doQuantifierElimination. */
SmtSolver& d_smtSolver;
};
namespace cvc5 {
-SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
+SmtEngine::SmtEngine(NodeManager* nm, const Options* optr)
: d_env(new Env(nm, optr)),
d_state(new SmtEngineState(*d_env.get(), *this)),
d_absValues(new AbstractValues(getNodeManager())),
// make the SMT solver
d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats));
// make the SyGuS solver
- d_sygusSolver.reset(
- new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
+ d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp));
// make the quantifier elimination solver
- d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
-
+ d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver));
}
bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
// subsolvers
if (d_env->getOptions().smt.produceAbducts)
{
- d_abductSolver.reset(new AbductionSolver(this));
+ d_abductSolver.reset(new AbductionSolver(*d_env.get(), this));
}
if (d_env->getOptions().smt.produceInterpols
!= options::ProduceInterpols::NONE)
{
- d_interpolSolver.reset(new InterpolationSolver(this));
+ d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this));
}
d_pp->finishInit();
Trace("smt") << "SMT getValue(" << ex << ")" << endl;
if (Dump.isOn("benchmark"))
{
- getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
+ getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex});
}
TypeNode expectedType = ex.getType();
for (const Node& skip : core)
{
std::unique_ptr<SmtEngine> coreChecker;
- initializeSubsolver(coreChecker);
+ initializeSubsolver(coreChecker, *d_env.get());
coreChecker->setLogic(getLogicInfo());
coreChecker->getOptions().smt.checkUnsatCores = false;
// disable all proof options
// initialize the core checker
std::unique_ptr<SmtEngine> coreChecker;
- initializeSubsolver(coreChecker);
+ initializeSubsolver(coreChecker, *d_env.get());
coreChecker->getOptions().smt.checkUnsatCores = false;
// disable all proof options
coreChecker->getOptions().smt.produceProofs = false;
if (Dump.isOn("benchmark"))
{
- getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
+ getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key);
}
if (key == "command-verbosity")
* If provided, optr is a pointer to a set of options that should initialize the values
* of the options object owned by this class.
*/
- SmtEngine(NodeManager* nm, Options* optr = nullptr);
+ SmtEngine(NodeManager* nm, const Options* optr = nullptr);
/** Destruct the SMT engine. */
~SmtEngine();
namespace cvc5 {
namespace smt {
-SygusSolver::SygusSolver(SmtSolver& sms,
- Preprocessor& pp,
- context::UserContext* u,
- OutputManager& outMgr)
- : d_smtSolver(sms),
+SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp)
+ : d_env(env),
+ d_smtSolver(sms),
d_pp(pp),
- d_sygusConjectureStale(u, true),
- d_outMgr(outMgr)
+ d_sygusConjectureStale(env.getUserContext(), true)
{
}
Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
if (Dump.isOn("raw-benchmark"))
{
- d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
+ d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut());
}
d_sygusConjectureStale = false;
{
// Start new SMT engine to check solutions
std::unique_ptr<SmtEngine> solChecker;
- initializeSubsolver(solChecker);
+ initializeSubsolver(solChecker, d_env);
solChecker->getOptions().smt.checkSynthSol = false;
solChecker->getOptions().quantifiers.sygusRecFun = false;
// get the solution for this conjecture
class SygusSolver
{
public:
- SygusSolver(SmtSolver& sms,
- Preprocessor& pp,
- context::UserContext* u,
- OutputManager& outMgr);
+ SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp);
~SygusSolver();
/**
* previously not stale.
*/
void setSygusConjectureStale();
+ /** Reference to the env class */
+ Env& d_env;
/** The SMT solver, which is used during checkSynth. */
SmtSolver& d_smtSolver;
/** The preprocessor, used for checkSynthSolution. */
* Whether we need to reconstruct the sygus conjecture.
*/
context::CDO<bool> d_sygusConjectureStale;
- /** Reference to the output manager of the smt engine */
- OutputManager& d_outMgr;
};
} // namespace smt
}
if (options::cegqiNestedQE())
{
- d_nestedQe.reset(new NestedQe(qs.getUserContext()));
+ d_nestedQe.reset(new NestedQe(qs.getEnv()));
}
}
#include "expr/node_algorithm.h"
#include "expr/subs.h"
+#include "smt/env.h"
#include "theory/smt_engine_subsolver.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
-NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {}
+NestedQe::NestedQe(Env& env) : d_env(env), d_qnqe(d_env.getUserContext()) {}
bool NestedQe::process(Node q, std::vector<Node>& lems)
{
return (*it).second != q;
}
Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl;
- Node qqe = doNestedQe(q, true);
+ Node qqe = doNestedQe(d_env, q, true);
d_qnqe[q] = qqe;
if (qqe == q)
{
return getNestedQuantification(q, nqs);
}
-Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
+Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel)
{
NodeManager* nm = NodeManager::currentNM();
Node qOrig = q;
return qOrig;
}
// just do ordinary quantifier elimination
- Node qqe = doQe(q);
+ Node qqe = doQe(env, q);
Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl;
return qqe;
}
for (const Node& nq : nqs)
{
Node nqk = sk.apply(nq);
- Node nqqe = doNestedQe(nqk);
+ Node nqqe = doNestedQe(env, nqk);
if (nqqe == nqk)
{
// failed
return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs);
}
-Node NestedQe::doQe(Node q)
+Node NestedQe::doQe(Env& env, Node q)
{
Assert(q.getKind() == kind::FORALL);
Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl;
NodeManager* nm = NodeManager::currentNM();
q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
std::unique_ptr<SmtEngine> smt_qe;
- initializeSubsolver(smt_qe);
+ initializeSubsolver(smt_qe, env);
Node qqe = smt_qe->getQuantifierElimination(q, true, false);
if (expr::hasBoundVar(qqe))
{
#include "expr/node.h"
namespace cvc5 {
+
+class Env;
+
namespace theory {
namespace quantifiers {
using NodeNodeMap = context::CDHashMap<Node, Node>;
public:
- NestedQe(context::UserContext* u);
+ NestedQe(Env& env);
~NestedQe() {}
/**
* Process quantified formula. If this returns true, then q was processed
* returned formula is quantifier-free. Otherwise, it is a quantified formula
* with no nested quantification.
*/
- static Node doNestedQe(Node q, bool keepTopLevel = false);
+ static Node doNestedQe(Env& env, Node q, bool keepTopLevel = false);
/**
* Run quantifier elimination on quantified formula q, where q has no nested
* quantification. This method invokes a subsolver for performing quantifier
* elimination.
*/
- static Node doQe(Node q);
+ static Node doQe(Env& env, Node q);
private:
+ /** Reference to the env */
+ Env& d_env;
/**
* Mapping from quantified formulas q to the result of doNestedQe(q, true).
*/
Assert (!query.isNull());
if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
{
- initializeSubsolver(
- checker, nullptr, true, options::sygusExprMinerCheckTimeout());
+ initializeSubsolver(checker,
+ d_env,
+ true,
+ options::sygusExprMinerCheckTimeout());
}
else
{
- initializeSubsolver(checker);
+ initializeSubsolver(checker, d_env);
}
// also set the options
checker->setOption("sygus-rr-synth-input", "false");
namespace quantifiers {
CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s)
- : d_sip(new SingleInvocationPartition),
+ : d_env(env),
+ d_sip(new SingleInvocationPartition),
d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)),
d_isSolved(false),
d_single_invocation(false),
}
// solve the single invocation conjecture using a fresh copy of SMT engine
std::unique_ptr<SmtEngine> siSmt;
- initializeSubsolver(siSmt);
+ initializeSubsolver(siSmt, d_env);
siSmt->assertFormula(siq);
Result r = siSmt->checkSat();
Trace("sygus-si") << "Result: " << r << std::endl;
std::map< Node, std::vector< Node > >& teq,
Node n, std::vector< Node >& conj );
private:
+ /** Reference to the env */
+ Env& d_env;
// single invocation inference utility
SingleInvocationPartition* d_sip;
/** solution reconstruction */
namespace theory {
namespace quantifiers {
-Cegis::Cegis(QuantifiersInferenceManager& qim,
+Cegis::Cegis(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : SygusModule(qim, tds, p),
+ : SygusModule(qs, qim, tds, p),
d_eval_unfold(tds->getEvalUnfold()),
d_usingSymCons(false)
{
class Cegis : public SygusModule
{
public:
- Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p);
+ Cegis(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
+ SynthConjecture* p);
~Cegis() override {}
/** initialize */
virtual bool initialize(Node conj,
return false;
}
-CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim,
+CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qim, tds, p)
+ : Cegis(qs, qim, tds, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
{
Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
- Result r = checkWithSubsolver(n, d_vars, mvs);
+ Env& env = d_qstate.getEnv();
+ Result r =
+ checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo());
Trace("sygus-ccore-debug") << "...got " << r << std::endl;
return r;
}
addSuccess = false;
// try a new core
std::unique_ptr<SmtEngine> checkSol;
- initializeSubsolver(checkSol);
+ initializeSubsolver(checkSol, d_qstate.getEnv());
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
std::vector<Node> rasserts = asserts;
rasserts.push_back(d_sc);
// In terms of Variant #2, this is the check "if S ^ U is unsat"
Trace("sygus-ccore") << "----- Check side condition" << std::endl;
std::unique_ptr<SmtEngine> checkSc;
- initializeSubsolver(checkSc);
+ initializeSubsolver(checkSc, d_qstate.getEnv());
std::vector<Node> scasserts;
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
scasserts.push_back(d_sc);
class CegisCoreConnective : public Cegis
{
public:
- CegisCoreConnective(QuantifiersInferenceManager& qim,
+ CegisCoreConnective(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p);
~CegisCoreConnective() {}
QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
+ : Cegis(qs, qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
{
}
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "options/smt_options.h"
+#include "smt/env.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
namespace theory {
namespace quantifiers {
-SygusInterpol::SygusInterpol() {}
+SygusInterpol::SygusInterpol(Env& env) : d_env(env) {}
void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
const Node& conj)
mkSygusConjecture(itp, axioms, conj);
std::unique_ptr<SmtEngine> subSolver;
- initializeSubsolver(subSolver);
+ initializeSubsolver(subSolver, d_env);
// get the logic
LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
// enable everything needed for sygus
namespace cvc5 {
+class Env;
class SmtEngine;
namespace theory {
class SygusInterpol
{
public:
- SygusInterpol();
+ SygusInterpol(Env& env);
/**
* Returns the sygus conjecture in interpol corresponding to the interpolation
* @param itp the interpolation predicate.
*/
bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
-
+ /** Reference to the env */
+ Env& d_env;
/**
* symbols from axioms and conjecture.
*/
namespace theory {
namespace quantifiers {
-SygusModule::SygusModule(QuantifiersInferenceManager& qim,
+SygusModule::SygusModule(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : d_qim(qim), d_tds(tds), d_parent(p)
+ : d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
{
}
class SynthConjecture;
class TermDbSygus;
+class QuantifiersState;
class QuantifiersInferenceManager;
/** SygusModule
class SygusModule
{
public:
- SygusModule(QuantifiersInferenceManager& qim,
+ SygusModule(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p);
virtual ~SygusModule() {}
virtual bool usingRepairConst() { return false; }
protected:
+ /** Reference to the state of the quantifiers engine */
+ QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** sygus term database of d_qe */
namespace theory {
namespace quantifiers {
-SygusPbe::SygusPbe(QuantifiersInferenceManager& qim,
+SygusPbe::SygusPbe(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : SygusModule(qim, tds, p)
+ : SygusModule(qs, qim, tds, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
class SygusPbe : public SygusModule
{
public:
- SygusPbe(QuantifiersInferenceManager& qim,
+ SygusPbe(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p);
~SygusPbe();
namespace theory {
namespace quantifiers {
-SygusQePreproc::SygusQePreproc() {}
+SygusQePreproc::SygusQePreproc(Env& env) : d_env(env) {}
Node SygusQePreproc::preprocess(Node q)
{
}
// create new smt engine to do quantifier elimination
std::unique_ptr<SmtEngine> smt_qe;
- initializeSubsolver(smt_qe);
+ initializeSubsolver(smt_qe, d_env);
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
<< std::endl;
#include "expr/node.h"
namespace cvc5 {
+
+class Env;
+
namespace theory {
namespace quantifiers {
class SygusQePreproc
{
public:
- SygusQePreproc();
+ SygusQePreproc(Env& env);
~SygusQePreproc() {}
/**
* Preprocess. Returns a lemma of the form q = nq where nq is obtained
* by the quantifier elimination technique outlined above.
*/
Node preprocess(Node q);
+
+ private:
+ /** Reference to the env */
+ Env& d_env;
};
} // namespace quantifiers
// initialize the subsolver using the standard method
initializeSubsolver(
repcChecker,
- nullptr,
+ d_env.getOptions(),
+ d_env.getLogicInfo(),
Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
options::sygusRepairConstTimeout());
// renable options disabled by sygus
d_treg(tr),
d_stats(s),
d_tds(tr.getTermDatabaseSygus()),
- d_verify(qs.options(), d_tds),
+ d_verify(qs.options(), qs.getLogicInfo(), d_tds),
d_hasSolution(false),
d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)),
d_templInfer(new SygusTemplateInfer),
d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)),
d_exampleInfer(new ExampleInfer(d_tds)),
- d_ceg_pbe(new SygusPbe(qim, d_tds, this)),
- d_ceg_cegis(new Cegis(qim, d_tds, this)),
+ d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)),
+ d_ceg_cegis(new Cegis(qs, qim, d_tds, this)),
d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
- d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)),
+ d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)),
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
}
Trace("sygus-engine") << "Check side condition..." << std::endl;
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
- Result r = checkWithSubsolver(sc);
+ Env& env = d_qstate.getEnv();
+ Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo());
Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
if (r == Result::UNSAT)
{
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp()
+ : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv())
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
new SynthConjecture(qs, qim, qr, tr, d_statistics)));
namespace theory {
namespace quantifiers {
-SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds)
+SynthVerify::SynthVerify(const Options& opts,
+ const LogicInfo& logicInfo,
+ TermDbSygus* tds)
+ : d_tds(tds), d_subLogicInfo(logicInfo)
{
// determine the options to use for the verification subsolvers we spawn
// we start with the provided options
}
}
Trace("sygus-engine") << " *** Verify with subcall..." << std::endl;
- Result r = checkWithSubsolver(query, vars, mvs, &d_subOptions);
+ Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo);
Trace("sygus-engine") << " ...got " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
class SynthVerify
{
public:
- SynthVerify(const Options& opts, TermDbSygus* tds);
+ SynthVerify(const Options& opts,
+ const LogicInfo& logicInfo,
+ TermDbSygus* tds);
~SynthVerify();
/**
* Verification call, which takes into account specific aspects of the
TermDbSygus* d_tds;
/** The options for subsolver calls */
Options d_subOptions;
+ /** The logic info for subsolver calls */
+ const LogicInfo& d_subLogicInfo;
};
} // namespace quantifiers
#include "theory/smt_engine_subsolver.h"
+#include "smt/env.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/rewriter.h"
}
void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
- Options* opts,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout,
unsigned long timeout)
{
NodeManager* nm = NodeManager::currentNM();
- SmtEngine* smtCurr = smt::currentSmtEngine();
- if (opts == nullptr)
- {
- // must copy the options
- opts = &smtCurr->getOptions();
- }
- smte.reset(new SmtEngine(nm, opts));
+ smte.reset(new SmtEngine(nm, &opts));
smte->setIsInternalSubsolver();
- smte->setLogic(smtCurr->getLogicInfo());
+ smte->setLogic(logicInfo);
// set the options
if (needsTimeout)
{
smte->setTimeLimit(timeout);
}
}
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ const Env& env,
+ bool needsTimeout,
+ unsigned long timeout)
+{
+ initializeSubsolver(
+ smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout);
+}
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
Node query,
- Options* opts,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout,
unsigned long timeout)
{
{
return r;
}
- initializeSubsolver(smte, opts, needsTimeout, timeout);
+ initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
smte->assertFormula(query);
return smte->checkSat();
}
Result checkWithSubsolver(Node query,
- Options* opts,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout,
unsigned long timeout)
{
std::vector<Node> vars;
std::vector<Node> modelVals;
return checkWithSubsolver(
- query, vars, modelVals, opts, needsTimeout, timeout);
+ query, vars, modelVals, opts, logicInfo, needsTimeout, timeout);
}
Result checkWithSubsolver(Node query,
const std::vector<Node>& vars,
std::vector<Node>& modelVals,
- Options* opts,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout,
unsigned long timeout)
{
return r;
}
std::unique_ptr<SmtEngine> smte;
- initializeSubsolver(smte, opts, needsTimeout, timeout);
+ initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
smte->assertFormula(query);
r = smte->checkSat();
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
* if the current SMT engine has declared a separation logic heap.
*
* @param smte The smt engine pointer to initialize
- * @param opts The options for the subsolver. If nullptr, then we copy the
- * options from the current SmtEngine in scope.
+ * @param opts The options for the subsolver.
+ * @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
- Options* opts = nullptr,
+ const Options& opts,
+ const LogicInfo& logicInfo,
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
+
+/**
+ * Version that uses the options and logicInfo in an environment.
+ */
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ const Env& env,
bool needsTimeout = false,
unsigned long timeout = 0);
*/
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
Node query,
- Options* opts = nullptr,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
*
* @param query The query to check
* @param opts The options for the subsolver
+ * @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
- Options* opts = nullptr,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
* @param vars The variables we are interesting in getting a model for.
* @param modelVals A vector storing the model values of variables in vars.
* @param opts The options for the subsolver
+ * @param logicInfo The logic info to set on the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
const std::vector<Node>& vars,
std::vector<Node>& modelVals,
- Options* opts = nullptr,
+ const Options& opts,
+ const LogicInfo& logicInfo,
bool needsTimeout = false,
unsigned long timeout = 0);
projects / cvc5.git / commitdiff