mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
12710 commits 49 branches 53 tags 182 MiB
Commit graph

12710 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
1371526062 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 16:15:21 -08:00
Lev Nachmanson
ad55f61580 roll back the defaults of invoking the nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-10 13:35:33 -08:00
Nikolaj Bjorner
f1abc71c35 fix #2962 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 11:44:10 -08:00
Lev Nachmanson
26eb23c05b move lp_params to smt_params_helper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-10 11:25:54 -08:00
Lev Nachmanson
514c3d7a3b move the content of nla_params.pyg to smt_params_helper.pyg 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-10 11:08:35 -08:00
Lev Nachmanson
e2514a2b19 make nla_solver the default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-10 10:22:05 -08:00
Nikolaj Bjorner
d770b5135d fix build warnings for theory_str_mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 09:02:14 -08:00
Nikolaj Bjorner
c36a980eb7 fix #2967 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 08:46:09 -08:00
Nikolaj Bjorner
a579ce1ea2 fix #2966 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 08:33:14 -08:00
Nikolaj Bjorner
83d1156a59 fix #2966 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 08:31:44 -08:00
Nuno Lopes
feba007696 fix #2965, fix #2968: bugs in domsimplify on cache usage and boolean trial propagation 2020-02-10 10:56:36 +00:00
Murphy Berzish
524434cfbb z3str3: pass correct subterm to negative regex model construction 2020-02-09 20:40:43 -08:00
Lev Nachmanson
fd3c3a2599 make the column shift in random_update divisible by m 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-09 16:30:09 -08:00
Nikolaj Bjorner
bc75e08a52 fix #2943 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 15:48:53 -08:00
Nikolaj Bjorner
82273da630 fix #2945 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 15:43:21 -08:00
Nikolaj Bjorner
1eb4459325 fix #2959 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 12:38:05 -08:00
Nikolaj Bjorner
1ef83351cb fix #2963 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 12:32:11 -08:00
Nikolaj Bjorner
053631e005 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 09:24:21 -08:00
Nikolaj Bjorner
c8b98d8b48 move hnf cut functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 09:22:02 -08:00
Nikolaj Bjorner
9451dd9a74 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 09:00:34 -08:00
Nikolaj Bjorner
5964969f29 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 08:38:07 -08:00
Nikolaj Bjorner
2512a958b9 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 08:25:52 -08:00
Nikolaj Bjorner
5dc8c93897 separate out gcd test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 16:44:25 -08:00
Nikolaj Bjorner
e964973f19 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 16:01:12 -08:00
Nikolaj Bjorner
7ec02fc11f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 16:00:13 -08:00
Nikolaj Bjorner
8b9a80e232 separate out int-branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 15:58:06 -08:00
Nikolaj Bjorner
3f1f4e0f67 remove pragma once from cpp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 15:41:13 -08:00
Nikolaj Bjorner
8d293171d5 separate int-cube functionalty 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 15:27:11 -08:00
Nikolaj Bjorner
c12c9a75e6 move all gomory functionality into gomory class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 15:03:58 -08:00
Nikolaj Bjorner
d44855f262 move all gomory functionality into gomory class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 13:02:19 -08:00
Nikolaj Bjorner
094f203167 fix #2949 fix #2955 experiment with cut selection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 10:41:35 -08:00
Nikolaj Bjorner
f29b455611 fix #2949 fix #2955 experiment with cut selection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 10:34:14 -08:00
Nikolaj Bjorner
140926e7c0 move assume eqs until __after__ other checks, big perf regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 20:23:27 -08:00
Nikolaj Bjorner
1c9b2637ba remove unused method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 20:01:36 -08:00
Nikolaj Bjorner
d22ad5e819 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 19:43:58 -08:00
Nikolaj Bjorner
d5dfe07203 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 19:42:44 -08:00
Nikolaj Bjorner
b2c265496e dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 19:41:50 -08:00
Nikolaj Bjorner
02b074e28b compile constraints during internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 19:28:17 -08:00
Lev Nachmanson
824c2674b9 roll back the branching experiment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 17:37:38 -08:00
Lev Nachmanson
5ee7103e3c roll back the branching experiment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 17:35:42 -08:00
Lev Nachmanson
bbfcd00627 experiment with branching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 15:40:33 -08:00
Lev Nachmanson
6027224e34 do not throttle lp bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 14:21:11 -08:00
Lev Nachmanson
6b01376f51 fix column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 13:42:39 -08:00
Lev Nachmanson
f45e17c47e fix column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-07 13:42:39 -08:00
Nikolaj Bjorner
8c016abb12 build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 11:16:57 -08:00
Nikolaj Bjorner
88374a15d0 build errors/warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 10:09:10 -08:00
Nikolaj Bjorner
bd444f8ec7 isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:25:06 -08:00
Nikolaj Bjorner
800bc757ae isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:24:45 -08:00
Nikolaj Bjorner
024ca86386 isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:16:14 -08:00
Nikolaj Bjorner
a59745c2f2 isolate constraints in a constraint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 09:13:40 -08:00