minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver

2 files changed, 13 insertions, 1 deletions

diff --git a/src/smt/options b/src/smt/options
index ab903c951..a3038cd4e 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -46,6 +46,9 @@ option unconstrainedSimp --unconstrained-simp bool :default false :read-write
 option repeatSimp --repeat-simp bool :read-write
  make multiple passes with nonclausal simplifier
 
+option sortInference --sort-inference bool :default false
+ apply sort inference to input problem
+
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ee0d9debc..e0d7c8e98 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -63,6 +63,7 @@
 #include "printer/printer.h"
 #include "prop/options.h"
 #include "theory/arrays/options.h"
+#include "util/sort_inference.h"
 
 using namespace std;
 using namespace CVC4;
@@ -898,7 +899,7 @@ void SmtEngine::setLogicInternal() throw() {
     if (options::checkModels()) {
       Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
       setOption("check-models", SExpr("false"));
-    }    
+    }
   }
 }
 
@@ -1298,6 +1299,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         }else{
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
           Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
+          //DOTHIS: set attribute on op, marking that it should not be selected as trigger
           std::vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
@@ -1965,6 +1967,13 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
 
+  if( options::sortInference() ){
+    //sort inference technique
+    //TODO: use this as a rewrite technique here?
+    SortInference si;
+    si.simplify( d_assertionsToPreprocess );
+  }
+
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();