3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Commit graph

11218 commits

Author SHA1 Message Date
Nikolaj Bjorner 2eea7709e0
Merge pull request #2438 from agurfinkel/issue_2430
Fix issue 2430
2019-07-26 08:18:29 -07:00
Nikolaj Bjorner 53aded3198 fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-25 18:55:44 -07:00
Arie Gurfinkel 92db639caf Use refutation to compute ground sat answer 2019-07-25 15:22:37 -04:00
Nikolaj Bjorner 8a0d79251e make sorting of soft constraints the same across implementations of std::sort
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-25 11:32:49 -07:00
Nikolaj Bjorner e6df7b73aa fix #2434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-25 09:40:18 -07:00
Nikolaj Bjorner ca25e482e5 temporarily disable elim_pure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 19:01:23 -07:00
Nikolaj Bjorner c75a57731f fix #2433
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 14:14:18 -07:00
Nikolaj Bjorner 859512d937 fix #2431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 12:14:02 -07:00
Nikolaj Bjorner e17b43617c na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 12:05:48 -07:00
Nikolaj Bjorner 604e6b2705 fix #2418, change types in sat_solver to avoid cast
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 11:52:28 -07:00
Nikolaj Bjorner 809b0ebca7 revert fix to #2417
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 11:24:01 -07:00
Nikolaj Bjorner 3a90de1cbe fix #2419
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 10:09:34 -07:00
Nikolaj Bjorner e65a5d0f47 fix #2420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 09:56:11 -07:00
Nikolaj Bjorner 019d78e219 fix #2422
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 09:51:04 -07:00
Nikolaj Bjorner 1a70fce92e add back nvars
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-24 09:51:04 -07:00
Nikolaj Bjorner 185b01dd35 fix #2416
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-23 19:01:49 -07:00
Nikolaj Bjorner c2264c73f2 debug mutex
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-23 19:01:49 -07:00
Nikolaj Bjorner df04d7f108
Merge pull request #2428 from danielschemmel/warnings
Fix Some Warnings
2019-07-23 08:45:34 -07:00
Daniel Schemmel 77d5b381ea
Order initialization to avoid -Wreorder 2019-07-23 11:12:29 +02:00
Daniel Schemmel 5e5c231712
Remove unused variables 2019-07-23 11:09:50 +02:00
Nikolaj Bjorner 364fbda925 expose reorder config
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-22 15:30:06 -07:00
Nikolaj Bjorner aff4b3022a fix #2417
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-21 10:57:52 -07:00
Nikolaj Bjorner a9a26e5f2e review comments by Elffers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-21 06:52:02 -07:00
Nikolaj Bjorner e593b5b2c8 fix #2415
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-20 16:23:01 -07:00
Nikolaj Bjorner 43a19cadf6 avoid reorder regression. affects performance of SAT and also noticably for #2405
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-20 12:40:22 -07:00
Nikolaj Bjorner 41ca956012 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 13:45:13 -07:00
Nikolaj Bjorner 7ed5ca05e3 fix #2408
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 08:37:00 -07:00
Nikolaj Bjorner d07f2d45e7 fix #2409
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 08:33:58 -07:00
Nikolaj Bjorner 1fca76b0a1 relax restriction on infinitesimal for rdl, #2410
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 08:26:23 -07:00
Nikolaj Bjorner 5820b16800 mark assumption literals to be skolem to hide them from models #2406
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 08:25:42 -07:00
Nikolaj Bjorner 4b6a7371dd insert fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-18 06:31:47 -07:00
Nikolaj Bjorner fb124d6e93
Merge pull request #2393 from Nils-Becker/master
Fix Incorrect Logging of Newly Introduced Terms During Rewrite
2019-07-14 09:25:06 -04:00
Nikolaj Bjorner 4deb9d2af2 use array interpretations whenever possible for #2378. Also strengthen equality test for lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-14 09:23:29 -04:00
Nikolaj Bjorner 3ca32efd18 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-13 16:22:09 -04:00
Nikolaj Bjorner 2d4e9a0f67 update managed APIs for lambda-based array models #2400
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-13 16:20:36 -04:00
Nikolaj Bjorner 659be6940b fix #2395
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 18:01:26 -04:00
Nikolaj Bjorner 26c1c744aa fix #2396
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 17:36:30 -04:00
Nikolaj Bjorner 0bca2aabff remove invocation of debugger
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 17:07:44 -04:00
Nikolaj Bjorner 559af09b07 fix index cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 19:01:39 +01:00
Nikolaj Bjorner 84990ffa27 fixing #2378
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 14:21:22 +01:00
Nikolaj Bjorner be72accaf5 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 12:37:46 +01:00
Nikolaj Bjorner 1538b31dd9 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 12:37:24 +01:00
Nikolaj Bjorner d861b91289 augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 11:13:05 +01:00
Nikolaj Bjorner 79e4b84507 augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 11:12:01 +01:00
Nikolaj Bjorner 1ba6d16c61 augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-12 08:38:33 +01:00
nilsbecker 308647efd9 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-07-11 17:22:10 +02:00
nilsbecker 335072eda2 extract logging into separate function 2019-07-11 17:22:03 +02:00
Nikolaj Bjorner cfb4d289b8 fix #2325
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-11 10:34:35 +01:00
Nikolaj Bjorner c7fb1e4c9f fix spelling of target folder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-11 09:56:08 +01:00
Nikolaj Bjorner 9474833c98 fix #2391
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-11 09:26:22 +01:00