z3-4.8.9

4.8.9 release

Changes:

• 79734f2 move to python3 for release.yml
• 6e7a80b change version number
• c481570 disable pip in trial release
• f4e8205 na
• cfa7c73 fixing #4670 (#4682)
• ee00542 update release notes
• 1c7d27b fix missing parenthesis in C++ API
• f976b16 add macros to model #4679
• 629e981 fix regression in get-consequence on QF_FD
• 80879ce remove xcode

See More

• 7327023 add variable replay, remove MacOS from Travis (#4681)
• af54a79 fixing issue #4651 (#4666) [ #4662, #4667, #4665, #4661, #4668, #4676 ]
• d02b0cd running updates to bv_solver (#4674)
• 4d1a2a2 update to xcode 9.2 for Travis
• 687a16a SMTFD is back (#4676)
• f370d8d na
• 7fbaf71 na
• 65bc77d na
• fe43f8d na
• aa66be9 na
• d83d0a8 na
• e4b7b7b na
• 95493f7 na
• 4b22434 na
• 54a75d6 remove SMTFD
• 7c2fe46 build fix
• daf7e9e file
• 1163908 prepare for theory plugins
• 141edef butterfly effect on fp?
• 527bf72 Remove duplicate binary condition. Fixes #4668.
• ecddaea na
• 74a2bf1 Merge branch 'master' of https://github.com/z3prover/z3
• 03e92f3 with bounded
• d4e92d4 move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph
• fa9cf0f mk-var during copy
• ed7d969 elaborate on smt/drat format outline, expose euf mode as config
• 4d41db3 adding euf
• 314bd92 avoid duplicate class names frame in sat_scc and sat_smt
• bee3077 free memory in egraph
• a003af4 release nodes
• bbe027f na
• 2510686 fix dotnet build
• 9f0b303 na
• 727ea43 remove lazy push from theory_lra
• 9b5dc0c fix misc issues around #4661 introduced when adding lazy push/pop to selected theories
• b992f59 expose name inclusion as optional
• dbe2c9b encoding options #4665
• e8826bb fix #4651
• 4682b48 na
• 86310a1 updated sat_smt
• e9a4e48 dbg
• a35d00e remove pragma
• 996905a fix warnings
• 35e3d84 move fpa
• 11c90cc move parameters from ast/rewriter to params
• 507b4c7 path
• 4983805 virtual method
• 98084d7 add depend
• 7c592d4 add depend
• f6b242e update cmake
• 455d53e missing cmakelists
• e2bdf54 update include
• 79fc3f2 warnings /errors
• b9cbb08 shuffle dependencies
• 4e6476c fix cmake build
• 60f8884 sr
• b8fb744 reset caches
• 739b537 dbg build
• 93ee2a6 persist fields
• 86c11b9 order
• b03d1c8 deps
• ba21ffa missing file
• 0440cfe add smt params dependency
• 4244ce4 adding ack/model
• 7f0b5bc Allow to skip System.loadLibrary() calls from Java Native class (#4667)
• 6706b0d na
• 872fd5e fix #4662
• c6135a4 virtual
• 4ab35a9 euf model
• e6e635b remove unneeded pragma
• 21e13bc re-add pb extraction
• 526d76b re-add pb extraction
• 9c77fbc use virtual destructors
• 1a36d44 na
• c21a2fc sat solver setup
• 78b88f7 updated rewrite rules to propagate nullability over nonground regexes (#4663)
• ab10616 fix build
• ecd3315 add sat-euf
• a7b51d0 remove unused file
• 22aee4d fix issue in #4655
• c722962 fix regressions in python API for user-propagator
• e46ad45 na
• 6beec7b na
• dc1783a na
• 3dedc13 na
• 65e6d94 euf
• 96587bf na
• 85b4fc1 void
• 43d9323 apply operator
• 84475ff fix #4637
• 666e835 na
• af389db build break
• 03276b1 na
• 96f10b8 user propagator
• 5e5ef50 re info extension (#4659)
• a58b8ce na
• db65381 extended calculation of info for regexes (#4656) [ #4658 ]
• 2d5b749 extend solver callbacks with methods
• 1e29ba7 renamed compl method (compl is a reserved c++ keyword) to complement
• 4dd9249 trying to remove invisible control characters
• 8285162 fixed type bug: bool to lbool
• 7b478c8 fixed loop lower bound bug in loop info and default nullable value in invalid_info
• 6b11af7 Merge branch 're-info-extension' of https://github.com/veanes/z3 into re-info-extension
• 3fb226d added missing return statements, reordered def of compl to match declaration order of methods
• 1099c51 took care of PR comments and fixed some info calculation bugs
• 93bc1bc extended calculation of info for regexes, updated tracing of state_graph with regex info
• 080be7a merge
• 22b5daf fix rlimit for clang-10 (#4658)
• 4879258 took care of PR comments and fixed some info calculation bugs
• 738d091 extended calculation of info for regexes, updated tracing of state_graph with regex info
• ecb43cc update smt logging format to follow SAT solver
• 7708874 missing override specifiers per #4654
• eef05e0 user propagator
• ba4a218 user propagator fixes
• de65c61 renamed re to rex and added custom pretty printing for info (#4650)
• 79aa345 prop
• 5aaa7e0 fix #4648
• ed258ca approximate min-length for complements
• 4857d60 user propagator over the API
• c50e869 computing and memoizing info for regexes (#4647)
• 747a8ff initial sketch of python bindings
• 0c93c7a adding user propagation to API
• 578ddf3 na
• 152c95f adding user-propagator ability
• c13e3ce fix #4640
• df8b14d fix #4641
• 2611484 fix #4642
• 33d96c1 fix #4643
• e591b32 set guard/cf and dynamic base in release
• f030843 use lazy scopes to avoid push/pop overhead
• 558233d build fixes, add lazy push/pop state to avoid overhead on unused theories
• ca3ec22 handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching
• fae206b add command-line help descriptions on tactics
• c0a07f9 tidy
• c4a03dc remove temporary comment
• 363b416 pp support for regex expressions in more-or-less standard syntax (#4638) [ #4636, #4637, #4588 ]
• 1233cb4 added missing const declarations that caused build failure on some platforms
• 0d9dc03 Merge branch 'regex-pp-compact' of https://github.com/veanes/z3 into regex-pp-compact
• 1567587 fixed bug in seq_unit
• e80b143 updated detection of when parenthesis can be omitted to cover empty and epsilon
• ae41336 further PR comment fixes
• 5f9a326 took care of comments for related PR
• 2c33bd6 pp support for regex expressions is more-or-less standard syntax
• bfae1c4 fixed bug in seq_unit
• 9729db1 always reduce macro expansions in model evaluation #4588
• 5b663aa updated detection of when parenthesis can be omitted to cover empty and epsilon
• be6f7bb further PR comment fixes
• 094e41d build
• 7d391d4 #4637
• 024ccf1 took care of comments for related PR
• a892e47 typo
• 2c02264 Regex solver updates (#4636)
• 3ab75bd pp support for regex expressions is more-or-less standard syntax
• 9df6c10 handle small powers in theory_lra #4616
• c63ad2e enable ranges for bit-vectors
• 72d1403 fixes for #4634
• c41abf2 fix #4624 #4633 #4632 #4631
• 8439057 fix #4624
• 11d5b50 fix #4625
• 4045563 fix #4626
• 5ecc59b fix #4627
• a5e4e52 fix #4628 - not really a bug, but style nit. uf1 and uf2 need both to be called
• be3c3da add bound refinement propagation
• 7fc4653 fix #4623
• 9f7e80c trace also declarations in assumptions
• 1f48eab allow Boolean arguments to bit-wise logical operators #4618
• e5693b8 added support for saving state graph in dot format (#4621)
• 3852d45 modular Axiom Profiler (#4619)
• 934f87a dgml output generation for regex state graphs (#4620)
• a51e40a gc perf fix
• f4ec63f z3str3: add auxiliary str.substr axioms (#4617)
• 4fa2e23 overload bit-wise operators to work for Booleans for convenience #4618
• db009e2 overload bit-wise operators to work for Booleans for convenience #4618
• 7ae7068 revert breaking change
• 7eb05dd ensure lengths are registered for disequality fixe #4613
• b82dff5 Use Z3_ option prefix in cmake with Java bindings build command (#4612)
• 7fa5b31 adding back dropped return statement (#4611)
• 06f34bd tidy
• 8137143 string to regex approximation used to strengthen membership constraints (#4610)
• fb035c0 fixed a but with insertion of a null vertex
• 566a0d5 simplify has-fixed-length
• 97ed1cd don't rewrite empty/non-empty checking predicates
• 615e2cf don't rewrite empty/non-empty checking predicates
• b4f994b fix loop
• 4392c03 better behavior on disequality and branch selection
• 02084dc misc
• 3f862cb better behavior on disequality and branch selection (#4605)
• e0d4669 na
• ac64a37 change default
• 6cfbda0 remove automata references
• 976e4c9 Integrate new regex solver (#4602)
• 293b0b8 fix build
• 3a26dcc fix build
• e0a9848 fixing build
• 69b4a81 rewrite to_int comparisons
• f6cbe3a propagate on variables
• 4039352 add ability to touch variables for bound propagation
• a74ef39 some more rewrites
• 59d8895 add accessors for implied values to API
• 4628cb8 check for negation, not complement
• 42b42dd use bounded pp for cubes
• f7b2407 for #4588
• 8857a67 fix model return after shutdown, reported in #4532
• b71a643 sketch fixed-length heuristic
• 5664b57 Seq rewriter integration (#4599)
• afdfc5e z3str3: fix incorrect automaton polarity in intersection check, and clean up code (#4595)
• 6910c0d Revert "Seq rewriter integration (#4597)" (#4598)
• e90f010 Seq rewriter integration (#4597)
• 2fb914d z3str3: construct correct counterexamples for string-integer in model construction (#4562)
• d591bf6 add to readme #4575
• 9624df9 na
• a08082e fix #4594
• ae502bc simplify a few of the several axiom trace commands
• c7704ef pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532
• ac39ddb flush gmc for sat-preprocessor model bug #4532
• e8ef9a8 fix #4327
• 4be6927 unused variable warning
• 78afa25 unused variable warning
• 4d586c2 remove stale references to gac/csc
• 105f97d #4582 again
• 2133ba0 prepare for theory variables othe rthan seq/re
• f789573 prepare for alternative axiom
• 2d4839f #4582 again
• 1059f6d #4582 again
• 963daab #4582 again
• e63992c fix #4589
• 780346c address model generation bugs raised in #4518 and #4324
• e1d2b88 access polynomial expressions from algebraic numerals
• a6a041e setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586
• 71a32f5 remove unused
• 45855fc fix
• dd5e2e8 check for 0
• 640cf18 Merge pull request #4585 from iscottb122/dotnet_fp_significand [ #4584 ]
• b6867d6 Return significand bits correctly (dotnet API). Fixes #4584
• ed58175 issue #4582
• aab50ff fixing bugs reported in #4518
• b1824fe fix lifetimes for crashes in #4525
• f17ead2 fix #4578
• 1d8d85a fix #4575 - correction set resolution only works with uniform weights
• ebce0b3 fix #4577

This list of changes was auto generated.