Leonardo de Moura
|
92b6a257ef
|
Added .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-20 08:37:46 -08:00 |
|
Leonardo de Moura
|
d226d2f381
|
renamed script
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-20 00:19:44 -08:00 |
|
Leonardo de Moura
|
e0f5c0bd8e
|
Added script for generating documentation for the C, .NET and Python APIs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-20 00:18:43 -08:00 |
|
Leonardo de Moura
|
09a62a18c2
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-11-19 21:31:04 -08:00 |
|
Leonardo de Moura
|
c9465848dc
|
Fixed typo found by Yuto Takei
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-19 21:30:39 -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 |
|