#include "expr/node_builder.h"
#include "options/options.h"
#include "util/lemma_output_channel.h"
+#include "util/resource_manager.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
if (d_logicInfo.isQuantified()) {
d_quantEngine->finishInit();
Assert(d_masterEqualityEngine == 0);
- d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
+ d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
if (d_theoryTable[theoryId]) {
void TheoryEngine::eqNotifyNewClass(TNode t){
d_quantEngine->addTermToDatabase( t );
- if( d_logicInfo.isQuantified() && options::quantConflictFind() ){
- d_quantEngine->getConflictFind()->newEqClass( t );
- }
}
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
- //TODO: add notification to efficient E-matching
- if( d_logicInfo.isQuantified() ){
- //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
- if( options::quantConflictFind() ){
- d_quantEngine->getConflictFind()->merge( t1, t2 );
- }
- }
+
}
void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
d_true(),
d_false(),
d_interrupted(false),
+ d_resourceManager(NodeManager::currentResourceManager()),
d_inPreregister(false),
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
* @param effort the effort level to use
*/
void TheoryEngine::check(Theory::Effort effort) {
-
- d_propEngine->checkTime();
+ // spendResource();
// Reset the interrupt flag
d_interrupted = false;
printAssertions("theory::assertions");
}
+ if(Theory::fullEffort(effort)) {
+ Trace("theory::assertions::fulleffort") << endl;
+ if (Trace.isOn("theory::assertions::fulleffort")) {
+ printAssertions("theory::assertions::fulleffort");
+ }
+ }
+
// Note that we've discharged all the facts
d_factsAsserted = false;
// The equality in question (order for no repetition)
Node equality = carePair.a.eqNode(carePair.b);
- EqualityStatus es = getEqualityStatus(carePair.a, carePair.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;
+ // EqualityStatus es = getEqualityStatus(carePair.a, carePair.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;
// 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);
+ Node e = ensureLiteral(equality);
+ d_propEngine->requirePhase(e, true);
// }
// else if (es == EQUALITY_FALSE_IN_MODEL) {
// Node e = ensureLiteral(equality);
Node TheoryEngine::preprocess(TNode assertion) {
Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
+ // spendResource();
// Do a topological sort of the subexpressions and substitute them
vector<preprocess_stack_element> toVisit;
{
Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
- d_propEngine->checkTime();
+ // spendResource();
// If we're in conflict, nothing to do
if (d_inConflict) {
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
- d_propEngine->checkTime();
+ // spendResource();
if(Dump.isOn("t-propagations")) {
Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
}
Node TheoryEngine::getModelValue(TNode var) {
+ if (var.isConst()) return var; // FIXME: HACK!!!
Assert(d_sharedTerms.isShared(var));
return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
}
theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
// For resource-limiting (also does a time check).
- spendResource();
+ // spendResource();
// Do we need to check atoms
if (atomsTo != theory::THEORY_LAST) {
Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
d_iteUtilities->clear();
- Rewriter::garbageCollect();
+ Rewriter::clearCaches();
d_iteRemover.garbageCollect();
nm->reclaimZombiesUntil(options::zombieHuntThreshold());
Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
return th->entailmentCheck(lit, params, seffects);
}
+
+void TheoryEngine::spendResource() {
+ d_resourceManager->spendResource();
+}