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

9134 commits

This branch
This branch
All branches
Author SHA1 Message Date
Arie Gurfinkel
4ca734528e Formatting 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
dd064bd8f9 Bug fix to spacer::sym_mux 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
38c2b56f0e Rewrite spacer::sym_mux 
Simpler implementation that only provides functionality actually used
by spacer
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
268274911a Fix to cube-and-clause interface in prop_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
e0e435582a Minor code cleanup 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
6464468cd8 Remove dead code 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
aa77a918cd Optimizing qe_lite 2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
bfeb15b876 move to list of clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
502e323678 Fixes to pred_tranformer::updt_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
862eef5ec0 Eliminate all existential variables from reach facts 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
70f4674b3a Code to update solver with all constraints of a pred_transformer 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
cfcc084688 reach_fact --> rf 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
7a8563a34c spacer: cleaner management of rf tags 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
ada548b5ae Removed unused options 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
0b387cd7eb Moved pool_solvers from spacer::manager into spacer::context 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
451d42319b Rename m_reach_ctx into m_reach_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
1e54237880 mbp_array: Fix set_model_completion bug 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
cdba0721e7 Extra stats in iuc_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
16fefe850a Factored mbp into pred_transformer and added stats 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fde58664f6 Moved mk_reach_fact to pred_transformer 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
2a2b21326b Stats on num_proxies in iuc_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
e2e1411707 Option to dump SMT queries as benchmarks during Spacer run 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
bebfac047e Dump benchmarks in pool_solver 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b50da20531 array_mbp: turn on model completion 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
0452bc3d43 qe_lite: simplify definitions before deciding on elimination order 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b120923dd5 qe_lite: bug fix in der::der_sort_vars() 
The case of

VAR 1 = (+ (:var 2) 10)
VAR 2 = (+ 0 foo)

was not properly handled whenever VAR2 has only one reference.
In that case, VAR2 is not marked as done when VAR1 is processed,
causing VAR2 to be duplicated in elimination order
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fb52c36210 spacer: switch to new IUC as default 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
3a97451f8c spacer: normalize the cube before creating a lemma 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fce68536d3 spacer: print all lemmas in json 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
bfa472faec New style of json dump based on lemmas at pob 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
5072a2a869 spacer: pobs keep track of their lemmas 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
61cd74818f Pin lemmas so that they don't disappear 2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
ebfb2a4a1e Fix mbp to respect reduce_all_selects option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
0c2e3c0894 fixes to clause proof tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
f7d015de8d Switch spacer_prop_solver to check_sat_cc 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
1343b272e7 Implement iuc_solver::check_sat_cc 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
26339119e4 solver::check_sat_cc : check_sat assuming cube and clause 
Extends check_sat with an ability to assume a single clause in
addition to assuming a cube of assumptions
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
4477f7d326 Fix memory leak in asserted_formulas 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
723e96175b spacer: prepare to use incremental clause smt_solver interface 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
c3edf8c8fa Restore assertion in smt_clause 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
ef58753ae7 Silence clang warning 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
56a29093d0 Cleanup transition creation in pred_transformer 2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
005a6d93bb cube and clause 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
ea032b56c0 Return false when clause cannot be decided 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
275b99e408 Add missing override 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
4db4547359 silence clang warning 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
b73aa3642a check with cube and clause 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
af57db0413 Anti-unification of two ground expressions 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
aa8dac2583 fix uninitialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
e6401908a5 fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00