Adding an option to the equality engine constructor to treat all constants as

[cvc5.git] / src / theory / theory_engine.cpp

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ed56890ae540c784fa82d08ab59b444c95ba2f52..22bf37470b424c0b05dfc1289aac657c5f42ee50 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,6 +26,7 @@
 #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"
@@ -73,7 +74,7 @@ void TheoryEngine::finishInit() {
   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]) {
@@ -92,19 +93,10 @@ void TheoryEngine::finishInit() {
 
 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){
@@ -151,6 +143,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true(),
   d_false(),
   d_interrupted(false),
+  d_resourceManager(NodeManager::currentResourceManager()),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -343,8 +336,7 @@ void TheoryEngine::dumpAssertions(const char* tag) {
  * @param effort the effort level to use
  */
 void TheoryEngine::check(Theory::Effort effort) {
-
-  d_propEngine->checkTime();
+  // spendResource();
 
   // Reset the interrupt flag
   d_interrupted = false;
@@ -387,6 +379,13 @@ void TheoryEngine::check(Theory::Effort effort) {
         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;
 
@@ -487,16 +486,16 @@ void TheoryEngine::combineTheories() {
 
     // 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;
@@ -505,8 +504,8 @@ void TheoryEngine::combineTheories() {
     // 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);
@@ -855,6 +854,7 @@ struct preprocess_stack_element {
 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;
@@ -1091,7 +1091,7 @@ void TheoryEngine::assertFact(TNode literal)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
 
-  d_propEngine->checkTime();
+  // spendResource();
 
   // If we're in conflict, nothing to do
   if (d_inConflict) {
@@ -1154,7 +1154,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
   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")
@@ -1201,6 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
 }
 
 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);
 }
@@ -1377,7 +1378,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 
 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) {
@@ -1562,7 +1563,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
         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;
@@ -1751,3 +1752,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
 
   return th->entailmentCheck(lit, params, seffects);
 }
+
+void TheoryEngine::spendResource() {
+  d_resourceManager->spendResource();
+}