This is a step towards breaking up the quantifiers engine.
The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.
This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
}
}
-QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
- : QuantifiersModule(qe) {
- d_sqc = new CDSkQuantCache(qe->getUserContext());
+QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe)
+{
+ d_sqc = new CDSkQuantCache(qs.getUserContext());
}
QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; }
bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
Assert(!quants.empty());
std::sort( quants.begin(), quants.end() );
- if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){
+ if (d_sqc->add(d_qstate.getUserContext(), quants))
+ {
//partition into connected components
if( pconnected && quants.size()>1 ){
Trace("anti-sk-debug") << "Partition into connected components..." << std::endl;
namespace quantifiers {
class QuantAntiSkolem : public QuantifiersModule {
-public:
- QuantAntiSkolem( QuantifiersEngine * qe );
+ public:
+ QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs);
virtual ~QuantAntiSkolem();
bool sendAntiSkolemizeLemma( std::vector< Node >& quants,
return d_parent->rewriteInstantiation(q, terms, inst, doVts);
}
-InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
- : QuantifiersModule(qe),
+InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
+ QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
d_irew(new InstRewriterCegqi(this)),
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
- d_added_cbqi_lemma(qe->getUserContext()),
+ d_added_cbqi_lemma(qs.getUserContext()),
d_vtsCache(new VtsTermCache(qe)),
d_bv_invert(nullptr)
{
}
if (options::cegqiNestedQE())
{
- d_nestedQe.reset(new NestedQe(qe->getUserContext()));
+ d_nestedQe.reset(new NestedQe(qs.getUserContext()));
}
}
d_dstrat[q].reset(
new DecisionStrategySingleton("CexLiteral",
ceLit,
- d_quantEngine->getSatContext(),
+ d_qstate.getSatContext(),
d_quantEngine->getValuation()));
dlds = d_dstrat[q].get();
}
typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
public:
- InstStrategyCegqi(QuantifiersEngine* qe);
+ InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs);
~InstStrategyCegqi();
/** whether to do counterexample-guided instantiation for quantifier q */
}
ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
- context::Context* c)
- : QuantifiersModule(qe),
+ QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
d_notify(*this),
- d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
- d_ee_conjectures(c),
+ d_uequalityEngine(
+ d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
+ d_ee_conjectures(qs.getSatContext()),
d_conj_count(0),
d_subs_confirmCount(0),
d_subs_unkCount(0),
if( eqc_i!=d_eqc_info.end() ){
return eqc_i->second;
}else if( doMake ){
- EqcInfo* ei = new EqcInfo( d_quantEngine->getSatContext() );
+ EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
d_eqc_info[n] = ei;
return ei;
}else{
bool d_hasAddedLemma;
//flush the waiting conjectures
unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
-public:
- ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
+
+ public:
+ ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs);
~ConjectureGenerator();
/* needs check */
namespace theory {
namespace quantifiers {
-InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
- : QuantifiersModule(qe),
+InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
+ QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
d_instStrategies(),
d_isup(),
d_i_ag(),
void doInstantiationRound(Theory::Effort effort);
public:
- InstantiationEngine(QuantifiersEngine* qe);
+ InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs);
~InstantiationEngine();
void presolve() override;
bool needsCheck(Theory::Effort e) override;
namespace quantifiers {
EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
- context::Context* c, QuantifiersEngine* qe)
- : d_qe(qe), d_eqi_counter(c), d_reset_count(0)
+ QuantifiersState& qs, QuantifiersEngine* qe)
+ : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0)
{
}
#include "context/context.h"
#include "expr/node.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_state.h"
namespace CVC4 {
namespace theory {
class EqualityQueryQuantifiersEngine : public EqualityQuery
{
public:
- EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
+ EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
bool reset(Theory::Effort e) override;
namespace quantifiers {
FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
- context::Context* c,
+ QuantifiersState& qs,
std::string name)
- : TheoryModel(c, name, true),
+ : TheoryModel(qs.getSatContext(), name, true),
d_qe(qe),
- d_forall_asserts(c),
+ d_forall_asserts(qs.getSatContext()),
d_forallRlvComputed(false)
{
}
return n.getAttribute(ModelBasisArgAttribute());
}
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(qe, c, name){
-
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ std::string name)
+ : FirstOrderModel(qe, qs, name)
+{
}
FirstOrderModelFmc::~FirstOrderModelFmc()
#include "context/cdlist.h"
#include "expr/attribute.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
class FirstOrderModel : public TheoryModel
{
public:
- FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
+ FirstOrderModel(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ std::string name);
virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
/** assert quantifier */
void processInitializeModelForTerm(Node n) override;
public:
- FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
+ FirstOrderModelFmc(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ std::string name);
~FirstOrderModelFmc() override;
FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
// initialize the model
return lem;
}
-BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe)
- : QuantifiersModule(qe)
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe)
{
}
d_ranges.push_back( r );
d_rms[r].reset(
new IntRangeDecisionHeuristic(r,
- d_quantEngine->getSatContext(),
- d_quantEngine->getUserContext(),
+ d_qstate.getSatContext(),
+ d_qstate.getUserContext(),
d_quantEngine->getValuation(),
isProxy));
d_quantEngine->getTheoryEngine()
}
};
std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-public:
- BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+ BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs);
virtual ~BoundedIntegers();
void presolve() override;
}
}
-
-FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
-QModelBuilder( c, qe ){
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : QModelBuilder(qe)
+{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
void mkCondVec( Node n, std::vector< Node > & cond );
Node evaluateInterpreted( Node n, std::vector< Node > & vals );
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
-public:
- FullModelChecker( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+ FullModelChecker(QuantifiersEngine* qe);
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
+QModelBuilder::QModelBuilder(QuantifiersEngine* qe)
: TheoryEngineModelBuilder(qe->getTheoryEngine()),
d_qe(qe),
d_addedLemmas(0),
- d_triedLemmas(0) {}
+ d_triedLemmas(0)
+{
+}
bool QModelBuilder::optUseModel() {
return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
class QModelBuilder : public TheoryEngineModelBuilder
{
-protected:
+ protected:
//quantifiers engine
QuantifiersEngine* d_qe;
// must call preProcessBuildModelStd
/** number of lemmas generated while building model */
unsigned d_addedLemmas;
unsigned d_triedLemmas;
-public:
- QModelBuilder( context::Context* c, QuantifiersEngine* qe );
+
+ public:
+ QModelBuilder(QuantifiersEngine* qe);
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
using namespace CVC4::theory::inst;
//Model Engine constructor
-ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
-QuantifiersModule( qe ),
-d_incomplete_check(true),
-d_addedLemmas(0),
-d_triedLemmas(0),
-d_totalLemmas(0)
+ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
+ d_incomplete_check(true),
+ d_addedLemmas(0),
+ d_triedLemmas(0),
+ d_totalLemmas(0)
{
}
int d_triedLemmas;
int d_totalLemmas;
public:
- ModelEngine( context::Context* c, QuantifiersEngine* qe );
- virtual ~ModelEngine();
+ ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+ virtual ~ModelEngine();
+
public:
bool needsCheck(Theory::Effort e) override;
QEffort needsModel(Theory::Effort e) override;
namespace quantifiers {
-InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd)
- : QuantifiersModule(qe), d_rd(rd), d_fullSaturateLimit(-1)
+InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ RelevantDomain* rd)
+ : QuantifiersModule(qs, qe), d_rd(rd), d_fullSaturateLimit(-1)
{
}
void InstStrategyEnum::presolve()
class InstStrategyEnum : public QuantifiersModule
{
public:
- InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd);
+ InstStrategyEnum(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ RelevantDomain* rd);
~InstStrategyEnum() {}
/** Presolve */
void presolve() override;
namespace quantifiers {
Instantiate::Instantiate(QuantifiersEngine* qe,
- context::UserContext* u,
+ QuantifiersState& qs,
ProofNodeManager* pnm)
: d_qe(qe),
+ d_qstate(qs),
d_pnm(pnm),
d_term_db(nullptr),
d_term_util(nullptr),
- d_total_inst_debug(u),
- d_c_inst_match_trie_dom(u),
+ d_total_inst_debug(qs.getUserContext()),
+ d_c_inst_match_trie_dom(qs.getUserContext()),
d_pfInst(pnm ? new CDProof(pnm) : nullptr)
{
}
if (it != d_c_inst_match_trie.end())
{
return it->second->existsInstMatch(
- d_qe, q, terms, d_qe->getUserContext(), modEq);
+ d_qe, q, terms, d_qstate.getUserContext(), modEq);
}
}
else
}
else
{
- imt = new inst::CDInstMatchTrie(d_qe->getUserContext());
+ imt = new inst::CDInstMatchTrie(d_qstate.getUserContext());
d_c_inst_match_trie[q] = imt;
}
d_c_inst_match_trie_dom.insert(q);
- return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq);
+ return imt->addInstMatch(d_qe, q, terms, d_qstate.getUserContext(), modEq);
}
Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
public:
Instantiate(QuantifiersEngine* qe,
- context::UserContext* u,
+ QuantifiersState& qs,
ProofNodeManager* pnm = nullptr);
~Instantiate();
/** pointer to the quantifiers engine */
QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
/** pointer to the proof node manager */
ProofNodeManager* d_pnm;
/** cache of term database for quantifiers engine */
return true;
}
-QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
- : QuantifiersModule(qe),
- d_conflict(c, false),
+QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
+ QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
+ d_conflict(qs.getSatContext(), false),
d_true(NodeManager::currentNM()->mkConst<bool>(true)),
d_false(NodeManager::currentNM()->mkConst<bool>(false)),
d_effort(EFFORT_INVALID)
public:
bool areMatchEqual( TNode n1, TNode n2 );
bool areMatchDisequal( TNode n1, TNode n2 );
-public:
- QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
+
+ public:
+ QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs);
/** register quantifier */
void registerQuantifier(Node q) override;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-
-QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
-
+QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe), d_added_split(qs.getUserContext())
+{
}
void QuantDSplit::checkOwnership(Node q)
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- QuantDSplit( QuantifiersEngine * qe, context::Context* c );
+ QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs);
/** determine whether this quantified formula will be reduced */
void checkOwnership(Node q) override;
/* whether this module needs to check this round */
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
using namespace CVC4::kind;
-using namespace CVC4::context;
namespace CVC4 {
namespace theory {
+QuantifiersModule::QuantifiersModule(quantifiers::QuantifiersState& qs,
+ QuantifiersEngine* qe)
+ : d_quantEngine(qe), d_qstate(qs)
+{
+}
+
QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
{
return QEFFORT_NONE;
#include <map>
#include <vector>
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
};
public:
- QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+ QuantifiersModule(quantifiers::QuantifiersState& qs, QuantifiersEngine* qe);
virtual ~QuantifiersModule(){}
/** Presolve.
*
protected:
/** pointer to the quantifiers engine that owns this module */
QuantifiersEngine* d_quantEngine;
+ /** The state of the quantifiers engine */
+ quantifiers::QuantifiersState& d_qstate;
};/* class QuantifiersModule */
/** Quantifiers utility
}
QuantifiersModules::~QuantifiersModules() {}
void QuantifiersModules::initialize(QuantifiersEngine* qe,
- context::Context* c,
+ QuantifiersState& qs,
std::vector<QuantifiersModule*>& modules)
{
// add quantifiers modules
if (options::quantConflictFind())
{
- d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
+ d_qcf.reset(new QuantConflictFind(qe, qs));
modules.push_back(d_qcf.get());
}
if (options::conjectureGen())
{
- d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c));
+ d_sg_gen.reset(new ConjectureGenerator(qe, qs));
modules.push_back(d_sg_gen.get());
}
if (!options::finiteModelFind() || options::fmfInstEngine())
{
- d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
+ d_inst_engine.reset(new InstantiationEngine(qe, qs));
modules.push_back(d_inst_engine.get());
}
if (options::cegqi())
{
- d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
+ d_i_cbqi.reset(new InstStrategyCegqi(qe, qs));
modules.push_back(d_i_cbqi.get());
qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
}
if (options::sygus())
{
- d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
+ d_synth_e.reset(new SynthEngine(qe, qs));
modules.push_back(d_synth_e.get());
}
// finite model finding
if (options::fmfBound())
{
- d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
+ d_bint.reset(new BoundedIntegers(qe, qs));
modules.push_back(d_bint.get());
}
if (options::finiteModelFind() || options::fmfBound())
{
- d_model_engine.reset(new quantifiers::ModelEngine(c, qe));
+ d_model_engine.reset(new ModelEngine(qe, qs));
modules.push_back(d_model_engine.get());
}
if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
{
- d_qsplit.reset(new quantifiers::QuantDSplit(qe, c));
+ d_qsplit.reset(new QuantDSplit(qe, qs));
modules.push_back(d_qsplit.get());
}
if (options::quantAntiSkolem())
{
- d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe));
+ d_anti_skolem.reset(new QuantAntiSkolem(qe, qs));
modules.push_back(d_anti_skolem.get());
}
if (options::quantAlphaEquiv())
{
- d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe));
+ d_alpha_equiv.reset(new AlphaEquivalence(qe));
}
// full saturation : instantiate from relevant domain, then arbitrary terms
if (options::fullSaturateQuant() || options::fullSaturateInterleave())
{
- d_rel_dom.reset(new quantifiers::RelevantDomain(qe));
- d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
+ d_rel_dom.reset(new RelevantDomain(qe));
+ d_fs.reset(new InstStrategyEnum(qe, qs, d_rel_dom.get()));
modules.push_back(d_fs.get());
}
if (options::sygusInst())
{
- d_sygus_inst.reset(new quantifiers::SygusInst(qe));
+ d_sygus_inst.reset(new SygusInst(qe, qs));
modules.push_back(d_sygus_inst.get());
}
}
* a pointer to each module it constructs to modules.
*/
void initialize(QuantifiersEngine* qe,
- context::Context* c,
+ QuantifiersState& qs,
std::vector<QuantifiersModule*>& modules);
+
private:
//------------------------------ quantifier utilities
/** relevant domain */
- std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+ std::unique_ptr<RelevantDomain> d_rel_dom;
//------------------------------ quantifiers modules
/** alpha equivalence */
- std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
+ std::unique_ptr<AlphaEquivalence> d_alpha_equiv;
/** instantiation engine */
- std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
+ std::unique_ptr<InstantiationEngine> d_inst_engine;
/** model engine */
- std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
+ std::unique_ptr<ModelEngine> d_model_engine;
/** bounded integers utility */
- std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
+ std::unique_ptr<BoundedIntegers> d_bint;
/** Conflict find mechanism for quantifiers */
- std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
+ std::unique_ptr<QuantConflictFind> d_qcf;
/** subgoal generator */
- std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+ std::unique_ptr<ConjectureGenerator> d_sg_gen;
/** ceg instantiation */
- std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
+ std::unique_ptr<SynthEngine> d_synth_e;
/** full saturation */
- std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
+ std::unique_ptr<InstStrategyEnum> d_fs;
/** counterexample-based quantifier instantiation */
- std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
+ std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
/** quantifiers splitting */
- std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
+ std::unique_ptr<QuantDSplit> d_qsplit;
/** quantifiers anti-skolemization */
- std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+ std::unique_ptr<QuantAntiSkolem> d_anti_skolem;
/** SyGuS instantiation engine */
- std::unique_ptr<quantifiers::SygusInst> d_sygus_inst;
+ std::unique_ptr<SygusInst> d_sygus_inst;
};
} // namespace quantifiers
namespace quantifiers {
Skolemize::Skolemize(QuantifiersEngine* qe,
- context::UserContext* u,
+ QuantifiersState& qs,
ProofNodeManager* pnm)
: d_quantEngine(qe),
- d_skolemized(u),
+ d_skolemized(qs.getUserContext()),
d_pnm(pnm),
d_epg(pnm == nullptr ? nullptr
- : new EagerProofGenerator(pnm, u, "Skolemize::epg"))
+ : new EagerProofGenerator(
+ pnm, qs.getUserContext(), "Skolemize::epg"))
{
}
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
public:
- Skolemize(QuantifiersEngine* qe,
- context::UserContext* u,
- ProofNodeManager* pnm);
+ Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm);
~Skolemize() {}
/** skolemize quantified formula q
* If the return value ret of this function is non-null, then ret is a trust
namespace theory {
namespace quantifiers {
-CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
- : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
+CegisUnif::CegisUnif(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ SynthConjecture* p)
+ : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
{
}
}
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
- QuantifiersEngine* qe, SynthConjecture* parent)
- : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
+ QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
+ : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
d_qe(qe),
d_parent(parent)
{
class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
{
public:
- CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent);
+ CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ SynthConjecture* parent);
/** Make the n^th literal of this strategy (G_uq_n).
*
* This call may add new lemmas of the form described above
class CegisUnif : public Cegis
{
public:
- CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
+ CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p);
~CegisUnif() override;
/** Retrieves enumerators for constructing solutions
*
namespace quantifiers {
SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
+ QuantifiersState& qs,
SygusStatistics& s)
: d_qe(qe),
+ d_qstate(qs),
d_stats(s),
d_tds(qe->getTermDatabaseSygus()),
d_hasSolution(false),
d_exampleInfer(new ExampleInfer(d_tds)),
d_ceg_pbe(new SygusPbe(qe, this)),
d_ceg_cegis(new Cegis(qe, this)),
- d_ceg_cegisUnif(new CegisUnif(qe, this)),
+ d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
d_sygus_ccore(new CegisCoreConnective(qe, this)),
d_master(nullptr),
d_set_ce_sk_vars(false),
d_feasible_strategy.reset(
new DecisionStrategySingleton("sygus_feasible",
d_feasible_guard,
- d_qe->getSatContext(),
+ d_qstate.getSatContext(),
d_qe->getValuation()));
d_qe->getDecisionManager()->registerStrategy(
DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
class SynthConjecture
{
public:
- SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s);
+ SynthConjecture(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ SygusStatistics& s);
~SynthConjecture();
/** presolve */
void presolve();
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
/** term database sygus of d_qe */
namespace theory {
namespace quantifiers {
-SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
- : QuantifiersModule(qe),
+SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
d_tds(qe->getTermDatabaseSygus()),
d_conj(nullptr),
d_sqp(qe)
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_quantEngine, d_statistics)));
+ new SynthConjecture(d_quantEngine, qs, d_statistics)));
d_conj = d_conjs.back().get();
}
if (d_conjs.back()->isAssigned())
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_quantEngine, d_statistics)));
+ new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
}
d_conjs.back()->assign(q);
}
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
public:
- SynthEngine(QuantifiersEngine* qe, context::Context* c);
+ SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs);
~SynthEngine();
/** presolve
*
return os;
}
-TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
+TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs)
: d_quantEngine(qe),
+ d_qstate(qs),
d_syexp(new SygusExplain(this)),
d_ext_rw(new ExtendedRewriter(true)),
d_eval(new Evaluator),
// TODO :issue #1235 split and document this class
class TermDbSygus {
public:
- TermDbSygus(context::Context* c, QuantifiersEngine* qe);
+ TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs);
~TermDbSygus() {}
/** Reset this utility */
bool reset(Theory::Effort e);
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
//------------------------------utilities
/** sygus explanation */
} // namespace
-SygusInst::SygusInst(QuantifiersEngine* qe)
- : QuantifiersModule(qe),
- d_ce_lemma_added(qe->getUserContext()),
- d_global_terms(qe->getUserContext()),
- d_notified_assertions(qe->getUserContext())
+SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs)
+ : QuantifiersModule(qs, qe),
+ d_ce_lemma_added(qs.getUserContext()),
+ d_global_terms(qs.getUserContext()),
+ d_notified_assertions(qs.getUserContext())
{
}
DecisionStrategy* ds =
new DecisionStrategySingleton("CeLiteral",
lit,
- d_quantEngine->getSatContext(),
+ d_qstate.getSatContext(),
d_quantEngine->getValuation());
d_dstrat[q].reset(ds);
class SygusInst : public QuantifiersModule
{
public:
- SygusInst(QuantifiersEngine* qe);
+ SygusInst(QuantifiersEngine* qe, QuantifiersState& qs);
~SygusInst() = default;
bool needsCheck(Theory::Effort e) override;
namespace theory {
namespace quantifiers {
-TermDb::TermDb(context::Context* c, context::UserContext* u,
- QuantifiersEngine* qe)
- : d_quantEngine(qe),
- d_inactive_map(c) {
+TermDb::TermDb(QuantifiersState& qs, QuantifiersEngine* qe)
+ : d_quantEngine(qe), d_inactive_map(qs.getSatContext())
+{
d_consistent_ee = true;
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
public:
- TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+ TermDb(QuantifiersState& qs, QuantifiersEngine* qe);
~TermDb();
/** presolve (called once per user check-sat) */
void presolve();
const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
- d_qstate(c, u, valuation)
+ d_qstate(c, u, valuation),
+ d_qengine(d_qstate, pnm)
{
out.handleUserAttribute( "fun-def", this );
out.handleUserAttribute("qid", this);
}
// indicate we are using the quantifiers theory state object
d_theoryState = &d_qstate;
+
+ // Set the pointer to the quantifiers engine, which this theory owns. This
+ // pointer will be retreived by TheoryEngine and set to all theories
+ // post-construction.
+ d_quantEngine = &d_qengine;
}
TheoryQuantifiers::~TheoryQuantifiers() {
#include "theory/quantifiers/proof_checker.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers_engine.h"
#include "theory/theory.h"
#include "theory/valuation.h"
QuantifiersProofRuleChecker d_qChecker;
/** The quantifiers state */
QuantifiersState d_qstate;
+ /** The quantifiers engine, which lives here */
+ QuantifiersEngine d_qengine;
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
namespace CVC4 {
namespace theory {
-QuantifiersEngine::QuantifiersEngine(TheoryEngine* te,
- DecisionManager& dm,
+QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate,
ProofNodeManager* pnm)
- : d_te(te),
- d_context(te->getSatContext()),
- d_userContext(te->getUserContext()),
- d_decManager(dm),
+ : d_qstate(qstate),
+ d_te(nullptr),
+ d_decManager(nullptr),
d_masterEqualityEngine(nullptr),
- d_eq_query(
- new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)),
+ d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
d_term_util(new quantifiers::TermUtil(this)),
d_term_canon(new expr::TermCanonize),
- d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)),
+ d_term_db(new quantifiers::TermDb(qstate, this)),
d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes(this)),
- d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)),
- d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)),
+ d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
+ d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
d_term_enum(new quantifiers::TermEnumeration),
- d_conflict_c(d_context, false),
- d_quants_prereg(d_userContext),
- d_quants_red(d_userContext),
- d_lemmas_produced_c(d_userContext),
- d_ierCounter_c(d_context),
- d_presolve(d_userContext, true),
- d_presolve_in(d_userContext),
- d_presolve_cache(d_userContext),
- d_presolve_cache_wq(d_userContext),
- d_presolve_cache_wic(d_userContext)
+ d_conflict_c(qstate.getSatContext(), false),
+ d_quants_prereg(qstate.getUserContext()),
+ d_quants_red(qstate.getUserContext()),
+ d_lemmas_produced_c(qstate.getUserContext()),
+ d_ierCounter_c(qstate.getSatContext()),
+ d_presolve(qstate.getUserContext(), true),
+ d_presolve_in(qstate.getUserContext()),
+ d_presolve_cache(qstate.getUserContext()),
+ d_presolve_cache_wq(qstate.getUserContext()),
+ d_presolve_cache_wic(qstate.getUserContext())
{
//---- utilities
d_util.push_back(d_eq_query.get());
if (options::sygus() || options::sygusInst())
{
// must be constructed here since it is required for datatypes finistInit
- d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this));
+ d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate));
}
d_util.push_back(d_instantiate.get());
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- this, d_context, "FirstOrderModelFmc"));
- d_builder.reset(
- new quantifiers::fmcheck::FullModelChecker(d_context, this));
+ this, qstate, "FirstOrderModelFmc"));
+ d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
d_model.reset(
- new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
- d_builder.reset(new quantifiers::QModelBuilder(d_context, this));
+ new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+ d_builder.reset(new quantifiers::QModelBuilder(this));
}
}else{
d_model.reset(
- new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
+ new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
}
}
QuantifiersEngine::~QuantifiersEngine() {}
-void QuantifiersEngine::finishInit()
+void QuantifiersEngine::finishInit(TheoryEngine* te,
+ DecisionManager* dm,
+ eq::EqualityEngine* mee)
{
- // Initialize the modules and the utilities here. We delay their
- // initialization to here, since this is after TheoryQuantifiers finishInit,
- // which has initialized the state and inference manager of this engine.
+ d_te = te;
+ d_decManager = dm;
+ d_masterEqualityEngine = mee;
+ // Initialize the modules and the utilities here.
d_qmodules.reset(new quantifiers::QuantifiersModules);
- d_qmodules->initialize(this, d_context, d_modules);
+ d_qmodules->initialize(this, d_qstate, d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
}
}
-void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
-{
- d_masterEqualityEngine = mee;
-}
-
TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
DecisionManager* QuantifiersEngine::getDecisionManager()
{
- return &d_decManager;
-}
-
-context::Context* QuantifiersEngine::getSatContext() { return d_context; }
-
-context::UserContext* QuantifiersEngine::getUserContext()
-{
- return d_userContext;
+ return d_decManager;
}
OutputChannel& QuantifiersEngine::getOutputChannel()
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_database.h"
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
+ QuantifiersEngine(quantifiers::QuantifiersState& qstate,
ProofNodeManager* pnm);
~QuantifiersEngine();
- /** finish initialize */
- void finishInit();
//---------------------- external interface
/** get theory engine */
TheoryEngine* getTheoryEngine() const;
/** Get the decision manager */
DecisionManager* getDecisionManager();
- /** get default sat context for quantifiers engine */
- context::Context* getSatContext();
- /** get default sat context for quantifiers engine */
- context::UserContext* getUserContext();
/** get default output channel for the quantifiers engine */
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
//---------------------- end utilities
private:
//---------------------- private initialization
- /** Set the master equality engine */
- void setMasterEqualityEngine(eq::EqualityEngine* mee);
+ /**
+ * Finish initialize, which passes pointers to the objects that quantifiers
+ * engine needs but were not available when it was created. This is
+ * called after theories have been created but before they have finished
+ * initialization.
+ *
+ * @param te The theory engine
+ * @param dm The decision manager of the theory engine
+ * @param mee The master equality engine of the theory engine
+ */
+ void finishInit(TheoryEngine* te,
+ DecisionManager* dm,
+ eq::EqualityEngine* mee);
//---------------------- end private initialization
/**
* Maps quantified formulas to the module that owns them, if any module has
Statistics d_statistics;
private:
+ /** The quantifiers state object */
+ quantifiers::QuantifiersState& d_qstate;
/** Pointer to theory engine object */
TheoryEngine* d_te;
- /** The SAT context */
- context::Context* d_context;
- /** The user context */
- context::UserContext* d_userContext;
/** Reference to the decision manager of the theory engine */
- DecisionManager& d_decManager;
+ DecisionManager* d_decManager;
/** Pointer to the master equality engine */
eq::EqualityEngine* d_masterEqualityEngine;
/** vector of utilities for quantifiers */
d_facts(satContext),
d_factsHead(satContext, 0),
d_sharedTermsIndex(satContext, 0),
- d_careGraph(NULL),
- d_quantEngine(NULL),
+ d_careGraph(nullptr),
d_decManager(nullptr),
d_instanceName(name),
d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
d_allocEqualityEngine(nullptr),
d_theoryState(nullptr),
d_inferManager(nullptr),
+ d_quantEngine(nullptr),
d_pnm(pnm)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
{
- Assert(d_quantEngine == nullptr);
// quantifiers engine may be null if not in quantified logic
d_quantEngine = qe;
}
/** The care graph the theory will use during combination. */
CareGraph* d_careGraph;
- /**
- * Pointer to the quantifiers engine (or NULL, if quantifiers are not
- * supported or not enabled). Not owned by the theory.
- */
- QuantifiersEngine* d_quantEngine;
-
/** Pointer to the decision manager. */
DecisionManager* d_decManager;
*/
TheoryInferenceManager* d_inferManager;
+ /**
+ * Pointer to the quantifiers engine (or NULL, if quantifiers are not
+ * supported or not enabled). Not owned by the theory.
+ */
+ QuantifiersEngine* d_quantEngine;
+
/** Pointer to proof node manager */
ProofNodeManager* d_pnm;
// initialize the quantifiers engine
if (d_logicInfo.isQuantified())
{
- // initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
+ // get the quantifiers engine, which is initialized by the quantifiers
+ // theory
+ d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
+ Assert(d_quantEngine != nullptr);
}
// initialize the theory combination manager, which decides and allocates the
// equality engines to use for all theories.
// get pointer to the shared solver
d_sharedSolver = d_tc->getSharedSolver();
- // set the core equality engine on quantifiers engine
+ // finish initializing the quantifiers engine
if (d_logicInfo.isQuantified())
{
- d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
+ d_quantEngine->finishInit(
+ this, d_decManager.get(), d_tc->getCoreEqualityEngine());
}
// finish initializing the theories by linking them with the appropriate
// finish initializing the theory
t->finishInit();
}
-
- // finish initializing the quantifiers engine
- if (d_logicInfo.isQuantified())
- {
- d_quantEngine->finishInit();
- }
}
ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
}
}
- delete d_quantEngine;
-
smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
std::unique_ptr<theory::CombinationEngine> d_tc;
/** The shared solver of the above combination engine. */
theory::SharedSolver* d_sharedSolver;
- /**
- * The quantifiers engine
- */
+ /** The quantifiers engine, which is owned by the quantifiers theory */
theory::QuantifiersEngine* d_quantEngine;
/**
* The decision manager
projects / cvc5.git / commitdiff