Nikolaj Bjorner
|
9a642215eb
|
avoid infinite loop between is-nullable and mk-bool-app
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-28 10:27:47 -07:00 |
|
Nikolaj Bjorner
|
7f3bdea0d5
|
unused methods
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-23 19:28:07 -07:00 |
|
Nikolaj Bjorner
|
5d36578684
|
some unused variables reported by Caleb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-22 19:04:10 -07:00 |
|
Lev Nachmanson
|
6ced6995d0
|
check for m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()) in equality propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-22 11:48:46 -07:00 |
|
Nikolaj Bjorner
|
4b6ca6a10c
|
replace size by data_size
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-22 11:16:36 -07:00 |
|
Lev Nachmanson
|
6524a70c32
|
remove un unnecessary call
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
8f588a9263
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
b703d2786c
|
fix the build cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
3bde9f54d8
|
add some comments cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
115ae8fe14
|
check for integrality when adding an equality
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
c4fbe05a96
|
simplify cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
e3503f060f
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
42ed1e62a9
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
2e2e98925a
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
ffaa7d0b27
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
525f747e3c
|
cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
c2cead4fb6
|
cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
b5fc9635c4
|
cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
3b00b34c6f
|
cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
80467f1400
|
cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
431bb36cf5
|
cheap_eqs tree
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
f7f9c15676
|
cheap_eqs tree
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-20 11:31:22 -07:00 |
|
Lev Nachmanson
|
f882219081
|
fix a bug in cheap_eqs with table
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-15 13:30:45 -07:00 |
|
Lev Nachmanson
|
d13e584706
|
simplify the fixed var table
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-15 13:30:45 -07:00 |
|
Nikolaj Bjorner
|
180fb3abf6
|
tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-14 11:36:09 -07:00 |
|
Nikolaj Bjorner
|
7387fc9dec
|
avoid some bignum overhead in addmul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-14 11:20:05 -07:00 |
|
Nikolaj Bjorner
|
5ee9edf46b
|
fix incorrect bound in order-lemma
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-13 14:28:42 -07:00 |
|
Lev Nachmanson
|
e5632736d2
|
review comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
fbfcc6796a
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
66701de157
|
fix the test build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
06826adec3
|
fix the race in add_var_bound and add_def_constraint
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
fe0e042e40
|
move m_fixed_var_table to lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
67eaff4490
|
testing cheap equalities
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
94263167ec
|
cheap eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
50b9915c57
|
avoid big nums in is_offset_row in cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
713eb6319d
|
fix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
1587497562
|
cheap equalities
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
ccc8651800
|
cheap eqs on table
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
b3bdce7837
|
make lp_bound_propagator a field of theory_lra::imp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
dd30b5e3af
|
some simplifications in cheap eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
4de38d09e2
|
cheap eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
4f0bd93124
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
110ab5e6ef
|
debug cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
9c078c6d59
|
relaxing asserts in column_to_reported_index
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
6a678fd5be
|
rename in lar_solver and memory corruption bug in cheap_eq
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
4936ace7cd
|
more guards on cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
0ff18dd5a7
|
a small example passing with cheap eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
54921d08dc
|
cheap_eq debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
4a9f031502
|
cheap_eqs progress
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|
Lev Nachmanson
|
62bd19242e
|
replace graph by a tree in cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-06-12 22:11:11 -07:00 |
|