From 2104624dfa2c8f3e47bb53514705f658ae1a4a64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 May 2020 10:33:25 -0700 Subject: [PATCH] updated release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 30 ++++++++++++++++++++++++---- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_context.cpp | 2 +- 3 files changed, 28 insertions(+), 6 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 48999dd36..7c5aefe64 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,12 +3,34 @@ RELEASE NOTES Version 4.8.next ================ - Planned features - - rewritten NIA (non-linear integer arithmetic) core solver + - rewritten arithmetic solver replacing legacy arithmetic solver and on by default - self-contained character theory, direct support for UTF8, Unicode character sets - - recursive function representation without hoisting ite expressions. Issue #2601 + - improvements to regular expression processing - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction - - model-based interpolation for quantifier-free UF, arithmetic, arrays - - circuit optimization techniques for BV pre-processing + - the smtfd solver and tactic implement this strategy, but is not prime for users. + - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. + - circuit optimization techniques for BV in-processing are available as the sat.cut + option, but at this point does not translate into benefits. It is currently + turned off by default. + +Version 4.8.8 +============= +- New features + - rewritten NIA (non-linear integer arithmetic) core solver + It is enabled in selected theories as default. + The legacy arithmetic solver remains the overall default in this release + as the rewritten solver shows regressions (on mainly NRA problems). + - recursive function representation without hoisting ite expressions. Issue #2601 + - model-based interpolation for quantifier-free UF, arithmetic + - Julia bindings over the C++ API, thanks to ahumenberger +- Bug fixes + - numerous, many based on extensive fuzz testing. + Thanks to 5hadowblad3, muchang, numairmansur, rainoftime, wintered +- Notes + - recursive functions are unfolded with separate increments based on unsat core + analysis of blocking literals that are separate for different recursive functions. + - the seq (string) solver has been revised in several ways and likely shows some + regressions in this release. Version 4.8.7 ============= diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 86db50e3c..25e611f4c 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -41,7 +41,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), + ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5043f0df1..c0958dbfc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1601,7 +1601,7 @@ namespace smt { if (inconsistent()) return false; } -#if 1 +#if 0 if (at_search_level() && induction::should_try(*this)) { get_induction()(); }