#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
using namespace std;
bool rewAccel,
bool silent,
bool filterPairs)
- : d_qe(nullptr),
- d_tds(nullptr),
+ : d_tds(nullptr),
d_ext_rewrite(nullptr),
d_doCheck(doCheck),
d_rewAccel(rewAccel),
Assert(ss != nullptr);
d_candidate = Node::null();
d_using_sygus = false;
- d_qe = nullptr;
d_tds = nullptr;
d_ext_rewrite = nullptr;
if (d_filterPairs)
}
void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
SygusSampler* ss)
{
Assert(ss != nullptr);
d_candidate = f;
d_using_sygus = true;
- d_qe = qe;
- d_tds = d_qe->getTermDatabaseSygus();
+ d_tds = tds;
d_ext_rewrite = nullptr;
if (d_filterPairs)
{
* Serves the same purpose as the above function, but we will be using
* sygus to enumerate terms and generate samples.
*
- * qe : pointer to quantifiers engine. We use the sygus term database of this
- * quantifiers engine, and the extended rewriter of the corresponding term
+ * tds : pointer to sygus term database. We use the extended rewriter of this
* database when computing candidate rewrites,
* f : a term of some SyGuS datatype type whose values we will be
* testing under the free variables in the grammar of f. This is the
* "candidate variable" CegConjecture::d_candidates.
*/
void initializeSygus(const std::vector<Node>& vars,
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
SygusSampler* ss);
/** add term
void setExtendedRewriter(ExtendedRewriter* er);
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** (required) pointer to the sygus term database of d_qe */
TermDbSygus* d_tds;
/** an extended rewriter object */
return ret;
}
-CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn, QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn)
{
std::map<TypeNode, CegHandledStatus> visited;
- return isCbqiSort(tn, visited, qe);
+ return isCbqiSort(tn, visited);
}
CegHandledStatus CegInstantiator::isCbqiSort(
- TypeNode tn,
- std::map<TypeNode, CegHandledStatus>& visited,
- QuantifiersEngine* qe)
+ TypeNode tn, std::map<TypeNode, CegHandledStatus>& visited)
{
std::map<TypeNode, CegHandledStatus>::iterator itv = visited.find(tn);
if (itv != visited.end())
}
for (const TypeNode& crange : consType)
{
- CegHandledStatus cret = isCbqiSort(crange, visited, qe);
+ CegHandledStatus cret = isCbqiSort(crange, visited);
if (cret == CEG_UNHANDLED)
{
Trace("cegqi-debug2")
return ret;
}
-CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q,
- QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q)
{
CegHandledStatus hmin = CEG_HANDLED_UNCONDITIONAL;
for (const Node& v : q[0])
{
TypeNode tn = v.getType();
- CegHandledStatus handled = isCbqiSort(tn, qe);
+ CegHandledStatus handled = isCbqiSort(tn);
if (handled == CEG_UNHANDLED)
{
return CEG_UNHANDLED;
return hmin;
}
-CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
+CegHandledStatus CegInstantiator::isCbqiQuant(Node q)
{
Assert(q.getKind() == FORALL);
// compute attributes
}
CegHandledStatus ret = CEG_HANDLED;
// if quantifier has a non-handled variable, then do not use cbqi
- // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
- CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe);
+ CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q);
Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
<< std::endl;
if (ncbqiv == CEG_UNHANDLED)
TypeNode pvtn = pv.getType();
TypeNode pvtnb = pvtn.getBaseType();
Node pvr = pv;
- eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
if (ee->hasTerm(pv))
{
pvr = ee->getRepresentative(pv);
d_curr_type_eqc.clear();
// must use master equality engine to avoid value instantiations
- eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
//for each variable
for( unsigned i=0; i<d_vars.size(); i++ ){
* This method returns whether the type tn is handled by cegqi techniques.
* If the result is CEG_HANDLED_UNCONDITIONAL, then this indicates that a
* variable of this type is handled regardless of the formula it appears in.
- *
- * The argument qe is used if handling sort tn is conditional on the
- * strategies initialized in qe. For example, uninterpreted sorts are
- * handled if dedicated support for EPR is enabled.
*/
- static CegHandledStatus isCbqiSort(TypeNode tn,
- QuantifiersEngine* qe = nullptr);
+ static CegHandledStatus isCbqiSort(TypeNode tn);
/** is cbqi quantifier prefix
*
* This returns the minimum value of the above method for a bound variable
* in the prefix of quantified formula q.
*/
- static CegHandledStatus isCbqiQuantPrefix(Node q,
- QuantifiersEngine* qe = nullptr);
+ static CegHandledStatus isCbqiQuantPrefix(Node q);
/** is cbqi quantified formula
*
* This returns whether quantified formula q can and should be handled by
* quantified formula using cegqi, however other strategies should also be
* tried.
*/
- static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr);
+ static CegHandledStatus isCbqiQuant(Node q);
//------------------------------------ end static queries
private:
/** The quantified formula of this instantiator */
* of the type tn, where visited stores the types we have visited.
*/
static CegHandledStatus isCbqiSort(
- TypeNode tn,
- std::map<TypeNode, CegHandledStatus>& visited,
- QuantifiersEngine* qe);
+ TypeNode tn, std::map<TypeNode, CegHandledStatus>& visited);
//------------------------------------ end static queries
};
{
std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
if( it==d_do_cbqi.end() ){
- CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
+ CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
d_do_cbqi[q] = ret;
return ret != CEG_UNHANDLED;
**/
#include "theory/quantifiers/expr_miner_manager.h"
-#include "theory/quantifiers_engine.h"
#include "options/quantifiers_options.h"
d_doQueryGen(false),
d_doFilterLogicalStrength(false),
d_use_sygus_type(false),
- d_qe(nullptr),
d_tds(nullptr),
d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false)
{
d_doFilterLogicalStrength = false;
d_sygus_fun = Node::null();
d_use_sygus_type = false;
- d_qe = nullptr;
d_tds = nullptr;
// initialize the sampler
d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
}
-void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
+void ExpressionMinerManager::initializeSygus(TermDbSygus* tds,
Node f,
unsigned nsamples,
bool useSygusType)
d_doFilterLogicalStrength = false;
d_sygus_fun = f;
d_use_sygus_type = useSygusType;
- d_qe = qe;
- d_tds = qe->getTermDatabaseSygus();
+ d_tds = tds;
// initialize the sampler
d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
}
// initialize the candidate rewrite database
if (!d_sygus_fun.isNull())
{
- Assert(d_qe != nullptr);
- d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler);
+ Assert(d_tds != nullptr);
+ d_crd.initializeSygus(vars, d_tds, d_sygus_fun, &d_sampler);
}
else
{
* If useSygusType is false, the terms are the builtin equivalent of these
* terms. The argument nsamples is used to initialize the sampler.
*/
- void initializeSygus(QuantifiersEngine* qe,
+ void initializeSygus(TermDbSygus* tds,
Node f,
unsigned nsamples,
bool useSygusType);
Node d_sygus_fun;
/** whether we are using sygus types */
bool d_use_sygus_type;
- /** pointer to the quantifiers engine, used if d_use_sygus is true */
- QuantifiersEngine* d_qe;
- /** the sygus term database of d_qe */
+ /** the sygus term database of the quantifiers engine */
TermDbSygus* d_tds;
/** candidate rewrite database */
CandidateRewriteDatabase d_crd;
#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"
#include "theory/smt_engine_subsolver.h"
namespace theory {
namespace quantifiers {
-CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s)
- : d_qe(qe),
- d_sip(new SingleInvocationPartition),
- d_srcons(new SygusReconstruct(qe->getTermDatabaseSygus(), s)),
+CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s)
+ : d_sip(new SingleInvocationPartition),
+ d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)),
d_isSolved(false),
- d_single_invocation(false)
+ d_single_invocation(false),
+ d_treg(tr)
{
}
ptn = ptn.getRangeType();
}
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
- s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0);
+ s = d_treg.getTermEnumeration()->getEnumerateTerm(ptn, 0);
}
else
{
}
//simplify the solution using the extended rewriter
Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl;
- s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
+ s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
// wrap into lambda, as needed
return SygusUtils::wrapSolutionForSynthFun(prog, s);
{
Trace("csi-sol") << "Post-process solution..." << std::endl;
Node prev = sol;
- sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
+ sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
if (prev != sol)
{
Trace("csi-sol") << "Solution (after post process) : " << sol
std::map< Node, std::vector< Node > >& teq,
Node n, std::vector< Node >& conj );
private:
- /** pointer to the quantifiers engine */
- QuantifiersEngine* d_qe;
// single invocation inference utility
SingleInvocationPartition* d_sip;
/** solution reconstruction */
Node d_single_inv;
public:
- CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s);
+ CegSingleInv(TermRegistry& tr, SygusStatistics& s);
~CegSingleInv();
// get simplified conjecture
* calls to the above method getSolutionFromInst.
*/
void setSolution();
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
/** The conjecture */
Node d_quant;
//-------------- decomposed conjecture
namespace theory {
namespace quantifiers {
-Cegis::Cegis(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+Cegis::Cegis(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p)
- : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false)
+ : SygusModule(qim, tds, p),
+ d_eval_unfold(tds->getEvalUnfold()),
+ d_usingSymCons(false)
{
- d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
}
bool Cegis::initialize(Node conj,
class Cegis : public SygusModule
{
public:
- Cegis(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
- SynthConjecture* p);
+ Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p);
~Cegis() override {}
/** initialize */
virtual bool initialize(Node conj,
return false;
}
-CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qe, qim, p)
+ : Cegis(qim, tds, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
class CegisCoreConnective : public Cegis
{
public:
- CegisCoreConnective(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+ CegisCoreConnective(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p);
~CegisCoreConnective() {}
/**
namespace theory {
namespace quantifiers {
-CegisUnif::CegisUnif(QuantifiersEngine* qe,
- QuantifiersState& qs,
+CegisUnif::CegisUnif(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p)
+ : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
{
}
{
// Init UNIF util for this candidate
d_sygus_unif.initializeCandidate(
- d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas);
+ d_tds, f, d_cand_to_strat_pt[f], strategy_lemmas);
if (!d_sygus_unif.usingUnif(f))
{
Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
}
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
- QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* parent)
: DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
- d_qe(qe),
d_qim(qim),
+ d_tds(tds),
d_parent(parent)
{
d_initialized = false;
- d_tds = d_qe->getTermDatabaseSygus();
options::SygusUnifPiMode mode = options::sygusUnifPi();
d_useCondPool = mode == options::SygusUnifPiMode::CENUM
|| mode == options::SygusUnifPiMode::CENUM_IGAIN;
class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
{
public:
- CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ CegisUnifEnumDecisionStrategy(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* parent);
/** Make the n^th literal of this strategy (G_uq_n).
*
void registerEvalPts(const std::vector<Node>& eis, Node e);
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** sygus term database of d_qe */
class CegisUnif : public Cegis
{
public:
- CegisUnif(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ CegisUnif(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p);
~CegisUnif() override;
/** Retrieves enumerators for constructing solutions
namespace theory {
namespace quantifiers {
-SygusModule::SygusModule(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+SygusModule::SygusModule(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p)
- : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
+ : d_qim(qim), d_tds(tds), d_parent(p)
{
}
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
class SynthConjecture;
class SygusModule
{
public:
- SygusModule(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+ SygusModule(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p);
virtual ~SygusModule() {}
/** initialize
virtual bool usingRepairConst() { return false; }
protected:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** sygus term database of d_qe */
namespace theory {
namespace quantifiers {
-SygusPbe::SygusPbe(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+SygusPbe::SygusPbe(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p)
- : SygusModule(qe, qim, p)
+ : SygusModule(qim, tds, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
<< std::endl;
std::map<Node, std::vector<Node>> strategy_lemmas;
d_sygus_unif[c]->initializeCandidate(
- d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
+ d_tds, c, d_candidate_to_enum[c], strategy_lemmas);
Assert(!d_candidate_to_enum[c].empty());
Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
<< " enumerators for " << c << "..." << std::endl;
class SygusPbe : public SygusModule
{
public:
- SygusPbe(QuantifiersEngine* qe,
- QuantifiersInferenceManager& qim,
+ SygusPbe(QuantifiersInferenceManager& qim,
+ TermDbSygus* tds,
SynthConjecture* p);
~SygusPbe();
}
}
-SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {}
+SynthConjectureProcess::SynthConjectureProcess() {}
SynthConjectureProcess::~SynthConjectureProcess() {}
Node SynthConjectureProcess::preSimplify(Node q)
{
class SynthConjectureProcess
{
public:
- SynthConjectureProcess(QuantifiersEngine* qe);
+ SynthConjectureProcess();
~SynthConjectureProcess();
/** simplify the synthesis conjecture q
* Returns a formula that is equivalent to q.
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers_engine.h"
#include "theory/smt_engine_subsolver.h"
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
-SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe)
- : d_qe(qe), d_allow_constant_grammar(false)
+SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
+ : d_tds(tds), d_allow_constant_grammar(false)
{
- d_tds = d_qe->getTermDatabaseSygus();
}
void SygusRepairConst::initialize(Node base_inst,
if (fo_body.getKind() == FORALL)
{
// must be a CBQI quantifier
- CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe);
+ CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
if (hstatus < CEG_HANDLED)
{
// abort if less than fully handled
class LogicInfo;
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
class TermDbSygus;
class SygusRepairConst
{
public:
- SygusRepairConst(QuantifiersEngine* qe);
+ SygusRepairConst(TermDbSygus* tds);
~SygusRepairConst() {}
/** initialize
*
static bool mustRepair(Node n);
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** pointer to the sygus term database of d_qe */
TermDbSygus* d_tds;
/**
namespace theory {
namespace quantifiers {
-SygusUnif::SygusUnif()
- : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
-{
-}
+SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {}
SygusUnif::~SygusUnif() {}
void SygusUnif::initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas)
{
- d_qe = qe;
- d_tds = qe->getTermDatabaseSygus();
+ d_tds = tds;
d_candidates.push_back(f);
// initialize the strategy
- d_strategy[f].initialize(qe, f, enums);
+ d_strategy[f].initialize(tds, f, enums);
}
Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
class TermDbSygus;
* the respective function-to-synthesize.
*/
virtual void initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas);
std::vector<Node>& lemmas) = 0;
protected:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
- /** sygus term database of d_qe */
- quantifiers::TermDbSygus* d_tds;
+ /** Pointer to the term database sygus */
+ TermDbSygus* d_tds;
//-----------------------debug printing
/** print ind indentations on trace c */
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/strings/word.h"
#include "util/random.h"
SygusUnifIo::~SygusUnifIo() {}
void SygusUnifIo::initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas)
}
}
d_ecache.clear();
- SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
+ SygusUnif::initializeCandidate(tds, f, enums, strategy_lemmas);
// learn redundant operators based on the strategy
d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
}
* multiple functions can be separated.
*/
void initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas) override;
}
SygusUnifRl::~SygusUnifRl() {}
void SygusUnifRl::initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas)
{
// initialize
std::vector<Node> all_enums;
- SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas);
+ SygusUnif::initializeCandidate(tds, f, all_enums, strategy_lemmas);
// based on the strategy inferred for each function, determine if we are
// using a unification strategy that is compatible our approach.
StrategyRestrictions restrictions;
/** initialize */
void initializeCandidate(
- QuantifiersEngine* qe,
+ TermDbSygus* tds,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas) override;
#include "theory/quantifiers/sygus/sygus_unif.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
using namespace std;
return os;
}
-void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
+void SygusUnifStrategy::initialize(TermDbSygus* tds,
Node f,
std::vector<Node>& enums)
{
Assert(d_candidate.isNull());
d_candidate = f;
d_root = f.getType();
- d_qe = qe;
+ d_tds = tds;
// collect the enumerator types and form the strategy
buildStrategyGraph(d_root, role_equal);
Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
<< std::endl;
- eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut);
+ eut = d_tds->getEvalUnfold()->unfold(eut);
Trace("sygus-unif-debug2") << " ...got " << eut;
Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
+class TermDbSygus;
+
/** roles for enumerators
*
* This indicates the role of an enumerator that is allocated by approaches
class SygusUnifStrategy
{
public:
- SygusUnifStrategy() : d_qe(nullptr) {}
+ SygusUnifStrategy() : d_tds(nullptr) {}
/** initialize
*
* This initializes this class with function-to-synthesize f. We also call
* This call constructs a set of enumerators for the relevant subfields of
* the grammar of f and adds them to enums.
*/
- void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums);
+ void initialize(TermDbSygus* tds, Node f, std::vector<Node>& enums);
/** Get the root enumerator for this class */
Node getRootEnumerator() const;
/**
void debugPrint(const char* c);
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
+ /** pointer to the term database sygus */
+ TermDbSygus* d_tds;
/** The candidate variable this strategy is for */
Node d_candidate;
/** maps enumerators to relevant information */
#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
namespace theory {
namespace quantifiers {
-SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
- QuantifiersState& qs,
+SynthConjecture::SynthConjecture(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
SygusStatistics& s)
- : d_qe(qe),
- d_qstate(qs),
+ : d_qstate(qs),
d_qim(qim),
d_qreg(qr),
+ d_treg(tr),
d_stats(s),
- d_tds(qe->getTermDatabaseSygus()),
+ d_tds(tr.getTermDatabaseSygus()),
d_hasSolution(false),
- d_ceg_si(new CegSingleInv(qe, s)),
+ d_ceg_si(new CegSingleInv(tr, s)),
d_templInfer(new SygusTemplateInfer),
- d_ceg_proc(new SynthConjectureProcess(qe)),
+ d_ceg_proc(new SynthConjectureProcess),
d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
- d_sygus_rconst(new SygusRepairConst(qe)),
+ d_sygus_rconst(new SygusRepairConst(d_tds)),
d_exampleInfer(new ExampleInfer(d_tds)),
- d_ceg_pbe(new SygusPbe(qe, qim, this)),
- d_ceg_cegis(new Cegis(qe, qim, this)),
- d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)),
- d_sygus_ccore(new CegisCoreConnective(qe, qim, this)),
+ d_ceg_pbe(new SygusPbe(qim, d_tds, this)),
+ d_ceg_cegis(new Cegis(qim, d_tds, this)),
+ d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
+ d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)),
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
{
Trace("sygus-engine") << " * Value is : ";
std::stringstream sygusEnumOut;
+ FirstOrderModel* m = d_treg.getModel();
for (unsigned i = 0, size = terms.size(); i < size; i++)
{
Node nv = enum_values[i];
- Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
+ Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
TypeNode tn = onv.getType();
std::stringstream ss;
TermDbSygus::toStreamSygus(ss, onv);
Node SynthConjecture::getModelValue(Node n)
{
Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
- return d_qe->getModel()->getValue(n);
+ return d_treg.getModel()->getValue(n);
}
void SynthConjecture::debugPrint(const char* c)
if (its == d_exprm.end())
{
d_exprm[prog].initializeSygus(
- d_qe, d_candidates[i], options::sygusSamples(), true);
+ d_tds, d_candidates[i], options::sygusSamples(), true);
if (options::sygusRewSynth())
{
d_exprm[prog].enableRewriteRuleSynth();
class SynthConjecture
{
public:
- SynthConjecture(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ SynthConjecture(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
SygusStatistics& s);
~SynthConjecture();
/** presolve */
SygusStatistics& getSygusStatistics() { return d_stats; };
private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** The quantifiers registry */
QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
/** term database sygus of d_qe */
**/
#include "theory/quantifiers/sygus/synth_engine.h"
-#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_registry.h"
using namespace CVC4::kind;
using namespace std;
QuantifiersRegistry& qr,
TermRegistry& tr)
: QuantifiersModule(qs, qim, qr, tr, qe),
- d_tds(tr.getTermDatabaseSygus()),
d_conj(nullptr),
d_sqp(qe)
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics)));
+ new SynthConjecture(qs, qim, qr, tr, d_statistics)));
d_conj = d_conjs.back().get();
}
// allocate a new synthesis conjecture if not assigned
if (d_conjs.back()->isAssigned())
{
- d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
- d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics)));
+ d_conjs.push_back(std::unique_ptr<SynthConjecture>(
+ new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
}
d_conjs.back()->assign(q);
}
// If it is a recursive function definition, add it to the function
// definition evaluator class.
Trace("cegqi") << "Registering function definition : " << q << "\n";
- FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+ FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
fde->assertDefinition(q);
return;
}
void preregisterAssertion(Node n);
private:
- /** term database sygus of d_qe */
- TermDbSygus* d_tds;
/** the conjecture formula(s) we are waiting to assign */
std::vector<Node> d_waiting_conj;
/** The synthesis conjectures that this class is managing. */
projects / cvc5.git / commitdiff