Changelog for libz3-4_5-4.5.0+git.20170523-25.1.x86_64.rpm :
Fri Jun 16 14:00:00 2017 mpluskalAATTsuse.com
- Update cmake parameters

Thu May 25 14:00:00 2017 jslabyAATTsuse.com
- Update to version 4.5.0+git.20170523:

* update readme

* ignore Z3-str source

* failing test case: SMT2 parse string constants

* create and register string theory plugin the parser gets a little bit further now! rejects input with \"unexpected character\"

* fix string constant representation in parser spec1 loopback OK

* pretty-printing of string constants in AST spec2 looks good now

* load str decl plugin; recognize String sorted constants

* register Concat function now reaches str_decl_plugin::mk_func_decl()

* at least for now, Concat is no longer associative this means that we\'ll always have (Concat a b) instead of variadic forms

* add Length function to theory of strings

* AND MUCH MORE...

Mon Mar 13 13:00:00 2017 jslabyAATTsuse.com
- Z3Config.cmake is not needed anymore
- Update to version 4.5.0+git.20170313:

* Fixed utf-8 version string handling for python2. Resolved #787

* Set soname version correctly in cmake build

* cmake build: set SOVERSION to include the minor version number

* fix overflow exposed in #880

* Thread labels through tactic system

* Add basic Sine Qua Non filtering

* adding parallel threads

* Fix off-by-one bug in array indexing in the OCaml bindings

* refine parsat

* add const &

* Introduce and use labels_vec

* ensure that parallel threads are only invoked when thread count > 1

* add name

* delete comment

* delete unused args

* reindent

* use insert_if_not_there

* fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver

* fix bug in propagation of parameters to combined solvers

* bypass combined solver when logic is set to QF_BV or QF_FD

* bypass combined solver when logic is set to QF_FD

* move exchange par

* enable pb theory always as pb terms can be introduced during transformations. Issue #884

* use is_uninterp

* correctly pretty-print

* add and use new is_pattern recognizer

* add par_or tactic to C++ API. #873

* fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases

* Fixed signed/unsigned warnings

* Fixed model-converter segfault in ::check_sat. Relates to #881

* Fixed model-converter segfault in ::check_sat. Relates to #881

* add itos/stoi conversion to API. Issue #895

* fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger

* expose numerator/denominators for Martin and Giles

* add missing mod/rem/is_int functionality to C++ API

* make parameters accessible from expressions. Issue #896

* add par_and_then

* use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions

* add recursive function graphs to model, adapt rewriter to bypass branches whose evaluation is redundant

* add octal escape to seq_decl_plugin

* C-style octal escapes, including 1- and 2-digit escapes

* add _re.unroll internal operator to seq_decl_plugin

* expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911

* expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911

* remove unreferenced label

* fix type on exception message

* fix unhandled finite domain sort rewrite case. Issue #918

* Java API for getting the objective value as a triple

* Sane indentation + removing extra spaces for Optimize.java

* Class Optimize#Handle should be static,

* fixed bug where `mk_make.py --build=...` would fail to handle absolute paths correctly.

* Free allocated char arrays in JNI API

