From 5aa5b7588230a4e61abb3a7bda132120618a3efa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Sep 2013 11:23:30 -0500 Subject: [PATCH] Change default option of simple ite lifting within quantifier bodies. add some debug messages. --- src/theory/quantifiers/bounded_integers.cpp | 2 ++ src/theory/quantifiers/full_model_check.cpp | 1 + src/theory/quantifiers/options | 3 +++ src/theory/quantifiers/quantifiers_rewriter.cpp | 2 +- 4 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 13e075265..e1e2f96c2 100644 --- 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 a0b195a9c..cdf697675 100644 --- 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 1c5e52869..57211ade7 100644 --- 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 b08752169..e27897a96 100644 --- 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 ){ -- 2.30.2