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

6 files changed, 6 insertions, 5 deletions

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 );