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

4037 commits

Author SHA1 Message Date
Nikolaj Bjorner
7d9254f122 fix multiple bugs in interfacing with fixedpoint context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 13:46:12 -08:00
Christoph M. Wintersteiger
985145d810 Beginnings of a Java API. This is under heavy construction. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-22 20:38:05 +00:00
Christoph M. Wintersteiger
e37a347b33 Formatting 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-22 20:37:24 +00:00
Leonardo de Moura
8bea5a3625 integrated unstable changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 11:16:37 -08:00
Leonardo de Moura
bffa941616 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-22 10:06:45 -08:00
Leonardo de Moura
5e7436cb50 Removed (some) dead parameters. Added doxygen documentation for the whole code base. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 10:06:24 -08:00
Nikolaj Bjorner
fcdde59438 add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 09:48:08 -08:00
Nikolaj Bjorner
8540b379ad add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 09:47:11 -08:00
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
Nuno Lopes
5af1e4bdf4 remove redudant is_well_sorted checks after var_subst 
var_subst already checks for well sortedness of the resulting expression

Signed-off-by: Nuno Lopes <nuno.lopes@ist.utl.pt>
 2012-11-22 15:03:11 +00:00
Nuno Lopes
0ccae8e2e3 remove unused m_max_num_cex parameter 
Signed-off-by: Nuno Lopes <nuno.lopes@ist.utl.pt>
 2012-11-22 14:23:18 +00: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
Leonardo de Moura
6679fc4c0b merged changes from unstable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 12:41:52 -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
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
dcf8291860 fix for OCaml API build 2012-11-20 13:10:07 +09: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