added QuantifiedPass class

4 files changed, 82 insertions, 57 deletions

diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index 26679c771..b389fa142 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -4,11 +4,15 @@
 #include <string>
 #include "theory/theory.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/fun_def_process.h"
+#include "theory/quantifiers/macros.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/sep/theory_sep_rewriter.h"
+#include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/bv_options.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
  
 namespace CVC4 {
 namespace preproc {
@@ -566,5 +570,67 @@ void SepPreSkolemEmpPass::apply(std::vector<Node>* assertionsToPreprocess){
   }
 }
 
+QuantifiedPass::QuantifiedPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, std::map<Node,TypeNode> fmfRecFunctionsAbs, std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_fmfRecFunctionsDefined(fmfRecFunctionsDefined), d_fmfRecFunctionsAbs(fmfRecFunctionsAbs), d_fmfRecFunctionsConcrete(fmfRecFunctionsConcrete){
+}
+
+void QuantifiedPass::apply(std::vector<Node>* assertionsToPreprocess){
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
+
+    dumpAssertions("pre-skolem-quant", *assertionsToPreprocess);
+    //remove rewrite rules, apply pre-skolemization to existential quantifiers
+    for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
+      Node prev = (*assertionsToPreprocess)[i];
+      Node next = theory::quantifiers::QuantifiersRewriter::preprocess( prev );
+      if( next!=prev ){
+        (*assertionsToPreprocess)[i] = theory::Rewriter::rewrite( next );
+        Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev <<std::endl;
+        Trace("quantifiers-preprocess") << "   ...got " << (*assertionsToPreprocess)[i] << std::endl;
+      }
+    }
+    dumpAssertions("post-skolem-quant", *assertionsToPreprocess);
+    if( options::macrosQuant() ){
+      //quantifiers macro expansion
+      theory::quantifiers::QuantifierMacros qm( d_theoryEngine->getQuantifiersEngine() );
+      bool success;
+      do{
+        success = qm.simplify( *assertionsToPreprocess, true );
+      }while( success );
+      //finalize the definitions
+      qm.finalizeDefinitions();
+    }
+
+    //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
+    if( options::fmfFunWellDefined() ){
+      theory::quantifiers::FunDefFmf fdf;
+      Assert( d_fmfRecFunctionsDefined!=NULL );
+      //must carry over current definitions (for incremental)
+      for( context::CDList<Node>::const_iterator fit = d_fmfRecFunctionsDefined->begin();
+           fit != d_fmfRecFunctionsDefined->end(); ++fit ) {
+        Node f = (*fit);
+        Assert( d_fmfRecFunctionsAbs.find( f )!= d_fmfRecFunctionsAbs.end() );
+        TypeNode ft = d_fmfRecFunctionsAbs[f];
+        fdf.d_sorts[f] = ft;
+        std::map< Node, std::vector< Node > >::iterator fcit = d_fmfRecFunctionsConcrete.find( f );
+        Assert( fcit!= d_fmfRecFunctionsConcrete.end() );
+        for( unsigned j=0; j<fcit->second.size(); j++ ){
+          fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
+        }
+      }
+      fdf.simplify(*assertionsToPreprocess);
+      //must store new definitions (for incremental)
+      for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
+        Node f = fdf.d_funcs[i];
+        d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+        d_fmfRecFunctionsConcrete[f].clear();
+        for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
+          d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
+        }
+        d_fmfRecFunctionsDefined->push_back( f );
+      }
+    }
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl;
+}
+
+
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index 383735cbe..d445e2e14 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -11,6 +11,7 @@ namespace preproc {
 
 typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
 typedef std::hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+typedef context::CDList<Node> NodeList;
   
 class NlExtPurifyPass : public PreprocessingPass {
  public:
@@ -117,6 +118,17 @@ class SepPreSkolemEmpPass : public PreprocessingPass {
    SepPreSkolemEmpPass(ResourceManager* resourceManager);
 };
 
+class QuantifiedPass : public PreprocessingPass {
+  public:
+    virtual void apply(std::vector<Node>* assertionsToPreprocess);
+    QuantifiedPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined, std::map<Node,TypeNode> fmfRecFunctionsAbs, std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete); 
+  private:
+    TheoryEngine* d_theoryEngine;
+    NodeList* d_fmfRecFunctionsDefined;
+    std::map<Node,TypeNode> d_fmfRecFunctionsAbs;
+    std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete;
+};
+    
 }  // namespace preproc
 }  // namespace CVC4
 
diff --git a/src/smt/.smt_engine.cpp.swo b/src/smt/.smt_engine.cpp.swo
index 72c40172c..0d4a4245e 100644
--- a/src/smt/.smt_engine.cpp.swo
+++ b/src/smt/.smt_engine.cpp.swo
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8d519e0ef..2553fc57e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3626,62 +3626,9 @@ void SmtEnginePrivate::processAssertions() {
  }
 
   if( d_smt.d_logic.isQuantified() ){
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
-
-    dumpAssertions("pre-skolem-quant", d_assertions);
-    //remove rewrite rules, apply pre-skolemization to existential quantifiers
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Node prev = d_assertions[i];
-      Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
-      if( next!=prev ){
-        d_assertions.replace( i, Rewriter::rewrite( next ) );
-        Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
-        Trace("quantifiers-preprocess") << "   ...got " << d_assertions[i] << endl;
-      }
-    }
-    dumpAssertions("post-skolem-quant", d_assertions);
-    if( options::macrosQuant() ){
-      //quantifiers macro expansion
-      quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
-      bool success;
-      do{
-        success = qm.simplify( d_assertions.ref(), true );
-      }while( success );
-      //finalize the definitions
-      qm.finalizeDefinitions();
-    }
-
-    //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
-    if( options::fmfFunWellDefined() ){
-      quantifiers::FunDefFmf fdf;
-      Assert( d_smt.d_fmfRecFunctionsDefined!=NULL );
-      //must carry over current definitions (for incremental)
-      for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
-           fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
-        Node f = (*fit);
-        Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() );
-        TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
-        fdf.d_sorts[f] = ft;
-        std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
-        Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() );
-        for( unsigned j=0; j<fcit->second.size(); j++ ){
-          fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
-        }
-      }
-      fdf.simplify( d_assertions.ref() );
-      //must store new definitions (for incremental)
-      for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
-        Node f = fdf.d_funcs[i];
-        d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
-        d_smt.d_fmfRecFunctionsConcrete[f].clear();
-        for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
-          d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
-        }
-        d_smt.d_fmfRecFunctionsDefined->push_back( f );
-      }
-    }
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
-  }
+    preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs, d_smt.d_fmfRecFunctionsConcrete);
+    pass.apply(&d_assertions.ref());
+ }
 
   if( options::sortInference() || options::ufssFairnessMonotone() ){
     //sort inference technique