z3-4.12.2

Z3Prover/z3

版本发布时间: 2023-05-13 05:30:35

Z3Prover/z3最新发布版本:z3-4.13.0(2024-03-08 03:21:18)

4.12.2 release

Changes:

e417f7d78509b2d0c9ebc911fee7632e6ef546b6 updated release notes for 12.2
ba911009e4fe9a823564bdf924cf559065739842 disable publish
046b80f6a43af5ceff96dfc7114088aa625319b2 remove output
f6ab5a61ac8306a78e09a8a55110c6a125bc8652 reformat code to remove brackets
12e45c9d17aa48151b2c20573fb3b527b32fdb54 Implement proposed smtlib2 bitvector overflow predicates (#6715)
62e1ec069853b22bb82090c17dfbcd013dfd5088 Merge branch 'master' of https://github.com/z3prover/z3
2e441e38c9c3ba202a4c215224c2526100dd422b fix #6713 fix #6714
0c9a5f69fd97e48e45da3dd7ab4edc7b2eb73e4f JS/TS: add Optimize class (#6712)
6c24a70c44aeab3d3de78f8af71fce454cd02342 remove debug output
f17691715bbe6c87e9e40921bd354336a43a8e52 make default argument to ensure_def and mk_def explicit

See More

c64d61bd0a19907233ac1bffa5b9fdc9edb15713 formatting updates
392266c278c3b1ca21a89610e8a731c40a41bca2 fix processing of else expression for model table
d5231f8b3318ca4eee922a29414218d9f7a82922 fix regressions #6703
c48dc6905056c7dbfc976ff7c54e3f7b962c240f adding stubs to find fixed variables
ef943347eec0fd7af188659fc5f7316518fcbb6b ensure assume-eqs is invoked after check-lia statically
d2e3e4895e5d672fe1cf4d748ab0da4e23584e95 add instrumentation to theory_lra for shuffling final check
3029fb24a16c7d22597ab529172cbf0584c68ecc remove references to validating
50c855e2ebc715972b1fa8365a5e4c8fc66cda06 count gcd conflicts, log row id in rows
59bc070268e955cc19a639fdc7f83df4abea49b4 count gcd conflicts
ace6e8eea107e93c5400caff92963c73e9ad4526 add gcd-conflicts stats, formatting updates
8fb45158724de904bb0cafd5b9df0ded1b201af0 remove redundant function, add checker function to test missed propagations
e689dea99ce257d4cef7c73c831448ebcc17616f basic formatting updates
d4fa990b6e5c433dc5205dfb1f012385fb7425da return diagnostics
d8156aeff31fb224531b026daacfafe2222f00e7 weird latent bug in wmax: init() succeeds and it returns undef
fdd5c923edce21a8690ff4c246a6c88e77579e63 use only maxres if there is a lexicographic objective, fix #6697
7a689c3298ea70d100eea427d3edc0d613c7cd73 disable destructive equality resolution simplification if there are patterns
a2bac119d3376ec9be68e88c51590e28772fade3 differentiate fixed from offset-eq in statistics
ec1480b12a2f10f6050124cfbcf4d3cdf51ecd2a fix #6693
cb041c1b6d43208597744233bfca90ae7340927d fix #6689
1319b64bb03b1db8e2c84b6d04e494aa69603f24 fix #6692
97b66d13c043dd392e5146affd0c7281af8f1311 fix soundness bug in disabled code
b75d81f3c2b878726982111dc48b9b4765ad7cca fix #6690
624907823dbf10e5df874eb72989d6afa807edf8 add tests for distribution utility and fix loose ends
1a70ac75df70fb02229d3eebd496721e9d7844e5 fix #6687
b783879752444527a9710fd356c3314bc4d9b1cf #6687
7cd8edce1fce4023fc6bcff54d6180987f5aa71e perf and memory smash fixes to internal node count routine
f0afbcbb877fb6ff222a19e0afa2adefa3debd50 fix #6686
eba0732629e257f67417a46481bd1e54fd61c79e fix #6675
e8222433c3676020b4dc03af7160f18be57c5b60 count internal nodes, use to block expanding use of hoist, #6683
444238bc538e4017c38cf2955daad873503b04f6 formatting updates
f61168cd538dcdaff586317636cf3d9f90251c7a module for maintaining probability distributions
0b5c38dea555a11a70f0ffe6a67ac8f8b5fee9a7 fix #6676 get rid of rem0 declare it to be mod0 semantics to simplify code paths
58a2a9c79c4b0b48a16c537225489fe3fde0c271 fix #6680
ccc4f2d382540b645c3ffdd4c9b0440d09121330 fix #6682
368d60f5536f1881ea10c62c605edf3cc5b30d27 add branch / cut selection heuristic from solver=2
bb44b91e45fbc7eb222baae8d35af15d343cd341 fix #6677
98d3fabc24068182e1b321624a84e14a12db2fc0 Bugfix relevancy propagation + UP (old core) (#6678)
4a142b0f81c16b3e60972a112233d21ee909c540 fix #6623
e6ea81546eb78b6ad1e5920954796f6d1c2074e4 fix #6662
af9c760a68376fb1bbdc2139f5b57869dfe719a7 fix #6670
ccb250c32b6c1075d97b2e43599100f45ac5b749 fix #6671
7b513b4a4012035464f650bfcf4183ed5e4638d6 Some UP bugfixes in the new core (#6673)
84b92046163239331fc6f20ac2951ff67a640ee1 inherit and reset rlimit counter on children limits
f8242c58dd41bdb6cda7860ecdafe1a056b07b56 fix regression from Grobner port
479f8442009987726e3c03fe5618b250acca383a fix #6661
def83ed26edbe786baabfdc760211d8537e10d9d fix #6661
5b385bd2fe03f781e0e59e25139006ae8d9354ce fix #6665
6324db207bd9300928ef610622a399a10040eb97 Only print func-decl names for indexed parameters (#6663)
e0a066efa3d509a7404c503cd95cb5febe32a6fc #6654
7664429fda65291ebe4d43c169f3923fc082a1a3 remove cast expression
a62e4b2893e57192dad477f9f48bb74e1e32a5bd extract multi-patterns when pattern can be decomposed
a849a29b4f0af61730e986b4aed89ba0d05c089f fix #6659
6aaaa3b0156c05ddd1a51b28f14eba91db038270 fix #6660
996e5b1755a30196cf540730954cf7462a7c88e7 fix #6655
b386b84f34b2995147a264c9efc97465592ec974 #6658
667080710366eab733cbf9ce404a7e7b9cb455b7 update ocaml binding to support more string apis (#6656)
130400d76e3cc37e4b6f3a9ed6e8a4781b7f3599 Remove non feasible costs (#6653)
fe348b84c96a50c64979b58feac7bff5e8bb57ef fix #6652
adec9372960c271d1e0b7f67706e8c926a333ead fix #6650
f366772f0c1ce34ee1f2fdaae1f8ad5e31609f51 use field 'm' for streamlined representation
0a59617bac66ceda59f50d67ea036ec75bb72bb7 Fix Ocaml bindings FuncEntry to_string (#6639)
ce09c2ea6dc4fbc92acd435c49c7dcb40650f2e2 fix build
b4ad747e0b1ab7926f9863910b39a9c642b9aad8 fix #6644
8a3a3dc91bf228209615d5c563c7713e47713873 fix #6648
ce501e0b6e6bab4c2d88f6eff434561f172920bf #6646
cd2ea6b703216eaa68b3c86ee182ae443431f882 add parameter access to C++ API
9ca0faa0918c25656bda75c86e9df32b53e99d5b enable interactive example
50bd6efea4baba343afffa26f742b49a47b30970 fix #6624
03a44803b6da631cf7d3773319685e0c0f9fb0da fix #6635
2683a2d6ed9039ddd1a59aeccbdd91f67f7b708a fix #6637
53ca65a62ec2bc441784f7e2ebff1308a0d3c0ef fix unsound rewrite
f075dc28826644052977be6dfe228d3f194b6029 remove experimental files
48de7c2da8dfdcd577c56d601f720d1aecbe390e missing updates
c6e3fb446abbf9c6d99619e0443ca53ee978d1e6 print lemmas2console faster
a9e6e567b054bf0aaa03463b56c15d2a743696c9 make generation of "some" Boolean value fair
d1c7ff1a369711f64bf16165efa5c6e8c8ad423a add unconstrained elimination for sequences
a0f3727e90c4446ba2c1fa7e4392637587ad9632 BV: add missing neg internalizer
cf4df08fd079d6a93a1ed679e9217c5ff07f9d77 fix typo (#6628)
1612b57e1a99c4874a761510161a9b4d376d2825 Make all methods show in java API (#6626)
4b3408696dfe37d41f30d350fda6e0a667086a21 use uintptr_t instead of size_t (tptr) for portability (#6627)
8b0aa22631bb49dac2fd550e783e32aa50ddb310 replace lp_assert(false) with UNREACHABLE
3efe91c3e323cc3e0ce2d48fd04ed57972b84c29 more dead code
1fb24ebc3583735c764ccaa38093536d8fa2a8df fix lp_tst
11eab94321b1efccf040155fea424d34d8440810 more dead code
13549aff6669bb9536bd3c1fe9f6aefbadf23abf rm dead code
c6be67bf3b8f19f7edc37ce34b03805cc0fc040c more dead code
c8c0a001907af348c54e885ebbd45d3a8fce4e79 remove more dead code
748c75275fa3f810e06b569ba04e7368fe8a691c more dead code removal
e430f2881397464bc6620b1c955ccba4ad6c0a13 remove dead code
f6445891f32c7f7c98204ad767779d9e31c0a8b9 rm lu related fields from lp_core_solver_base.h
f351eb3ab276e9ec084311ecd9c807a794412278 remove many methods dealing with double
9ec82632a3e3e746b6fed4b6ea6b85f8e8f587a1 rp precise
569f5be91f4101eaa5cce897f84501b165f9c2b4 rm dead code
f33f8c265ee4ec52d37ec6c27c0e608fddaf6741 more cleanup
0fb65dea3f68e16d9c9dd53f365d27cda71a3a57 rm square_sparse_matrix
178135486c5fb8f20bd433604208ffa54a79f4fd rm scaler
6eedbd4f35d6cee4c2c50ebc0cca88135ac22a38 rm lu
e04e726f45c375c9b4efd0c621812e5782ec71d2 rm lu
2e9dc3d090ba3b91c3996cb9742d2b9696a08ddb rm lu
d00fcc87c9a822d3a995f527e5bca69c400f60b0 Revert "rm dealing with doubles"
a4189186cc5b3b9786ae8415f5faaa9874502097 rm dealing with doubles
6201eda05531dc641e37c2f8812580441eaf5d37 rm breakpoints
73224adc48b6468d8aa48b082919fab1b90d7139 cleanup
377ceba6d58e436a05092b2f57ebe5f068cc78eb rm lu
6132bf93f7b4adddc039b00da4ebe1f606e2b2e2 rm lu
bfe73c01a6e3fbc309213832c051eeb093391b9e rm lu
1da4c018e458919f012f83057026f4f8913aae4f rm lu
62bd3bd1e6f7145564dc444453918b34757e09cd rm lu
5f03c93270b35e2cf43a3063bb6accd548ecf7d4 rm lu
9a7c99da332fae795dc52ea82e4ccba000e2b778 rm lu
c251151d6631bfaf11f9d8eae6cb20979d96ffc0 rm_lu
25f103db1abc5d76412f85ddeb74d24bcb453f5e rm_lp
527f0d124280c59641177087b9c5dd58d9af4c9d rm lu
a38be432642598b2afcaccb050d0f29652d1ea4e rm lu
97c1ba4641138b3990cb93a8aa10c3a1ea6d3f4e rm get_column_in_lu_mode
ea16f6608cafada28378e2707a3ee40a6f2f5f41 before rm lu
f7c9c9ef72fde0e00ef9409e6c24456effb8b930 fix unsound slice criteria (#6625) [ #6617 ]
42076a3c13e67f89e6ab577f1de3f67e870905fd bug fixes to new core, elim_predicates and elim_unconstrained
b9a87e493babf0d545614610942fda0988d3e8c0 minor code simplifications
92fe8c59688b89b165287e63cb560a43139e427e restore the previous state
ff1dc0424ca73b70c314f710737213ea30a3fefe rm lp_solver
5e4bca3d26d5f86edce6baf1331d6e4d72c00ae0 small removals
2dd30fa350a78c9ef7419f8ae8ffde2cc6090000 rm lp_primal_simplex
8989e10e7141d52d9696b5c1a39100e16fb0e6e1 rm lp_dual_simplex
d2e8297d4142f9b58c9bdd16293dae2bdb72af37 remove includes of lp_dual_simplex
2ec09944d726b2bba610423692e2696c729a3b68 removals
a44772424c75a2b5b9219cbdb6799c46602df9f4 more removals
8db2f1409b2c1a17402ac8c3911b83308f252d86 lp_dual_simplex.cpp removed from CMakeLists.txt
cd24c9973945b1338784c43c1b4dc5d2e760534f remove a lp_primal_simplex.cpp from CMakeLists
f986ac6a75b22ea0b7bafe9c5ddaed6cde048007 remove mps_reader
55d45e0c0c2075ebca1b597c8230716a0c26a93a bug fix. Prevent resetting gg stats #6062 (#6618)
b82d177276ae7ff87691c695b086c5b50cc878bd fix build
aa75ba8a6b213e3bb4e2293893a061864cb95fb1 remove parenthesis
fd97be0e3e3f20270ff5968414c184b9894d45c9 move sat.smt.proof.check_rup into solver.proof.check_rup #6616
94b79eefea222f1250e3f569bbd003fb08be0c10 add back max_occs parameter dependency to solve-eqs
acd2eaa39070057af515a43d992de96e988dc64c add (disabled) code path to enable nested conjunctions
46d37b6e307abba2e782e18d907dc2024ebe68d9 fix #6615
027770930e251b72d8c6a4db6e77aab5d73a553d fix bug in quasi macro identification: require quantifiers
25d45a3500cac1291198b00da0f83b147ef08914 fixes and tests for arith-sls
e87fa1c299b9a24503eba580281d154a41ff46d1 remove stale file
79d47eb3029e01635ac12d71bd47a06bfc67e330 add preprocessor parameter whether to use bound simplifier
76aad689c65383f207684510afda9ca5b54c999a Update smt_context_pp.cpp
5974a2dc58221e1037919512bc83880e86c3596e remove m_b from lar_core_solver
1a9990a92f5986a7ed8baf8eca3f211b1e482558 Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612)
6e7d80633da849da13633ca000a05e1573ad509a Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. (#6613)
358caa85e29e56038fe81f2b1cc9e1bc44050e2e Merge pull request #6608 from hgvk94/bugfix [ #6543 ]
828fff96849f5f102e8217b4882650c20f31520b fix #6543. don't assume order on bindings
146f0eae0687c3ee5e7030deff64e5ea6c2774e4 wip - arith local search
4aa05b2b5759a1049464e9ff453c9b448d82b835 remove limiting error mode #6600
755b517001cf3f6926fd448a8e568e32efde0689 fix #6600
0758c930868959937b09d94568ea26bc6297a196 fix #6591
6454e7fa3f541029868519c04acd16433ee2b33b apply rewriting if result of destructive equality resolution is simplified
bc6037464d4f63e7ff8721c36f9b3d7709cf924c clean up build warnings
9b6ac45e022d53b263d5507500ec72b76a5ccb13 compile warnings
6352340478e605711348a1abc8d2fdba23e9474d update do logging
a6eed9f00c1a070e7c97871d2d2f9319b6e82480 Update api.cpp
cb814732603b584511b49a759fe5c99d3627bdb7 add destructive equality resolution to the main simplifier.
c0f80f92ba5f84671dfb56334959202ccc761f78 deal with compiler warnings (unused variables etc)
6092bf534c38ffc9573e4f8475f418f31faacad9 fix #6599
daeaed1e82748c5b404d514bfc418a6ce69c21ee revert debug only changes to sat-solver
c5e33b79b580ddf228c508549fc93bdbd855a0d6 wip - arith sls
f66a082de9e51205b42a910a0640a73172aa5eeb fix #6595
828ff98c77eb5437178b7b8aff902394e29e0445 fix tpl instantiation issue for mingw (#6597)
bd10ddf6aea3808968bbea9f30ad532844d410bf wip - local search - use dispatch model from bool local search instead of separate phases.
ac068888e79c61c037bfdfc58f23b14d853ad55b add trichotomy for sequence comparison. #6586
554a9e8efe71f9bc0aa19b61d8e2cefda7b03a37 fix #6346
7c08e53e944f806af7db74cc512a197c4d76c7f6 fixes for #6590
c1ecc49021c53072d65aba54c2f9cc9ca8d8a284 wip - local search - move to plugin model
a1f73d3805dfa2f32a8d30b36662ab02bb0ebfc8 wip - local search - fix build
4f20b8e2ba92de6d78fcbe0806f70a07dd63fdaf wip - local search
8ce0c56ff5580e199c7c940b49419e792582786b fix #6590
c2fe76569fdb118101e8131f982cc5bfd7cc4438 remove dependency on bool-rewriter in hoist rewriter
a976b781a04e26abf763b2f8029c98a7b0a294b7 fix #6585
44fcf60a72342e0580e92ed70a4d2f528a50b520 wip experiments with sls
9ce5fe707d5d6444843d1647c969f18ccb614d74 track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587
3dc91de531dd835b723b5d572f5024a491a966cf fix #6582
2b7701299371a72c66aa2bab739dca45db9a19bb fix build
52804b5c8f1c67bf6b699d17bb33b2424e2832d0 save on dtt
7956cf120147b4b8cdfb74851196d1026c8c57ca annotate arith_sls
bb81bc5452f9c93a1044544b8b4d6034b22177ce fix #6580
102eee77dcd955a0b938d198444312d46c3e0a34 patch regressions
cac5052685eedb9dca304b623616fc9b8659bf58 fixes related to #6577
ede9e5ffc225f98a02cc27e35de8a99f6ca6c91c [WIP] More TS Binding Features (#6412)
5e30323b1ac7626634e2d1f167296d9f828ed676 wip - bounded local search for arithmetic
4b2c166e8b749f55e420b08653f3e7b7fbb919d6 fixes to build
7bef2f3e6f312b979077ed53dfb4218659321b84 wip - local search for euf/arithmetic
46c8d78ecef31bb24577370400acda501c59522c fixes for #6577
d22e4aa5259137961bc5ae2c45403b9655aa5f1e wip - integrating arithmetic local search
1b0c76e3f0585cde680efcf14bb6b304fca09fc8 fixes to mbqi in the new core based on #6575
d52e893528249b512ef9a302ac291e6ffc1f4ba7 Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576)
02d48adae556ca0e472ec19dfc1dab414e2e55b1 fix #6573
a8335f2d5eb634a0ed6591cf96c8c2fcff8e00a5 use phase
b3ebce3966aa4923550076064ab66193dc5c8632 fix compilation
96d815b9049e7feba128fa32c27a81aa2c42350c adding arith sls
6a2d60a6ba2c8b7012cd3afd32366991d2eb08c3 fix #6571
601e506d54874fe9216ca9881134d517ea34a83d remove debug out
a150e58893b242b093d627b32f1aacd500fc9945 update release script
90a75866fbe1eb66813444ea7c7d0d9a26046fb4 elaborating on local-search rephase strategy
f3ae7692ca6bfe40f677245e8b98d127b709991d update stage name
c1cadd37cc1284e22b15c50d24a76206bd0ea77e update stage name
a7231027c369ff8d7b4a7aee10b70eb8ff96f956 try side-by-side nightly
c1c26f07269539707b3dda264f8bac1843ff8fc2 restart after sat solution
03a4920f3df09ed6ee04dd5f13777fde74ee3a89 fix build
75c573877d0bec64e36a7cf69689915a52c1ba81 updates to ddfw, initial local search phase option
992793bd56d0c9736ae8c407f1fb44ec52df1e1f update nuget packaging targets #6570
3712cbdbfd61237779219c49d06fb69e4d77f852 fix #6559
d69155b9e992df203c7b1240964c1b5829fc548f Shared features from polysat branch (#6567)
be44ace995b0f653406d9e9867a183cbe657ea3c fix typo (#6569)
cb72b962d1f9e73716b9867f7f724c4d65db44f1 Merge branch 'master' of https://github.com/z3prover/z3
839f87a10c919d1c61040c1e91e4d831c3d46071 don't apply tactics in parse mode
39d28189235aba92da2f50a36ad864e7cf7fd66e compiler warnings/bugs
0d05104d8c68eaa15ce2659eb8b7c1f3de277af0 remove unused field
741634b7032a9c449c19d571f8e8622e0df61176 compiler warning fix
efbecb19b162a767afe3ee62291018a757413791 compiler warning
ed4a84e5d3637d3a0e4088dd1613055a7972cf07 compiler warning
4143c542571948368a6a36334a21392ed50ddb3f add simplifier to java API
2e068e3f563a04a0ddf085b55fd249ccb226b92d add simplifiers to .net API
72e7a8a4817537e82cd851d93f1879b0f51635bf fix incremental pre-processing to work with consequences/cubes
6c7dd4a8634886e6ede8ccfaf71bb21f2a9d6641 fix incremental pre-processing to work with assumptions/cores and consequences
7767144051d877945080c0ca83df1e4289263775 fix test
30fa37e3936fc5508a34c262a68b9444368e53c8 fix warnings
38d526ee4505c9109ecdc9e1f134946539c4e3a1 fix warning
682e86812927f00fe69b532fb7660018aa2de64e initialize field
0f86a00229991b7e42ba86119d4460db853106d9 use setter method to easier track updates to settings.
19fed09122a07cf177361d7012fc0682849e6374 protecting add_simplifier API against mis-use
151a62338cf3cfb9858d7bc7ad8d84154dcf44a0 Bump docker/build-push-action from 3.3.0 to 4.0.0 (#6562)
63c0f35978773c24f8c29c6279e1f0d3c99215ac update ml api
d51d518f96778ad27a67160ed214c959829843c6 update ml api
1289937d1a7b0aa28b311dcbb59a4338a7de8149 update ml api
9a94a9aa6f49fd7bd3e21f0a34563e7fab0c4456 update ml api
17bae9b4c1897f6ac2163aeb7f84b869b3abda77 update ml api
162fa3dc96f8aafadc2562a6dd528871694d18fe disambiguate overloaded with for Julia bindings
4c6d44f974d16210436c51b07c3f57ab8f0e649d add ocaml signature for simplifier
550619bfcf7bb7fcf958f18389d34d7b3e6286ed add API for creating and attaching simplifiers
ebc2cd572b1952635842ada67d239b52d739df06 fix build
88bf3c6e516276bb813b2e57be6309aec529a9a3 check if trail is empty to avoid collecting variables
8495be11f97862a61a184789ed55e73bb43f1246 add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model
6d8d8f197105d86d3af180e382533f2839756f0c fix release message
e6f8fe359e2bb5e8216d409e312d1e6250c09be7 remove empty file
d263b373edc551709e8d4f222af6d2e12a65baf1 update release notes