Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).

17 files changed, 39 insertions, 32 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 036877b6a..2a2a60391 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -111,10 +111,6 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
-  if(Dump.isOn("lemmas")) {
-    Dump("lemmas") << AssertCommand(node.toExpr());
-  }
-
   // Assert as removable
   d_cnfStream->convertAndAssert(node, removable, negated);
 }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 239385bfc..85d9d1f9b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -52,7 +52,7 @@ void TheoryArith::addSharedTerm(TNode n){
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
-  CodeTimer timer(d_ppRewriteTimer);
+  CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
   return d_internal->ppRewrite(atom);
 }
 
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 44b89e8cb..51187b7dd 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -113,10 +113,12 @@ public:
    *
    * @param n - a theory lemma valid at decision level 0
    * @param removable - whether the lemma can be removed at any point
+   * @param preprocess - whether to apply more aggressive preprocessing
    * @return the "status" of the lemma, including user level at which
    * the lemma resides; the lemma will be removed when this user level pops
    */
-  virtual LemmaStatus lemma(TNode n, bool removable = false)
+  virtual LemmaStatus lemma(TNode n, bool removable = false,
+                            bool preprocess = false)
     throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
 
   /**
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 5ad4cef92..78f989807 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -363,7 +363,7 @@ void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l,
       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );
       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem);
+      d_quantEngine->getOutputChannel().lemma(lem, false, true);
       l = Node::null();
       u = Node::null();
       return;
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 9a3c07c5e..99dc29bf8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           nb << f << ceLit;
           Node lem = nb;
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          d_quantEngine->getOutputChannel().lemma( lem );
+          d_quantEngine->getOutputChannel().lemma( lem, false, true );
           addedLemma = true;
         }
       }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 06d11f70f..6d333521b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -94,7 +94,7 @@ option flipDecision --flip-decision/ bool :default false
 option internalReps /--disable-quant-internal-reps bool :default true
  disables instantiating with representatives chosen by quantifiers engine
 
-option finiteModelFind --finite-model-find bool :default false :read-write
+option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
  use finite model finding heuristic for quantifier instantiation
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
index 66a3ac79f..0023b05bc 100644
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -298,7 +298,7 @@ bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
   //flush pending lemmas
   if( !d_pending_lemmas.empty() ){
     for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){
-      getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i] );
+      getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i], false, true );
       ++( getStrongSolver()->d_statistics.d_sym_break_lemmas );
     }
     d_pending_lemmas.clear();
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6a3a6fca1..19a915ae9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -164,7 +164,7 @@ void TheoryQuantifiers::assertExistential( Node n ){
       nb << n[0] << body.notNode();
       Node lem = nb;
       Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
-      d_out->lemma( lem );
+      d_out->lemma( lem, false, true );
       d_skolemized[n] = true;
     }
   }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 8ace5f181..84b65cacd 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -73,6 +73,7 @@ public:
   bool flipDecision();
   void setUserAttribute( const std::string& attr, Node n );
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
+  bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
 private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 36410bd50..41f53740a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -458,7 +458,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
     Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
     lem = Rewriter::rewrite(lem);
     if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
-      //d_curr_out->lemma( lem );
+      //d_curr_out->lemma( lem, false, true );
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
       Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
@@ -567,7 +567,7 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){
     //take default output channel if none is provided
     d_hasAddedLemma = true;
     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
-      out->lemma( d_lemmas_waiting[i] );
+      out->lemma( d_lemmas_waiting[i], false, true );
     }
     d_lemmas_waiting.clear();
   }
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 30e6f9709..2cefe7f07 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -211,7 +211,7 @@ private:
 
   Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
-  bool ppDontRewriteSubterm(TNode atom){ return true; }
+  bool ppDontRewriteSubterm(TNode atom) { return true; }
 
 
  private:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 63024e5d5..c29177b49 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -475,7 +475,7 @@ void TheoryEngine::combineTheories() {
 
     // We need to split on it
     Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-    lemma(equality.orNode(equality.notNode()), false, false, carePair.theory);
+    lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory);
   }
 }
 
@@ -779,7 +779,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) {
 
   Node newTerm;
   if (theoryOf(term)->ppDontRewriteSubterm(term)) {
-    newTerm = term;
+    newTerm = Rewriter::rewrite(term);
   } else {
     NodeBuilder<> newNode(term.getKind());
     if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -1320,7 +1320,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
   }
 }
 
-theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo) {
+theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
 
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
@@ -1344,15 +1344,18 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
     options::lemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
+  // Run theory preprocessing, maybe
+  Node ppNode = preprocess ? this->preprocess(node) : Node(node);
+
   // Remove the ITEs
   std::vector<Node> additionalLemmas;
   IteSkolemMap iteSkolemMap;
-  additionalLemmas.push_back(node);
+  additionalLemmas.push_back(ppNode);
   d_iteRemover.run(additionalLemmas, iteSkolemMap);
   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
 
   if(Debug.isOn("lemma-ites")) {
-    Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl;
+    Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
     Debug("lemma-ites") << " + now have the following "
                         << additionalLemmas.size() << " lemma(s):" << endl;
     for(std::vector<Node>::const_iterator i = additionalLemmas.begin();
@@ -1417,11 +1420,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, true, true, THEORY_LAST);
+    lemma(fullConflict, true, true, false, THEORY_LAST);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    lemma(conflict, true, true, THEORY_LAST);
+    lemma(conflict, true, true, false, THEORY_LAST);
   }
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d5de8e3b2..db31ef9b7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -292,18 +292,18 @@ class TheoryEngine {
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, theory::THEORY_LAST);
+      return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST);
     }
 
     theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, d_theory);
+      return d_engine->lemma(lemma, false, removable, false, d_theory);
     }
 
     void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {
@@ -451,7 +451,7 @@ class TheoryEngine {
    * @param removable can the lemma be remove (restrictions apply)
    * @param needAtoms if not THEORY_LAST, then
    */
-  theory::LemmaStatus lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo);
+  theory::LemmaStatus lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index e4921b163..28a749a41 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -87,7 +87,7 @@ public:
     push(PROPAGATE_AS_DECISION, n);
   }
 
-  LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
+  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index bd33557d9..8246bfdd2 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -824,6 +824,7 @@ public:
  */
 class CodeTimer {
   TimerStat& d_timer;
+  bool d_reentrant;
 
   /** Private copy constructor undefined (no copy permitted). */
   CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
@@ -831,11 +832,15 @@ class CodeTimer {
   CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
 
 public:
-  CodeTimer(TimerStat& timer) : d_timer(timer) {
-    d_timer.start();
+  CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
+    if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
+      d_timer.start();
+    }
   }
   ~CodeTimer() {
-    d_timer.stop();
+    if(!d_reentrant) {
+      d_timer.stop();
+    }
   }
 };/* class CodeTimer */
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 803b24527..e32e49801 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -58,7 +58,7 @@ class FakeOutputChannel : public OutputChannel {
   void propagateAsDecision(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
+  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) {
     Unimplemented();
   }
   void requirePhase(TNode, bool) throw(AssertionException) {
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index e2dfcc464..3259381ad 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -70,7 +70,7 @@ public:
     // ignore
   }
 
-  LemmaStatus lemma(TNode n, bool removable)
+  LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false)
     throw(AssertionException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
@@ -301,7 +301,7 @@ public:
 
   void testOutputChannel() {
     Node n = atom0.orNode(atom1);
-    d_outputChannel.lemma(n, false);
+    d_outputChannel.lemma(n);
     d_outputChannel.split(atom0);
     Node s = atom0.orNode(atom0.notNode());
     TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);