mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
11921 commits 49 branches 53 tags 182 MiB
Commit graph

11921 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
1902360361 debugging mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
49279d7047 debugging mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
732a8149d8 vurtego update 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
a56c9faedb A sketch of vurtego 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
f0e105612c adding dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
9ba76a1332 fixing eufi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
b62d73f209 first round for combined mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
9109968e55 Cleanup fixedpoint options 
Replace pdr options with spacer
Repace fixedpoint module with fp
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
619f681d28 Fix bug in iuc_solver::get_unsat_core() that prevented clean cores 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
d38879e478 Renamed spacer options 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
81575fae7c Remove unused function 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
535b8893ae Complete euf project with eq and diseq on pure representatives 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
b246389267 Don't reset m_is_var in project 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
5e198f4119 Fix clang compilation issues 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ec8e3f2aee consolidate use of plugin by moving declarations up front (separate from constructor at this point) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
0ae246ad2b add defs to arith solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
5fce4a1d1a Wire qe_solve_plugin into qe_term_graph 
Compiles. Not tested.
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
d5081a48b0 merge while skyping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
8da84ec69e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
5dc2b7172d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
74621e0b7d first eufi example running 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
2288931b46 fix mk_unpure_equalities 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
0f799eb2ae formatting. no change to code 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
6d79b19170 fix a few bugs, debugging eufi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ba504e4243 debugging mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
e0aaf4452b wip: term_graph::project and term_graph::solve 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
144d8df5d5 Rewrite term_graph::project and term_graph::solve 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
771d3b1349 wip: term_graph::project and term_graph::solve 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
7714d05c1a fill out qe_solve_plugin functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
e226b39914 Remove pragma once from cpp 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
2e616c482b plugin work 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
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