Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.
d_containing(containing),
d_ee(ee),
d_needsLastCall(false),
+ d_extTheory(&containing),
d_model(containing.getSatContext()),
d_trSlv(d_model),
d_nlSlv(containing, d_model),
d_iandSlv(containing, d_model),
d_builtModel(containing.getSatContext(), false)
{
+ d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
+ d_extTheory.addFunctionKind(kind::EXPONENTIAL);
+ d_extTheory.addFunctionKind(kind::SINE);
+ d_extTheory.addFunctionKind(kind::PI);
+ d_extTheory.addFunctionKind(kind::IAND);
d_true = NodeManager::currentNM()->mkConst(true);
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_one = NodeManager::currentNM()->mkConst(Rational(1));
NonlinearExtension::~NonlinearExtension() {}
+void NonlinearExtension::preRegisterTerm(TNode n)
+{
+ // register terms with extended theory, to find extended terms that can be
+ // eliminated by context-depedendent simplification.
+ d_extTheory.registerTermRec(n);
+}
+
bool NonlinearExtension::getCurrentSubstitution(
int effort,
const std::vector<Node>& vars,
<< ", built model = " << d_builtModel.get() << std::endl;
if (e == Theory::EFFORT_FULL)
{
- d_containing.getExtTheory()->clearCache();
+ d_extTheory.clearCache();
d_needsLastCall = true;
if (options::nlExtRewrites())
{
std::vector<Node> nred;
- if (!d_containing.getExtTheory()->doInferences(0, nred))
+ if (!d_extTheory.doInferences(0, nred))
{
Trace("nl-ext") << "...sent no lemmas, # extf to reduce = "
<< nred.size() << std::endl;
// get the extended terms belonging to this theory
std::vector<Node> xts;
- d_containing.getExtTheory()->getTerms(xts);
+ d_extTheory.getTerms(xts);
if (Trace.isOn("nl-ext-debug"))
{
#include "theory/arith/nl/stats.h"
#include "theory/arith/nl/transcendental_solver.h"
#include "theory/arith/theory_arith.h"
+#include "theory/ext_theory.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
public:
NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee);
~NonlinearExtension();
+ /**
+ * Does non-context dependent setup for a node connected to a theory.
+ */
+ void preRegisterTerm(TNode n);
/** Get current substitution
*
* This function and the one below are
NlStats d_stats;
// needs last call effort
bool d_needsLastCall;
+ /** Extended theory, responsible for context-dependent simplification. */
+ ExtTheory d_extTheory;
/** The non-linear model object
*
* This class is responsible for computing model values for arithmetic terms
d_proofRecorder(nullptr)
{
smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
- // if logic is non-linear
- if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
- {
- setupExtTheory();
- getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
- getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
- getExtTheory()->addFunctionKind(kind::SINE);
- getExtTheory()->addFunctionKind(kind::PI);
- getExtTheory()->addFunctionKind(kind::IAND);
- }
}
TheoryArith::~TheoryArith(){
if (d_nonlinearExtension != nullptr)
{
- d_containing.getExtTheory()->registerTermRec( n );
+ d_nonlinearExtension->preRegisterTerm(n);
}
try {
using namespace CVC4::theory::bv;
using namespace CVC4::theory::bv::utils;
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
- : SubtheorySolver(c, bv),
- d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::bv::ee", true),
- d_slicer(new Slicer()),
- d_isComplete(c, true),
- d_lemmaThreshold(16),
- d_useSlicer(false),
- d_preregisterCalled(false),
- d_checkCalled(false),
- d_reasons(c)
+CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
+ : SubtheorySolver(c, bv),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::bv::ee", true),
+ d_slicer(new Slicer()),
+ d_isComplete(c, true),
+ d_lemmaThreshold(16),
+ d_useSlicer(false),
+ d_preregisterCalled(false),
+ d_checkCalled(false),
+ d_extTheory(extt),
+ d_reasons(c)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
d_bv->setConflict(conflict);
}
-void CoreSolver::eqNotifyNewClass(TNode t) {
- Assert(d_bv->getExtTheory() != NULL);
- d_bv->getExtTheory()->registerTerm( t );
-}
+void CoreSolver::eqNotifyNewClass(TNode t) { d_extTheory->registerTerm(t); }
bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
if (d_useSlicer)
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "theory/bv/bv_subtheory.h"
+#include "theory/ext_theory.h"
namespace CVC4 {
namespace theory {
bool d_useSlicer;
bool d_preregisterCalled;
bool d_checkCalled;
-
+
+ /** Pointer to the extended theory module. */
+ ExtTheory* d_extTheory;
+
/** To make sure we keep the explanations */
context::CDHashSet<Node, NodeHashFunction> d_reasons;
ModelValue d_modelValues;
bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
Statistics d_statistics;
public:
- CoreSolver(context::Context* c, TheoryBV* bv);
- ~CoreSolver();
- bool isComplete() override { return d_isComplete; }
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void preRegister(TNode node) override;
- bool check(Theory::Effort e) override;
- void explain(TNode literal, std::vector<TNode>& assumptions) override;
- bool collectModelInfo(TheoryModel* m, bool fullModel) override;
- Node getModelValue(TNode var) override;
- void addSharedTerm(TNode t) override
- {
- d_equalityEngine.addTriggerTerm(t, THEORY_BV);
+ CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
+ ~CoreSolver();
+ bool isComplete() override { return d_isComplete; }
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void preRegister(TNode node) override;
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode var) override;
+ void addSharedTerm(TNode t) override
+ {
+ d_equalityEngine.addTriggerTerm(t, THEORY_BV);
}
EqualityStatus getEqualityStatus(TNode a, TNode b) override
{
d_invalidateModelCache(c, true),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
+ d_extTheory(new ExtTheory(this)),
d_propagatedBy(c),
d_eagerSolver(),
d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
d_extf_range_infer(u),
d_extf_collapse_infer(u)
{
- setupExtTheory();
- getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
- getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
+ d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
+ d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
if (options::bitblastMode() == options::BitblastMode::EAGER)
{
d_eagerSolver.reset(new EagerBitblastSolver(c, this));
if (options::bitvectorEqualitySolver() && !options::proof())
{
- d_subtheories.emplace_back(new CoreSolver(c, this));
+ d_subtheories.emplace_back(new CoreSolver(c, this, d_extTheory.get()));
d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->preRegister(node);
}
-
- // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
- //getExtTheory()->registerTermRec( node );
+
+ // AJR : equality solver currently registers all terms to ExtTheory, if we
+ // want a lazy reduction without the bv equality solver, need to call this
+ // d_extTheory->registerTermRec( node );
}
void TheoryBV::sendConflict() {
//last call : do reductions on extended bitvector functions
if (e == Theory::EFFORT_LAST_CALL) {
- std::vector<Node> nred = getExtTheory()->getActive();
+ std::vector<Node> nred = d_extTheory->getActive();
doExtfReductions(nred);
return;
}
if (Theory::fullEffort(e)) {
//do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
std::vector< Node > nred;
- if( getExtTheory()->doInferences( 0, nred ) ){
+ if (d_extTheory->doInferences(0, nred))
+ {
return;
}
d_needsLastCallCheck = false;
bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
std::vector< Node > nredr;
- if( getExtTheory()->doReductions( 0, terms, nredr ) ){
+ if (d_extTheory->doReductions(0, terms, nredr))
+ {
return true;
}
Assert(nredr.empty());
namespace proof {
class BitVectorProof;
}
-} // namespace CVC4
-namespace CVC4 {
namespace theory {
+
+class ExtTheory;
+
namespace bv {
class CoreSolver;
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
+ /** Extended theory module, for context-dependent simplification. */
+ std::unique_ptr<ExtTheory> d_extTheory;
+
/**
* Keeps a map from nodes to the subtheory that propagated it so that we can explain it
* properly.
ExtfSolver::~ExtfSolver() {}
+void ExtfSolver::addSharedTerm(TNode n) { d_extt.registerTermRec(n); }
+
bool ExtfSolver::doReduction(int effort, Node n)
{
Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
SequencesStatistics& statistics);
~ExtfSolver();
+ /**
+ * Called when a shared term is added to theory of strings, this registers
+ * n with the extended theory utility for context-depdendent simplification.
+ */
+ void addSharedTerm(TNode n);
/** check extended functions evaluation
*
* This applies "context-dependent simplification" for all active extended
d_equalityEngine(d_notify, c, "theory::strings::ee", true),
d_state(c, u, d_equalityEngine, d_valuation),
d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
- d_im(nullptr),
+ d_extTheory(this),
+ d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
d_rewriter(&d_statistics.d_rewrites),
- d_bsolver(nullptr),
- d_csolver(nullptr),
- d_esolver(nullptr),
- d_rsolver(nullptr),
+ d_bsolver(d_state, d_im),
+ d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+ d_esolver(c,
+ u,
+ d_state,
+ d_im,
+ d_termReg,
+ d_rewriter,
+ d_bsolver,
+ d_csolver,
+ d_extTheory,
+ d_statistics),
+ d_rsolver(d_state, d_im, d_csolver, d_esolver, d_statistics, c, u),
d_stringsFmf(c, u, valuation, d_termReg)
{
- setupExtTheory();
- ExtTheory* extt = getExtTheory();
- // initialize the inference manager, which requires the extended theory
- d_im.reset(
- new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics));
- // initialize the solvers
- d_bsolver.reset(new BaseSolver(d_state, *d_im));
- d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver));
- d_esolver.reset(new ExtfSolver(c,
- u,
- d_state,
- *d_im,
- d_termReg,
- d_rewriter,
- *d_bsolver,
- *d_csolver,
- *extt,
- d_statistics));
- d_rsolver.reset(new RegExpSolver(
- d_state, *d_im, *d_csolver, *d_esolver, d_statistics, c, u));
-
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
if (options::stringExp())
{
- getExtTheory()->registerTermRec(t);
+ d_esolver.addSharedTerm(t);
}
Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
}
{
Debug("strings-explain") << "explain called on " << literal << std::endl;
std::vector< TNode > assumptions;
- d_im->explain(literal, assumptions);
+ d_im.explain(literal, assumptions);
Node ret;
if( assumptions.empty() ){
ret = d_true;
for( unsigned i=0; i<vars.size(); i++ ){
Node n = vars[i];
Trace("strings-subs") << " get subs for " << n << "..." << std::endl;
- Node s = d_esolver->getCurrentSubstitutionFor(effort, n, exp[n]);
+ Node s = d_esolver.getCurrentSubstitutionFor(effort, n, exp[n]);
subs.push_back(s);
}
return true;
//check if col[i][j] has only variables
if (!eqc.isConst())
{
- NormalForm& nfe = d_csolver->getNormalForm(eqc);
+ NormalForm& nfe = d_csolver.getNormalForm(eqc);
if (nfe.d_nf.size() == 1)
{
// is it an equivalence class with a seq.unit term?
{
if (processed.find(rn) == processed.end())
{
- NormalForm& nf = d_csolver->getNormalForm(rn);
+ NormalForm& nf = d_csolver.getNormalForm(rn);
if (Trace.isOn("strings-model"))
{
Trace("strings-model")
TNode fact = assertion.d_assertion;
Trace("strings-assertion") << "get assertion: " << fact << endl;
- d_im->sendAssumption(fact);
+ d_im.sendAssumption(fact);
}
- d_im->doPendingFacts();
+ d_im.doPendingFacts();
Assert(d_strat.isStrategyInit());
if (!d_state.isInConflict() && !d_valuation.needCheck()
Trace("strings-check") << " * Run strategy..." << std::endl;
runStrategy(e);
// flush the facts
- addedFact = d_im->hasPendingFact();
- addedLemma = d_im->hasPendingLemma();
- d_im->doPendingFacts();
- d_im->doPendingLemmas();
+ addedFact = d_im.hasPendingFact();
+ addedLemma = d_im.hasPendingLemma();
+ d_im.doPendingFacts();
+ d_im.doPendingLemmas();
if (Trace.isOn("strings-check"))
{
Trace("strings-check") << " ...finish run strategy: ";
} while (!d_state.isInConflict() && !addedLemma && addedFact);
}
Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
- Assert(!d_im->hasPendingFact());
- Assert(!d_im->hasPendingLemma());
+ Assert(!d_im.hasPendingFact());
+ Assert(!d_im.hasPendingLemma());
}
bool TheoryStrings::needsCheckLastEffort() {
if( options::stringGuessModel() ){
- return d_esolver->hasExtendedFunctions();
+ return d_esolver.hasExtendedFunctions();
}
return false;
}
void TheoryStrings::checkRegisterTermsPreNormalForm()
{
- const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver.getStringEqc();
for (const Node& eqc : seqc)
{
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
while (!eqc_i.isFinished())
{
Node n = (*eqc_i);
- if (!d_bsolver->isCongruent(n))
+ if (!d_bsolver.isCongruent(n))
{
d_termReg.registerTerm(n, 2);
}
// str.code applied to the proxy variables for each equivalence classes that
// are constants of size one
std::vector<Node> const_codes;
- const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver.getStringEqc();
for (const Node& eqc : seqc)
{
- NormalForm& nfe = d_csolver->getNormalForm(eqc);
+ NormalForm& nfe = d_csolver.getNormalForm(eqc);
if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
{
Node c = nfe.d_nf[0];
if (!d_state.areEqual(cc, vc))
{
std::vector<Node> emptyVec;
- d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
+ d_im.sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
}
const_codes.push_back(vc);
}
}
}
}
- if (d_im->hasProcessed())
+ if (d_im.hasProcessed())
{
return;
}
Node eqn = c1[0].eqNode(c2[0]);
// str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
- d_im->sendPhaseRequirement(deq, false);
+ d_im.sendPhaseRequirement(deq, false);
std::vector<Node> emptyVec;
- d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
+ d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
}
}
}
void TheoryStrings::checkRegisterTermsNormalForms()
{
- const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver.getStringEqc();
for (const Node& eqc : seqc)
{
- NormalForm& nfi = d_csolver->getNormalForm(eqc);
+ NormalForm& nfi = d_csolver.getNormalForm(eqc);
// check if there is a length term for this equivalence class
EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
Node lt = ei ? ei->d_lengthTerm : Node::null();
if( !options::stringLazyPreproc() ){
//eager preprocess here
std::vector< Node > new_nodes;
- StringsPreprocess* p = d_esolver->getPreprocess();
+ StringsPreprocess* p = d_esolver.getPreprocess();
Node ret = p->processAssertion(atomRet, new_nodes);
if (ret != atomRet)
{
Trace("strings-process") << "..." << std::endl;
switch (s)
{
- case CHECK_INIT: d_bsolver->checkInit(); break;
- case CHECK_CONST_EQC: d_bsolver->checkConstantEquivalenceClasses(); break;
- case CHECK_EXTF_EVAL: d_esolver->checkExtfEval(effort); break;
- case CHECK_CYCLES: d_csolver->checkCycles(); break;
- case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); break;
+ case CHECK_INIT: d_bsolver.checkInit(); break;
+ case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
+ case CHECK_EXTF_EVAL: d_esolver.checkExtfEval(effort); break;
+ case CHECK_CYCLES: d_csolver.checkCycles(); break;
+ case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
- case CHECK_NORMAL_FORMS_EQ: d_csolver->checkNormalFormsEq(); break;
- case CHECK_NORMAL_FORMS_DEQ: d_csolver->checkNormalFormsDeq(); break;
+ case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break;
+ case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
case CHECK_CODES: checkCodes(); break;
- case CHECK_LENGTH_EQC: d_csolver->checkLengthsEqc(); break;
+ case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
- case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break;
- case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break;
- case CHECK_CARDINALITY: d_bsolver->checkCardinality(); break;
+ case CHECK_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break;
+ case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(); break;
+ case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
default: Unreachable(); break;
}
Trace("strings-process") << "Done " << s
- << ", addedFact = " << d_im->hasPendingFact()
- << ", addedLemma = " << d_im->hasPendingLemma()
+ << ", addedFact = " << d_im.hasPendingFact()
+ << ", addedLemma = " << d_im.hasPendingLemma()
<< ", conflict = " << d_state.isInConflict()
<< std::endl;
}
InferStep curr = it->first;
if (curr == BREAK)
{
- if (d_im->hasProcessed())
+ if (d_im.hasProcessed())
{
break;
}
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "expr/node_trie.h"
+#include "theory/ext_theory.h"
#include "theory/strings/base_solver.h"
#include "theory/strings/core_solver.h"
#include "theory/strings/extf_solver.h"
SolverState d_state;
/** The term registry for this theory */
TermRegistry d_termReg;
+ /** Extended theory, responsible for context-dependent simplification. */
+ ExtTheory d_extTheory;
/** The (custom) output channel of the theory of strings */
- std::unique_ptr<InferenceManager> d_im;
+ InferenceManager d_im;
/** The theory rewriter for this theory. */
StringsRewriter d_rewriter;
/**
* The base solver, responsible for reasoning about congruent terms and
* inferring constants for equivalence classes.
*/
- std::unique_ptr<BaseSolver> d_bsolver;
+ BaseSolver d_bsolver;
/**
* The core solver, responsible for reasoning about string concatenation
* with length constraints.
*/
- std::unique_ptr<CoreSolver> d_csolver;
+ CoreSolver d_csolver;
/**
* Extended function solver, responsible for reductions and simplifications
* involving extended string functions.
*/
- std::unique_ptr<ExtfSolver> d_esolver;
+ ExtfSolver d_esolver;
/** regular expression solver module */
- std::unique_ptr<RegExpSolver> d_rsolver;
+ RegExpSolver d_rsolver;
/** regular expression elimination module */
RegExpElimination d_regexp_elim;
/** Strings finite model finding decision strategy */
d_careGraph(NULL),
d_quantEngine(NULL),
d_decManager(nullptr),
- d_extTheory(NULL),
d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
d_computeCareGraphTime(getStatsPrefix(id) + name
+ "::computeCareGraphTime"),
Theory::~Theory() {
smtStatisticsRegistry()->unregisterStat(&d_checkTime);
smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
-
- delete d_extTheory;
}
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
return make_pair(false, Node::null());
}
-ExtTheory* Theory::getExtTheory() {
- Assert(d_extTheory != NULL);
- return d_extTheory;
-}
-
void Theory::addCarePair(TNode t1, TNode t2) {
if (d_careGraph) {
d_careGraph->insert(CarePair(t1, t2, d_id));
d_decManager = dm;
}
-void Theory::setupExtTheory() {
- Assert(d_extTheory == NULL);
- d_extTheory = new ExtTheory(this);
-}
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
class QuantifiersEngine;
class TheoryModel;
class SubstitutionMap;
-class ExtTheory;
class TheoryRewriter;
namespace rrinst {
/** Pointer to the decision manager. */
DecisionManager* d_decManager;
- /** Extended theory module or NULL. Owned by the theory. */
- ExtTheory* d_extTheory;
-
protected:
// === STATISTICS ===
/* equality engine TODO: use? */
virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
- /* Get extended theory if one has been installed. */
- ExtTheory* getExtTheory();
-
/* get current substitution at an effort
* input : vars
* output : subs, exp
projects / cvc5.git / commitdiff