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

662 commits

This branch
This branch
All branches
Author SHA1 Message Date
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 93dfafb6d4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 15:30:44 -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
Leonardo de Moura e22805c139 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 23:28:05 +00:00
Leonardo de Moura ee0f0d231b Fixed missing space for OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 23:27:41 +00:00
Leonardo de Moura 8f4518d28b updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 15:24:38 -08:00
Leonardo de Moura d21cd210ed Fixed new mk_make for OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 23:21:39 +00:00
Leonardo de Moura 2adbc61f1b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 15:13:54 -08:00
Leonardo de Moura bd021815b1 eliminated autoconf dependency 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 15:13:37 -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 4d3a653309 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 09:38:47 -08:00
Leonardo de Moura f9c9d5e342 updated website 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 09:38:28 -08:00
Leonardo de Moura b3e048782c Updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:48:19 -08:00
Leonardo de Moura c097b5620d fixed release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:46:48 -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 6c11a78e61 fixed .gitignore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:41:45 -08:00
Leonardo de Moura 051e84de20 Updated .gitignore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:40:05 -08:00
Leonardo de Moura c769c683a7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 08:38:07 -08:00
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 b3b13541fb improved doc/README 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 00:31:55 -08:00
Leonardo de Moura 14944356f8 improving script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 00:27:20 -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