1 files changed, 25 insertions, 11 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 76d4c973f..ca89ce36d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -74,6 +74,7 @@
 #include "util/sort_inference.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
+#include "theory/quantifiers/first_order_reasoning.h"
 
 using namespace std;
 using namespace CVC4;
@@ -349,8 +350,8 @@ private:
   bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache);
 
   // Lift bit-vectors of size 1 to booleans
-  void bvToBool(); 
-  
+  void bvToBool();
+
   // Simplify ITE structure
   void simpITE();
 
@@ -1009,11 +1010,18 @@ void SmtEngine::setLogicInternal() throw() {
 
   //for finite model finding
   if( ! options::instWhenMode.wasSetByUser()){
+    //instantiate only on last call
     if( options::fmfInstEngine() ){
       Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
       options::instWhenMode.set( INST_WHEN_LAST_CALL );
     }
   }
+  if ( ! options::fmfInstGen.wasSetByUser()) {
+    //if full model checking is on, disable inst-gen techniques
+    if( options::fmfFullModelCheck() ){
+      options::fmfInstGen.set( false );
+    }
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
@@ -1824,15 +1832,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   hash_set<TNode, TNodeHashFunction> s;
-  Trace("debugging") << "NonClausal simplify pre-preprocess\n"; 
+  Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Node assertion = d_assertionsToPreprocess[i];
     Node assertionNew = d_topLevelSubstitutions.apply(assertion);
     Trace("debugging") << "assertion = " << assertion << endl;
-    Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+    Trace("debugging") << "assertionNew = " << assertionNew << endl;
     if (assertion != assertionNew) {
       assertion = Rewriter::rewrite(assertionNew);
-      Trace("debugging") << "rewrite(assertion) = " << assertion << endl; 
+      Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
     }
     Assert(Rewriter::rewrite(assertion) == assertion);
     for (;;) {
@@ -1841,11 +1849,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         break;
       }
       ++d_smt.d_stats->d_numConstantProps;
-      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
       assertion = Rewriter::rewrite(assertionNew);
-      Trace("debugging") << "assertionNew = " << assertionNew << endl; 
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
     }
-    Trace("debugging") << "\n"; 
+    Trace("debugging") << "\n";
     s.insert(assertion);
     d_assertionsToCheck.push_back(assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1936,7 +1944,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 void SmtEnginePrivate::bvToBool() {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
   std::vector<Node> new_assertions;
-  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); 
+  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions);
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
     d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]);
   }
@@ -2790,6 +2798,12 @@ void SmtEnginePrivate::processAssertions() {
     }while( success );
   }
 
+  Trace("fo-rsn-enable") << std::endl;
+  if( options::foPropQuant() ){
+    FirstOrderPropagation fop;
+    fop.simplify( d_assertionsToPreprocess );
+  }
+
   if( options::sortInference() ){
     //sort inference technique
     d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
@@ -2810,7 +2824,7 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-static-learning", d_assertionsToCheck);
 
-  // Lift bit-vectors of size 1 to bool 
+  // Lift bit-vectors of size 1 to bool
   if(options::bvToBool()) {
     Chat() << "...doing bvToBool..." << endl;
     bvToBool();
@@ -2820,7 +2834,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  
+
   dumpAssertions("pre-ite-removal", d_assertionsToCheck);
   {
     Chat() << "removing term ITEs..." << endl;