mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
11930 commits 23 branches 48 tags 157 MiB
Commit graph

1165 commits

Author SHA1 Message Date
Lev
ce48605d99 some renaming in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
540ea825b0 cleanup nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
6ce6922c5a cleanup nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
ccd978e43b cleanup nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
8d02c1ee5d some renaming in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
9654480842 move vars_equivalence to a separate file 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
ca0ddb42c5 cleanup 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
2fd32ce62d rename 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1ed9639898 Nikolaj's changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
e30743c2cf commit after rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
7f85840a10 fixes in factorization and its testing 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
c672cf5c46 switch to general factorizations in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
6ce69233c7 work on nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
301f8d40fd changes in signed_factorization 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
8c59557099 fix generation of basic sign lemmas 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
17ed9c39be add a comment 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
2fb63f559c rebase with up/master 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
dd00cc89a2 simplify get_factors() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
e7441cf01e add conflict detection for a list of monomials having the same rooted monomial 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
012131df73 tesing factorization of monomials in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
83dda2f162 tesing factorization of monomials in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
771cbb31bb test nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
a1f572d55a generate lemma for proportional_case_ge 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4deccebeb4 generate lemma for proportional_case_ge 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
8350d8702f generate lemma for proportional_case_le 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
f8e4f5c5c6 lemma_for_proportional_factors_on_vars_le 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
51e08188f5 simplify getting explanations functionality 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
da700c7cff move some functionality from vars_equivalence to nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
36d587e519 fix the build 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4ba7b6b047 progress with proportional factors 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
0e557467d7 rename minimal to rooted in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
85cd566e1f add right side to struct ineq in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
de56ead538 start using the tree for var_equivalence 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
a82316a172 rebase with z3prover 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
3cf0eae5e1 work on vars_equivalence 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4c4f70f4bb work on vars_equivalence 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
d301a9c403 rebase with z3prover 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
4ca0ca3ce8 basic case proportionality 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
5344dedf42 going over the binary factor for basic lemmas 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
318b505a2e comments are added in nla_solver 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
96aaa8638e rename niil to nla 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
56ae577c97 rename the files 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
103808094a clear the model in lar_solver::get_model() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
c09c944922 rebase with upstream 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
11d37d97a1 branch of an int inf base if the row is not a gomory target 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0be5fc5693 revert to a previous state: avoid adding branches for free vars when creating a gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
822b0c1d5c in get_modele do not return values for terms 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
2b18627fa1 fix assertions (#83) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9b5996fcd5 clear lemma in int_solver before the first push_back 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
064cf9e983 allow gomory cut for a row with free non-basic vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00