From 8dc1280a5161633fddfb8334811a86c911bb25c1 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 2 Sep 2014 18:28:52 -0400
Subject: [PATCH] check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
---
 contrib/theoryskel/theory_DIR.cpp             | 3 +++
 src/theory/bv/theory_bv.cpp                   | 3 +++
 src/theory/datatypes/theory_datatypes.cpp     | 4 ++++
 src/theory/idl/theory_idl.cpp                 | 4 ++++
 src/theory/quantifiers/theory_quantifiers.cpp | 4 ++++
 src/theory/sets/theory_sets.cpp               | 3 +++
 src/theory/strings/theory_strings.cpp         | 6 +++++-
 src/theory/theory.h                           | 2 +-
 src/theory/uf/theory_uf.cpp                   | 4 ++++
 9 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
index 72101a5a6..535a54fd7 100644
--- a/contrib/theoryskel/theory_DIR.cpp
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -16,6 +16,9 @@ Theory$camel::Theory$camel(context::Context* c,
 }/* Theory$camel::Theory$camel() */
 
 void Theory$camel::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
 
   while(!done()) {
     // Get all the assertions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 40bc2417b..91150f663 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -357,6 +357,9 @@ void TheoryBV::checkForLemma(TNode fact) {
 
 void TheoryBV::check(Effort e)
 {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true); 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f74384d59..87d1f6517 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -118,6 +118,10 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
 }
 
 void TheoryDatatypes::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
+
   Trace("datatypes-debug") << "Check effort " << e << std::endl;
   while(!done() && !d_conflict) {
     // Get all the assertions
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 8597c117d..9e402f430 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -49,6 +49,10 @@ Node TheoryIdl::ppRewrite(TNode atom) {
 }
 
 void TheoryIdl::check(Effort level) {
+  //// Not needed for now, as no code outside while() loop below.
+  // if (done() && !fullEffort(e)) {
+  //   return;
+  // }
 
   while(!done()) {
 
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 4e8a0a411..18546b09c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -109,6 +109,10 @@ void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
 }
 
 void TheoryQuantifiers::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
+
   CodeTimer codeTimer(d_theoryTime);
 
   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index faba2aab1..106ad6e56 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -39,6 +39,9 @@ void TheorySets::addSharedTerm(TNode n) {
 }
 
 void TheorySets::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
   d_internal->check(e);
 }
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 30e529663..ac1b1b1ed 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -550,6 +550,10 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
 
 
 void TheoryStrings::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
+
   bool polarity;
   TNode atom;
 
@@ -3330,4 +3334,4 @@ TheoryStrings::Statistics::~Statistics(){
 
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
-}/* CVC4 namespace */
\ No newline at end of file
+}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index ac3d018fb..867dd7c31 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -377,7 +377,7 @@ public:
   /**
    * Returns true if the assertFact queue is empty
    */
-  bool done() throw() {
+  bool done() const throw() {
     return d_factsHead == d_facts.size();
   }
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0da8e8c32..4fcf4166b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -89,6 +89,10 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 }/* mkAnd() */
 
 void TheoryUF::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
   while (!done() && !d_conflict)
   {
     // Get all the assertions
-- 
2.30.2