mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
10887 commits 49 branches 53 tags 182 MiB
Commit graph

10887 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
c6e22cd2b0 hack for compiling ML API with recent changes in the Z3 API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-19 21:27:27 -08:00
Yuto Takei
0bee012f2c typo 2012-11-20 13:12:37 +09:00
Yuto Takei
dcf8291860 fix for OCaml API build 2012-11-20 13:10:07 +09:00
Leonardo de Moura
6ae3929a92 test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-19 14:05:52 -08:00
Christoph M. Wintersteiger
a20c4ad199 FPA tactic refactoring; put fpa2bv rewriter into separate file. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-19 20:51:35 +00:00
Nikolaj Bjorner
62c713129a rename pdr_tactic to horn_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 09:24:19 -08:00
Nikolaj Bjorner
b30fc79bf1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-19 05:21:15 -08:00
Nikolaj Bjorner
5bf20f9125 fix bug in qe-lite when substituting inside quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 05:20:45 -08:00
Nikolaj Bjorner
a94d3a21ee use same quotation mechanism as ast_smt2 parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 05:00:02 -08:00
Nikolaj Bjorner
57c4ce4082 bit-blast equalities before checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 04:39:18 -08:00
Nikolaj Bjorner
f98e107d0e insert fresh name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 20:11:48 -08:00
Nikolaj Bjorner
f014ab9598 use different symbols for named rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 19:00:01 -08:00
Nikolaj Bjorner
9c304d7642 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-18 18:31:59 -08:00
Nikolaj Bjorner
3ce0e900ff register also head predicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 18:31:35 -08:00
Leonardo de Moura
8d887e57a6 Updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-18 00:22:44 -08:00
Leonardo de Moura
8f2a17e20b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-18 00:14:08 -08:00
Leonardo de Moura
b169963909 fixed FreeBSD support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-18 00:09:45 -08:00
Leonardo de Moura
1a3eb3a2ed Added support for FreeBSD 2012-11-18 00:05:32 -08:00
Leonardo de Moura
c3ee9d0f74 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-17 20:29:30 -08:00
Leonardo de Moura
3711f8e42c replaced simplifier with rewriter at pull_quant.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 20:29:09 -08:00
Nikolaj Bjorner
3dbf617a46 avoid compiler warning casting int to bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 18:42:54 -08:00
Nikolaj Bjorner
f9f303e934 add pdr tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 18:18:58 -08:00
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