mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 17:59:24 +00:00
Code Activity
9253 commits 44 branches 52 tags 177 MiB
Commit graph

9253 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c0e378b045 remove { 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:44:33 -07:00
Nikolaj Bjorner
e350bf8a27 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-15 15:28:26 -07:00
Nikolaj Bjorner
caca07c85f fix path to moved header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:28:18 -07:00
Nikolaj Bjorner
d7ba178d53
Merge pull request #1684 from agurfinkel/deep_space 
Remove spurious quote
 2018-06-15 15:16:52 -07:00
Nikolaj Bjorner
b6c43f6143 move files for build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:13:55 -07:00
Arie Gurfinkel
3ad1446597 Remove spurious quote 2018-06-15 15:09:25 -07:00
Nikolaj Bjorner
6e27ad42c8 remove pdr reference from legacy build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:02:50 -07:00
Nikolaj Bjorner
1debbc29c4 release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 14:59:33 -07:00
Nikolaj Bjorner
6fc08e9c9f Merge branch 'master' of https://github.com/z3prover/z3 2018-06-15 14:58:10 -07:00
Nikolaj Bjorner
a51d6cbcbc debug model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 14:58:02 -07:00
Nikolaj Bjorner
a5b5985963
Merge pull request #1679 from agurfinkel/deep_space 
warp space
 2018-06-15 14:57:23 -07:00
Arie Gurfinkel
f936c92efc Improve distinct constraint generation 
still many more optimizations possible
 2018-06-14 22:27:57 -07:00
Nikolaj Bjorner
baa96909cc mb-skolem for arithmetic with model repair 
The contract is that users of mb-skolem ensure that
interface equalities are preserved (by adding a
sufficient set of disequalities, such as a chain
x1 < x2 < x3 .., to force that solutions for
x_i does not clash).

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 17:26:04 -07:00
Nikolaj Bjorner
a0af3383db fixes to bdd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 17:25:18 -07:00
Arie Gurfinkel
05abf19009 comment 2018-06-14 16:38:27 -07:00
Arie Gurfinkel
a3de478c93 typo 2018-06-14 16:13:53 -07:00
Arie Gurfinkel
83cee9e81f Comments 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
87715620d9 Fix mk_distict in term_graph 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
2a6b7e5482 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
bc8ddedc54 fix a few build regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
e355123e37 Change declaration of projector 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
bbd917a0e6 Remove dead comment 2018-06-14 16:08:52 -07:00
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