* [CMake] For single configuration generators only allow `CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations that we support.

* add boolean operators to zstring and fix ostream

* Tabs, whitespace

* fix bug for bit-vector optimization. Issue #919

* fix bug for bit-vector optimization. Issue #928

* ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917

* check that formulas are in lira before invoking qsat. Issue #919

* add notes to README based on feedback in #916

* remove scratch notes from readme

* include recursive functions to models. Issue #898

* remove print breaking build

* fixing build break, adding fixedpoint object to C++ API

* adding fixedpoint object to C++ API

* fixing build break, addressing #935

* z3py: With tactical should not try to use context as a parameter

* move restore relevancy until after literals have been replayed

* [CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git\'s HEAD so that the necessary code is rebuilt when the build system is invoked.

* [CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree.

* [CMake] Python examples should only be copied over if python bindings are being built.

* [CMake] Build `c_example`, `cpp_example` and `z3_tptp5` as external projects.

* [CMake] Fix typo handling OpenMP flags.

* [CMake] Fix examples linking against libz3 when it is built as a static library on Linux.

* [CMake] On Windows when building the examples copy the Z3 library into the directory of the example executable so that it works \"out of the box\".

Sat Feb 25 13:00:00 2017 jslabyAATTsuse.com
- add Z3Config for cmake

Fri Jan 27 13:00:00 2017 mpluskalAATTsuse.com
- Update to version 4.5.0+git.20170126:

* streamline logging in arithmetic

* adding preferred sat, currently disabled, to wmax. Fixing issue #815

* make a few functions static

* remove 2 outdated comments

* add a few more statics to avoid symbol clashes

* Re-added context creation locks in the Java API. Relates to #819.

* Bugfix for model construction. Fixes #828.

* adding range to C API. Issue #831

* add range constructor to .NET API

* add regular expression operations to C and C++ API

* add regular expression features to C# API

* add missing complement

* add python API for newly exposed regex constructors

* exposing regular expression features to address issue #831

* produce error message for cores with optimization. Issue #825

* Whitespace

* Bugfix for special-case handling in fp.fma.

* fix bug in encoding of axioms for indexof. Issue #806

* Bugfix for special-case handling in fp.fma.

* Build fix for C++ example

* add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d\'Antoni

* address #835

* address #835

* address warnings from #836

* add virtual destructor to intermediary class in case this helps for #835

* address other warnings per input from delcypher

* bail out on failure to properly project

* bail out on failure to properly project. issue #837

* remove nested booleans during pre-processing. issue #837

* add suggestions from #835

* fix bug in handling of repeated soft constraints. #815

* Add rewrite rule for property encoded in #812

* Fix implementation of `scoped_timer` under Linux where it was incorrectly assumed that `pthread_cond_timedwait()` would exit due to a condition variable being signaled or a timeout occuring.

* handle model generation from issue #748. Deal with warnings from #836

* Build fix for C/C++ example programs.

* Style, whitespace.

* ensure that FD logic understands pb from command context

* Making z3 python look in its installation directory for the z3 lib

* fix generation of wcnf

* Build fix for static binaries + shared examples

* Fix for parallel builds of the OCaml API. Relates to #797.

* Fix inconsistent emission of OCaml enumeration files. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary\'s keys being iterated over which has no defined order.

* Refactor `mk_z3consts_ml()` code into `mk_z3consts_ml_internal()` and move that into `mk_genfile_common.py`. Then adapt `mk_util.py` and `mk_consts_files.py` to call into the code at its new location.

* Refactor `update_api.mk_ml()` so that the source and output directories can be different. This feature will be needed by the CMake build system to build the OCaml bindings.

* Fix issue with bd1f07f864a7f1790cec08a306ccc17507f7e5a8 pointed out by AATTnunolopes .

* remove sources for unused variable warnings

* fix debug build, unused variable warnings

* fix build again

* Add -fpic to armv7/armv8 build

* updated encodings

* remove redundant disjunction in compilation of at-most-1 constraints, log mutexes

* fix missing else reported in #855

* improve parser error message over API, streamline names of statistics for arithmetic solver

* add restart.max parameter to control cancellation based on restart count

* initialize watch in assign_eh

* make get_consequence call skip check-sat if a model is already there

* enable incremental consequence finding with restart timeout

* Fixed initialization order warning.

* add operator for issue #860

* allow disabling exceptions from C++. Issue #861

* moderate exception behavior for issue #861

* fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared

* add at-least and pbge to API, fix for issue #864

* remove polynomial factorization as suggested by issue #852

* Removed polynomial factorization test cases. Relates to #852 and fixes #865.

* GCC compilation/keyword fix. Relates to #864

* update CMakeList to remove polynomial-factorization

* Formatting, whitespace

* Added option to extend unsat cores with literals that (potentially) provide quantifier instances.

* Cleaned up #include in api
* objects.

* Formatting, whitespace, and Z3_API annotations.

* Bugfix for smt.core.extend_patterns

* Omit \'.dll\' from library name for DllImport.

* Mark void DummyContracts as Conditional to avoid compiling their arguments.

* Corner-case fix for smt::solver::pop_core

* Update README.md

* remove unused features related to weighted check-sat

* Added win64 build badge

* Separated win32/64 builds

* Added MAKEJOBS env var to mk_unix_dist.py

* Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847

* use stirngs for env variables

* fix crash with unary xor #870

* fix memory leaks from cancellations

* update macro_util logging to uniform format

* build fix

* Added (include ...) SMT2 command.

* Added filenames to error messages for when we have more than one file.

* Enabled filenames in error messages during inclusion of files.

* Updated cmake build

* Windows build fix.

* Bugfix for macro finder. Fixes #832.

* fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences)

* Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints

* Added .NET 3.5 solution/project files

* x64 build fix for .NET 3.5 API

* Windows build fix.

* access parameters from Python API

* Added option to limit the distance of unsat core extension through patterns.

* fix test for int-value

* fix regression for z3num

* fix bug in sat-simplifier decreasing heap values of variables that are not in the heap

* fix part 1 of #875

* add warning for scearios of #876

* add format #879

* rework sat.mus to use restart count for bounded minimization

Wed Nov 30 13:00:00 2016 jslabyAATTsuse.com
- Update to version 4.5.0+git.20161129:

* remove legacy interface to dt2bv tactic

* Fixed potential problems with invalidated iterators.

* Fix for previous commit.

* whitespace

* Silenced GCC warning about empty loop body.

* local

* fix mutex finding for smt-core: it was returning mutexes for negations of literals

* Bugfixes for the FPA API

* fix at-most-1 constraint compiler bug

* fix at-most-1 constraint compiler bug

* add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic

* add example to exercise at-most-1 constraints

* add documentation

* add missing file

* disable local optimization in presence of non-linear constraints, addresses issue #758

* whitespace

* Added accessors to extract sign/exponent/significand BV numerals from FP numerals.

* Added functions to test FP numerals for special values.

* Fixed FP numeral special value sig/exp extraction functions.

* Resolved rebase conflicts

* Refactored FPA numeral accessors.

* Replaced antiquated header with modern equivalent.

* removed unused variables

* fixed GCC build issue in tests

* a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors

* merge

* fix incorrect assertion when checking signs of literals, exposed by mitls regressions

* fix incorrection assertion when checking signs of literals, exposed by miTLS regressions

* remove dead (and incorrect) code

* add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates

* fix sign of constant in pb constraint

* removed debug output

* fix for biased flag on get_numeral_exponent_string

* fix for Python API installation

* fixed initialization order warning in pb2bv_rewriter

* fixed unhandled case warning in test/qe_arith.cpp

* additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755

* fix unit tests for pb

* disabled unnecessary assertion

* Bugfix for Python API.

* Marked .NET Z3Exception as serializable

* Fixed FPA unbiased exponent accessors

* Bugfix for bv2fpa_converter. Fixes #767.

* Added FPA numeral predicates to .NET API

* Added FPA numeral predicates to Java API

* Added FPA numeral predicates to ML API

* remove conflict on false disequality, introduced regression

* Added Z3_fpa_is_numeral_negative to FPA API

* Added is_numeral_negative to .NET and Java APIs

* Added FPA numeral accessors/predicates to Python API

* speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase

* fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don\'t

* rewind qhead to ensure re-propagation after cancellation

* catch cancellation exceptions, return undef

* fixing cancellation code paths for inc_sat_solver

* removed debug output

* Build fix for libz3.vcxproj.

* whitespace

* Bugfix for bouned_int2bv_solver

* ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints

* merge

* fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic

* fix memory abuse in internalization in inc-sat-solver

* remove buggy and unused equivalence relation plugin. Github issue #770

* disable sat solver when proofs are turned on. Fixes issue #768

* fix bug in mutex extraction, reported by Patrick Trentin

* build fix

* bugfix for disequality propagation in smt_context

* enable unsat core extraction in nlsat_tactic

* Fixes for .NET Core build

* fixing unsat core extraction for tactics

* fix evaluator for array store expressions

* remove recursive expansion of else-case

* fixed log output typo

* Added signed .NET assemblies in unix builds

* Whitespace

* Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks).

* check for logic in solver

* fix generation of fresh constants for uninterpreted sort in EPR, Issue #649

* Added release notes for the upcoming 4.5.0 release

* fix crash in poly normalizer exposed by qe. Issue #775

* Updated optimization ML API. Addresses #776.

* Whitespace, typo

* eliminated unnecessary variable

* fix breaking change to theory-seq

* Whitespace

* Whitespace

* updated release notes

* added is_numeral_negative to ML API.

* FPA API clarification

* Bugfix for denormal numeral exponents

* build fix

* bugfix for macro finder

* detect quantifiers in model expressions to quiet down failing model validation

* Include Python API files in distributions.

* Bumped version to 4.5.0

* Standardize on __uint64 instead of unsigned __int64

* Bumped version number.

* [CMake] Bump the version number in the CMake build.

* fixed hard-coded version number in setup.py

* Whitespace

* Typo

* Bugfix for Z3_fpa_get_numeral_
*_uint64. Relates to #570.

* Bugfix for Z3_fpa_get_numeral_sign. Relates to #570.

* typo

* fix crash reported in #784

* Fixed problems with aborted rewriters in theory_fpa. Relates to #570.

* Fix cleanup/initialization of sat::simplifier. Relates to #570.

* Fixed compiler warning

* Fixed interruption cleanup bug in sat_solver. Relates to #570.

* Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570.

* fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782

* make semantics of extract/substr deterministic. Issue #781

* Fixed Windows distribution script.

* Bugfix for rewriter exceptions in theory_fpa. Relates to #570.

* Assertion fix for theory_fpa. Relates to #570.

* improving perf of mutex finding, revert semantics of 0 timeout to no-timeout. Issue #791

* fix perf bug reported in #790

* Fixed interruption/cancelation issue in rewriter.

* Cleaned up hacky rewriter cancelation fix in theory_fpa.

* fix and coallesce clique functionality

* tune initialization for wmax and sortmax

* fix bug incorrect clearing of goals during node creation. Issue #777

* fix unsoundness reported in issue #777, disable ematching on recursive function definition axioms exposed in #793

* Fix GCC/Clang compilation.

* fix crash in new clique code

* re-enable ematching on recursive function definitions, disabling ematching breaks regressions

* Fix for the documentation scripts. Fixes #799.

* Added optional synchronization for multi-thread API logs. Relates to #798.

* Fixed OpenMP problems in log synchronization. Relates to #798.

* fix handling of AC operator ++ on regular expressions. Issue #804

* fix warnings in configure script

* Do not request time stamp if not needed

* Fixed iterator invalidation bug in SAT probing. Relates to #798.

* optimize pattern matching code generator for DAG patterns generated code now uses COMPARE instructions to compare subtrees instead of diving into both subtrees. Code is thus smaller and fails faster.

* small optimization in compilation of multi-patterns also make the path faster for single patterns

* mam compiler: move reset of matched_exprs cache next to code reset

* blast distinct in incremental BV solver

Wed Oct 19 14:00:00 2016 jslabyAATTsuse.com
- Update to version 4.4.1+git.20161018:

* adding enumeration tests

* spacing, unit test

* Bugfix for bv2fpa (model) conversion.

* Removed unnecessary variables.

* [CMake] Fix building the Java bindings.

* adding unit test for enumeration types

* Tabs

* undo breaking commit

* Whitespace

* Fixed iterator invalidation bug in theory_arith_nl.

* add fd solver for finite domain queries
- remove link-against_libs.patch

Mon Oct 17 14:00:00 2016 jslabyAATTsuse.com
- make -devel require libz3, not z3
- add link-against_libs.patch

Mon Oct 10 14:00:00 2016 mpluskalAATTsuse.com
- Update to version 4.4.1+git.20161007:

* Z3_query_constructor documentation clarification

* add mutex pass

* Build/test fix for python3

* Test fix for python3

* Added dummy code contracts for .NET Core/CoreCLR builds.

* Remove unnecessary \"unsafe\" qualifier on internal .NET API class.

* add mutex preprocessing to maxsat, add parsing functions to C++ API

* add example of parsing with external declarations
- Speedup build by using ninja

Fri Sep 16 14:00:00 2016 mpluskalAATTsuse.com
- Update to version 4.4.1+git.20160914:

* addressing max-segment issue for AMD64 + Debug

* safe sat clause_offset in debug mode

* safe sat clause_offset in debug mode

* fixes to consequence generation and cancellation

* move from uint_set to hashtable over unsigned to save memory overhead in consequence generation

* ensure stoi axiom even when no value is present for argument. Issue #731

* add missing rewrite rule. Issue #731

* fix heisenbug, unintialized variable, issue #720

* add patch to deal with bug exposed in issue #721

* fix regression in seq-replace rewriting

* ensure that status is displayed in SMT-LIB2 compliant way. Issue #734

* Create socrates.py

* remove special characters

* Update socrates.py
- Rename python bindnigs to follow openSUSE guidelines
- Change _service to disabled to avoid unnecessary executions
- Small packaging changes

Wed Jul 20 14:00:00 2016 jengelhAATTinai.de
- Update descriptions

Mon Jul 18 14:00:00 2016 mpluskalAATTsuse.com
- Update to version 4.4.1+git.20160717:

* fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization

* garbage collect all api::object references when calling del_context. Request issue #679

* add proper garbage collection to ast_manager. Issue #679

* remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once

* fix rounding mode for pseudo-boolean constraint creation, Issue #683

* add object z3 objects to target context during translation, to fix build regression failure on z3test.py

* add tptp5 example to cmake, adding output SZS directives for Geoff

* fix ubuntu build failure

* mark also ast in parameters as GC roots. Issue #676
- Use cmake macros
- Some spec file polishing with spec-cleaner

Mon Jul 18 14:00:00 2016 jslabyAATTsuse.com
- update to 20160717

* a lot of changes, see the repo
- remove CMake-Provide-a-way-to-customise-the-install-directo.patch
- add remove-timestamp.patch

Thu Mar 10 13:00:00 2016 jslabyAATTsuse.com
- disable build of examples (unused)

Wed Mar 9 13:00:00 2016 jslabyAATTsuse.com
- update to 20160309
- remove: 0001-cmake-add-base-files.patch (not needed anymore)
- add CMake-Provide-a-way-to-customise-the-install-directo.patch
- correct packaging

Mon Oct 12 14:00:00 2015 jslabyAATTsuse.com
- initial package