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

1065 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
39e6453f4a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-17 18:03:46 -08:00
Leonardo de Moura
3e50a65dfc isolating elim_term_ite inside smt module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 17:12:30 -08:00
Nikolaj Bjorner
8592f5cef4 make verbose model only use simplified rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 15:27:51 -08:00
Nikolaj Bjorner
29a45e34a2 fixing bugs in model evaluator. remove wrong assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 22:09:15 +01:00
Nikolaj Bjorner
50385e7e29 add option to validate result of PDR. Add PDR tactic. Add fixedpoint parsing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 20:47:49 +01:00
Leonardo de Moura
ed5d154f78 broke dependency between components that need initialization and memory_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 11:30:25 -08:00
Leonardo de Moura
570147e326 removed dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 10:33:09 -08:00
Leonardo de Moura
93bfcaa404 Making ast_smt2_pp the default pretty printer. Now, mk_pp is just an alias for mk_ismt2_pp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 10:20:08 -08:00
Leonardo de Moura
1645f61d85 added READMEs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 09:32:01 -08:00
Leonardo de Moura
3f52f30f9c updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 11:15:12 -08:00
Leonardo de Moura
1ec0d02ead added get_version to z3py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 11:14:09 -08:00
Leonardo de Moura
b472a36b42 added --staticlib option to mk_make.py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 09:03:13 -08:00
Leonardo de Moura
ead762e0d0 bumped version number 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 09:02:53 -08:00
Leonardo de Moura
79eca95a95 bumped version number 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 22:46:57 -08:00
Leonardo de Moura
89c1785b73 fixed clang++ for linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 21:49:37 -08:00
Leonardo de Moura
ad3aa96726 improving clang++ support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 21:26:28 -08:00
Leonardo de Moura
3e8d3db290 fixed gcc compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:26:01 -08:00
Leonardo de Moura
b335661d5a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-13 09:17:35 -08:00
Leonardo de Moura
50e00b615f updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:16:51 -08:00
Leonardo de Moura
f9ec1f2a63 making sure par-or and par-then combinators work correctly even when OpenMP is not available 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:14:36 -08:00
Leonardo de Moura
8ad12a7dd4 Missing config option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:14:02 -08:00
Nikolaj Bjorner
68ae5d434c fix cover retrieval for slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-13 17:00:01 +01:00
Leonardo de Moura
854641c8db updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 22:09:51 -08:00
Leonardo de Moura
00dbe92cea polishing clang++ support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 22:05:17 -08:00
Leonardo de Moura
504ba8236d added support for clang++ on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 21:42:36 -08:00
Leonardo de Moura
ed6e688b94 updated RELEASE_NOTES. fixed mk_make.py 2012-11-11 21:06:17 -08:00
Leonardo de Moura
e0fcbc101c Added support for clang++ on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-12 04:56:48 +00:00
Leonardo de Moura
99b7f7509d bump version number in unstable branch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-11 10:50:24 -08:00
Leonardo de Moura
a6db55d21f Display version number using new format 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-10 19:03:16 -08:00
Leonardo de Moura
caced62f40 New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-10 15:54:31 -08:00
Nikolaj Bjorner
108bbb0597 add missing check for difference logic fragment for clause heads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-10 11:50:17 +01:00
Leonardo de Moura
a5ceff98ea cleaned exampled 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:11:22 -08:00
Leonardo de Moura
1cf8d61def new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:00:27 -08:00
Leonardo de Moura
73a13f209b fixed bug detected in regression tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 10:46:00 -08:00
Leonardo de Moura
c5b91aef68 Fixed bug reported by Heizmann at codeplex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 07:52:07 -08:00
Leonardo de Moura
8d6a091083 fixed bugs found in regression tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 07:36:40 -08:00
Leonardo de Moura
c3a0a29c4f fixed problem with Python 2.5 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 05:55:41 -08:00
Nikolaj Bjorner
cec851440e fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-06 15:38:07 +02:00
Leonardo de Moura
2c66afadd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 12:49:58 -08:00
Leonardo de Moura
10b95de82e resurrected test/quant_elim.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-04 12:49:33 -08:00
Nikolaj Bjorner
5ef505c357 set model completion to force value computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:22:56 +02:00
Nikolaj Bjorner
37a13b1d09 update slicing to fix unbound variables. test datatype realizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:15:24 +02:00
Nikolaj Bjorner
bfbdad3ce6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 08:40:23 +02:00
Nikolaj Bjorner
927dc2e490 fix if-lifting, added light-weight FM to qe_lite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 08:40:16 +02:00
Leonardo de Moura
6580a83594 minor fix for ramdisk build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 21:16:52 -07:00
Leonardo de Moura
c1587dc37d fixed some warnings reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 17:28:27 -07:00
Leonardo de Moura
ed52dce9b0 Merge branch 'solver_na2as' into unstable 2012-11-02 16:35:23 -07:00
Leonardo de Moura
b70687acc9 cleanning solver initialization, and fixing named assertion support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 16:35:08 -07:00
Leonardo de Moura
181bdb6815 removed dead files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 14:18:12 -07:00
Leonardo de Moura
e2f6a65aa2 added support for named assertions 2012-11-02 14:00:43 -07:00