Change default option of simple ite lifting within quantifier bodies. add some debug...

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 13e07526547ce76c936cebe32ffcc177cc4a80d6..e1e2f96c2ba73dfbc3ea129e1af5ae3f99c2c795 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -290,6 +290,8 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           }
         }
       }
+    }else{
+      Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
     }
   }
 }

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index a0b195a9c6c522ffc1c67ec84248afec17a6b584..cdf6976756af526a3f439585dbf2f353b9724b9d 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -854,6 +854,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       }
     }
     if( !success ){
+      Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
       Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 1c5e5286944d445b814ad94d53025e957d45d78f..57211ade77fbbe5a1aca5c001fd64959cd9118bd 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -27,6 +27,9 @@ option prenexQuant /--disable-prenex-quant bool :default true
 option varElimQuant /--disable-var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 
+option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
+ disable simple ite lifting for quantified formulas
+
 # Whether to CNF quantifier bodies
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b08752169febc1b124a93a61600808f33a26c042..e27897a969d164d237c8e5ace78e9345a51c3d10 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -914,7 +914,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-    return !options::finiteModelFind();
+    return options::simpleIteLiftQuant();//!options::finiteModelFind();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){