Nikolaj Bjorner
|
4f33c123c9
|
add placeholder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 20:31:05 -08:00 |
|
Nikolaj Bjorner
|
d02d90dab2
|
add assert to catch bad lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 20:00:48 -08:00 |
|
Nikolaj Bjorner
|
ba2f587c26
|
rm eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 18:39:32 -08:00 |
|
Nikolaj Bjorner
|
c46e36ce58
|
bug fixes to LUT extraction, bug fix for real value case of freedom intervals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 14:25:25 -08:00 |
|
Nikolaj Bjorner
|
806ee85759
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 14:25:25 -08:00 |
|
Murphy Berzish
|
8d3ed19981
|
z3str3: loop and trace cleanup
|
2020-02-11 12:37:42 -08:00 |
|
Nikolaj Bjorner
|
b1e6031230
|
partial parity fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 03:35:25 -08:00 |
|
Lev Nachmanson
|
ba4cc27817
|
squash blanks more in tableau pp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-02-10 17:08:28 -08:00 |
|
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 |
|