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

3977 commits

Author SHA1 Message Date
Lev Nachmanson
3237bd9243 better tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson
907d310600 get rid of arith.nla parameter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 14:33:40 -07:00
Lev Nachmanson
f9151a7a8e correct the default options: smt.arith.nla=False 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 13:55:23 -07:00
Nikolaj Bjorner
4b7bd3a881 fix #3536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 12:59:24 -07:00
Nikolaj Bjorner
f8dcaa8885 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 10:23:00 -07:00
Nikolaj Bjorner
12f62e73d5 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:24:34 -07:00
Nikolaj Bjorner
7a04e52c41 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:22:24 -07:00
Nikolaj Bjorner
73ab95d338 remove canonize in seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 12:47:30 -07:00
Nikolaj Bjorner
0fa04179d0 fix #3522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 11:06:04 -07:00
Nikolaj Bjorner
ee2e81b696 fix #3517 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:02:41 -07:00
Nikolaj Bjorner
c165f69248 fix #3525 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Lev Nachmanson
b34f841421 setting the old defaul options for nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
f5b62015fc change the return type of ival.var() to tv 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
119a491b17 tracking stats for max columns in theore_arith_core.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
96cc58f67c instrument the tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
ab34ef9daf fix crash exposed by #3503 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
0ec12f497c reduce use of m_core as attribute reference, instead pass as parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
ee8aa50750 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
e16c62d6e2 don't reset core after it has been populated for the cut #3451 and presumably other bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
b964976b3f remove debug code from theory_lra.cpp and restore gomory.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
cc74dd6373 emonics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
b52150de22 cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
c88d5e6468 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
e50082b484 add tv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
6c5d7fbe96 fixes in max term with tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
45980694b7 fetch explanations earlier than setting the bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
4c5c17c7d8 fixes for #3376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
eb0f318686 fix #3361 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
562be531e9 fix #3317 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
4dfc0d6d88 fix #3334 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
b41b83cd63 fix #3314 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
31e2a9b163 add scoping for variable equivalences between new monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
919f687df6 expose settings, not all of core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
8af245a410 use a simpler encoding for term indices 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
4917475f9e remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
8dcec5c4ad add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
dcb81f0ad2 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
5556b82989 introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
fc62ecb8d1 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
1b92400801 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
3b10318183 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
981aafa59c introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
5dbe4a6c8b introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
a80b48a597 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
252eb5e856 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
db94109827 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
f9f1960c73 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
d39d64176e introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
84933c4435 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
f1f974638d track variables used by nla_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00