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

9200 commits

This branch
This branch
All branches
Author SHA1 Message Date
Arie Gurfinkel
5566b5689c Silence clang warning 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
5ab6d6ca16 term_le -> term_lt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
f963fc06f4 sketch out euf-solver based on complete projection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
44a32bc076 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
6e61a7c1b2 minor 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
73486be590 fix typo in mk_pure 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
9c7d9818d3 get_app --> get_expr + fix term_lt() 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
dda65fdd2e mk_not: fix clang compilation issue 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
9a0406d181 replace app by expr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
0d71d85069 redo representative algorithm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ad153592a2 fix parent list 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
a6848c79b7 redo representative generator to respect stratification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
c4188fc4be initial working version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
1f634efe04 initial working version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
008f003aa0 initial working version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
da18f0e0b7 prepare term-graph unit testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
362d9258a4 prepare term-graph for cc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
d26609ebdd prepare term-graph for cc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
14696f03f7 add some review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
2e44850df9 move term graph closer to qe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
0784074b67 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
688cf79619 working on mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
e6468726f5 more code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
5fc0f56281 sketch mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
4a2eb909bf Re-fixing a bug in compute_implicant_literals() 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
8445e2a7a2 Fix bug in weak abs 
Must ensure that weak model makes all summaries true. Otherwise,
it is possible to get stuck discovering the same lemma forever.
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
df7ab0e496 pred_transformer: factor rule bookkeeping to a separate class 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
4099f31f4f Fix refutation generation 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
18e3c7b13d Fix bug introduced by formatting 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
f3466bb3e4 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
1920450f98 throttle ite-blasting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
1f0fd38c99 ground sat refutation from spacer (wip) 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
0534b72c4d sort hypotheses 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
c5fb1c1223 Use vector instead of a hashtable to represent a set 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
e84ca25f05 Check whether one proof node is an ancestor of another on-demand 
Instead of pre-computing sets
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
a40e0dce0c proof_utils: use expr_mark instead of hashtable 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
2a6b694373 Imrove hypothesis_reducer 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
4b2196f114 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
6adaed718f remove pdr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
cefdb8c01d Use reachable cache 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
9fef466c63 Respect children order in spacer/pdr 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
f74ca2f0c0 Fix caching bug in mbc 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
54add824e9 Debug print 2018-06-14 16:08:51 -07:00
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