mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
12963 commits 46 branches 52 tags 178 MiB
Commit graph

12963 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev
47d7331dd5 fix in neutral lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
5b786c428d avoid cleaning m_var_to_its_monomial 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
09f5ae7521 add a clear() method to nla_solver, fix a bug in abs values tables, add assertions, fix newtral lemma generation 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
0ff07aed3f add equivalence explanations 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
7c05d5e5d3 bug fix in order lemma, add more asserts 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
1c190c401b simplify order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
89c2ecbace add a test with equivalent variales for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
70612fb109 more tests and fixes in order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
261c664654 improve the test for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
f3f9372eac fixes after the rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
98823ef8ac move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
00acf408bf move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
64a7231079 move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
b43a0e184c introduce rooted monomial table 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4aa5fe1a46 cleanup 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
95ee5fa681 passing test solver::test_order_lemma() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
5c0f76a702 fix a bug in nla_solver's divide 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
c30190f941 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
7775afdcc3 order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
fc277f5648 order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
cebee656bd order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
99e21e0977 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
28732b1def toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
254a40535e call order_lemma_on_ac_and_bd 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4db4a8da3f toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
a5c146a740 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
82589ad325 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
f211be1e49 introduce factor 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
c5c89704a6 remove sign from factorization 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
e5e50f8c1d bug fix in basic_lemma_for_mon_zero 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
882dd06df9 small changes 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
11dae38ae6 reimplement lemmas on rooted monomials 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
d3c9cdab4a reimplement lemmas on rooted monomials 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
7e03e900b8 reimplement lemmas on rooted monomials 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
cc6dc9e7d4 switching to rooted monomials if there is no sign lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
aefd7eefb6 simplify factorization 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
667d1be8c3 start switching to rooted monomials if there is no sign lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
2d144cd774 simplify m_monomials_by_abs_vals 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
e4cbe980e9 limit the number of tactics in qfnia 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
ca0ce579b1 work on order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
6a1c2e4766 work on order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
d63c051d20 work on order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
f926ec7f4a add TRACE statements 2020-01-28 10:04:21 -08:00
Lev
0470547842 work on test for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
54f447d118 change the signature of int_solver::check by adding explanation* parameter 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
9dbb56fdfc toward order_lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
23a7e5e302 a bug fix for handling infeasibilities created in add_var_bound() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
2993453798 remove explanation.reset() and fixes in add_var_bound() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1d51c5689e roll back add_var api 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4fa38b5aa2 process conflicts immediately aftep add_var_bound() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00