mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
12707 commits 49 branches 53 tags 182 MiB
Commit graph

12707 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
086e25b7fa lemmas with less equivalence explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
90bda39aef towards full factorizations on a monomial 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1810d7e77d cleanup mostly, more asserts in tangent lemma 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9c62b431e4 address the NB's comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
d028dd65e4 disable the args dump 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9302d8bef3 Guard the creation of solvers in qfnia_tactic.cpp by a define 2020-01-28 10:04:21 -08:00
Lev Nachmanson
53e329b324 enable more order lemmas 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f784120312 rebase with Z3Prover/master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
cbe920756b simpler order lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1959710a5b prepare to simplify order lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
4963108277 better tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0dbfcad560 try simple monotoniciy lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
d1a5635b4a better model based lemmaas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
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