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
|
c121c5d2d8
|
remove dead code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
9a71ed87d9
|
rebase with z3prover and fix term indices in monomials
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
|
2d5595eddc
|
add trace statements
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f0cebd69fc
|
get bounds from interval multiplication
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3948af630d
|
mult interval signs with deps
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
70824a68b6
|
before getting explanations for monomials upper and low bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
6a6cb3822c
|
before getting explanations for monomials upper and low bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
02133bbcc5
|
before getting explanations for monomials upper and low bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
74ecdf3191
|
guery intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f22252112e
|
remove lar_solver from nla_intervals fields
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f5c3484fe2
|
nla_intervals builds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
9ce2733105
|
unresolved in nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a4ad71bf33
|
hook up nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
453a5d2de1
|
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
|
58003f9f97
|
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
|
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 |
|