mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
11272 commits 23 branches 48 tags 157 MiB
Commit graph

9236 commits

Author SHA1 Message Date
Nikolaj Bjorner ce84e0f240 remove strategic solver header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 15:56:04 -07:00
Nikolaj Bjorner fc41a61b6e expose strategic solver factory prototype at level of solver module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 15:52:12 -07:00
Nikolaj Bjorner 1ae0a98132 fix #2466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 13:37:22 -07:00
Arie Gurfinkel 52acbf1f14 bug in qe_lite 2019-08-09 13:31:49 -07:00
Nikolaj Bjorner e2d91ce1fc distribute concat over bvxor and bvor, #2470 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 10:03:21 -07:00
Nikolaj Bjorner 8579a004d0 distribute concat over bvxor and bvor, #2470 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-07 15:14:58 -07:00
Nikolaj Bjorner e950453685 force propagation for smt cubing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 14:19:16 -07:00
Nikolaj Bjorner bbfac99b22 fix #2469 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 13:52:42 -07:00
Nikolaj Bjorner 0af249d651 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 13:44:12 -07:00
Bruce Mitchener f90439fdc5 docs: Fix a number of identifier formatting issues. 2019-08-04 18:48:30 -07:00
Bruce Mitchener 077f518241 Fix -Wreorder warning. 2019-08-04 18:37:31 -07:00
Bruce Mitchener ce7f9c3f3d Remove unused variable. 2019-08-04 18:37:05 -07:00
Bruce Mitchener 6be36f18c6 Fix typo. 2019-08-05 07:31:55 +07:00
Nikolaj Bjorner bc3b0f6e33 introduce fresh term when none is available in context or model to fix #2456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-04 12:00:48 -07:00
Nikolaj Bjorner 01920abf46 introduce fresh term when none is available in context or model to fix #2456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-04 11:57:30 -07:00
Nikolaj Bjorner 59f69bbe0d introduce fresh term when none is available in context or model to fix #2456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-04 11:56:03 -07:00
Nikolaj Bjorner c7dc420b3b let me guess, ASAN doesn't like 0-byte memcpy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 23:19:59 -07:00
Nikolaj Bjorner 90415a18d3 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 08:42:16 -07:00
Nikolaj Bjorner d7ac8dbc7d fix #2458 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 08:36:25 -07:00
Nikolaj Bjorner 3147d2351d fix #2460 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 08:06:38 -07:00
Nikolaj Bjorner 4431a534b3 fix #2450 - track assumptions across lazy explanations and variable equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 07:57:16 -07:00
Nikolaj Bjorner db5af3088b logging for #2450 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 16:47:18 -07:00
Nikolaj Bjorner 1d488d07fa nlsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 2d5714a5d4 fixing #2443 #2445 #2447 #2448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 584eee2cf4 fixing #2448 and #2445 and #2443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Nikolaj Bjorner c4480337c4 fixing #2448 and #2445 and #2443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 3d1c40ce23 fixing #2448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Lev Nachmanson 95eb0a0521 remove an unnecessary call m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-08-02 09:53:32 -07:00
Nikolaj Bjorner 294dcf7b1c
Merge pull request #2455 from levnach/fix 
fix a bug in lar_solver in querying if a column is int
 2019-08-02 08:19:34 +08:00
Lev Nachmanson e9e950062a fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-08-01 14:09:26 -07:00
Lev Nachmanson db5ac5afa8 fix a bug in lar_solver in queryaing if a column is int 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-08-01 11:51:56 -07:00
Nikolaj Bjorner 9d6728aa71 fix unsound rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 01:14:31 +08:00
Nikolaj Bjorner 0a29002c2f return unknown if m_array_weak was used and result is satisfiable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 00:20:41 +08:00
Nikolaj Bjorner 3f032e85e0 remove include of thread 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-01 16:34:37 +08:00
Nikolaj Bjorner bec38f268b remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-01 16:32:08 +08:00
Nikolaj Bjorner 7f073a0585 fix #2452 fix #2451 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-01 16:28:15 +08:00
Nikolaj Bjorner a2b18a37ec fix #2449 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-31 06:55:10 +08:00
Nikolaj Bjorner e1fd167e01 remove stale assertions due to lambda #2446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-30 14:35:09 +08:00
Nikolaj Bjorner 74631265b9 remove stale assertions due to lambda #2446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-30 14:32:06 +08:00
Nikolaj Bjorner 902c683b92 expose _get_ctx for scope semantics of newer versions of python #2441 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-29 07:54:47 +08:00
Nikolaj Bjorner 2bd8d3b485 fixes for input4/5 #2416 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-28 10:28:01 +08:00
Nikolaj Bjorner 728139599c unfinalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 16:43:42 -07:00
Nikolaj Bjorner 00a4f6ad3d throw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 15:28:38 -07:00
Nikolaj Bjorner 1d223b0403 setting ctx to null after close 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 14:59:19 -07:00
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
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 9474833c98 fix #2391 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 09:26:22 +01:00
Nikolaj Bjorner adb91ae93c compile 0 case regardless of numerical value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 09:07:18 +01:00
Nikolaj Bjorner 8d9a631c5d try to copy artifacts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 16:21:14 +01:00
Nils Becker 1d859a98e5 updating comment 2019-07-10 17:12:08 +02:00
Nils Becker 7a48524213 count subterm references correctly 2019-07-10 17:09:21 +02:00
Nils Becker b226f3a77c cleaning up includes 2019-07-10 16:43:48 +02:00
Nils Becker 035101f399 Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2019-07-10 16:18:00 +02:00
Nils Becker 23d01f5974 fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with) 2019-07-10 16:17:30 +02:00
Nikolaj Bjorner 5de35d46eb fix #2390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 08:55:00 +01:00