#include "theory/arith/arith_ite_utils.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/care_graph.h"
+#include "theory/combination_care_graph.h"
#include "theory/decision_manager.h"
-#include "theory/ee_manager_distributed.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
}
void TheoryEngine::finishInit() {
- // initialize the quantifiers engine
- if (d_logicInfo.isQuantified())
+ // NOTE: This seems to be required since
+ // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
+ // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
+ std::vector<theory::Theory*> paraTheories;
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::isParametric \
+ && d_logicInfo.isTheoryEnabled(THEORY)) \
+ { \
+ paraTheories.push_back(theoryOf(THEORY)); \
+ }
+ // Collect the parametric theories, which are given to the theory combination
+ // manager below
+ CVC4_FOR_EACH_THEORY;
+
+ // Initialize the theory combination architecture
+ if (options::tcMode() == options::TcMode::CARE_GRAPH)
{
- // initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+ d_tc.reset(new CombinationCareGraph(*this, paraTheories));
}
-
- // Initialize the equality engine architecture for all theories, which
- // includes the master equality engine.
- d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
- d_eeDistributed->initializeTheories();
-
- // Initialize the model and model builder.
- if (d_logicInfo.isQuantified())
+ else
{
- d_curr_model_builder = d_quantEngine->getModelBuilder();
- d_curr_model = d_quantEngine->getModel();
- } else {
- d_curr_model = new theory::TheoryModel(
- d_userContext, "DefaultModel", options::assignFunctionValues());
- d_aloc_curr_model = true;
+ Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
+ << options::tcMode() << " not supported";
}
// create the relevance filter if any option requires it
if (options::relevanceFilter())
new RelevanceManager(d_userContext, theory::Valuation(this)));
}
- //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
- if( d_curr_model_builder==NULL ){
- d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
- d_aloc_curr_model_builder = true;
+ // initialize the quantifiers engine
+ if (d_logicInfo.isQuantified())
+ {
+ // initialize the quantifiers engine
+ d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
}
-
- // Initialize the model
- // !!!! temporary, will be part of combination engine initialization
- d_eeDistributed->initializeModel(d_curr_model, nullptr);
+ // initialize the theory combination manager, which decides and allocates the
+ // equality engines to use for all theories.
+ d_tc->finishInit();
// set the core equality engine on quantifiers engine
if (d_logicInfo.isQuantified())
{
- d_quantEngine->setMasterEqualityEngine(
- d_eeDistributed->getCoreEqualityEngine());
+ d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
}
- // finish initializing the theories
+ // finish initializing the theories by linking them with the appropriate
+ // utilities and then calling their finishInit method.
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
Theory* t = d_theoryTable[theoryId];
if (t == nullptr)
continue;
}
// setup the pointers to the utilities
- const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
+ const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
Assert(eeti != nullptr);
// the theory's official equality engine is the one specified by the
// equality engine manager
d_userContext(userContext),
d_logicInfo(logicInfo),
d_sharedTerms(this, context),
- d_eeDistributed(nullptr),
+ d_tc(nullptr),
d_quantEngine(nullptr),
d_decManager(new DecisionManager(userContext)),
d_relManager(nullptr),
- d_curr_model(nullptr),
- d_aloc_curr_model(false),
- d_curr_model_builder(nullptr),
- d_aloc_curr_model_builder(false),
+ d_preRegistrationVisitor(this, context),
+ d_sharedTermsVisitor(d_sharedTerms),
d_eager_model_building(false),
d_possiblePropagations(context),
d_hasPropagated(context),
d_resourceManager(rm),
d_inPreregister(false),
d_factsAsserted(context, false),
- d_preRegistrationVisitor(this, context),
- d_sharedTermsVisitor(d_sharedTerms),
d_attr_handle(),
d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
{
}
}
- if( d_aloc_curr_model_builder ){
- delete d_curr_model_builder;
- }
- if( d_aloc_curr_model ){
- delete d_curr_model;
- }
-
delete d_quantEngine;
smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
<< std::endl;
Assert(!expr::hasFreeVar(preprocessed));
+
// Pre-register the terms in the atom
- Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+ Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(
+ d_preRegistrationVisitor, preprocessed);
theories = Theory::setRemove(THEORY_BOOL, theories);
- // Remove the top theory, if any more that means multiple theories were involved
+ // Remove the top theory, if any more that means multiple theories were
+ // involved
bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
- TheoryId i;
- // These checks don't work with finite model finding, because it
- // uses Rational constants to represent cardinality constraints,
- // even though arithmetic isn't actually involved.
- if(!options::finiteModelFind()) {
- while((i = Theory::setPop(theories)) != THEORY_LAST) {
- if(!d_logicInfo.isTheoryEnabled(i)) {
- LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
- newLogicInfo.enableTheory(i);
- newLogicInfo.lock();
- stringstream ss;
- ss << "The logic was specified as " << d_logicInfo.getLogicString()
- << ", which doesn't include " << i
- << ", but found a term in that theory." << endl
- << "You might want to extend your logic to "
- << newLogicInfo.getLogicString() << endl;
- throw LogicException(ss.str());
+ if (Configuration::isAssertionBuild())
+ {
+ TheoryId i;
+ // This should never throw an exception, since theories should be
+ // guaranteed to be initialized.
+ // These checks don't work with finite model finding, because it
+ // uses Rational constants to represent cardinality constraints,
+ // even though arithmetic isn't actually involved.
+ if (!options::finiteModelFind())
+ {
+ while ((i = Theory::setPop(theories)) != THEORY_LAST)
+ {
+ if (!d_logicInfo.isTheoryEnabled(i))
+ {
+ LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
+ newLogicInfo.enableTheory(i);
+ newLogicInfo.lock();
+ std::stringstream ss;
+ ss << "The logic was specified as " << d_logicInfo.getLogicString()
+ << ", which doesn't include " << i
+ << ", but found a term in that theory." << std::endl
+ << "You might want to extend your logic to "
+ << newLogicInfo.getLogicString() << std::endl;
+ throw LogicException(ss.str());
+ }
}
}
}
if (multipleTheories) {
// Collect the shared terms if there are multiple theories
- NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+ NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor,
+ preprocessed);
}
}
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
- theoryOf(THEORY)->check(effort); \
- if (d_inConflict) { \
- Debug("conflict") << THEORY << " in conflict. " << std::endl; \
- break; \
- } \
- }
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasCheck \
+ && d_logicInfo.isTheoryEnabled(THEORY)) \
+ { \
+ theoryOf(THEORY)->check(effort); \
+ if (d_inConflict) \
+ { \
+ Debug("conflict") << THEORY << " in conflict. " << std::endl; \
+ break; \
+ } \
+ }
// Do the checking
try {
{
d_relManager->resetRound();
}
+ d_tc->resetRound();
}
// Check until done
if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
// Do the combination
Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
- combineTheories();
+ {
+ TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
+ d_tc->combineTheories();
+ }
if(d_logicInfo.isQuantified()){
d_quantEngine->notifyCombineTheories();
}
if (Trace.isOn("theory::assertions-model")) {
printAssertions("theory::assertions-model");
}
+ // reset the model in the combination engine
+ d_tc->resetModel();
//checks for theories requiring the model go at last call
- d_curr_model->reset();
- // !!! temporary, will be part of distributed model manager
- context::Context* meec = d_eeDistributed->getModelEqualityEngineContext();
- meec->pop();
- meec->push();
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
if( theoryId!=THEORY_QUANTIFIERS ){
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
if( theory->needsCheckLastEffort() ){
- if( !d_curr_model->isBuilt() ){
- if( !d_curr_model_builder->buildModel(d_curr_model) ){
- break;
- }
+ if (!d_tc->buildModel())
+ {
+ break;
}
theory->check(Theory::EFFORT_LAST_CALL);
}
// are in "SAT mode". We build the model later only if the user asks
// for it via getBuiltModel.
d_inSatMode = true;
- if (d_eager_model_building && !d_curr_model->isBuilt())
+ if (d_eager_model_building)
{
- d_curr_model_builder->buildModel(d_curr_model);
+ d_tc->buildModel();
}
}
}
Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
- // case where we are about to answer SAT, the master equality engine,
- // if it exists, must be consistent.
- eq::EqualityEngine* mee = d_eeDistributed->getCoreEqualityEngine();
- if (mee != NULL)
- {
- AlwaysAssert(mee->consistent());
- }
- if (d_curr_model->isBuilt())
- {
- // model construction should always succeed unless lemmas were added
- AlwaysAssert(d_curr_model->isBuiltSuccess());
- if (options::produceModels())
- {
- // Do post-processing of model from the theories (used for THEORY_SEP
- // to construct heap model)
- postProcessModel(d_curr_model);
- // also call the model builder's post-process model
- d_curr_model_builder->postProcessModel(d_incomplete.get(),
- d_curr_model);
- }
- }
+ // Do post-processing of model from the theories (e.g. used for THEORY_SEP
+ // to construct heap model)
+ d_tc->postProcessModel(d_incomplete.get());
}
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
}
}
-void TheoryEngine::combineTheories() {
-
- Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl;
-
- TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
-
- // Care graph we'll be building
- CareGraph careGraph;
-
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
- theoryOf(THEORY)->getCareGraph(&careGraph); \
- }
-
- // Call on each parametric theory to give us its care graph
- CVC4_FOR_EACH_THEORY;
-
- Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
-
- // Now add splitters for the ones we are interested in
- CareGraph::const_iterator care_it = careGraph.begin();
- CareGraph::const_iterator care_it_end = careGraph.end();
-
- for (; care_it != care_it_end; ++ care_it) {
- const CarePair& carePair = *care_it;
-
- Debug("combineTheories")
- << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
- << carePair.d_b << " from " << carePair.d_theory << endl;
-
- Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst());
- Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst());
-
- // The equality in question (order for no repetition)
- Node equality = carePair.d_a.eqNode(carePair.d_b);
- // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
- // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
- // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
- // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
- // es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
- // es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
- // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
- // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
- // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
- // "Unexpected case") << endl;
-
- // We need to split on it
- Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-
- lemma(equality.orNode(equality.notNode()),
- RULE_INVALID,
- false,
- LemmaProperty::NONE,
- carePair.d_theory);
-
- // This code is supposed to force preference to follow what the theory models already have
- // but it doesn't seem to make a big difference - need to explore more -Clark
- // if (true) {
- // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
- Node e = ensureLiteral(equality);
- d_propEngine->requirePhase(e, true);
- // }
- // else if (es == EQUALITY_FALSE_IN_MODEL) {
- // Node e = ensureLiteral(equality);
- // d_propEngine->requirePhase(e, false);
- // }
- // }
- }
-}
-
-void TheoryEngine::propagate(Theory::Effort effort) {
+void TheoryEngine::propagate(Theory::Effort effort)
+{
// Reset the interrupt flag
d_interrupted = false;
return true;
}
-bool TheoryEngine::properPropagation(TNode lit) const {
- if(!getPropEngine()->isSatLiteral(lit)) {
- return false;
- }
- bool b;
- return !getPropEngine()->hasValue(lit, b);
-}
-
-bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
- // Explanation must be either a conjunction of true literals that have true SAT values already
- // or a singled literal that has a true SAT value already.
- if (expl.getKind() == kind::AND) {
- for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
- bool value;
- if (!d_propEngine->hasValue(expl[i], value) || !value) {
- return false;
- }
- }
- } else {
- bool value;
- return d_propEngine->hasValue(expl, value) && value;
- }
- return true;
+TheoryModel* TheoryEngine::getModel()
+{
+ Assert(d_tc != nullptr);
+ TheoryModel* m = d_tc->getModel();
+ Assert(m != nullptr);
+ return m;
}
-bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+TheoryModel* TheoryEngine::getBuiltModel()
{
- //have shared term engine collectModelInfo
- // d_sharedTerms.collectModelInfo( m );
- // Consult each active theory to get all relevant information
- // concerning the model.
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
- if(d_logicInfo.isTheoryEnabled(theoryId)) {
- Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl;
- if (!d_theoryTable[theoryId]->collectModelInfo(m))
- {
- return false;
- }
- }
- }
- Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl;
- // Get the Boolean variables
- vector<TNode> boolVars;
- d_propEngine->getBooleanVariables(boolVars);
- vector<TNode>::iterator it, iend = boolVars.end();
- bool hasValue, value;
- for (it = boolVars.begin(); it != iend; ++it) {
- TNode var = *it;
- hasValue = d_propEngine->hasValue(var, value);
- // TODO: Assert that hasValue is true?
- if (!hasValue) {
- Trace("model-builder-assertions")
- << " has no value : " << var << std::endl;
- value = false;
- }
- Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
- if (!m->assertPredicate(var, value))
- {
- return false;
- }
+ Assert(d_tc != nullptr);
+ // If this method was called, we should be in SAT mode, and produceModels
+ // should be true.
+ AlwaysAssert(options::produceModels());
+ if (!d_inSatMode)
+ {
+ // not available, perhaps due to interuption.
+ return nullptr;
}
- return true;
-}
-
-void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
- if(d_logicInfo.isTheoryEnabled(theoryId)) {
- Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId << endl;
- d_theoryTable[theoryId]->postProcessModel( m );
- }
+ // must build model at this point
+ if (!d_tc->buildModel())
+ {
+ return nullptr;
}
+ return d_tc->getModel();
}
-TheoryModel* TheoryEngine::getModel() {
- return d_curr_model;
-}
-
-TheoryModel* TheoryEngine::getBuiltModel()
+bool TheoryEngine::buildModel()
{
- if (!d_curr_model->isBuilt())
- {
- // If this method was called, we should be in SAT mode, and produceModels
- // should be true.
- AlwaysAssert(options::produceModels());
- if (!d_inSatMode)
- {
- // not available, perhaps due to interuption.
- return nullptr;
- }
- // must build model at this point
- d_curr_model_builder->buildModel(d_curr_model);
- }
- return d_curr_model;
+ Assert(d_tc != nullptr);
+ return d_tc->buildModel();
}
bool TheoryEngine::getSynthSolutions(
TNode atom = polarity ? literal : literal[0];
if (d_logicInfo.isSharingEnabled()) {
-
// If any shared terms, it's time to do sharing work
if (d_sharedTerms.hasSharedTerms(atom)) {
// Notify the theories the shared terms
if (atom.getKind() == kind::EQUAL) {
// Assert it to the the owning theory
assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
- // Shared terms manager will assert to interested theories directly, as the terms become shared
+ // Shared terms manager will assert to interested theories directly, as
+ // the terms become shared
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
// Now, let's check for any atom triggers from lemmas
}
bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
-
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
});
}
-SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
-{
- return &d_sharedTerms;
-}
-
void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
Assert(explanationVector.size() > 0);
// not relevant, skip
continue;
}
- Node val = getModel()->getValue(assertion);
+ Node val = d_tc->getModel()->getValue(assertion);
if (val != d_true)
{
std::stringstream ss;
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
#include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
#include "theory/sort_inference.h"
#include "theory/substitutions.h"
#include "theory/term_registration_visitor.h"
/* Forward declarations */
namespace theory {
-class CombinationEngine;
class TheoryModel;
-class TheoryEngineModelBuilder;
-class EqEngineManagerDistributed;
-
+class CombinationEngine;
class DecisionManager;
class RelevanceManager;
friend class theory::CombinationEngine;
friend class theory::quantifiers::TermDb;
friend class theory::EngineOutputChannel;
+ friend class theory::CombinationEngine;
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
*/
SharedTermsDatabase d_sharedTerms;
- /**
- * The distributed equality manager. This class is responsible for
- * configuring the theories of this class for handling equalties
- * in a "distributed" fashion, i.e. each theory maintains a unique
- * instance of an equality engine. These equality engines are memory
- * managed by this class.
- */
- std::unique_ptr<theory::EqEngineManagerDistributed> d_eeDistributed;
-
+ /** The combination manager we are using */
+ std::unique_ptr<theory::CombinationEngine> d_tc;
/**
* The quantifiers engine
*/
/** The relevance manager */
std::unique_ptr<theory::RelevanceManager> d_relManager;
- /**
- * Default model object
- */
- theory::TheoryModel* d_curr_model;
- bool d_aloc_curr_model;
- /**
- * Model builder object
- */
- theory::TheoryEngineModelBuilder* d_curr_model_builder;
- bool d_aloc_curr_model_builder;
+ /** Default visitor for pre-registration */
+ PreRegisterVisitor d_preRegistrationVisitor;
+
+ /** Visitor for collecting shared terms */
+ SharedTermsVisitor d_sharedTermsVisitor;
+
/** are we in eager model building mode? (see setEagerModelBuilding). */
bool d_eager_model_building;
d_incomplete = true;
}
-
/**
* Mapping of propagations from recievers to senders.
*/
*/
context::CDO<bool> d_factsAsserted;
- /**
- * Map from equality atoms to theories that would like to be notified about them.
- */
-
-
/**
* Assert the formula to the given theory.
* @param assertion the assertion to send (not necesserily normalized)
*/
void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
-public:
-
+ public:
/**
* Signal the start of a new round of assertion preprocessing
*/
* or during LAST_CALL effort.
*/
bool isRelevant(Node lit) const;
-
/**
* This is called at shutdown time by the SmtEngine, just before
* destruction. It is important because there are destruction
*/
void check(theory::Theory::Effort effort);
- /**
- * Run the combination framework.
- */
- void combineTheories();
-
/**
* Calls ppStaticLearn() on all theories, accumulating their
* combined contributions in the "learned" builder.
Node getNextDecisionRequest();
bool properConflict(TNode conflict) const;
- bool properPropagation(TNode lit) const;
- bool properExplanation(TNode node, TNode expl) const;
/**
* Returns an explanation of the node propagated to the SAT solver.
*/
Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
- /**
- * collect model info
- */
- bool collectModelInfo(theory::TheoryModel* m);
- /** post process model */
- void postProcessModel( theory::TheoryModel* m );
-
/**
* Get the pointer to the model object used by this theory engine.
*/
* was interrupted), then this returns the null pointer.
*/
theory::TheoryModel* getBuiltModel();
+ /**
+ * This forces the model maintained by the combination engine to be built
+ * if it has not been done so already. This should be called only during a
+ * last call effort check after theory combination is run.
+ *
+ * @return true if the model was successfully built (possibly prior to this
+ * call).
+ */
+ bool buildModel();
/** set eager model building
*
* If this method is called, then this TheoryEngine will henceforth build
*/
bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
- /**
- * Get the model builder
- */
- theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; }
-
/**
* Get the theory associated to a given Node.
*
std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
private:
- /** Default visitor for pre-registration */
- PreRegisterVisitor d_preRegistrationVisitor;
-
- /** Visitor for collecting shared terms */
- SharedTermsVisitor d_sharedTermsVisitor;
/** Dump the assertions to the dump */
void dumpAssertions(const char* tag);
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
public:
- SharedTermsDatabase* getSharedTermsDatabase();
-
SortInference* getSortInference() { return &d_sortInfer; }
/** Prints the assertions to the debug stream */
projects / cvc5.git / commitdiff