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

12251 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
7e67e1ce99 fix loop in equiv_monomials (#91) 
* fix loop in equiv_monomials

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
e6561c983f debug emons 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
884a2628de debug emons 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
e28e83a25e port to emonomials (#90) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b52e79b648 emons branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
14f00b3749 remove a test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
be5170fc3b hook up more lp_params 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c96c37e878 fix an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c557743be4 fix in rounding rows 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
7f12dfbbe8 fix in rounding rows 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
2d12874f30 fix errors in cube rounding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
43758cbc66 more efficiend handling of rounded in cube heuristic rows 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b47e0cd4fb fix tableau's Ax=b after cube heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
48fcd66bb9 refactor tests from nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c9e989ae85 fix build of lp_tst 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
facf0b80c0 refactor monotone lemmas out of core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
8331207b81 clean up nla_core.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
25198c91b3 clean up nla_core.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
2e9b4f643a fix a reference to random 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1a0d68e1b7 remove shadow m_core fields 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9e82e6965c refactoring nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
7fa4371d96 remove a method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c1ee4600d1 call core::random() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c7c2d81f53 Refactor basic lemmas out of nla_core 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3e11b87aaf avoid unnecessary inequalities 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f2ec3b362a refactor nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c9f2f6f110 Forgotten file 2020-01-28 10:04:21 -08:00
Lev Nachmanson
2513deb817 Add forgotten file 2020-01-28 10:04:21 -08:00
Lev Nachmanson
7f05907f91 refactor nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
bddda1674d Disable collect_equivs_of_fixed_vars() that led to long explanations 2020-01-28 10:04:21 -08:00
Lev Nachmanson
5c949d74d8 add an assert in add_abs_bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c7dec3ef4d a fix in add_abs_bound() and integrating NB changes 2020-01-28 10:04:21 -08:00
Lev Nachmanson
a323eaf1c8 add some nla statistics generate not more than one pl lemma an a rm monomial 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
4ba3ccfc99 fix in generate_ol() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9ad0197e14 create shortcuts var_abs_val_le(), var_abs_val_ge() and remove some lemma redundancy 2020-01-28 10:04:21 -08:00
Lev Nachmanson
32d1217499 Create explanations for octogonal constraints by the var equivalence 2020-01-28 10:04:21 -08:00
Lev Nachmanson
ab1b2ae86d remove dead code and a fix in no_lemmas_hold 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
826d2582e2 var_eqs seems working 2020-01-28 10:04:21 -08:00
Lev Nachmanson
98dca454ae debug var_eqs 2020-01-28 10:04:21 -08:00
Lev Nachmanson
7a3a696b6f debugging var_eqs 2020-01-28 10:04:21 -08:00
Lev Nachmanson
09152013b3 var_eqs compiles but broken 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f828dc9451 treat monomial factorization in a special way in generate_pl() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
e32c1bdee8 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3f9229a698 stop keying monomials by abs values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
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