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

10886 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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