Lev Nachmanson
|
8dec4bf8d0
|
better model based lemmaas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
dd235be4d2
|
add randomness when generating model based sign lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
afc9c902f8
|
bug fix in a factorization of a binom, unroll the previous commit
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
754656212d
|
allow more sign lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e6d134b9fa
|
a stronger zero lemma when the signs are known
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
6637747fd9
|
no special treatment for NE
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
34262ae02c
|
rollback but leave the change with llc::NE
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
649d47d92c
|
detect more variable equivalances
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
65b950ec4f
|
stronger mon_zero_lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
a80f6ad3a2
|
generate fixed zero lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
8018e27643
|
use m_rm_table.to_refine() when applying tangent lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1507f54fe3
|
fixes in the explanations of the tangent lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f9df9f48bd
|
more lemmas but return after if sign lemmas found
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
0dcebde060
|
replace s() to lp() it theory_lra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1abb109faf
|
move the indices housekeeping from theory_lra to lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
76e1aeb2bb
|
move the indices housekeeping from theory_lra to lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
63e62ec1bb
|
stronger lemmas to avoid branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
580ebead79
|
no derived search
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b102710b2f
|
map term indices to columns when test checking lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
c9a6d23897
|
generate explanations inside of a lemma if possible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3987cc5f1b
|
substitute the term columns in nla_solver before returning a term to theory_nra
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b2943c34f1
|
create class lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
4243bd3e2a
|
a bug fix in simple sign lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
286cebd9db
|
bug fixes in tangent_lemma explanations and the strict case of monotone lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
2bab591ef3
|
restore qfnia_tactic.cpp to expose a bug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
45ea23be21
|
add simple sign lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
34137cfa0a
|
a bug fix in internalize_atom, by NB
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
6071e08822
|
a bug fix is the sign lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
158a3db330
|
cosmetics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
228ef48628
|
more derived lemmas
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
d08f8a2512
|
fix test_basic_lemma_for_mon_zero_from_monomial_to_factors
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
d06182d199
|
split between derived and model based lemma generation
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
53b6b65a16
|
fix the test test_basic_lemma_for_mon_neutral_from_monomial_to_factors
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
389d2cee04
|
split lemma generatin on to derived and model based
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
1a788d24fd
|
a fix in the initialization
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
1ff81ba26e
|
a fix in the initialization
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
1dca8abc05
|
model based sign lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
6b96ba3ef7
|
derived lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
ff1bfdbfc6
|
derived order lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
62772468b5
|
add explanations to proportional lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
348faf15b1
|
propogation based order lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
1235621610
|
search for the sign lemma on the equivalence class of monomials
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
7c074dc65c
|
access by indeq from regular monomials to rooted
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
5599dc984c
|
introduce to_refine in rooted_table
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
403743cb30
|
switch to constraint based sign lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3441f565b2
|
before changes is basic_sign_lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
1230b46008
|
perf in equiv_monomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
5104ec881a
|
fix in tangent lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
9f51d91acf
|
tangent lemma passes first tests
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev
|
4886acfae5
|
tangent lemma
Signed-off-by: Lev <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|