From 1382cdefea3cf595cea3ca03f752277c696f741d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner <nbjorner@microsoft.com> Date: Sat, 3 Sep 2022 10:04:48 -0700 Subject: [PATCH] release notes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> --- RELEASE_NOTES.md | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index cdde16323..86707318c 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -13,7 +13,27 @@ Version 4.next Version 4.11.1 ============== - add error handling to fromString method in JavaScript -- fix regression in default parameters for CDCL (Nuno Lopes) +- fix regression in default parameters for CDCL, thanks to Nuno Lopes +- fix model evaluation bugs for as-array nested under functions (data-type constructors) +- add rewrite simplifications for datatypes with a single constructor +- add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind. + The commit logs related to Global Guidance contain detailed information. +- change proof logging format for the new core to use SMTLIB commands. + The format was so far an extension of DRAT used by SAT solvers, but not well compatible + with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with + three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses. + They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas". + "rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when + the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the + format. Quantifier instantiations are also tracked as proof hints. + Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in, + self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally + insufficient as generated clauses are in principle required to only be satisfiability preserving. + Proof checking and tranformation operations is overall open ended. + The log for the first commit introducing this change contains further information on the format. +- fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer). +- handle _toExpr for quantified formulas in JS bindings + Version 4.11.0 ==============