Lev Nachmanson
f7f9c15676
cheap_eqs tree
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-06-20 11:31:22 -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
ccc8651800
cheap eqs on table
...
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
110ab5e6ef
debug cheap_eqs
...
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
Lev Nachmanson
1e4e887221
propagate cheap eqs
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-06-12 22:11:11 -07:00
Lev Nachmanson
742be83503
Lpbounds ( #4492 )
...
* remove inheritance from bound propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* less inheritance
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* less inheritance
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-06-02 01:00:06 -07:00
Nikolaj Bjorner
d372af4782
add stub for cheap equality propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-05-30 15:36:27 -07:00
Lev Nachmanson
7caae3f5d2
small improvements in tableau in rows and bound propagation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-13 16:04:25 -07:00
Nikolaj Bjorner
03e411c22d
fix #3868
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 02:28:38 -07:00
Lev Nachmanson
19120bee81
fix the debug build
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
80245f05ad
rebase with Z3Prover and Nikolaj's changes in lp bound propagation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
3f6ecfb3b6
generate lemmas from nla_intervals
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
46b9273a79
fixes in interval explanations
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
9c18ede687
hook up nla_solver it lp bound propagation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
33cbd29ed0
mv util/lp to math/lp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
