Changelog for libz3-4_12-4.12.1-lp154.2.1.x86_64.rpm :

* Thu Feb 23 2023 gwassermannAATTcert.org- Update to v4.12.1 final release
* Sun Jan 15 2023 gwassermannAATTcert.org- Update to v4.12.0 final release
* Sun Dec 11 2022 gwassermannAATTcert.org- Update to v4.11.2 final release
* Fri May 06 2022 gwassermannAATTcert.org- Update to v4.8.17 final release
* Thu Mar 24 2022 gwassermannAATTcert.org- Update to v4.8.15 final release
* Wed Jan 12 2022 gwassermannAATTcert.org- Update to v4.8.14 final release
* Mon Dec 06 2021 gwassermannAATTcert.org- Update to v4.8.13 final release
* Thu Sep 02 2021 gwassermannAATTcert.org- Update to v4.8.12 final release
* Tue Jun 08 2021 gwassermannAATTcert.org- Update to v4.8.11 final release
* Wed May 26 2021 gwassermannAATTcert.org- Add java bindings packages
* Thu Feb 04 2021 gwassermannAATTcert.org- Update to v4.8.10 final release
* Thu Sep 24 2020 gwassermannAATTcert.org- Update to v4.8.9 final release
* Fri May 22 2020 gwassermannAATTcert.org- Update to v4.8.8 final release
* Fri Jan 10 2020 gwassermannAATTcert.org- Update to v4.8.7 final release
* Fri Sep 27 2019 gwassermannAATTcert.org- Update to v4.8.6 final release
* Sun Sep 08 2019 gwassermannAATTcert.org- Update to Nightly 20190908, pre-release of v4.8.6, bugfix release
* Fixes a giant list of bugs in 4.8.5
* Mon Aug 19 2019 gwassermannAATTcert.org- Update to Nightly 20190816, pre-release of v4.8.6, bugfix release
* Fixes a giant list of bugs in 4.8.5
* Tue Jun 11 2019 gwassermannAATTcert.org- Update to v4.8.5, bugfix release
* Thu Jan 03 2019 gwassermannAATTcert.org- Update to v4.8.4, bugfix release
* Fri Nov 23 2018 gwassermannAATTcert.org- Update to v4.8.3, bugfix release
* Tue Nov 06 2018 gwassermannAATTcert.org- Update to v4.8.1, required for latest ROSE/Pharos features
* Tue Oct 16 2018 gwassermannAATTcert.org- Revert to v4.6.3, git.b81165167304c20e28bc42549c94399d70c8ae65 for use with Pharos, as required in README
* Fri Jun 15 2018 mimi.vxAATTgmail.com- Update to version 4.7.1+git.20180614:
* fix memory leak in relation_manager, use for loops
* fix #1665
* remove trial with mfsr flag
* enable non-expression bodies of quantifiers to fix #1667
* fix bugs exposed by Nuno\'s PB example
* z3.py: add overflow checks to PB API
* gcc mode
* int64_t
* deal with shift exponent error
* deal with shift exponent error
* try flags to fix gcc build
* int64_t
* try new gcd
* add set operations to python request by Francois
* fix #1662
* fix #1661
* fix memory leak from Arie
* fix ml build breakd #1659, #1660
* fix #1655
* fix #1653
* remove stale file
* clean up python build files
* fix #1650 fix #1648
* fix #1647
* remove interp from documentation
* Set the SONAME field of libz3.so to libz3.so.
* remove interpolation from test_capi
* remove interpolation from test_capi
* deprecating interp
* fix #1638
* fix #1645
* remove interpolation and duality dependencies
* updated release notes for merge
* work around VS2012 compiler bug
* GLU -> GNU fix #1643
* fix x86 warning
* Fix missing word in C++ API docs.
* Update OCaml docs for changes made elsewhere.
* Z3_TRUE/Z3_FALSE should be true/false, not 1/0.
* fix python build script dependencies
* dealing with compilers that don\'t take typename in non-template classes
* stale files
* merge with master
* fix bug reported in #1637
* delay dereferencing justification
* release notes
* bumping version number by 1 for release tagging
* Use CMake\'s own mechanism for selecting language version if CMake version is new enough
* Add missing include The code should not have compiled previously, as smt::context was only forward declared at this point.
* Remove unnecessary (and confusing) parantheses around variable name in its declaration. Also fixes GCC warning [-Wparentheses].
* Add comments
* Implement parallel python example
* As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value
* NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized
* remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized
* fix #1621
* fix #1625
* fix #1621
* fix #1625
* updated sat state
* Big_int is no longer a part of OCaml\'s standard library and must be included via the num package: https://github.com/ocaml/num
* tune for unit test, delay initialize re-solver
* fix build
* add support for core extraction in parallel mode
* unreferenced variables
* fix osx build
* fix removal bug, tune all-interval usage
* disable slow validation code
* fix parenthesis
* use __builtin_prefetch for clang/gcc
* Fixed Segfault when failing to load datalog file
* The Permutation Matrix\' `values` function attempted an incorrect conversion. This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE.
* fix if-def
* fix ema
* adding ema
* Revert \"Specify encoding of source files in mk_util.py\"
* update model conversion
* touch
* fix java
* fix #1607 by filtering exceptions when the context is canceled
* fixing compilation errors
* Specify encoding of source files in mk_util.py
* fix java
* fix dotnet example
* fix dotnet example
* create empty model
* fix #1609
* fix build
* resolve
* resolve
* fix build issues
* fix build
* fix build errors
* fix build
* fix build
* fix build errors
* fix build errors
* try string in pragma
* pragma
* use C99 pragma
* merge
* n/a
* merge
* merge
* merge
* n/a
* fix #1604
* fix local search initialization of units, encode offset in clauses
* testing memory defragmentation, prefetch, delay ate
* fix #1599. fix #1600
* fix #1599. fix #1600
* WMax conflict budget bug fix
* Revert \"MSS based MaxSMT solver\"
* Revert \"implemented CLD\"
* Revert \"disjoint cores\"
* Revert \"WMax conflict budget bug fix\"
* fix memory leak related to #1575
* change order of concatentation for empty string, #1595
* fix #1595
* fix #1594
* fix #1592 #1587
* WMax conflict budget bug fix
* Z3 now will also try to find libz3 in PYTHONPATH
* Updated CMakelists.txt
* Added tactic for QF_FPLRA
* Fancy dots are not allowed here!!
* fix #1581
* add warning message for optimization with quantifiers. Fix #1580
* fix #1583
* fix #1575, fix #1585
* enable patterns on equality, add trace for variables for axiom profiling.
* add web assembly link
* add web assembly link
* fix #1576, hopefully
* fix #1579
* Fixed corner-case in fp.to_ubv.
* remove extra file
* add params
* move parallel-tactic to solver level
* clean up parallel tactic
* adding smt parallel solving
* add backtracking conquer
* fix build
* fix build warnings
* adding the orphaned shorthand #1574
* adding orphaned function declaration #1574
* fix accounting for branches
* add filter cubes parameter
* parallel params
* updates
* fix regex automata leaked memory
* fix #1571
* escape ascii above 127, issue #1571
* fixes
* including all touched tautology literals each round
* Bugfixes for fpa2bv_converter. Fixes #1564.
* fix #1567
* move some methods from header to cpp, format fixing, remove special characters
* fix cast in tests
* disambiguate calls to set
* disambiguate calls to set
* fix in occurs_check (early exit)
* replace by int64_t and uint64_t
* fixes
* style(datatype): use modern iteration
* chore(datatype): small fixes
* fix(datatypes): additional explanation in occurs_check
* fix(datatypes): update following AATTnikolajbjorner \'s review
* fix(datatype): always use root nodes for the `parent` table
* chore(datatype): small improvements
* fix(datatype): only use pointer equality for enode_tbl
* perf(datatype): whole-graph implementation of occurs_check
* chore: add definition for `enode_tbl`
* perf(datatype): improve caching in occurs_check
* shorthands in enode to access args and partents
* remove comment
* Fixed bug in to_fp/to_fp_unsigned. Thanks to Florian Schanda for reporting this bug.
* add re.plus length enumeration; fix reordering warning
* flip literals in ATEs produced using RI
* Resolved merge conflict
* Bugfix for fp.to_sbv. Thanks to Florian Schanda for reporting this bug.
* Bugfix for unspecified semantics of some fp.
* operators.
* Fixed overflow bug in fp.to_ubv. Thanks to Florian Schanda for reporting this bug.
* Fixed model completion for unspecified cases of floating-point functions. Thanks to Florian Schanda for reporting this bug.
* Fixed overflow problem in fp.to_?bv. Thanks to Florian Schanda for reporting this bug.
* Fixed MPF to_sbv. Thanks to Florian Schanda for reporting this bug.
* add tuple shortcut and example to C++ API
* fix collection error
* Fix buffering issue in print_success for declare-datatype
* disable bdd variable elimination
* fix bug in blocked clause elimination: it was ignoring unit literals
* bit-blaster
* increment version number due to ABI/API breaking change #1556
* Remove int64, uint64 typedefs in favor of int64_t / uint64_t.
* model conversion and acce tracking
* Use stdint.h for int64_t / uint64_t in API.
* Update Z3_bool doc.
* fix use of Z3_bool -> Z3_lbool
* use stdbool #1526 instead of int
* add stdbool.h
* move propagation to after binary clause addition
* fix indent
* propagate during asymmetric branching
* updates
* remove stdout
* add correct badge
* remove lns code
* fix bugs in scc_tr
* fix diagnostic output #1553
* initialize solvers to ensure that eval mode has a solver Signed-off-by: Nikolaj Bjorner
* add eval feature #1553
* update build definition to 4
* updated OSX build
* update script
* update script
* update script
* back to path
* updated script
* updated script
* fix mac build error
* check-error
* fix mac build error
* fix mac build error
* fix mac build error
* mac build
* fix mac build error
* mac
* mac
* cd below
* add ls
* add mac build
* add vstsmac
* remove python doc test
* use vc path in 2013
* remove python tests from x86 build
* add vstsvs2013 outline
* add missin bar
* adding build definition
* add error checking and command argument
* vsts script
* fixing after clone
* fix use-after-free
* fix example test
* add test-benchmarks
* update vsts
* fix java API
* update script
* fix java
* re-add indexof-contains heuristic
* fix indexof subterm
* fixups to theory_str indexof and axiom handling loop
* update build script
* theory_str fixups for new collections
* fix #1547 by rewriting legacy recognizers to SMT-LIB2.6 style recognizers which are assumed by theory_datatype
* remove unreachable from vector
* comment out pull
* update vsts script
* fix test build
* add const to iterator loops where it can be used
* move script
* vsts cmd
* try paths to vsvars
* vsts cmd
* fix #1545
* fix #1538
* moving more std::map std::set to obj_
*, #1529
* fix #1544
* fix build
* added TODO markers in theory_str.h for moving to obj_map, remove include of stdbool for now
* Fix minor issues in docs.
* Fix #1540 Remove extraneous function
* fixing local search
* experimental axiom-persist for regex conflict clauses
* fixing local search
* fix #1539
* change lemma display utility to use updated pretty printer
* java
* remove unused operators #1530
* fixing nls
* Add support for NetBSD
* adding lns
* fix pbge and reduce_tr
* refactor: use c++11 for (part 1)
* preliminary refactoring to use obj_map
* fix #1534
* fix pb rewriter
* fix include path
* bump revision
* add stdbool.h to see whether build system breaks #1526
* fix build
* remove references to deprecated uses of PROOF_MODE #1531
* disable GCC flag change to see if this affects build
* Fix parameter expansion when configuring Z3
* remove stale deprecated annotation #1525
* Fix typos.
* integrate contains and indexof in theory_str
* fix #1521
* remove useless get_assignments in theory_str final check
* fix #1522
* Force color output with Ninja.
* Make proof_checker more const correct.
* add hiding to auxiliary declarations created in mc
* radix sort experiment
* add unit extraction
* delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
* inherit solver parameters in asserted formulas rewriter. #1511
* remove buggy legacy code, rely on pull_cheap_ite option in rewriter, #1511
* save last model to ensure it is available fixes #1514
* fix #1510 by reintroducing automatic declaration of recognizers
* fix #1512
* fix bugs found while running sample from #1112 in debug mode
* fix topological traversal crash
* fix #1488 for smtlib basic printer
* add re.allchar support in z3str3
* update registration of built-ins
* fix z3.py
* address accessor inconsistencies between - and from #1506
* fixes to #1500 and #1457
* don\'t reinit assumptions when the solver is unsat. fixes #1502
* Fix assignment of family ids
* Convert BVULT(X,Y) into !BVULE(Y,X)
* fix the build
* fix the override warning
* fix build
* fix more warnings with override
* fix more warnings with override
* fix #1496
* try another build fix
* try another build fix
* try another build fix
* fix build
* fix rule inlining, add WithParams to pass parameters directly to python API
* Fix Python FiniteDomainSortRef.size()
* working on propagation with undef main literal
* bug fixes
* Insert sort declaration for nullary sorts declared using declare-datatype
* disjoint cores
* fix #1492
* remove unused code
* implemented CLD
* MSS based MaxSMT solver
* fix #1491
* fix #1488
* Revert \"Fix encoding error\"
* Use bool literal `false` instead of `0`.
* Remove redundant void arg.
* fix #1484
* fixups to theory_str for regex
* remove deprecated comments about bv2int/int2bv being treated as uninterpreted, raise in #1481
* ensure that final model is logged by the time it is produced fix #1463
* Use nullptr.
* support self-subsumption, remove verbose log 0
* add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits
* perf improvements
* disable lookahead simplification when external solver is used
* Use override rather than virtual.
* fix parameter processing
* fix another recompilation bug
* fix missing clear of weights
* fix wrong check
* Use override rather than virtual.
* fix reset code for level marking
* Remove unnecessary value parameter copies.
* Fix typos.
* fix validation code, disable PB compilation code
* add model checker to external
* fix bugs, add soft timeout to opt frontend
* fix configuration for compiling equalities, add extended binaries
* fix local search encoding bug
* fixing build
* align semantics of re.allchar with string proposal. #1475
* remove redundant tactic
* remove tautology
* reference get_wlist
* dbl-max
* remove file
* remove file
* re-add cpp file
* remove files
* fix build isses
* fix errors
* xor to xr to avoid clang issue
* rename to core2 to avoid overloaded virtual
* fix errors
* fix errors
* fix compiler error reported by Luca
* lia2card simplifications, move up before elim01 (which could be deprecated)
* to fix #1476
* add LP parser option to front-end and opt context
* fix #1468
* remove a duplicate definition
* Fix inconsistent missing override warnings.
* Reserve vector space when possible.
* fix #1471
* fix #1469
* remove static from format (not thread safe), remove std::move #1466
* adding template definitions
* fix #1458
* add logging for #1470
* set uninitialized fields. Maybe related to #1468
* fix more bugs with compilation of pb equalities
* fix bug in translation of pbeq into sat
* neatify rewriting
* update lia2card to handle broader intervals
* remove legacy bce
* Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug.
* Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun.
* Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug.
* ate/acce
* Fixed pattern rewriting to produce only valid patterns (which led to a segfault). Bug reported by Youcheng Sun.
* fix gcc compilation error
* fix ugcd
* fix python build
* disable uhle from lookahead solver
* Fix typos.
* throttle cce pass
* fix build
* fixup cce
* fix updates to cce
* add cce minimization
* Use char version of rfind.
* Use const refs to reduce copying.
* fix learned annotation on ternary
* adding initial model to updated #1463
* working on completing ATE/ALA for acce and abce
* fix license in sstream
* fix build
* add solution_prefix per #1463, have parto with single objective behave similar to multipe-objectives #1439
* use regex instead of head/tail split for string-integer conversion; check sort of refreshed vars; add intersection difficulty estimation
* Fix encoding error
* experimental str.to.int fix
* always rewrite regex length constraints as they are sometimes malformed
* fix regex difficulty overflow bug; fix final check on regex terms that don\'t get path constraints
* Added rewrite cycle detection in demodulator/ufbv_rewriter. Partial fix for #1456.
* fix constant eqc bug in mk_concat
* fix setup of path constraints when the path constraint is False
* fix hidden tautology bug on non-learned clauses
* fix model conversion bugs
* debugging opt
* debugging mc
* local
* temporarily disable final check progress checking it is interfering with regex automata solving
* fix null pointer dereference
* check polarity
* zero-length automaton solution fix
* fix static
* more updates for #1439
* correct generation of linear length constraints for regex star terms
* short path for length-0 regex terms
* fix bugs related to model-converter
* disable regex length constraint generation as it currently makes unsound axioms
* check duplicate bounds info for regex terms
* regex fail count and automaton fallback
* regex length term assertion WIP
* regex length linearity check WIP
* disable buggy clausification in ba_solver
* intersection of regex constraints produces a conflict clause
* reuse regex character constraints for the same string
* intersection WIP; fix polarity of generated path constraint LHS
* change behavior of single-objective pareto to use Pareto GIA algorithm (so not a good idea with MaxSAT solving, but then uniform behavior #1439
* fix xor processing
* fix model bugs
* fix model bugs
* regex failsafe and intersect WIP
* add clausification features
* updates to model generation
* add path constraint generation for regex terms
* regex path constraint generation (WIP)
* lower bound refinement
* regex lower bound (WIP)
* full upper bound refinement
* fix up convertion and printing
* fix up convertion and printing
* adding ad-hoc method for converting models
* fix update to variables
* bug fixes
* bug fixes
* add upper bound refinement (WIP)
* fix sat model converter to work with incrementality
* add unit walk engine
* restored commented out code
* fixes
* remove cache reset that causes crash
* reset cache in ast_translation periodically to avoid congestion
* commented non-compiling debug traces
* fix uninitialized variable m_gc_burst in config, have cuber accept and receive optional vector of variables indicating splits and global autarky as output
* prepare for variable scoping and autarkies
* fix crash regression
* pre-merge
* fix assertion in model converter for incremental mode
* add checks for flipping externals / assumptions in model converter, fix scc converter bug
* pre-merge commit
* merge
* inherit incremental override on the solver state
* fixes
* local changes
* fix model conversions for incremental SAT, fix lookahead with ba_solver
* snapshot
* fixed adaptive apsat
* fix bug in double collection of declarations
* disable UHLT
* use safer mk_and in extended indexof
* length estimation
* adaptive psat cutoff
* new regex automata start; add complexity estimation
* fixed freevars and psat cube cutoffs
* remove deprecated options
* fixes to inprocessing code
* freevars cube cutoff
* add statistics to cubing
* fix perf bug
* fix bug in PB constraint init_watch handling, adding transitive reduction, HLE, ULT,
* set eliminated to false on literals used in clauses
* adding uhle/uhte for faster asymmetric branching
* preparing for more efficient asymmetric branching
* model converter fixes
* correctly check third argument of str.indexof in theory_str
* translation?
* fix missing conversions
* fix model converter to include negation
* update scoring approach
* add option to bypass model converter during constraint addition. Simplify model definitions that come from blocked clauses
* add options to perform transitive reduction and add hyper binary clauses
* prepare for transitive reduction / hyper-binary clause addition
* remove output
* fix mc efficiency issues
* print model-add in display method
* include mc0 for display method
* add solver_from_string to APIs
* add solver_from_string to APIs
* add notes about quantifier ordering, bypass
* use expr-vectors
* change lookahead equivalence filter
* re-adding simplified constraints based on model converter
* expose probing configuration parameters
* adding handlers for dimacs for solver_from_file, and opb, wncf for opt_from_file, #1361
* add converters
* remove also cores as arguments to tactics
* re-organize proof and model converters to be associated with goals instead of external
* merge commit
* fix copy function
* remove proof_converter from tactic application, removing nlsat_tactic
* prepare for inverse model conversion for formulas
* remove extension model converter
* add stubs for converting assertions, consolidate filter_model_converter
* re-organize iterators
* initialize glue in constructor to ensure it gets set
* add global autarky option, update translation of solvers to retain vsids, remove stale code
* add useful shorthands to Solver interface
* fix bug in contains function
* fixes
* bug fixes in uninitialized variables
* fix crash bugs in sat solver
* fix crash bugs in sat solver
* add iterators to C++ vectors
* update to vector format
* reset backtrack level at each cube
* updates
* reset backtrack level after first backtrack
* add backtrack level to cuber interface
* use failed literal to asym branching
* asymm branch
* fixes
* missing files
* allow incremental mode override
* update error code
* fix race condition, exception handling/throwing
* remove ad-hoc parameters, deprecating dimacs cube mode
* updates to parallel tactic
* work on parallel-tactic
* cube and conquer parallel tactic
* disable symbol fixing in pretty printer
* add direct FromFile method to solvers so that model transformations are loaded along with assertions.
* model-add/del
* implementing model updates
* adding Cube method to .NET API, removing lookahead and get-lemmas
* fix variable naming bug for internal (fresh) constants clashing with external names
* fix scc omitting blocked clauses
* ensure that bca takes also lemmas into account
* Clean-up
* Python API context fix
* fix bca condition for tautology check
* fix non-termination bug with retained clauses
* bug fixes reported by Miguel
* Removed incremental disabling
* bug fixes
* Tidy
* Fixed infinite loop bugs in blocked clause retention. Added option to disable incremental sat solver
* fix bugs related to reading configuration flags
* Fixes
* updates to simplifier
* bug fixes, prepare for retaining blocked clauses
* Merge
* Reverted to March_CU like lookahead
* fixup bdd reordering, assertions and perf
* testing bdd for elim-vars
* testing bdd for elim-vars
* expose missed propagations
* debugging reordering
* compress elimination stack representation
* Added literal promotion
* working on BDD reordering
* local
* Lookahead clause size optimization. Fixed some missing propagations
* add elimination stack for model reconstruction
* adding elim sequences
* fix debug build
* fixing cce
* add cce
* more agressive variable elimination
* fixing projection
* adding BDD-based variable elimination routine
* adding bdd package
* adding bdd package
* adding bdd
* updates
* More failed literals
* fix faulty merge
* Commit
* tidy
* removing failed literal macro
* Changed lookahead backtrack. Parent lookahead re-use fix
* micro opt
* remove traces of old n-ary representation, add checks
* fix lookahead with ba extension
* fixing lookahead/ba + parallel
* fixes
* parallel
* Dynamic delta trigger decrease
* use clause structure for nary
* adding outline for parallel tactic
* bug fixes
* bug fixes
* remove verificaiton code
* bug fixes
* clean up debug output
* bug fixes
* Cuber fixes. Added March_CU heuristics
* assertion fixes
* bug fixes
* update pb rewriter to be non-full on assertions
* fixed encoding for order constraints
* remove NEW_CLAUSE variant
* expose incremental cubing over API
* adding incremental cubing from API
* fix python parsing API
* tidy
* local updates
* n/a
* fix new clause encoding
* n/a
* n/a
* tidy
* working on new clause organization
* adding new clause management
* working on new clause management
* working on new clause management
* adding new clause management
* local changes
* add cube functionality
* updates to sorting networks
* add HS and unit literal reward schemes
* n/a
* experiments with ccc
* n/a
* update for equivalences
* add handling for nested terms
* track the set of integer variables that are not set to integer values
* fix term indices for the time being when exiting from check()
* add a check in gomory cut
* a cleaner version of subs_term_columns
* gomory cut worked on a toy example
* rename a function
* fix term_is_int
* the first version of Gomory cut, probably broken
* n/a
* add a file
* progress in gomory cut
* branch on a free variable before trying Gomory cuts
* start gomory cut
* start gomory cut
* speed up in get_model and fix in git_model_do_not_care_...
* fix a bug in the lar_solver::m_status update during push/pop
* change the order of initializations in the constructor of imp in theory_lra
* use a faster version of get_model in debug checks
* replace clp to clean
* replace lean to lp
* solve all smt2 from QF_LIA/calypto with int_solver
* fixing overflow checking
* solve more integer smt problems
* n/a
* solve more ilp smt
* Dev (#64)
* fix in init_int_int_set
* correct handling of integer vars by NB
* return a value from pivot_column_general
* fix a bug in pivot_fixed_vars_from_basis
* Dev (#63)
* n/a
* n/a
* n/a
* update to avoid difference in debug/release builds
* updates
* n/a
* n/a
* n/a
* add pb to local search
* n/a
* rename to ba_solver
* reorg
* Dev (#56)
* debugging
* fixes
* added in-processing features to card/pb
* adding in-processing
* updates and fixes to copying and cardinalities
* translate
* bug fixes
* cleaning up lookahead
* fixes top lookahead simplification
* add N-ary clause reward heuristic based on discussions with Heule
* disable anti-exploration by default
* add facility to add lemmas
* init search before returning
* atomic
* 64 bit clause offset fix
* lookahead
* fixes to lookahead
* lookahead on cardinality extension
* update lookahead to include extensions
* fix iz3parse for updated API
* extract lemmas
* fix lookahead code
* have parser produce ast-vector instead of single ast
* add tracking for reason unknown
* remove dependencies on fd_tactic.h
* adding lookahead and lemmas
* enable exposing internal solver state on interrupted solvers
* updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver
* debugging nra
* test
* adding nra
* Dev (#51)
* adding nra solver
* add missing initialization
* adding nra solver
* adding some content to the new check_int_feasibility()
* adding constraints
* nlsat integration
* adding more nlsat
* small fix in lar_solver.cpp
* Dev (#50)
* initial skeletons for nra solver
* initial skeletons for nra solver
* adding stub check_int_feasibility()
* local updates
* rewrite pb
* bug fixes
* bug fixes
* bug fixes
* pb propagation
* after merge with Z3Prover
* fix add_constraint and substitute_terms_in_linear_expression
* add_constraint has got a body
* add file
* resurrect lp_tst in its own director lp
* add queries for integrality of vars
* track which var is an integer
* add int_solver class
* introduce int_solver.h
* local changes
* fix bugs related to use of lookahead equivalences and encoding of pb constraints
* local
* enable pb solver
* adding pb
* disable newer pb encoding
* parallelizing lh
* parallel verison of ccc
* parallelizing ccc
* parallelizing ccc
* parallelizing ccc
* ccc
* debugging ccc
* ccc
* use lookahead for simplification
* fixing local search
* gt encoding of pb constraints
* testing double lookahead
* fix autarky detection
* debugging double lookahead and autarkies
* working on lookahead
* diagnosing lookahead solver
* add debugging
* lookeahead updates
* adding pb
* constraint id
* fix local search
* add logging to lookahead
* fix build of tests
* fix xor handling, and defaults for cardinality
* enable multiple local search threads
* adding ability to ahve multiple local search threads
* local search updates
* use iterators
* updates
* current updates
* walk/gsat
* parameter example
* fiddle with phase
* updates to local search integration
* tweaking local search
* refine logging for local search, add handling of <= for opb front-end
* disable pb sorting
* debugging local
* integrating local search, supporting top-level inequalities
* Sixue\'s updates
* add local search parameters and co-processor mode
* updates
* updates
* updates
* updates
* adapt to vectors
* latest updates from Cliff
* working on lookahead
* expose xor solver separate from cardinality solver
* merge with master
* working on lookahead
* hackvector!
* update for layout
* working on pre-selection
* working on lookahead solver
* initialize
* initial pass
* adding unit test entry point
* porting more code
* porting more code
* porting more code
* adding skeleton for local search
* fix handling of global parameters, exceptions when optimization call gets cancelled
* fix build on downlevel compilers
* add xor parity solver feature
* tune cardinalities
* add sorting-based pb encoding in the style of minisat+
* add option to disable cardinality solver
* add option to disable cardinality solver
* testing lookahead
* testing lookahead
* fix parallel solving bugs
* fix non-linear model bug found Giles Reger and Martin Suda
* fix drat checker
* fixing bugs in dealing with non-0 based cardinality constraints
* updates
* tuning and fixing drat checker
* tune cardinality solver for cache misses
* fix compiler errors and memory issue with drat
* fix issues in par
* fixes to sat-par
* adding clause sharing to par mode
* expose extension conflict resolution as plugin to sat solver
* adding drat forward checking
* adding drat
* debugging card
* local updates
* local
* updates on cardinality solver
* fix translation of <=
* fixing card
* local
* memory allocate
* updates
* preparing for cardinality
* working on card extension
* working on card for sat
* experimenting with cardinalities
* updates
* fixing card
* working on card
* working on conflict resolution
* updated cardinality
* working on card
* cardinality reduction
* fixing bounds calculation
* update conflict resolution for cardinality case
* added cardinality solver
* local changes
* Fri May 18 2018 mpluskalAATTsuse.com- Use python3 exclusively- Do not call contrib/cmake/bootstrap.py - it is obsolete
* Thu Mar 22 2018 dimstarAATTopensuse.org- Fix python packaging: create python3-z3 on SLE/Leap 15.0 and Tumbleweed, and python-z3 on older distros.
* Tue Jan 16 2018 jslabyAATTsuse.com- Update to version 4.6.0+git.20180112:
* add missing interpreted tail during bottom-up simplification #1452
* Added apply_result::as_expr to the C++ API. Requested here: https://stackoverflow.com/questions/48071840/get-result-of-tactics-application-as-an-expression-in-z3
* to ascii or not to ascii #1447
* fix build
* avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444
* make linear search the default for theory_str
* [CMake] Fix #1437.
* Use noreturn attribute and __declspec version.
* revert use of [[noreturn]]. It\'s not fully supported on compilers #1435
* add noreturn attribute #1435
* raise_exception: Annotate that this doesn\'t return.
* Remove unnecessary copy of coeff in iteration.
* Remove ignored const qualifiers.
* Fix code formatting: Incorrect indentation.
* fix #1429
* print_stat_f: Remove implicit conversion of float to double.
* Typo fixes.
* set default rewriter behavior in incremental mode to distribute multiplication over addition #1373
* removing axiom exposing unsoundness, replace by weaker axiom
* add shorthand for translating models #1407
* add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver
* fix build of test
* adding pre-processing to nlsat for equations
* fix get-objectives error #1419 message (get-objectives)
* initialize additional assumptions after setup_context is called the first time
* alternate strategies for QF_NIA
* remove custom exception, perhaps this handles exception issue
* add virtual destructor to see if this helps ASan error
* Allowing slices and negative index in assertions
* add Python facility for int2bv, fix #1398
* Documentation fixes.
* Bumped version number.
* Updated release notes
* add back missing initialization of lo
* fix nlsat regression
* avoid crash on nl
* fix crashes in nlsat
* fix crashes in nlsat
* remove comment out
* add integer branch and bound to nlsat
* small improvements to QF_NIA tactic
* fixes compilation flags for OCaml plugins
* Mon Jan 15 2018 jslabyAATTsuse.com- Look for python3_sitelib in tumbleweed
* Thu Dec 14 2017 jslabyAATTsuse.com- Update to version 4.5.0+git.20171213:
* generalize model finder code to be independent of conjunction elimination
* Turned assertion failure into proper error message.
* fix incorrect clause in argumentsValid subterm of substr reduction
* add shortcuts for concatenation and equality propagation
* fix build of obj_ref_hashtable
* fix setup for non-linear real arithmetic per QF_UFNRA regresssions
* add obj_ref_map to make it easier to maintain reference counts with a map of objects
* remove deprecated functions from ML API. #1393
* [Release Notes] Note that C++11 is required to build Z3 and is also required by the C++ API bindings.
* [CMake] Use C++11 when building C++ API example.
* fix #1390
* disable C++11 dependency to fix the travis build
* deal with ambiguity
* circumvent build errors introduced when using the ast_vector_tpl iterator
* include path
* include special functionality in parsers for solvers and opt for additional file formats
* include special functionality in parsers for solvers and opt for additional file formats
* fix issues found in parsing examples
* remove assertion that gets violated on exception path (declaration of datatypes are not getting removed)
* fix lack of warning/error for unbounded objectives in context of quantifiers #1382
* fix test build
* fix test build
* set version, fix build of test files
* fix java
* fix dotnet example
* fix example file to be smt2 format
* fix maxsat compilation for maxsat example
* fix maxsat compilation for maxsat example
* fix c example, remove more smtlib1 printing
* remove SMTLIB1 printing
* Update version
* add parser error
* increase minor version, update java/.net apis
* fix error messaging for parsers
* remove smtlib1 dependencies
* fix #1371
* remove std::cout
* save model from level 0, fix #1380
* fix #1377
* fix #1377
* fix #1375
* fix #1376
* fix #1368
* fix different bug reported on #1366
* fix break
* fix #1366
* expose extra symbols for logic ALL, requested in #1364
* fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help
* remove redundant argument #1364
* fix argument validation to new overflow/underflow functions #1364
* add bit-vector over/underflow checks to Python API, #1364
* fix #1233
* debugging #1233
* adding instrumentation to debug #1233
* avoid rationals for addition in checked_int64
* Fixed bug check in bv2fpa converter. Fixes #1291.
* avoid a warning
* add bvsmod
* additional bit-vector operators over C++ API
* fix occurs function used in qe_lite #1241
* fix crash
* fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI
* fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI
* fix #1358
* fix slicer for unsoundness. #1304
* fix java build problem with bool arrays
* clean up bv_numeral code and fix bug in how they are initialized
* add method to create bit-vectors directly from an array of Booleans
* include information whether rule is reachable in del_rule model converter for simpler model presentation #1241
* insert total relations in model converter. #1291
* [CMake] When invoking `mk_api_doc.py` pass the build directory.
* fix rewriter loop reported in #1354
* make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization
* Fixed MSYS/MinGW build. Fixes #1335.
* Improved support for MSYS/MINGW. Fixes #969.
* API doc build fix. Related to #1350.
* Fixed API doc build
* Fixed Windows build of C example.
* Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349.
* Fixed error handlers in Python API.
* Fixed C example build.
* Fixed C example build.
* Fixed default library path order in Python API.
* Fixed library path order in Python API.
* Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989.
* fix #877 by bypassing exception generation during label collection
* fix #889
* remove a few unneded mem allocations
* fix proof mode related segfaults #1241
* remove asserts for proof generation to enable mode switch in spacer virtual solver
* fix segfault reported as part of #1241
* fix build
* fix model converter bug in coi-filter #1241
* MSYS offers a MINGW shell as well. (uses different os.uname())
* fix order of instantiation for recursive functions, #1274
* internalize free var before iterating eqc in theory_str
* Added support for MSYS2
* fix virtual method override
* fix build break with virtual method override
* fix stack overflow
* add proofs dependency to solver
* add solver pool abstraction for Spacer
* fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR
* fix #1326
* fix #1326
* more C fixes to model example
* re-add model example
* disable model example pending C compliance or C99 or whatever adjustment
* remove ast.h reference
* missing files
* [CMake] Try to unbreak the C example build with older GCC versions by forcing the language version to be C99.
* move min_cut, fix #1321
* ifndef/define match
* fix build errors
* fix build, fix #1322
* more build errors in debug mode
* missing file
* move more proof utils
* move proof utils under ast
* Add example of using Z3\'s new model construction C API. This API was requested in #1223.
* rename repeated class apart
* unused warnings
* backward comp
* fix build issues
* move spacer_marshal to under parsers/smt2
* create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs
* account for review
* fixing regressions introduced when reducing astm proof dependencies
* add parameter to specify the file into which dot proofs are to be printed
* add some colors to the proof output
* add a basic printer into graphviz (http://graphviz.org/) for proofs
* patch build failure
* streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223
* fix #1319, fix #1320
* fix #1316, segmentation fault when numeric value is not internalized
* disable eager clear of check-sat-result to fix #1318
* remove debug code
* remove redundant and wrong range type, in extension to changes made for #1223
* additional array functions exposed over API, ping #1223
* add special case handling for string constant backpropagation in theory_str
* Update README.md
* gift for Nuno
* fix scope accounting for dom simplifier
* nnf: let\'s try a different version of compatible frames wo/ copying
* Backward compatibility
* frame, again
* moving out construction of expr_ref
* trying to fix mac build
* add macro for _Exit under WINDOWS
* Backwards compatibility
* Whitespace
* [TravisCI] Don\'t run Python regression tests under ASan for now. The script that runs them doesn\'t propagate LD_PRELOAD and so the tests fail.
* [TravisCI] Try to unbreak running Python regression tests under ASan.
* [TravisCI] Add ASan/UBSan configuration that runs unit tests.
* [TravisCI] Add `RUN_API_EXAMPLES` option so that we can disable building/running examples in some configurations.
* More LSan workarounds.
* [TravisCI] Try again to not show suppressions by default
* [TravisCI] Swap `run_quiet` and `run_non_native_binding`. In the previous order `grep` inside `run_quiet` would get ASan LD_PRELOAD\'ed which would sometimes fail.
* [TravisCI] Try to fix case in `run_quiet` where the script would fail with.
* [TravisCI] Don\'t print sanitizer suppressions by default because that breaks Z3\'s regression tests.
* Workaround `regressions/smt2/error.smt2` test timing out.
* [ASan] Ignore Clang OpenMP leaks for now.
* [TravisCI] Fix typo
* [TravisCI] Fix `Z3_BUILD_TYPE` variable that was not propagated into the Docker image as an environment variable.
* [UBSan] Remove a bunch of suppressions.
* [TravisCI] Try to run the Python and .NET examples under ASan.
* [LSan] Remove suppression files. The were fixed on rebase
* [LSan] Don\'t run `c_maxsat_example` with LeakSanitizer because it contains leaks that the Z3 developers don\'t intend to fix.
* [LSan] Suppress another leak until I can figure out what is going on.
* [LSan] Add suppression for part of #1297.
* [TravisCI] Fix typo in created directory for suppression files
* [TravisCI] For ASan/LSan use larger context so we get larger stack traces if needed.
* [TravisCI] Make ASan/UBSan configuration a debug build.
* [TravisCI] Add ASan configuration
* [CMake] When building C/C++ API examples use the same build type as Z3 if doing a single configuration build.
* [TravisCI] Fix getting proper stack traces for ASan/LSan. The `llvm-symbolizer` tool needs to be installed and ASan/LSan needs to be told where to find it.
* [UBSan] Update UBSan suppression file to suppress all undefined behaviour I have observed running in CI.
* [TravisCI] Don\'t run the python binding system tests when building with UBSan.
* [TravisCI] Fix undefined SCRIPT_DIR variable
* [TravisCI] Add a UBSan configuration
* [TravisCI] Don\'t run the non-native example when building with UBSan.
* [TravisCI][CMake] Add `Z3_C_EXAMPLES_FORCE_CXX_LINKER` CMake option and propagate its value into the C API examples.
* [TravisCI] Add ASan/LSan/UBSan suppression files and use them in CI.
* adding explicit assignment for auto-generated function.
* make vector friendly to gcc < 5
* add move constructor to ref_vector
* add move constructor to watch_list
* vector: make expand_vector() less prone to mem leaks by calling the destructors after move
* add move constructor to obj_ref
* nnf: remove ast incref
* add move constructor to rational
* fix build of unit tests
* add move constructor to mpf
* remove noexcept since MSVC 2012 doest support it
* fpa_rewriter: remove a mpq copy
* bv_decl_plugin: remove mem allocation
* fix crash in vector::expand()
* mpz.h: fix typo in previous commit (found by Nikolaj)
* fix vector<> to support non-POD types adjust code to std::move and avoid unnecessary/illegal
* fix leaks reported in #1309
* fix the fixme of #1307
* unused variables
* change nullptr to 0
* take shortcuts during binary search length testing when length is known from integer theory
* bypass UBSan error warnings by using nullptr as error handler. Has same no-op effect. Issue #1287
* fix #1306
* address some ASan leaks
* command to exit tests early
* fix #1305
* disable failing unit tests
* fix #1303
* [ASan] Fix some leaks reported in the small object allocator test.
* harden a few API methods against longjumps in set_error. Memory leak exposed in #1297
* update C-example that fails to not use longjumps. Issue #1297
* trying to address leak reported in #1297
* Added bv_sort_ac=true to asserted_formulas::m_rewriter
* whitespace
* redo length testing with concrete length, linear search only
* take shortcuts during length testing when length is known from integer theory
* enable binary search for theory_str
* rewrite theory_str replace instances
* don\'t rewrite on every axiom in theory_str
* rewriter patch for theory_str
* Tue Oct 10 2017 jslabyAATTsuse.com- Update to version 4.5.0+git.20171009:
* allowing non-literal assumptions
* adding escape characters to reason-unknown #1043
* add colon to assertion stack levels #1046
* remove throw in reason-unknown #1043
* add pb built in ops for logic ALL #1045
* enable get-unsat-assumptions command per request in #1048
* Fix Expr.update in java API returning superclass
* Remove tab
* put temporaries on trail
* Tabs
* Fixed signed/unsigned comparison warnings
* add string accessors to managed APIs #1051
* expose operator kinds for internal functions using their sequence variants. Issue #1051
* fix regression in str
* fix reference count issue with pinning to expr_ref
* add shorthand for enumerating constants in a model
* print success after reset assertions #1057
* add documentation per #1058
* add documentation per #1058
* Added __deepcopy__ operators to ref-counted objects in the Python API
* [Doxygen] Fix bug where some header files were not being scanned.
* [Doxygen] Fix some Doxygen warnings for `z3_optimization.h`
* [Doxygen] Fixed mismatched `AATT{` and `AATT}` declaration which prevented the `capi` group from being declared properly. For example this prevented from `Z3_mk_solver()` from appearing in the `capi` group.
* print success #1068
* filter assumptions by membership in initial list #1065
* revert change to 1065
* print_core as a function
* [Doxygen] Rewrite documentation of `Z3_mk_solver()` and `Z3_mk_simple_solver()` to try to make it clearer what the differences are between these APIs.
* apply correction by ddcc #1069
* escaping names in get-assignment #1061
* [CMake] Move CMake files into their intended location so the `contrib/cmake/bootstrap.py` script no longer needs to be executed.
* [CMake] Remove bootstrap check. Now that the CMake files are in their correct location we don\'t need it anymore.
* [CMake] Modify `contrib/cmake/bootstrap.py` to do nothing except print a warning.
* [CMake] Remove documentation on \"Bootstrapping\". It is no longer relevant.
* properly quote symbols #1061
* Add translate method for FuncDecl in java api
* Fix docstrings for FuncDecl.translate
* fix unsoundness bug in axiomatization of str.at. #1067
* port FuncDecl copy to dotnet, continuation of #1073
* fix build warning
* add sequence recognizers
* add concat recognizer
* Fix Z3_PRINT_SMTLIB_FULL not working as expected
* Fixed AST translation functions in .NET and Java APIs. Fixes #1073.
* use less memory #1078
* fix build
* address issues raised in #998
* address issues raised in #998
* revert internalize logic for re until debugged
* typo
* fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas
* disable tweak to seq until there are cycles to test further
* Whitespace, typo.
* Whitespace
* Reverted fix for quoted echo strings when smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062.
* Fix for the fix for #1062.
* Fix bug #1079, integrality testing seems to have been wrong
* fix build break
* fix assertion, start addressing #1087 by using size_t
* add is_hypothesis() method
* ensure that variable names are properly quoted
* expose iterators in expr_map
* api to accumulate stopwatches
* expose iterator api of obj_hashtable
* remove debug code
* factored out is_variable_proc to a header file
* improve comments
* make qe_lite prefer simpler definitions
* typo in a comment
* api for accessing dl_rule name
* preserve dl rule names during xforms
* disable dt2bv for quantified variables as enum2bv does not handle them. #1092
* refine test for non-fd to be more inclusive while addressing #1092
* [CMake] Fix dependencies for generating `install_tactic.cpp`.
* [CMake] Fix dependencies for generating `gparams_register_modules.cpp`.
* [CMake] Fix dependencies for generating `mem_initializer.cpp`.
* (mev) renamed variable to clarify that it is unused
* (mev) bug fix in expanding array equalities
* (mev) call expand_value only at the end
* add note to Context documentation about scoped uses of contexts #1077
* (mev) only reduce function interpretation
* [CMake] Fix CMake warning about CMP0042 on macOS
* add a template instantination
* #1101
* [CMake] typos in cmake
* fix missing initialization
* propagate rule names during xform
* another fix for #1101
* add separate get-objectives command #1107
* adding change notes to release notes for a future release
* make the option soup dependencies more user-friendly, #1109
* [CMake] Fix missing sanitization in `z3_add_cxx_flag flag()` function which caused CMake 2.8.12 to hit an error when handling the `-std=c++11` flag.
* [CMake] Unbreak detection of pthreads for CMake versions < 3.4
* [CMake] Remove use of `INSTALL_PREFIX` argument to `configure_package_config_file()`. This argument wasn\'t available until CMake 3.1 and we don\'t appear to be really using it anyway.
* [CMake] Unbreak the configure step for CMake 2.8.12
* [CMake] Fix detection of git description and hash for CMake 2.8.12
* Added rlimit increments in theory_arith to avoid non-termination issues via F
*.
* Adjusted rlimit increments in theory_arith to avoid non-termination issues
* Unbreak Z3 C++ API exception support for GCC < 5.0. This was broken by 0b1d5645097d41eec4c43946407e08d57b41ad64 .
* [CMake] Add missing python example files.
* Fix Python API examples so they work with Python 3 as well as Python 2.
* [CMake] Teach CMake to build the `maxsat` example as an external project. The project can be built by building the new `c_maxsat_example` target.
* fix bitrot in maxsat example reference management #1116
* ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations
* fix maybe non initialized warning
* fix run of lp_solver for mps files
* Fixed x86/x64 issues in theory_str
* Fixed backwards compatibility problem in maxsat example
* use worklist algorithm to avoid stack overflow #1125
* fix unsoundness bug instroduced when fixing #1125
* [TravisCI] Implement TravisCI build and testing infrastructure for Linux
* cleanup for warning message
* use iterators, update build icon for osx
* revert icon update
* icon update, take 2
* icon update, take 3
* icon update, take 4
* clean up warnings in theory_str
* fix compiler warnings
* fix compiler warnings
* fix compiler warnings
* fix compiler warnings
* deal with warning messages
* fix trace/debug build for unreferenced variables
* fix theory_str warnings: rename get_value() to get_arith_value()
* adding doc #1132
* Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard.
* update documentation according to #1058
* detect overlapping signatures #1134
* revert update to #1134
* fix check for finite sorts #1122
* avoid complaining about division by 0 as unhandled in theory-lra
* doc fixes
* [CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`.
* [TravisCI] Add `Z3_WARNINGS_AS_ERRORS` environment variable to control the `WARNINGS_AS_ERRORS` CMake option.
* proper theory_arith integration in theory_str::get_arith_value()
* add get_num_scopes to python solver api
* Fix typo that prevented uses of `bvsmod_i` being parsed.
* Fix minor typo in C API documentation
* Fixed bug in sat model converter. Fixes #1148.
* improved get_arith_value() in theory_str
* remove disabled code block in get_arith_value()
* add e_internalized() check in theory_str::get_arith_value()
* Improved collect-statistics tactic
* Fixed inconsistent state upon solver interruption. Partially fixes #951.
* Bugfix for fp.fma. One piece of puzzle #872.
* pretty printer: fix typo with ReSort sort name
* fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format
* fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format
* fix compiler warnings
* fix uninitialized warning
* fix regression reported in #1159
* Fix for fp.fma encoding. Relates to #872.
* Fixed normalization shift in MPF rounder. Relates to #872.
* fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction
* [TravisCI] Fix running unit tests.
* Adding ENABLE_CFI flag to CMake.
* fix for #1161
* ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163
* address ASAN bug report #1160
* address #1167
* fixes #1168
* fixes #1171
* fixes #1172
* fixes #1169
* attempt at addressing #989 by referencing _lib directly instead of over lib() in function calls
* unexpressing interpolants #1172
* add suspenders for #989
* updated suspenders for #989
* another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure)
* Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872.
* fix #1173
* revert first fix for #1173, replace by handling single arity chainables
* remove arity check
* fixing a build error
* add dummy initialization to unused variables to avoid compiler warnings
* Bugfix for fp.fma. Fixes #872.
* Fixed sign bug in mpf fp.fma. Relates to #872.
* Fixed renormalization in fp.fma. Relates to #872.
* fix #1177
* fixes #1176
* fixes #1180
* fixes #1179
* Fixed renormalization in fp.mul. Relates to #872.
* make proof_checker less verbose
* extra flags to control quant_hoist
* mark mk_true() and mk_false() const
* option to control array_der in qe_lite
* move semantics for ref
* Injected 3 missing bits of precision into fp.rem. Relates to #872.
* Simplified bit-vector bounds in fp.rem. Relates to #872.
* fix build break based on new assertion in smt-eq-justification
* Fixed bug in fpa2bv converter. Fixes #1178.
* make include paths uniformly use path relative to src. #534
* fix build break based on ambiguous path resolution
* comments on proof_utils
* extra smt params used by spacer
* increased verbosity level of smt_context
* Spacer engine for HORN logic
* preserve rule names when changing rules
* do not use array_der when simplifying rules
* stubs for spacer-specific API
* implemented spacer-specic muz API
* public API for spacer
* python spacer-specific API
* optionally disable propagate variable equivalences in interp_tail_simplifier
* optionally disable subsumption checker
* Optionally blast arrays
* eager quantifier instantiation for quantified array properties
* small improvements to bmc engine
* add initialization to unused parameters
* Added missing float conversion in fpa2bv converter. Relates to #1178.
* fixing include paths
* updating includes
* Debug fix in fpa2bv converter. Relates to #872.
* remove relative include from API
* remove local change
* fix build errors
* removing pragmas to make travis happy
* more includes
* updated include directives
* a few more spacer related warning messages
* z3-qe-lite?
* adding cdecl directive to Z3_qe_lite to address build failure for Java bindings
* Fixed build problems with .vcxproj
* renamed LP bound propagator to avoid linker name clashes
* Fixed cmake build
* fixed typo in optimized unsat core plugin code
* refactored variable names and added comments to min_cut-related methods for unsat-core-computation
* Fixed MPF fp.rem(0,0,0). Relates to #872.
* Fixed ML API build.
* Fixed ML API build again
* Fixed LP tests
* updated include directives
* trying to fix build break on use of iterator
* instrument unit test to use reproducible random number generator
* use ifdef instead of if for _TRACE
* moved obj_equiv_class to ast
* use common idioms for factor-equivalence code
* [TravisCI] Try to make the LTO build more reliable.
* update API functions
* update header include generation to use relative paths #534
* fix a but in adjusting term indices for implied_bounds
* use rfind instead of index to avoid prefix clashes #534
* more efficient lar_solver::get_model
* fix #1195
* fix regex bug in theory_str for empty string match. need to fix indents
* fix indentation and add support for re.allchar
* enable overloading resolution on define-fun declarations, fix #1199
* Revert \"fix indentation and add support for re.allchar\"
* fix indentation
* add re.all to theory_str
* update Ackerman reduction for division to make Andre and Nathan happy
* [CMake] Change how the default value of `USE_OPENMP` is set.
* [TravisCI] Unbreak showing interactive log output for non-LTO builds.
* [TravisCI] Add scripts to build and test Z3 on macOS (OSX) and add a single configuration to TravisCI to test.
* rewrite to address some cases like #1203, updates to division handling in NRA
* address bug reported in #1196 and include additional ad-hoc rewrites to handle some string cases
* inc version
* update handling of contains constraints taking string literals into account
* fix for #1202
* recognize theory_i_arith to fix #1200
* address inconsistent states encountered when cancelling, #1197
* deal with absence of integer congruence root by querying arithmetic theory directly, #1202
* revert unsound change in integer extraction from expressions
* handle undefined constant cases for int.to.str
* fix string rewriting according to definition. Relates to examples in #1202
* another fix to str.to.int/int.to.str semantics
* add documentation to string rewriting
* [TravisCI] Temporarily disable the macOS build configuration.
* Drop no-strict-aliasing and fix 2 places where it was violated
* use static_assert in COMPILE_TIME_ASSERT
* micro-optimization in tactics\' cleanup(): avoid dealloc+alloc traffic
* another stab at #989
* fix crash introduced in my previous commit
* revert the patch to remove no-strict-aliasing VS 2012 doesnt support C++11 unions..
* enable QF_UF mode use same parameters whether with or without static featues, #1141
* enable QF_UF mode use same parameters whether with or without static featues, #1141, revert some breaking changes that should not have been part of commit
* add logic \'SAT\' as an alternative name to QF_FD some solverFor(SAT) works too. #1152
* patch
* add missing functions to serialize optimize benchmarks for Java #1215
* add missing functions to serialize optimize benchmarks for Java #1215
* Whitespace
* Bugfix for MAM. Fixes #1213. Partially addresses #1212.
* mam
* Whitespace
* Added diagnostic output for pattern inference.
* Update header includes to be relative to `src/` directory.
* [CMake] Clean up setting include paths.
* Whitespace
* Fixed ref-counting bug in smt_model_checker. Fixes #1212.
* remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210
* remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210
* change typename to class in optional to deal with compilation
* fix compilation of tests
* fix #1217
* :q
* add sequences to ML API #1214
* improve error message in theory_str when an invalid term in str.to.re is encountered
* ensure that timeouts are distinguished from other cancel events #848
* missing parameters for OSX/Linus
* add re.all to NFA in theory_str
* register auxiliary constants from projection operation
* revert local changes to theory_str
* purge iterators
* compiler warnings
* Fixed typo in ML API. Relates to #1214.
* fix regression exposed by segfault2.smt2 crash
* fix crash
* another crash fix
* obj_hashtable: Constify
* First version of the inj. tactic
* add ability to create and manipulate model objects
* Update debug output
* Remove unnecessary parameter
* add comments addressing some questions #1223
* injectivity: Fixup rewriter
* reducing dependencies on simplifier
* fix regressions introduced when modifying macro_util
* trying to get rid of last simplifier dependency in macros
* injectivity: Cleanup whitespace
* injectivity: Add tactic to CMake-based builds
* (Re-)added option to disable lemma deletion in the smt_context.
* added missing addition to smt_params_helper.pyg
* fix build
* [CMake] Teach CMake to support git worktrees. This fixes the bug reported by AATTnbraud reported in #1227.
* removing dependency on simplifier in pattern_inference
* remove simplifier dependencies from ufbv tactics
* [Doxygen] Fix function name in docstring
* remove simplifier dependencies from cmakelist.txt files
* pruning simplifier dependencies
* using rewrite in push_app_ite
* Bugfix: get_objectives in ML API
* fix build issues
* Whitespace
* Whitespace
* move pull/push files
* remove dead code
* Whitespace
* Eliminated the dependency of the macro-finder on the simplifier.
* Revert \"Eliminated the dependency of the macro-finder on the simplifier.\"
* Re-enabled macro-related options for the smt_context
* Whitespace
* Whitespace
* Added unsat core support to the macro-finder.
* update new assertions
* moved files
* remove simplify dependencies
* remove simplify dependencies
* remove simplify dependencies
* remove simplify dependencies
* remove simplify dependencies
* remove simplify dependencies
* mising files
* mising files
* mising files
* mising files
* removing more dependencies
* separate out, add copy constructor
* enforce arithmetic normalization
* removing dependencies on simplifier
* removing dependencies on simplifier
* fixes based on regression tests
* fixes
* purify
* add API methods for creating and modifying models, #1223
* n/a
* fix naming for functions #1223
* update names
* raise an exception if trying proof generation for the SAT solver. Stackoverflow question https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception
* add pre-processing simplificaiton of power to the legacy simplifier Fixes #1237
* complement regular expressions when used in negated membership constraints #1224
* complement regular expressions when used in negated membership constraints #1224
* port simplifications on bv2int
* remove old_simplify dependencies
* include epsilon closure in initial state set, streamline final configuration computation #1224
* initial sketch for dominator based simplifiation
* fix some basic mistakes in dominator code
* remove simplifier files
* elaborate on dom simplifier
* Added global model completion for the SMT2 frontend.
* Model completion bug fix
* update to theory_seq following examples from PJLJ
* update to theory_seq following examples from PJLJ
* fix ordering for value propagation to ensure values are preferred
* prune dead states from automata
* fix perf regression with negative polynomial normalization, adding new datatype plugin
* working on parametric datatype redo
* update rewriting of equalities and monomials for regressions
* remove dom-simplifier from build
* build fixes
* build fixes
* build fixes
* build fixes
* doctest fix
* hide new datatype plugin
* aligning simplifier and rewriter for regression tests
* aligning simplifier and rewriter for regression tests
* re-introduce eq2ineq name for rewriting parameter
* support for smtlib2.6 datatype parsing
* support for smtlib2.6 datatype parsing
* fix seg-fault from #1244
* fix missin clause generation for ad-hoc handling of conjunction #1245
* support for legacy datatype test
* fix bug in generation of non-recursive constructor, modular starting point shifts during recursive calls
* remove extra token
* merge
* rename del to remove to avoid compiler error
* fix front-end for datatype
* fix instantiations
* fix parse/print of ADTs
* fix for #1247
* fixes
* adding declarations for regression tests
* remove unstable sequence interpolant from doc test
* fix #1248, fix #1249
* expand select/store in pre-processor
* copy declarations
* iterator -> for
* na
* fix plugin translation
* remove V2 reference
* fix OSX build
* fix exposed memory leak
* Exposed internal FPA func_decl kinds. Added missing FPA simplifications. Fixes #1242.
* Renamed FPA-internal functions now that they are exposed.
* remove verbose
* add alias bv2nat for bv2int to make it easier to interoperate #1252
* Eliminated unspecified operators for fp.to_
*bv, fp.to_real. Also fixes #1191.
* Fixed BV encoding of fp.to_{s,u}bv.
* Improved FPA models of partial theory functions
* Revert \"[TravisCI] Temporarily disable the macOS build configuration.\"
* Style, formatting
* Fixed bug in ackermannization model converter
* Refactored treatment of unspecified FPA functions.
* Taught the model_evaluator to look for definitions of partial theory functions in the model upon evaluation failure.
* Whitespace
* Debug traces
* Removed unused function
* Fix for model completion (via cmd_context)
* Bugfixes for fp.to_
* operators
* Portability fixes
* add QF_DT
* Fixed bug in fp.to_{s,u}bv
* Tabs, formatting.
* Partial cleanup of util/lp/
*
* Cleaned up LP test code.
* Copyright messages
* Tabs, formatting.
* removed temp file
* Removed unused variable
* Tabs, whitespace
* typo
* check for datatype selectors when model validation fails
* fix generation of symbolic automata with no moves but accepting initial state
* fix #1258
* have quantified tactics work with bound Boolean variables. Adding stubs for match
* add match expression construct to SMT-LIB2.6 frontend
* fix #1261
* remove type annotation from var printing
* Fix warnings in C++ API
* add pattern match validation
* Eliminated the remaining operator kinds for partially unspecified FP operators.
* Eliminated the remaining operator kinds for partially unspecified FP operators from the AST API.
* removing iterators
* add feature to display benchmark in format seen by SAT solver
* add newline
* remove utf fixes #1265
* n/a
* fix #1266 by bypassing topological ordering on theory symbols
* remove display
* check for eof, based on testing garbled repro from #1267
* fixing issue [1269]
* disregard model validation when source expression contains uninterpreted theory functions
* model validation update take 2
* fix pydoc part of `make api_docs`
* fix Python API doxygen (`make api_docs`)
* Removed -std=c++11 from OCaml stubs build command. Fixes #1263.
* fix #1277 fix #1278
* add diagnostics to DDNF and fix #1268
* fix #1276 related crashes for re-sumption after cancellation
* missing setup datatypes for QF_DT
* update to _get_args to convert arguments from AstVector to a python list
* add cancellation checks
* add this->
* dom_simplify_tactic: micro opt
* [TravisCI] Refactor as many CI default options as possible so that the Docker and \"TravisCI macOS\" builds share most of the same defaults by sourcing the `ci_defaults.sh` file.
* [TravisCI] Fix bug where `Z3_BUILD_TYPE` was not being passed as a Docker build argument.
* [TravisCI] Fix bug. `PYTHON_EXECUTABLE` should not be in common defaults. The location is dependent on the implementation.
* dom_simplify improvements with Nikolaj
* #1284 build problems
* deal with empty set of post-orders
* pin elements in expr2depth
* bail out dominators after log number of steps
* adding bv_bounds tactic dominator style
* Removed Ubuntu x86 VSTS/CI build (not supported by VSTS anymore).
* [TravisCI] Workaround slow unit test execution for Debug builds.
* Fix typo
* [TravisCI] Update out of date `README.md` file.
* removed unused variables
* adding backwards pass
* fix debug build
* [TravisCI] Modify Debug configuration that I forgot to change with `RUN_UNIT_TESTS=BUILD_ONLY`.
* reverse arguments
* fix leak
* dom_simplifier: fix dominator computation
* have quantifier equality take names into account
* disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children
* fix build by including mk_pp
* distinguish simplify_rec from simplify immediate argument
* use idom for checking dominator relationships
* fix #1288
* likely fix for #1287
* fix #1286
* fix #1290
* fix #1287, again
* fix #1288, again
* fix #1288, again
* fix build break
* another fix for #1288
* fixes for #1296, removing COMPILE_TIME_ASSERT
* Fri Jun 16 2017 mpluskalAATTsuse.com- Update cmake parameters
* Thu May 25 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 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 2017 jslabyAATTsuse.com- add Z3Config for cmake
* Fri Jan 27 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 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 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 2016 jslabyAATTsuse.com- make -devel require libz3, not z3- add link-against_libs.patch
* Mon Oct 10 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 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 2016 jengelhAATTinai.de- Update descriptions
* Mon Jul 18 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 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 2016 jslabyAATTsuse.com- disable build of examples (unused)
* Wed Mar 09 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 2015 jslabyAATTsuse.com- initial package