Lev Nachmanson
|
bf885bf9b3
|
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
|
28c057fd7b
|
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
|
2ad94026a0
|
do not produce proportional lemma for non-integral vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
0ee541204f
|
fix in gomory: revert some changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
b8d7af59f4
|
fix in gomory cut
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
6396857ee2
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
87f80ce022
|
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
|
8e55a77ee7
|
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
|
406bd98a39
|
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
|
3e4720abbd
|
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
|
0229ab2811
|
remove debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
66dd93a035
|
fix a bug in nla_intervals - add explanations when getting intervals from a term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
ab92c20106
|
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
|
b9bfa950f6
|
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
|
37c72b71f5
|
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
|
c0b49e95c4
|
use lar_solver directly to compare variable values in assume_eqs()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
6549984dd4
|
call init_variable_values() from assume_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
c469ea2717
|
do not call get_model() from assume_eqs()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
0db112ef8f
|
Update nla_core.cpp
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
697fd37d26
|
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
|
762f265616
|
merge with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
cf86e6ef73
|
disable dubious eq adapter code causing perf hit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 16:41:01 -07:00 |
|
Nikolaj Bjorner
|
73d73e6c95
|
enhance rewriting for indexof based on #3516
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 13:29:36 -07:00 |
|
Nikolaj Bjorner
|
f92050c7e5
|
fix #3515
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 13:21:02 -07:00 |
|
Nikolaj Bjorner
|
145ec8f248
|
pick up log configuration consistently #3513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 10:51:55 -07:00 |
|
Nikolaj Bjorner
|
e5e6f481f9
|
update bounds and assert values during initialization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 04:05:58 -07:00 |
|
Nikolaj Bjorner
|
477fd3fba0
|
remove model initialization all-together because assumption literals are not connected with model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 04:00:21 -07:00 |
|
Nikolaj Bjorner
|
a7495876fd
|
fix #3506 fix #3505
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 03:06:02 -07:00 |
|
Nikolaj Bjorner
|
504a7550b3
|
fix #3509
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 02:42:30 -07:00 |
|
Nikolaj Bjorner
|
ea396a008a
|
fix #3504
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 02:30:51 -07:00 |
|
Nikolaj Bjorner
|
0609408fd7
|
fix #3510
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 01:50:30 -07:00 |
|
Nikolaj Bjorner
|
b8c25ac20b
|
fix #2909
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 01:43:20 -07:00 |
|
Nikolaj Bjorner
|
41c68d64d4
|
avoid deref on null
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 17:06:06 -07:00 |
|
Nikolaj Bjorner
|
69783db5e8
|
print roots as part of test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 15:28:51 -07:00 |
|
Nikolaj Bjorner
|
af51d98a32
|
avoid unintialized value build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 15:02:31 -07:00 |
|
Nikolaj Bjorner
|
a557913307
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 12:45:16 -07:00 |
|
Nikolaj Bjorner
|
a4f668eef0
|
add unit test for #2867
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 11:52:41 -07:00 |
|
Nikolaj Bjorner
|
33b644adad
|
fix #3500
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-24 10:25:42 -07:00 |
|
Nikolaj Bjorner
|
601b3998f3
|
fix #3430
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 18:59:07 -07:00 |
|
Nikolaj Bjorner
|
2494709e98
|
fix #3421
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 17:33:23 -07:00 |
|
Nikolaj Bjorner
|
0cf401c67b
|
fix #3458
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 17:27:10 -07:00 |
|
Nikolaj Bjorner
|
28bdda326b
|
fix #3499
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 13:37:08 -07:00 |
|
rashchedrin
|
b34f72dd00
|
Fix #3439, print type of value in exception msg (#3498)
|
2020-03-23 12:36:36 -07:00 |
|
Nikolaj Bjorner
|
519c0d5f11
|
fix #3434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 11:51:21 -07:00 |
|
Nikolaj Bjorner
|
acb9376ea0
|
fix #3488
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 10:57:15 -07:00 |
|
Nikolaj Bjorner
|
bb451c39c9
|
fix #3495
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 10:32:19 -07:00 |
|
Nikolaj Bjorner
|
84090aaf24
|
fix #3423
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-23 10:27:42 -07:00 |
|
Nikolaj Bjorner
|
f158ab8395
|
fix #3426
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 20:48:31 -07:00 |
|
Nikolaj Bjorner
|
19c72ab519
|
fix #3474
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 20:40:34 -07:00 |
|
Nikolaj Bjorner
|
2c078b01da
|
fix #3422
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 16:56:26 -07:00 |
|