diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-13 11:23:30 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-15 13:43:31 -0500 |
commit | 5aa5b7588230a4e61abb3a7bda132120618a3efa (patch) | |
tree | b0c3556247cf3777cfa0352da3aa15f858e57458 /src/theory | |
parent | c46f66e6e50506f5e9c10df3dcb6db5affc45c78 (diff) |
Change default option of simple ite lifting within quantifier bodies. add some debug messages.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 |
4 files changed, 7 insertions, 1 deletions
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 ){ |