mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity
474 commits 23 branches 48 tags 157 MiB
Commit graph

224 commits

Author SHA1 Message Date
Leonardo de Moura
66b02eb88d Temporary fix for the build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 07:44:03 -08:00
Leonardo de Moura
28dabd2441 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-21 18:32:48 -08:00
Leonardo de Moura
59b95a54e6 working on JNI bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 18:14:25 -08:00
Nikolaj Bjorner
ec21c7bbc5 rewrite quantifier module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-21 16:54:41 -08:00
Leonardo de Moura
2a9014ff57 Added directory for future Java bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 12:51:07 -08:00
Christoph M. Wintersteiger
a103f0e288 Made macro-finder and quasi-macros tactics public. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-21 14:39:39 +00:00
Nikolaj Bjorner
ec8b7948bf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 21:52:00 -08:00
Nikolaj Bjorner
21eca20b9e fix slice bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 21:51:41 -08:00
Nikolaj Bjorner
a935c64e15 expose assertions that are pushed to the context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 21:00:02 -08:00
Nikolaj Bjorner
a38a7ab506 delay rule flushing so that pretty printing retains original format of rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 15:30:22 -08:00
Nikolaj Bjorner
2c54bbba5f more general predicate recognizer for quantified Horn clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 11:16:54 -08:00
Nikolaj Bjorner
6a18015622 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 10:43:05 -08:00
Nikolaj Bjorner
01ddb20441 recognize array and bv theories in HORN format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 10:42:59 -08:00
Leonardo de Moura
557cda70b0 Set :global-decls to false 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:45:31 -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
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
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
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
ead762e0d0 bumped version number 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-14 09:02:53 -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
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
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
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