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

1203 commits

Author SHA1 Message Date
Nikolaj Bjorner d174f87c5e #5532 2021-09-21 20:21:23 -07:00
Nikolaj Bjorner 2e96557827 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:55:28 -07:00
Nikolaj Bjorner 72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
Nikolaj Bjorner da60abd84b #5445 2021-08-03 11:19:42 -07:00
Nikolaj Bjorner 202ed79a24 #5445 2021-08-03 11:17:23 -07:00
Nikolaj Bjorner a4cc9e7895 #5429 #5445 2021-08-01 12:49:36 -07:00
Nikolaj Bjorner 16413b4f9a #5429 2021-07-27 17:18:22 -07:00
Nikolaj Bjorner 005d35f9c9 #5422 2021-07-21 07:39:39 -07:00
Nikolaj Bjorner ca8f914dd8 #5422 2021-07-21 07:22:05 -07:00
Nikolaj Bjorner b0a22105d6 na 2021-07-19 13:28:20 -07:00
Nikolaj Bjorner 188a478214 #5417 
strict inequality (over reals) require solving for least-upper/greatest-lower bounds that may coincide with non-strict inequalities (be epsilon stronger). Instead of using the coefficient 'a' to turn the inequality into an equality, add the slack value as a constant.
 2021-07-19 13:19:03 -07:00
Nikolaj Bjorner cab1076514 #5336 2021-07-11 21:00:58 +02:00
Nikolaj Bjorner 55daa2424c fix #5362 2021-06-22 12:26:27 -07:00
Nikolaj Bjorner c1ab7987f6 #5324 2021-06-07 11:41:35 -07:00
Lev Nachmanson 3a5b88e52b set status to CANCELLED on the total_iterations threshold bailout 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-06-07 07:34:16 -07:00
Nikolaj Bjorner 9afc59d5b4 #5324 2021-06-06 15:39:23 -07:00
Nikolaj Bjorner 7cd901019f #5324 2021-06-05 17:14:51 -07:00
Nikolaj Bjorner 5da4b29136 turn on parity test 2021-06-04 10:18:24 -07:00
Nikolaj Bjorner 0182187296 fix regression in arithmetic resource bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-03 11:41:42 -07:00
Nikolaj Bjorner 8a02167e30 get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:08:08 -07:00
Nikolaj Bjorner 3e773fba5e get-universe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 21:07:48 -07:00
Nikolaj Bjorner 6a5cdd48e7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:43:45 -07:00
Nikolaj Bjorner ab3b387076 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:37:43 -07:00
Nikolaj Bjorner 45adfc6a66 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 20:31:05 -07:00
Nikolaj Bjorner 0e6d530518 std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-01 18:49:37 -07:00
Nikolaj Bjorner 2156c74d51 #4702 
initial gcd test implementation for accumulated parity constraints
 2021-06-01 15:26:36 -07:00
Nikolaj Bjorner 5127014f18 track cuts 2021-06-01 15:26:36 -07:00
Nuno Lopes f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nikolaj Bjorner 8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Nikolaj Bjorner 00deb12238 signed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 15:51:27 -07:00
Nikolaj Bjorner ec034679ce #5215 
memory leaks
 2021-05-19 12:42:38 -07:00
Lev Nachmanson 179988e161
support recursive terms (#5246) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-05-05 12:53:20 -07:00
Nikolaj Bjorner 0c6722f48b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 11:47:00 -07:00
Nikolaj Bjorner 60cf482cea fix #5239 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 11:44:44 -07:00
Nikolaj Bjorner 51a4db862a #5223 2021-05-02 10:40:22 -07:00
Nikolaj Bjorner 0810720267 #5223 2021-05-02 10:30:35 -07:00
Nikolaj Bjorner 22a76e4985 fix typos in comments 2021-04-26 15:15:27 -07:00
Nikolaj Bjorner c03fac8390 Investigating std::vector and #5178 2021-04-24 14:50:59 -07:00
Nikolaj Bjorner d67919373e add bailout option for code review #5208 
@levnach
Could you review and maybe make this much more streamlined?
The patch is to simply bail out the iterator if it fails to find canonical monics.
If m_ff could produce the existing canonical monics up front this kind of bail-out could maybe avoided.
 2021-04-22 11:30:11 -07:00
Nikolaj Bjorner 770c79a939 prepare for std::vector 2021-04-20 09:24:24 -07:00
Nikolaj Bjorner 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Lev Nachmanson 1a7c9fa54d rename a metod 2021-04-10 08:54:52 -07:00
Lev Nachmanson 6a1fd3b4d6 simplify the check for polarity, remove the struct with vertex and polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00
Lev Nachmanson 8848e5b4c3 correctly explain the all fixed test in the octaganal tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00
Lev Nachmanson 18610bf31f debug issue 5127 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00
Nikolaj Bjorner 46831e7ebb provisionary fix for #5127 2021-04-06 22:32:22 -07:00
Nikolaj Bjorner 0b0efa83ca debugging #5127 2021-04-06 20:09:50 -07:00
Nikolaj Bjorner c2b353ba72 adding factorization 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner 67e419d20d yada yada 2021-03-21 19:57:17 -07:00
Nikolaj Bjorner 2ee971ef68 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-21 12:32:01 -07:00