TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
TheoryArrays* ta)
- : d_ta(ta)
+ : DecisionStrategy(ta->d_env), d_ta(ta)
{
}
void TheoryArrays::TheoryArraysDecisionStrategy::initialize() {}
#ifndef CVC5__THEORY__BV__BV_SOLVER_H
#define CVC5__THEORY__BV__BV_SOLVER_H
-#include "smt/env.h"
#include "smt/env_obj.h"
#include "theory/theory.h"
d_bitblaster(new NodeBitblaster(env, s)),
d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
d_nullContext(new context::Context()),
- d_bbFacts(s->getSatContext()),
- d_bbInputFacts(s->getSatContext()),
- d_assumptions(s->getSatContext()),
- d_assertions(s->getSatContext()),
- d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+ d_bbFacts(context()),
+ d_bbInputFacts(context()),
+ d_assumptions(context()),
+ d_assertions(context()),
+ d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "")
: nullptr),
- d_factLiteralCache(s->getSatContext()),
- d_literalFactCache(s->getSatContext()),
+ d_factLiteralCache(context()),
+ d_literalFactCache(context()),
d_propagate(options().bv.bitvectorPropagate),
- d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
+ d_resetNotify(new NotifyResetAssertions(userContext()))
{
if (pnm != nullptr)
{
#include "proof/eager_proof_generator.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
+#include "smt/env_obj.h"
#include "theory/bv/bitblast/node_bitblaster.h"
#include "theory/bv/bv_solver.h"
#include "theory/bv/proof_checker.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
+#include "smt/env_obj.h"
#include "theory/bv/bitblast/proof_bitblaster.h"
#include "theory/bv/bv_solver.h"
#include "theory/bv/proof_checker.h"
namespace theory {
namespace bv {
-BVSolverLayered::BVSolverLayered(TheoryBV& bv,
- Env& env,
+BVSolverLayered::BVSolverLayered(Env& env,
+ TheoryBV& bv,
context::Context* c,
context::UserContext* u,
ProofNodeManager* pnm,
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
+#include "smt/env_obj.h"
#include "theory/bv/bv_solver.h"
#include "theory/bv/bv_subtheory.h"
#include "theory/bv/theory_bv.h"
d_subtheoryMap;
public:
- BVSolverLayered(TheoryBV& bv,
- Env& env,
+ BVSolverLayered(Env& env,
+ TheoryBV& bv,
context::Context* c,
context::UserContext* u,
ProofNodeManager* pnm = nullptr,
switch (options().bv.bvSolver)
{
case options::BVSolver::BITBLAST:
- d_internal.reset(new BVSolverBitblast(d_env, &d_state, d_im, d_pnm));
+ d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm));
break;
case options::BVSolver::LAYERED:
d_internal.reset(new BVSolverLayered(
- *this, d_env, context(), userContext(), d_pnm, name));
+ env, *this, context(), userContext(), d_pnm, name));
break;
default:
- AlwaysAssert(options().bv.bvSolver
- == options::BVSolver::BITBLAST_INTERNAL);
+ AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
d_internal.reset(
new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
}
d_im(im),
d_tds(tds),
d_ssb(tds),
- d_testers(s.getSatContext()),
- d_testers_exp(s.getSatContext()),
- d_active_terms(s.getSatContext()),
- d_currTermSize(s.getSatContext())
+ d_testers(context()),
+ d_testers_exp(context()),
+ d_active_terms(context()),
+ d_currTermSize(context())
{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_true = NodeManager::currentNM()->mkConst(true);
d_anchor_to_ag_strategy.find(e);
if (itaas == d_anchor_to_ag_strategy.end())
{
- d_anchor_to_ag_strategy[e].reset(
- new DecisionStrategySingleton("sygus_enum_active",
- ag,
- d_state.getSatContext(),
- d_state.getValuation()));
+ d_anchor_to_ag_strategy[e].reset(new DecisionStrategySingleton(
+ d_env, "sygus_enum_active", ag, d_state.getValuation()));
}
d_im.getDecisionManager()->registerStrategy(
DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
d_szinfo.find(m);
if( it==d_szinfo.end() ){
Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
- d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_im, m, d_state));
+ d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_env, d_im, m, d_state));
// register this as a decision strategy
d_im.getDecisionManager()->registerStrategy(
DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get());
}
SygusExtension::SygusSizeDecisionStrategy::SygusSizeDecisionStrategy(
- InferenceManager& im, Node t, TheoryState& s)
- : DecisionStrategyFmf(s.getSatContext(), s.getValuation()),
+ Env& env, InferenceManager& im, Node t, TheoryState& s)
+ : DecisionStrategyFmf(env, s.getValuation()),
d_this(t),
d_curr_search_size(0),
d_im(im)
class SygusSizeDecisionStrategy : public DecisionStrategyFmf
{
public:
- SygusSizeDecisionStrategy(InferenceManager& im, Node t, TheoryState& s);
+ SygusSizeDecisionStrategy(Env& env,
+ InferenceManager& im,
+ Node t,
+ TheoryState& s);
/** the measure term */
Node d_this;
/**
namespace cvc5 {
namespace theory {
-DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext,
- Valuation valuation)
- : d_valuation(valuation),
- d_has_curr_literal(false, satContext),
- d_curr_literal(0, satContext)
+DecisionStrategyFmf::DecisionStrategyFmf(Env& env, Valuation valuation)
+ : DecisionStrategy(env),
+ d_valuation(valuation),
+ d_has_curr_literal(false, context()),
+ d_curr_literal(0, context())
{
}
return ret;
}
-DecisionStrategySingleton::DecisionStrategySingleton(
- const char* name,
- Node lit,
- context::Context* satContext,
- Valuation valuation)
- : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit)
+DecisionStrategySingleton::DecisionStrategySingleton(Env& env,
+ const char* name,
+ Node lit,
+ Valuation valuation)
+ : DecisionStrategyFmf(env, valuation), d_name(name), d_literal(lit)
{
}
#include "context/cdo.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/valuation.h"
namespace cvc5 {
/**
* Virtual base class for decision strategies.
*/
-class DecisionStrategy
+class DecisionStrategy : protected EnvObj
{
public:
- DecisionStrategy() {}
+ DecisionStrategy(Env& env) : EnvObj(env) {}
virtual ~DecisionStrategy() {}
/**
* Initalize this strategy, This is called once per satisfiability call by
class DecisionStrategyFmf : public DecisionStrategy
{
public:
- DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
+ DecisionStrategyFmf(Env& env, Valuation valuation);
virtual ~DecisionStrategyFmf() {}
/** initialize */
void initialize() override;
class DecisionStrategySingleton : public DecisionStrategyFmf
{
public:
- DecisionStrategySingleton(const char* name,
+ DecisionStrategySingleton(Env& env,
+ const char* name,
Node lit,
- context::Context* satContext,
Valuation valuation);
/**
* Make the n^th literal of this strategy. This method returns d_literal if
d_irew(new InstRewriterCegqi(this)),
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
- d_added_cbqi_lemma(qs.getUserContext()),
+ d_added_cbqi_lemma(userContext()),
d_vtsCache(new VtsTermCache(qim)),
d_bv_invert(nullptr),
d_small_const_multiplier(
DecisionStrategy* dlds = nullptr;
if (itds == d_dstrat.end())
{
- d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
- ceLit,
- d_qstate.getSatContext(),
- d_qstate.getValuation()));
+ d_dstrat[q].reset(new DecisionStrategySingleton(
+ d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
dlds = d_dstrat[q].get();
}
else
if( eqc_i!=d_eqc_info.end() ){
return eqc_i->second;
}else if( doMake ){
- EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
+ EqcInfo* ei = new EqcInfo(context());
d_eqc_info[n] = ei;
return ei;
}else{
: QuantifiersUtil(env),
d_qstate(qs),
d_model(m),
- d_eqi_counter(qs.getSatContext()),
+ d_eqi_counter(context()),
d_reset_count(0)
{
}
QuantifiersState& qs,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : d_model(nullptr),
+ : EnvObj(env),
+ d_model(nullptr),
d_qreg(qr),
d_treg(tr),
d_eq_query(env, qs, this),
- d_forall_asserts(qs.getSatContext()),
+ d_forall_asserts(context()),
d_forallRlvComputed(false)
{
}
#define CVC5__FIRST_ORDER_MODEL_H
#include "context/cdlist.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
class QuantifiersRegistry;
// TODO (#1301) : document and refactor this class
-class FirstOrderModel
+class FirstOrderModel : protected EnvObj
{
public:
FirstOrderModel(Env& env,
using namespace cvc5::kind;
BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
- Node r,
- context::Context* c,
- context::Context* u,
- Valuation valuation,
- bool isProxy)
- : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
+ Env& env, Node r, Valuation valuation, bool isProxy)
+ : DecisionStrategyFmf(env, valuation),
+ d_range(r),
+ d_ranges_proxied(userContext())
{
if( options::fmfBoundLazy() ){
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
{
Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
d_ranges.push_back( r );
- d_rms[r].reset(
- new IntRangeDecisionHeuristic(r,
- d_qstate.getSatContext(),
- d_qstate.getUserContext(),
- d_qstate.getValuation(),
- isProxy));
+ d_rms[r].reset(new IntRangeDecisionHeuristic(
+ d_env, r, d_qstate.getValuation(), isProxy));
dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
d_rms[r].get());
}
class IntRangeDecisionHeuristic : public DecisionStrategyFmf
{
public:
- IntRangeDecisionHeuristic(Node r,
- context::Context* c,
- context::Context* u,
+ IntRangeDecisionHeuristic(Env& env,
+ Node r,
Valuation valuation,
bool isProxy);
/** make the n^th literal of this strategy */
d_data.clear();
}
-bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::existsInstMatch(context::Context* context,
+ quantifiers::QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq,
unsigned index)
{
- return !addInstMatch(qs, q, m, modEq, index, true);
+ return !addInstMatch(context, qs, q, m, modEq, index, true);
}
-bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::addInstMatch(context::Context* context,
+ quantifiers::QuantifiersState& qs,
Node f,
const std::vector<Node>& m,
bool modEq,
std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
if (it != d_data.end())
{
- bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
+ bool ret =
+ it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
if (!onlyExist || !ret)
{
return reset || ret;
std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
if (itc != d_data.end())
{
- if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
+ if (itc->second->addInstMatch(
+ context, qs, f, m, modEq, index + 1, true))
{
return false;
}
if (!onlyExist)
{
- CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
+ CDInstMatchTrie* imt = new CDInstMatchTrie(context);
Assert(d_data.find(n) == d_data.end());
d_data[n] = imt;
- imt->addInstMatch(qs, f, m, modEq, index + 1, false);
+ imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
}
return true;
}
#include "context/cdlist.h"
#include "context/cdo.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
- bool existsInstMatch(QuantifiersState& qs,
+ bool existsInstMatch(context::Context* context,
+ QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
- bool addInstMatch(QuantifiersState& qs,
+ bool addInstMatch(context::Context* context,
+ QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
d_qreg(qr),
d_treg(tr),
d_pnm(pnm),
- d_insts(qs.getUserContext()),
- d_c_inst_match_trie_dom(qs.getUserContext()),
- d_pfInst(
- pnm ? new CDProof(pnm, qs.getUserContext(), "Instantiate::pfInst")
- : nullptr)
+ d_insts(userContext()),
+ d_c_inst_match_trie_dom(userContext()),
+ d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst")
+ : nullptr)
{
}
std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
- return it->second->existsInstMatch(d_qstate, q, terms, modEq);
+ return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq);
}
}
else
const auto res = d_c_inst_match_trie.insert({q, nullptr});
if (res.second)
{
- res.first->second = new CDInstMatchTrie(d_qstate.getUserContext());
+ res.first->second = new CDInstMatchTrie(userContext());
}
d_c_inst_match_trie_dom.insert(q);
- return res.first->second->addInstMatch(d_qstate, q, terms);
+ return res.first->second->addInstMatch(userContext(), d_qstate, q, terms);
}
Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
return it->second.get();
}
std::shared_ptr<InstLemmaList> ill =
- std::make_shared<InstLemmaList>(d_qstate.getUserContext());
+ std::make_shared<InstLemmaList>(userContext());
d_insts.insert(q, ill);
return ill.get();
}
QuantifiersRegistry& qr,
TermRegistry& tr)
: QuantifiersModule(env, qs, qim, qr, tr),
- d_conflict(qs.getSatContext(), false),
+ d_conflict(context(), false),
d_true(NodeManager::currentNM()->mkConst<bool>(true)),
d_false(NodeManager::currentNM()->mkConst<bool>(false)),
d_effort(EFFORT_INVALID)
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : QuantifiersModule(env, qs, qim, qr, tr),
- d_added_split(qs.getUserContext())
+ : QuantifiersModule(env, qs, qim, qr, tr), d_added_split(userContext())
{
}
ProofNodeManager* pnm)
: InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
- d_skolemize(new Skolemize(state, tr, pnm))
+ d_skolemize(new Skolemize(env, state, tr, pnm))
{
}
namespace theory {
namespace quantifiers {
-Skolemize::Skolemize(QuantifiersState& qs,
+Skolemize::Skolemize(Env& env,
+ QuantifiersState& qs,
TermRegistry& tr,
ProofNodeManager* pnm)
- : d_qstate(qs),
+ : EnvObj(env),
+ d_qstate(qs),
d_treg(tr),
- d_skolemized(qs.getUserContext()),
+ d_skolemized(userContext()),
d_pnm(pnm),
- d_epg(pnm == nullptr ? nullptr
- : new EagerProofGenerator(
- pnm, qs.getUserContext(), "Skolemize::epg"))
+ d_epg(pnm == nullptr
+ ? nullptr
+ : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
{
}
#include "expr/type_node.h"
#include "proof/eager_proof_generator.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
* default and can be enabled by option:
* --quant-ind
*/
-class Skolemize
+class Skolemize : protected EnvObj
{
typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
- Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm);
+ Skolemize(Env& env,
+ QuantifiersState& qs,
+ TermRegistry& tr,
+ ProofNodeManager* pnm);
~Skolemize() {}
/** skolemize quantified formula q
* If the return value ret of this function is non-null, then ret is a trust
QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* parent)
- : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
+ : DecisionStrategyFmf(env, qs.getValuation()),
d_qim(qim),
d_tds(tds),
d_parent(parent)
}
// register the strategy
- d_feasible_strategy.reset(
- new DecisionStrategySingleton("sygus_feasible",
- d_feasible_guard,
- d_qstate.getSatContext(),
- d_qstate.getValuation()));
+ d_feasible_strategy.reset(new DecisionStrategySingleton(
+ d_env, "sygus_feasible", d_feasible_guard, d_qstate.getValuation()));
d_qim.getDecisionManager()->registerStrategy(
DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
// this must be called, both to ensure that the feasible guard is
*/
Assert(d_dstrat.find(q) == d_dstrat.end());
DecisionStrategy* ds = new DecisionStrategySingleton(
- "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
+ d_env, "CeLiteral", lit, d_qstate.getValuation());
d_dstrat[q].reset(ds);
d_qim.getDecisionManager()->registerStrategy(
d_qim(nullptr),
d_qreg(qr),
d_termsContext(),
- d_termsContextUse(options::termDbCd() ? qs.getSatContext()
- : &d_termsContext),
+ d_termsContextUse(options::termDbCd() ? context() : &d_termsContext),
d_processed(d_termsContextUse),
d_typeMap(d_termsContextUse),
d_ops(d_termsContextUse),
d_opMap(d_termsContextUse),
- d_inactive_map(qs.getSatContext())
+ d_inactive_map(context())
{
d_consistent_ee = true;
d_true = NodeManager::currentNM()->mkConst(true);
QuantifiersState& qs,
QuantifiersRegistry& qr)
: EnvObj(env),
- d_presolve(qs.getUserContext(), true),
- d_presolveCache(qs.getUserContext()),
+ d_presolve(userContext(), true),
+ d_presolveCache(userContext()),
d_termEnum(new TermEnumeration),
d_termPools(new TermPools(env, qs)),
d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
d_qreg(qr),
d_treg(tr),
d_model(nullptr),
- d_quants_prereg(qs.getUserContext()),
- d_quants_red(qs.getUserContext()),
+ d_quants_prereg(userContext()),
+ d_quants_red(userContext()),
d_numInstRoundsLemma(0)
{
Trace("quant-init-debug")
<< std::endl;
Node g = sm->mkDummySkolem("G", nm->booleanType());
d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
- "sep_neg_guard", g, context(), getValuation()));
+ d_env, "sep_neg_guard", g, getValuation()));
DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
d_im.getDecisionManager()->registerStrategy(
DecisionManager::STRAT_SEP_NEG_GUARD, ds);
namespace theory {
namespace sets {
-CardinalityExtension::CardinalityExtension(SolverState& s,
+CardinalityExtension::CardinalityExtension(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& treg)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_treg(treg),
- d_card_processed(s.getUserContext()),
+ d_card_processed(userContext()),
d_finite_type_constants_processed(false)
{
d_true = NodeManager::currentNM()->mkConst(true);
#include "context/cdhashset.h"
#include "context/context.h"
+#include "smt/env_obj.h"
#include "theory/sets/inference_manager.h"
#include "theory/sets/solver_state.h"
#include "theory/sets/term_registry.h"
* normal forms, where the normal form for Set terms is a set of (equivalence
* class representatives of) Venn regions that do not contain the empty set.
*/
-class CardinalityExtension
+class CardinalityExtension : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
* Constructs a new instance of the cardinality solver w.r.t. the provided
* contexts.
*/
- CardinalityExtension(SolverState& s,
+ CardinalityExtension(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& treg);
namespace theory {
namespace sets {
-TermRegistry::TermRegistry(SolverState& state,
+TermRegistry::TermRegistry(Env& env,
+ SolverState& state,
InferenceManager& im,
SkolemCache& skc,
ProofNodeManager* pnm)
- : d_im(im),
+ : EnvObj(env),
+ d_im(im),
d_skCache(skc),
- d_proxy(state.getUserContext()),
- d_proxy_to_term(state.getUserContext()),
+ d_proxy(userContext()),
+ d_proxy_to_term(userContext()),
d_epg(
pnm ? new EagerProofGenerator(pnm, nullptr, "sets::TermRegistry::epg")
: nullptr)
#include "context/cdhashmap.h"
#include "proof/eager_proof_generator.h"
+#include "smt/env_obj.h"
#include "theory/sets/inference_manager.h"
#include "theory/sets/skolem_cache.h"
#include "theory/sets/solver_state.h"
* Term registry, the purpose of this class is to maintain a database of
* commonly used terms, and mappings from sets to their "proxy variables".
*/
-class TermRegistry
+class TermRegistry : protected EnvObj
{
typedef context::CDHashMap<Node, Node> NodeMap;
public:
- TermRegistry(SolverState& state,
+ TermRegistry(Env& env,
+ SolverState& state,
InferenceManager& im,
SkolemCache& skc,
ProofNodeManager* pnm);
d_state(state),
d_im(im),
d_skCache(skc),
- d_treg(state, im, skc, pnm),
- d_rels(new TheorySetsRels(state, im, skc, d_treg)),
- d_cardSolver(new CardinalityExtension(state, im, d_treg)),
+ d_treg(d_env, state, im, skc, pnm),
+ d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)),
+ d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)),
d_rels_enabled(false),
d_card_enabled(false)
{
typedef std::map<Node, std::map<Node, std::unordered_set<Node> > >::iterator
TC_IT;
-TheorySetsRels::TheorySetsRels(SolverState& s,
+TheorySetsRels::TheorySetsRels(Env& env,
+ SolverState& s,
InferenceManager& im,
SkolemCache& skc,
TermRegistry& treg)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_skCache(skc),
d_treg(treg),
- d_shared_terms(s.getUserContext())
+ d_shared_terms(userContext())
{
d_trueNode = NodeManager::currentNM()->mkConst(true);
d_falseNode = NodeManager::currentNM()->mkConst(false);
#include "context/cdhashset.h"
#include "context/cdlist.h"
+#include "smt/env_obj.h"
#include "theory/sets/inference_manager.h"
#include "theory/sets/rels_utils.h"
#include "theory/sets/solver_state.h"
* extension of the theory of sets. That is, it shares many components of the
* TheorySets object which owns it.
*/
-class TheorySetsRels {
+class TheorySetsRels : protected EnvObj
+{
typedef context::CDList<Node> NodeList;
typedef context::CDHashSet<Node> NodeSet;
typedef context::CDHashMap<Node, Node> NodeMap;
public:
- TheorySetsRels(SolverState& s,
+ TheorySetsRels(Env& env,
+ SolverState& s,
InferenceManager& im,
SkolemCache& skc,
TermRegistry& treg);
namespace theory {
namespace strings {
-BaseSolver::BaseSolver(SolverState& s, InferenceManager& im)
- : d_state(s), d_im(im), d_congruent(s.getSatContext())
+BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im)
+ : EnvObj(env), d_state(s), d_im(im), d_congruent(context())
{
d_false = NodeManager::currentNM()->mkConst(false);
d_cardSize = utils::getAlphabetCardinality();
#include "context/cdhashset.h"
#include "context/cdlist.h"
+#include "smt/env_obj.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/normal_form.h"
* current context, and techniques for inferring when equivalence classes
* are equivalent to constants.
*/
-class BaseSolver
+class BaseSolver : protected EnvObj
{
using NodeSet = context::CDHashSet<Node>;
public:
- BaseSolver(SolverState& s, InferenceManager& im);
+ BaseSolver(Env& env, SolverState& s, InferenceManager& im);
~BaseSolver();
//-----------------------inference steps
CoreInferInfo::CoreInferInfo(InferenceId id) : d_infer(id), d_index(0), d_rev(false) {}
-CoreSolver::CoreSolver(SolverState& s,
+CoreSolver::CoreSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& tr,
BaseSolver& bs)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_termReg(tr),
d_bsolver(bs),
- d_nfPairs(s.getSatContext())
+ d_nfPairs(context())
{
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
#include "context/cdhashset.h"
#include "context/cdlist.h"
+#include "smt/env_obj.h"
#include "theory/strings/base_solver.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/inference_manager.h"
* This implements techniques for handling (dis)equalities involving
* string concatenation terms based on the procedure by Liang et al CAV 2014.
*/
-class CoreSolver
+class CoreSolver : protected EnvObj
{
friend class InferenceManager;
using NodeIntMap = context::CDHashMap<Node, int>;
public:
- CoreSolver(SolverState& s,
+ CoreSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& tr,
BaseSolver& bs);
namespace theory {
namespace strings {
-ExtfSolver::ExtfSolver(SolverState& s,
+ExtfSolver::ExtfSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& tr,
StringsRewriter& rewriter,
CoreSolver& cs,
ExtTheory& et,
SequencesStatistics& statistics)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_termReg(tr),
d_rewriter(rewriter),
d_extt(et),
d_statistics(statistics),
d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
- d_hasExtf(s.getSatContext(), false),
- d_extfInferCache(s.getSatContext()),
- d_reduced(s.getUserContext())
+ d_hasExtf(context(), false),
+ d_extfInferCache(context()),
+ d_reduced(userContext())
{
d_extt.addFunctionKind(kind::STRING_SUBSTR);
d_extt.addFunctionKind(kind::STRING_UPDATE);
#include "context/cdo.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/ext_theory.h"
#include "theory/strings/base_solver.h"
#include "theory/strings/core_solver.h"
* functions for the theory of strings using a combination of context-dependent
* simplification (Reynolds et al CAV 2017) and lazy reductions.
*/
-class ExtfSolver
+class ExtfSolver : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
public:
- ExtfSolver(SolverState& s,
+ ExtfSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
TermRegistry& tr,
StringsRewriter& rewriter,
namespace theory {
namespace strings {
-RegExpSolver::RegExpSolver(SolverState& s,
+RegExpSolver::RegExpSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
SkolemCache* skc,
CoreSolver& cs,
ExtfSolver& es,
SequencesStatistics& stats)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_csolver(cs),
d_esolver(es),
d_statistics(stats),
- d_regexp_ucached(s.getUserContext()),
- d_regexp_ccached(s.getSatContext()),
- d_processed_memberships(s.getSatContext()),
+ d_regexp_ucached(userContext()),
+ d_regexp_ccached(context()),
+ d_processed_memberships(context()),
d_regexp_opr(skc)
{
d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
#define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
#include <map>
+
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/strings/extf_solver.h"
#include "theory/strings/inference_manager.h"
-#include "theory/strings/skolem_cache.h"
#include "theory/strings/regexp_operation.h"
#include "theory/strings/sequences_stats.h"
+#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
#include "util/string.h"
namespace theory {
namespace strings {
-class RegExpSolver
+class RegExpSolver : protected EnvObj
{
typedef context::CDList<Node> NodeList;
typedef context::CDHashMap<Node, bool> NodeBoolMap;
typedef context::CDHashSet<Node> NodeSet;
public:
- RegExpSolver(SolverState& s,
+ RegExpSolver(Env& env,
+ SolverState& s,
InferenceManager& im,
SkolemCache* skc,
CoreSolver& cs,
namespace theory {
namespace strings {
-StringsFmf::StringsFmf(context::Context* c,
- context::UserContext* u,
- Valuation valuation,
- TermRegistry& tr)
- : d_sslds(nullptr),
- d_satContext(c),
- d_userContext(u),
- d_valuation(valuation),
- d_termReg(tr)
+StringsFmf::StringsFmf(Env& env, Valuation valuation, TermRegistry& tr)
+ : EnvObj(env), d_sslds(nullptr), d_valuation(valuation), d_termReg(tr)
{
}
void StringsFmf::presolve()
{
- d_sslds.reset(new StringSumLengthDecisionStrategy(
- d_satContext, d_userContext, d_valuation));
+ d_sslds.reset(new StringSumLengthDecisionStrategy(d_env, d_valuation));
Trace("strings-dstrat-reg")
<< "presolve: register decision strategy." << std::endl;
const NodeSet& ivars = d_termReg.getInputVars();
}
StringsFmf::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
- context::Context* c, context::UserContext* u, Valuation valuation)
- : DecisionStrategyFmf(c, valuation), d_inputVarLsum(u)
+ Env& env, Valuation valuation)
+ : DecisionStrategyFmf(env, valuation), d_inputVarLsum(userContext())
{
}
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/decision_strategy.h"
#include "theory/strings/term_registry.h"
#include "theory/valuation.h"
* This class manages the creation of a decision strategy that bounds the
* sum of lengths of terms of type string.
*/
-class StringsFmf
+class StringsFmf : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
public:
- StringsFmf(context::Context* c,
- context::UserContext* u,
- Valuation valuation,
- TermRegistry& tr);
+ StringsFmf(Env& env, Valuation valuation, TermRegistry& tr);
~StringsFmf();
/** presolve
*
class StringSumLengthDecisionStrategy : public DecisionStrategyFmf
{
public:
- StringSumLengthDecisionStrategy(context::Context* c,
- context::UserContext* u,
- Valuation valuation);
+ StringSumLengthDecisionStrategy(Env& env, Valuation valuation);
/** make literal */
Node mkLiteral(unsigned i) override;
/** identify */
};
/** an instance of the above class */
std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
- /** The SAT search context for the theory of strings. */
- context::Context* d_satContext;
- /** The user level assertion context for the theory of strings. */
- context::UserContext* d_userContext;
/** The valuation object of theory of strings */
Valuation d_valuation;
/** The term registry of theory of strings */
typedef expr::Attribute<StringsProxyVarAttributeId, bool>
StringsProxyVarAttribute;
-TermRegistry::TermRegistry(SolverState& s,
+TermRegistry::TermRegistry(Env& env,
+ SolverState& s,
SequencesStatistics& statistics,
ProofNodeManager* pnm)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(nullptr),
d_statistics(statistics),
d_hasStrCode(false),
- d_functionsTerms(s.getSatContext()),
- d_inputVars(s.getUserContext()),
- d_preregisteredTerms(s.getSatContext()),
- d_registeredTerms(s.getUserContext()),
- d_registeredTypes(s.getUserContext()),
- d_proxyVar(s.getUserContext()),
- d_lengthLemmaTermsCache(s.getUserContext()),
- d_epg(pnm ? new EagerProofGenerator(
- pnm,
- s.getUserContext(),
- "strings::TermRegistry::EagerProofGenerator")
- : nullptr)
+ d_functionsTerms(context()),
+ d_inputVars(userContext()),
+ d_preregisteredTerms(context()),
+ d_registeredTerms(userContext()),
+ d_registeredTypes(userContext()),
+ d_proxyVar(userContext()),
+ d_lengthLemmaTermsCache(userContext()),
+ d_epg(
+ pnm ? new EagerProofGenerator(
+ pnm, userContext(), "strings::TermRegistry::EagerProofGenerator")
+ : nullptr)
{
NodeManager* nm = NodeManager::currentNM();
d_zero = nm->mkConst(Rational(0));
#include "context/cdlist.h"
#include "proof/eager_proof_generator.h"
#include "proof/proof_node_manager.h"
+#include "smt/env_obj.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/sequences_stats.h"
* (5) Maintaining a skolem cache. Notice that this skolem cache is the
* official skolem cache that should be used by all modules in TheoryStrings.
*/
-class TermRegistry
+class TermRegistry : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
- TermRegistry(SolverState& s,
+ TermRegistry(Env& env,
+ SolverState& s,
SequencesStatistics& statistics,
ProofNodeManager* pnm);
~TermRegistry();
d_statistics(),
d_state(env, d_valuation),
d_eagerSolver(d_state),
- d_termReg(d_state, d_statistics, d_pnm),
+ d_termReg(env, d_state, d_statistics, d_pnm),
d_extTheoryCb(),
d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
d_rewriter(&d_statistics.d_rewrites),
- d_bsolver(d_state, d_im),
- d_csolver(d_state, d_im, d_termReg, d_bsolver),
- d_esolver(d_state,
+ d_bsolver(env, d_state, d_im),
+ d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
+ d_esolver(env,
+ d_state,
d_im,
d_termReg,
d_rewriter,
d_csolver,
d_extTheory,
d_statistics),
- d_rsolver(d_state,
+ d_rsolver(env,
+ d_state,
d_im,
d_termReg.getSkolemCache(),
d_csolver,
d_esolver,
d_statistics),
d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()),
- d_stringsFmf(context(), userContext(), valuation, d_termReg)
+ d_stringsFmf(env, valuation, d_termReg)
{
d_termReg.finishInit(&d_im);
void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
-context::Context* TheoryState::getSatContext() const { return context(); }
-
-context::UserContext* TheoryState::getUserContext() const
-{
- return userContext();
-}
-
bool TheoryState::hasTerm(TNode a) const
{
Assert(d_ee != nullptr);
* of theory.
*/
void setEqualityEngine(eq::EqualityEngine* ee);
- /** Get the SAT context */
- context::Context* getSatContext() const;
- /** Get the user context */
- context::UserContext* getUserContext() const;
//-------------------------------------- equality information
/** Is t registered as a term in the equality engine of this class? */
virtual bool hasTerm(TNode a) const;
void Region::setRep( Node n, bool valid ) {
Assert(hasRep(n) != valid);
if( valid && d_nodes.find( n )==d_nodes.end() ){
- d_nodes[n] = new RegionNodeInfo(d_cf->d_state.getSatContext());
+ d_nodes[n] = new RegionNodeInfo(d_cf->d_thss->context());
}
d_nodes[n]->setValid(valid);
d_reps_size = d_reps_size + ( valid ? 1 : -1 );
}
SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
- Node t, context::Context* satContext, Valuation valuation)
- : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t)
+ Env& env, Node t, Valuation valuation)
+ : DecisionStrategyFmf(env, valuation), d_cardinality_term(t)
{
}
Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
d_state(state),
d_im(im),
d_thss(thss),
- d_regions_index(d_state.getSatContext(), 0),
- d_regions_map(d_state.getSatContext()),
- d_split_score(d_state.getSatContext()),
- d_disequalities_index(d_state.getSatContext(), 0),
- d_reps(d_state.getSatContext(), 0),
- d_cardinality(d_state.getSatContext(), 1),
- d_hasCard(d_state.getSatContext(), false),
- d_maxNegCard(d_state.getSatContext(), 0),
- d_initialized(d_state.getUserContext(), false),
+ d_regions_index(thss->context(), 0),
+ d_regions_map(thss->context()),
+ d_split_score(thss->context()),
+ d_disequalities_index(thss->context(), 0),
+ d_reps(thss->context(), 0),
+ d_cardinality(thss->context(), 1),
+ d_hasCard(thss->context(), false),
+ d_maxNegCard(thss->context(), 0),
+ d_initialized(thss->userContext(), false),
d_c_dec_strat(nullptr)
{
d_cardinality_term = n;
// We are guaranteed that the decision manager is ready since we
// construct this module during TheoryUF::finishInit.
d_c_dec_strat.reset(new CardinalityDecisionStrategy(
- n, d_state.getSatContext(), thss->getTheory()->getValuation()));
+ thss->d_env, n, thss->getTheory()->getValuation()));
}
}
d_regions[d_regions_index]->setValid(true);
Assert(d_regions[d_regions_index]->getNumReps() == 0);
}else{
- d_regions.push_back(new Region(this, d_state.getSatContext()));
+ d_regions.push_back(new Region(this, d_thss->context()));
}
d_regions[d_regions_index]->addRep(n);
d_regions_index = d_regions_index + 1;
return lit;
}
-CardinalityExtension::CardinalityExtension(TheoryState& state,
+CardinalityExtension::CardinalityExtension(Env& env,
+ TheoryState& state,
TheoryInferenceManager& im,
TheoryUF* th)
- : d_state(state),
+ : EnvObj(env),
+ d_state(state),
d_im(im),
d_th(th),
d_rep_model(),
- d_min_pos_com_card(state.getSatContext(), 0),
- d_min_pos_com_card_set(state.getSatContext(), false),
+ d_min_pos_com_card(context(), 0),
+ d_min_pos_com_card_set(context(), false),
d_cc_dec_strat(nullptr),
- d_initializedCombinedCardinality(state.getUserContext(), false),
- d_card_assertions_eqv_lemma(state.getUserContext()),
- d_min_pos_tn_master_card(state.getSatContext(), 0),
- d_min_pos_tn_master_card_set(state.getSatContext(), false),
- d_rel_eqc(state.getSatContext())
+ d_initializedCombinedCardinality(userContext(), false),
+ d_card_assertions_eqv_lemma(userContext()),
+ d_min_pos_tn_master_card(context(), 0),
+ d_min_pos_tn_master_card_set(context(), false),
+ d_rel_eqc(context())
{
if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
{
// Register the strategy with the decision manager of the theory.
// We are guaranteed that the decision manager is ready since we
// construct this module during TheoryUF::finishInit.
- d_cc_dec_strat.reset(new CombinedCardinalityDecisionStrategy(
- state.getSatContext(), th->getValuation()));
+ d_cc_dec_strat.reset(
+ new CombinedCardinalityDecisionStrategy(env, th->getValuation()));
}
}
}
CardinalityExtension::CombinedCardinalityDecisionStrategy::
- CombinedCardinalityDecisionStrategy(context::Context* satContext,
- Valuation valuation)
- : DecisionStrategyFmf(satContext, valuation)
+ CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation)
+ : DecisionStrategyFmf(env, valuation)
{
}
Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
#include "context/cdhashmap.h"
#include "context/context.h"
+#include "smt/env_obj.h"
#include "theory/decision_strategy.h"
#include "theory/theory.h"
#include "util/statistics_stats.h"
* CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
* Modulo Theories".
*/
-class CardinalityExtension
+class CardinalityExtension : protected EnvObj
{
protected:
typedef context::CDHashMap<Node, bool> NodeBoolMap;
class CardinalityDecisionStrategy : public DecisionStrategyFmf
{
public:
- CardinalityDecisionStrategy(Node t,
- context::Context* satContext,
- Valuation valuation);
+ CardinalityDecisionStrategy(Env& env, Node t, Valuation valuation);
/** make literal (the i^th combined cardinality literal) */
Node mkLiteral(unsigned i) override;
/** identify */
}; /** class SortModel */
public:
- CardinalityExtension(TheoryState& state,
+ CardinalityExtension(Env& env,
+ TheoryState& state,
TheoryInferenceManager& im,
TheoryUF* th);
~CardinalityExtension();
class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
{
public:
- CombinedCardinalityDecisionStrategy(context::Context* satContext,
- Valuation valuation);
+ CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation);
/** make literal (the i^th combined cardinality literal) */
Node mkLiteral(unsigned i) override;
/** identify */
namespace theory {
namespace uf {
-HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
- : d_state(state),
+HoExtension::HoExtension(Env& env,
+ TheoryState& state,
+ TheoryInferenceManager& im)
+ : EnvObj(env),
+ d_state(state),
d_im(im),
- d_extensionality(state.getUserContext()),
- d_uf_std_skolem(state.getUserContext())
+ d_extensionality(userContext()),
+ d_uf_std_skolem(userContext())
{
d_true = NodeManager::currentNM()->mkConst(true);
}
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/theory_inference_manager.h"
#include "theory/theory_model.h"
#include "theory/theory_state.h"
*
* For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al.
*/
-class HoExtension
+class HoExtension : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
- HoExtension(TheoryState& state, TheoryInferenceManager& im);
+ HoExtension(Env& env, TheoryState& state, TheoryInferenceManager& im);
/** ppRewrite
*
if (options::finiteModelFind()
&& options::ufssMode() != options::UfssMode::NONE)
{
- d_thss.reset(new CardinalityExtension(d_state, d_im, this));
+ d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this));
}
// The kinds we are treating as function application in congruence
bool isHo = logicInfo().isHigherOrder();
if (isHo)
{
d_equalityEngine->addFunctionKind(kind::HO_APPLY);
- d_ho.reset(new HoExtension(d_state, d_im));
+ d_ho.reset(new HoExtension(d_env, d_state, d_im));
}
}
projects / cvc5.git / commitdiff