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

12806 commits

Author SHA1 Message Date
Nikolaj Bjorner d8423a4b46 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 20:53:58 -08:00
Nikolaj Bjorner 11199619a5 prepare for throttling gcd test and patching based on cost/success ratio 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 19:02:56 -08:00
Nikolaj Bjorner 4f3fbd3c11 align parity with signs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 15:49:58 -08:00
Nikolaj Bjorner 833b54a12c fix dotnet build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 09:44:21 -08:00
Nikolaj Bjorner 915ff38f97 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 09:28:45 -08:00
Nikolaj Bjorner f0689546f3 return non-escaped string value for Python 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 09:16:23 -08:00
Nikolaj Bjorner dddd740846 make aig/ite extraction conditional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-25 16:27:13 -08:00
Nikolaj Bjorner afa34a1c12 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-25 12:58:45 -08:00
Nikolaj Bjorner 39061d7388 disable unsound simplify, rename stats, delay region allocation for cutsets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-25 12:40:16 -08:00
Christoph M. Wintersteiger 963f8240c2
Throw proper warning instead of assertion violation in fp.rem. Fixes . 2020-02-25 17:17:41 +00:00
Nikolaj Bjorner 198622b61a fix fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-25 02:18:01 -08:00
Nikolaj Bjorner e1ece7e968 CTRACE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-24 20:24:42 -08:00
Nikolaj Bjorner 238ff78374 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-24 09:01:31 -08:00
Nikolaj Bjorner b68efe44af fix fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-23 12:28:15 -08:00
Nikolaj Bjorner cb6eb0fc96 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-23 09:48:45 -08:00
Nikolaj Bjorner 5af139055d fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-23 09:45:05 -08:00
Nikolaj Bjorner c71da17a10 add output for inprocessing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-22 11:50:51 -08:00
Nikolaj Bjorner d1e95a133b add simplifiation pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-22 11:21:53 -08:00
Nikolaj Bjorner ab9bcfdcce fix , bound iterations of subpaving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 20:36:58 -08:00
Nikolaj Bjorner 589db2052a fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 20:26:57 -08:00
Nikolaj Bjorner dcd4fff284 fixes to cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 18:06:57 -08:00
Nuno Lopes 7d8b56027f fix : unsound cache of exprs in or expression 
this tactic has a quite broken caching mechanism (needs a stack).. :S
 2020-02-21 18:48:54 +00:00
Nikolaj Bjorner 1aea0d2c8b fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-20 21:05:21 -08:00
Nikolaj Bjorner 84b12dddac fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-20 20:41:59 -08:00
Murphy Berzish f604fad779 z3str3: fix negated str.contains, add reduction for str.at 2020-02-20 11:46:29 -10:00
Nuno Lopes 55df045f85 fix : missing cache reset in dom_simplify of not 
just introduced the bug 5 mins ago..
 2020-02-20 18:05:52 +00:00
Nikolaj Bjorner 8b97e26fd7 cut fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-20 09:55:17 -08:00
Nuno Lopes c9be09b18c fix : incorrect handling of ands simplified to false in dom-simplify 
+ add support for not operations
 2020-02-20 16:21:46 +00:00
Nikolaj Bjorner 3bb05b5e01 fix lut augment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 18:36:28 -08:00
Nikolaj Bjorner a543099a4f fix again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 10:04:44 -08:00
Nikolaj Bjorner ff436ecb10 fix again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 09:52:27 -08:00
Nikolaj Bjorner a4d81b2847 fix fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 09:52:26 -08:00
Mathias Soeken 290b4dfabc More cases needed to find all ite clauses. 2020-02-19 09:03:58 -08:00
Mathias Soeken 00e43b6b88 Constructor compares arguments, not member variables. 2020-02-19 07:00:37 -08:00
Mathias Soeken b464cf26bc Passing functor by const-reference allows to use lambdas as arguments. 2020-02-19 07:00:37 -08:00
Nikolaj Bjorner 44a79d05c8 debugging cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 06:45:23 -08:00
Nikolaj Bjorner f962dc8b00 disable msan build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-19 06:44:31 -08:00
Nuno Lopes 1ac365ca74 fix : soudness bug in dom-simplify 2020-02-19 13:02:45 +00:00
Nikolaj Bjorner 006caea5ba fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 23:11:45 -08:00
Nikolaj Bjorner 953ea7c880 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 23:08:59 -08:00
Nikolaj Bjorner 4bad2dd92c fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 22:58:14 -08:00
Nikolaj Bjorner cc2cd5b557 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 22:57:30 -08:00
Nikolaj Bjorner dd3e77107e rename aig_simplifier to cut_simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 18:29:59 -08:00
Nikolaj Bjorner 8860de39bb ull 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 18:08:11 -08:00
Nikolaj Bjorner e016979ff6 ull 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 18:07:18 -08:00
Nikolaj Bjorner 2882a6708e fix - arrays are treated as values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 16:35:13 -08:00
Nikolaj Bjorner c428db0bf2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 14:51:58 -08:00
Nikolaj Bjorner 559c3ca012 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 10:46:25 -10:00
Nikolaj Bjorner 98bd437e46 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 12:45:16 -08:00
Nikolaj Bjorner 3210dce63c fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 12:38:25 -08:00