Files changed (1)
+- Fixed bug in Z3Py. The method that builds Z3 applications could crash if one of the arguments have to be "casted" into the correct sort (Thanks to Dennis Yurichev).
+- Display warning message and ignore option CASE_SPLIT=3,4 or 5 when auto configuration is enabled (AUTO_CONFIG=true) (Thanks Tobias from StackOverflow).
+- Made the predicates <, <=, > and >= chainable as defined in the SMT 2.0 standard (Thanks to Matthias Weiler).
+- Added missing Z3_decl_kind's for datatypes: Z3_OP_DT_CONSTRUCTOR, Z3_OP_DT_ACCESSOR, Z3_OP_DT_RECOGNISER.
+- Added support for numbers in scientific notation at Z3_ast Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty).
+- New builtin symbols in the arithmetic theory: pi, euler, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh. The first two are constants, and the others are unary functions. These symbols are not available if the a SMT 2.0 logic is specified (e.g., QF_LRA, QF_NRA, QF_LIA, etc) because these symbols are not defined in these logics. That is, the new symbols are only available if the logic is not specified.
+- Fixed bug in preprocessor that eliminated rational powers (e.g., (^ x (/ 1.0 2.0))), the bug affected only problems where the denominator was even (Thanks to Johannes Eriksson).
+- Fixed bug in the k-th root operation in the algebraic number package. The result was correct, but the resulting polynomial could be incorrectly tagged as minimal and trigger nontermination on comparison operations. (Thanks to Johannes Eriksson).
+- Fixed bug affecting problems containing patterns with n-ary arithmetic terms such as (p (+ x y 2)). This bug was introduced in Z3 4.0. (Thanks to Paul Jackson).
+- Fixed crash reported by Alex Summers. The crash was happening on scripts that contain quantifiers, and use boolean formulas inside terms.
+- Fixed bug in the E-matching engine. It was missing instances of multi-patterns (Thanks Alex Summers).
+- The pattern inference module does not generate warning messages by default anymore. This module was responsible for producing messages such as: "WARNING: failed to find a pattern for quantifier (quantifier id: k!199)". The option PI_WARNINGS=true can be used to enable these warning messages.
+- Removed support for "SMT 1.5" input format (aka .smtc files). This was a hybrid input format that was implemented while the SMT 2.0 standard was being designed. Users should move to SMT 2.0 format. Note that SMT 1.0 format is still available.
+- Made tseitin-cnf tactic more "user friendly". It automatically applies required transformations needed to eliminate operators such as: and, distinct, etc.
+- Implemented new PSC (principal subresultant coefficient) algorithm. This was one of the bottlenecks in the new nlsat solver/tactic.
+- <a class="el" href="http://research.microsoft.com/apps/pubs/default.aspx?id=159549">NLSAT solver</a> for nonlinear arithmetic.
+- iZ3: an interpolating theorem prover built on top of Z3 (\ref iz3documentation). iZ3 is only available for Windows and Linux.
+- New logging infrastructure. Z3 logs are used to record every Z3 API call performed by your application.
+ The following APIs were removed: Z3_trace_to_file, Z3_trace_to_stderr, Z3_trace_to_stdout, Z3_trace_off.
+ However, they still have two limitations. They are not useful for logging applications that use callbacks (e.g., theory plugins)
+ They are not precise for applications that are using multiple threads for processing multiple Z3 contexts.
+- Z3 1.x backwards compatibility macros are defined in z3_v1.h. If you still use them, you have to explicitly include this file.
+- User theories cannot be used with the new Solver API yet. Users may still use them with the deprecated solver API.
+- Parallel Z3 is also disabled in this release. However, we have parallel combinators for creating stragegies (See <a href="http://rise4fun.com/Z3/tutorial/strategies"> tutorial</a>).
+- Fixed model generation for QBVF (aka UFBV) logic. Now, Z3 officially supports the logics BV and UFBV.
+- Fixed a bug in Z3_check_assumptions that prevented it from being used between satisfiable instances. Thanks to Krystof Hoder.
+- Fully compliant SMT-LIB 2.0 (SMT2) front-end. The old front-end is still available (command line option -smtc).
+ The <a class="el" href="http://rise4fun.com/z3/tutorial/guide">Z3 Guide</a> describes the new front-end.
+- New Bitvector (QF_BV) solver. The new solver is only available when using the new SMT2 front-end.
+- Performance improvements for linear and nonlinear arithmetic. The improvements are only available when using the the SMT2 front-end.
+- Fixed bug in the Z3 simplifier cache. It was not being reset during backtracking. Thanks to Alberto Griggio.
+- In the SMT-LIB 1.0 frontend, Z3 will only display the model when requested by the user (MODEL=true).
+- Fixed bug when model generation is used in the context of user-defined-theories. Thanks to Philippe Suter.
+ The command <tt>(check-sat [assumptions])</tt> checks the satisfiability of the logical context modulo
+- DISTRIBUTE_FORALL=true (distributes universal quatifiers over conjunctions, this transformation may affect pattern inference).
+- Rewriter that uses universally quantified equations PRE_DEMODULATOR=true (yes, the option name is not good, we will change it in a future release).
+- REDUCE_ARGS=true (this transformation is essentially a partial ackermannization for functions where a particular argument is always an interpreted value).
+- Better support for macro detection (a macro is a universally quantified formula of the form Forall X. F(X) = T[X]). We also change the option name, now it is called MACRO_FINDER=true.
+- ELIM_QUANTIFIERS=true enables quantifier elimination methods. Previous variants called QUANT_ARITH are deprecated.
+- Incorrect simplification of map over store in the extendted array theory. Reported by Catalin Hritcu.
+- <a href="http://research.microsoft.com/en-us/um/people/leonardo/parallel_z3.pdf">Parallel Z3</a>.