mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity
9442 commits 45 branches 52 tags 177 MiB
Commit graph

7842 commits

Author SHA1 Message Date
Nikolaj Bjorner
c3fb863ad1 formatting/reviewing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
d2ae3b4025 Create children for pdr in spacer 
This is first working version of gpdr strategy. Passes one test.
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
e1a45671b3 Cleanup spacer options 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
1994f1d7e4 Cleanup of spacer options 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
fca0442487 Fix proof_checker to use is_int_expr 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
8b689ae27f Moved is_int_expr into arith_recognizers 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
cb683389f6 spacer::context: Factor params into udpt_params 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
521392a8f1 First partially working pdr strategy in spacer 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
ab5f579d0b Comments in pdr_context.cpp 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
ece2e53c98 Ported model_search and model_node from pdr into spacer 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
478d7c790e mbc: moved code under get_subst() 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
e860e4d045 Bug fix for quantified pob generation 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
2a243d38d1 Model based Cartesian decomposition 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
fee7828b51 fix solve bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
3178f7f86d Add random order of children in spacer 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
5756871738 Always attempt to eliminate all existential variables 
Sometimes variables that cannot be eliminated in one context, can be
eliminated in the other. Pass all available variables to MBP to be
eliminated if possible
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
7396ad72ab Give up when a lemma is re-discovered too many times 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
6fb6279f07 Cleanup array_eq_generalizer 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
da66ad6f80 Cleanup derivation::create_next_child 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
c5ff5ac2a1 Clen up spacer::pred_transformer::get_origin_summary 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
d7dc10212e Clean up spacer::context::create_children 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b61da6fcc0 Debug print in org-mode format 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
6b82068d8d Bug fix in spacer::derivation::exist_skolemize 2018-06-14 16:08:50 -07:00
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