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

1101 commits

Author SHA1 Message Date
Nikolaj Bjorner
a9a45b7b47 change conflict to th_axiom (#78) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3138c929ee niil_solver basic case progress 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3fb361c886 niil_solver basic case progress 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
1fce8ee0b1 niil_solver basic case progress 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
c1b976fbf4 niil_solver basic case progress 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
10871ad76e towards basic newtral check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
08d891891e handle unsorted monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
237db5cb3d niil_solver basic case zero 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
eca5ddaa04 base case zero in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
d8f5ec3b52 basic case - zero for niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
95ffc029d4 rename var_info to var_lists in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
93ec6360bd map vars to constraints 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
49ae42cebd produce the first lemma in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0911fc2bda use explanation.h for conflict explanations everywhere 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
fd0f6bcbf9 about to create a lemma in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0340c8c338 work on niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b4aaaffc99 work on niil base case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
406a021310 work on niil_solver base case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
134ebb5712 start on generate_lemma in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
31d44471a1 remove some warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9958f42d5c add files 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
92b5a9b134 work on niil 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
91086baa54 check monomial values in niil_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f6291abccb change the type of lar_solver:get_model to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
a86601f7d2 work on niil_solver::check() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
07c9e22303 refactor mon_eq out or nra_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b6f07e2a23 roll back changes in get_model 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0dbe8982ce simplify lar_solver::get_model 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
fa5d10b6dd work on switcher 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
253facff46 work on switcher 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev
a5c62bfcc4 preparing niil files 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
9c0e350bc4 rewrite3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-26 18:50:58 -08:00
Nikolaj Bjorner
3efe311c25 remove commented out code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-24 17:45:24 -06:00
Lev Nachmanson
f2015b3f49 rename m_rounded_columns to m_incorrect_columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-23 15:31:07 -08:00
Lev Nachmanson
4ba4d41346 track rounded columns in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-23 17:21:55 -06:00
Nikolaj Bjorner
ad965ac896 fix #2817 - rows may apparently not be correct (root cause of this tbd), but avoid Gomory on incorrect rows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 14:29:02 -06:00
Nikolaj Bjorner
05da2508bf fix #2873 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-22 11:08:44 -06:00
Nikolaj Bjorner
3931dd5da0 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:48:00 -06:00
Nikolaj Bjorner
045448e5b2 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:47:37 -06:00
Nikolaj Bjorner
683eed0c1e use get_sign 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 11:15:13 -06:00
Nikolaj Bjorner
d3b105f9f8 move out sign 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:38 -06:00
Nikolaj Bjorner
93d1091ad9 bcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-16 20:37:22 -08:00
Nikolaj Bjorner
0d614b8c36 check underflows, aig fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-14 19:46:56 -08:00
Nikolaj Bjorner
9f964be3f4 add don't care option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 17:00:05 -08:00
Nikolaj Bjorner
e0a41a18c3 add validation to aig_simplifier, start BIG-based masking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-11 20:47:38 -08:00
Nikolaj Bjorner
ab1f2f2e63 reduce use of symbols in gparams 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:54:26 -08:00
Nikolaj Bjorner
541658fe02 move to abstract symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:14:13 -08:00
Nikolaj Bjorner
55554215ac add include of thread, build warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 20:45:47 -08:00
Nikolaj Bjorner
670e8f8d67 reduce contention around the symbol table #2842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 16:47:06 -08:00
Nikolaj Bjorner
0278612328 build issues, add equivalence finding to probing (disabled) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 04:31:19 -08:00