Nikolaj Bjorner
|
04e51ffcb5
|
fix #3569
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:40:59 -07:00 |
|
Nikolaj Bjorner
|
53b5ca3c2b
|
disambiguate call
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:35:40 -07:00 |
|
Nikolaj Bjorner
|
5152c9500d
|
fix #3591
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:08:58 -07:00 |
|
Nikolaj Bjorner
|
bf9779cb87
|
fix #3593
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 12:46:18 -07:00 |
|
Nikolaj Bjorner
|
aeee44398d
|
fix #3594
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 12:40:24 -07:00 |
|
Nikolaj Bjorner
|
ba4765f16f
|
debugging #3511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Nikolaj Bjorner
|
f74079de01
|
fix #3529
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Nikolaj Bjorner
|
c142f99127
|
fix #3532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Lev Nachmanson
|
3237bd9243
|
better tracing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-29 15:03:46 -07:00 |
|
Lev Nachmanson
|
907d310600
|
get rid of arith.nla parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 14:33:40 -07:00 |
|
Lev Nachmanson
|
f9151a7a8e
|
correct the default options: smt.arith.nla=False
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 13:55:23 -07:00 |
|
Nikolaj Bjorner
|
4b7bd3a881
|
fix #3536
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 12:59:24 -07:00 |
|
Nikolaj Bjorner
|
f8dcaa8885
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 10:23:00 -07:00 |
|
Nikolaj Bjorner
|
12f62e73d5
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:24:34 -07:00 |
|
Nikolaj Bjorner
|
7a04e52c41
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:22:24 -07:00 |
|
Nikolaj Bjorner
|
73ab95d338
|
remove canonize in seq solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 12:47:30 -07:00 |
|
Nikolaj Bjorner
|
0fa04179d0
|
fix #3522
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 11:06:04 -07:00 |
|
Nikolaj Bjorner
|
ee2e81b696
|
fix #3517
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 10:02:41 -07:00 |
|
Nikolaj Bjorner
|
c165f69248
|
fix #3525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
Lev Nachmanson
|
b34f841421
|
setting the old defaul options for nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
f5b62015fc
|
change the return type of ival.var() to tv
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
119a491b17
|
tracking stats for max columns in theore_arith_core.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
96cc58f67c
|
instrument the tableau
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
ab34ef9daf
|
fix crash exposed by #3503
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
0ec12f497c
|
reduce use of m_core as attribute reference, instead pass as parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
ee8aa50750
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
e16c62d6e2
|
don't reset core after it has been populated for the cut #3451 and presumably other bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b964976b3f
|
remove debug code from theory_lra.cpp and restore gomory.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
cc74dd6373
|
emonics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b52150de22
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
c88d5e6468
|
remove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
e50082b484
|
add tv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
6c5d7fbe96
|
fixes in max term with tableau
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
45980694b7
|
fetch explanations earlier than setting the bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
4c5c17c7d8
|
fixes for #3376
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
eb0f318686
|
fix #3361
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
562be531e9
|
fix #3317
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
4dfc0d6d88
|
fix #3334
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
b41b83cd63
|
fix #3314
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
31e2a9b163
|
add scoping for variable equivalences between new monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
919f687df6
|
expose settings, not all of core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
8af245a410
|
use a simpler encoding for term indices
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
4917475f9e
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
8dcec5c4ad
|
add option branch_flip to lp_settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
dcb81f0ad2
|
introduce a bug int theory_array.cpp - look for a counter example
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
5556b82989
|
introduce a bug into theory_array - looking for a counterexample
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
fc62ecb8d1
|
relax the literal check in theory_lra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
1b92400801
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
3b10318183
|
add option branch_flip to lp_settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
981aafa59c
|
introduce a bug int theory_array.cpp - look for a counter example
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|