mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity
18901 commits 23 branches 48 tags 156 MiB
Commit graph

18901 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura 6d25a3bd2b Added Visual Solution Generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 15:33:49 -07:00
Leonardo de Moura ae400c4b2a checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 14:39:59 -07:00
Leonardo de Moura cf47f6ce60 renamed user_ext => user_plugin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 14:19:00 -07:00
Leonardo de Moura dcf778a287 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 14:16:35 -07:00
Leonardo de Moura 3003ee5cb6 Integrating Nikolaj's Saturday changes (at unstable branch) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 13:40:22 -07:00
Leonardo de Moura add684d8e9 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 13:32:12 -07:00
Leonardo de Moura 4722fdfca5 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 08:12:38 -07:00
Leonardo de Moura 6bc591c67e Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 22:44:27 -07:00
Leonardo de Moura aa949693d4 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 22:28:22 -07:00
Leonardo de Moura 492484c5aa Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 22:03:58 -07:00
Leonardo de Moura 2b8fb6c718 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 20:53:33 -07:00
Leonardo de Moura 6bdb009c3e Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 20:42:28 -07:00
Leonardo de Moura d8cd3fc3ab Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 19:54:08 -07:00
Leonardo de Moura 8b70f0b833 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 19:30:14 -07:00
Nikolaj Bjorner 452ea65189 move to z3.dll instead of z3_dbg.dll 2012-10-20 19:26:31 -07:00
Nikolaj Bjorner 61de6433c0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-20 19:11:50 -07:00
Nikolaj Bjorner 1cae83183a add missing /** so that OCaml can build 2012-10-20 19:10:25 -07:00
Leonardo de Moura ded42feeb6 Reorganizing code base 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 16:33:01 -07:00
Leonardo de Moura 9a84cba6c9 Reorganizing the code. Moved nlsat to its own directory. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 15:48:18 -07:00
Leonardo de Moura c66b9ab615 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 15:30:42 -07:00
Leonardo de Moura 8a6997960a Reorganizing code. Added script for generating VS project files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 15:16:37 -07:00
Nikolaj Bjorner 090ca2e46c refined difference logic check, consolidate scoped modes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-20 10:47:30 -07:00
Leonardo de Moura 2c464d413d Reorganizing source code. Created util dir 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 10:19:38 -07:00
Nikolaj Bjorner 14aff67684 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-20 06:36:30 -07:00
Nikolaj Bjorner 630ba0c675 use a more liberal static feature for difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-20 06:33:14 -07:00
Nikolaj Bjorner c2f9f2e9cd Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-20 04:27:42 -07:00
Nikolaj Bjorner 4e94fa7d37 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-20 04:26:46 -07:00
Nikolaj Bjorner 2e73957f97 enable proof production with difference logic, integrate with PDR engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-20 04:25:58 -07:00
Leonardo de Moura 472b8caa41 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-19 18:39:01 -07:00
Leonardo de Moura b505fe13cd updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-19 18:38:34 -07:00
Nikolaj Bjorner 36f7bad1da Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-19 08:33:57 -07:00
Nikolaj Bjorner ccb50f5d8a updated comments to create_children 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-19 08:33:43 -07:00
Nikolaj Bjorner 28a4f51ea5 qe-lite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-19 08:30:23 -07:00
Nikolaj Bjorner cadfb804c5 remove dead code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-19 08:22:31 -07:00
Nikolaj Bjorner b22fb74c5c working on symbolic execution for PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-18 21:09:32 -07:00
Nikolaj Bjorner 8f5fc3716e working on symbolic execution for PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-18 21:01:28 -07:00
Leonardo de Moura 8cde0c0672 fixed update_api.py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-18 12:55:28 -07:00
Leonardo de Moura 5fa96ccb0b Renamed z3_dbg.dll to z3.dll 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-18 12:52:33 -07:00
Leonardo de Moura fae9a1b760 Fixed bug in DLL .def generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-18 04:51:41 -07:00
Leonardo de Moura 2a4e6d03f3 Extending public API with internal objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-18 04:47:46 -07:00
Leonardo de Moura 9cb29777e2 fixed update_api.py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-17 23:13:43 -07:00
Leonardo de Moura 15fb18c65d Simplified binding and logging support generation. Now, everything is generated by update_api.py script. The binding commands can be included in the .h files (e.g., z3_api.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-17 23:00:21 -07:00
Nikolaj Bjorner 8459401b6e working on expansion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-17 08:34:42 -07:00
Nikolaj Bjorner 3a837037d4 working on symbolic execution trace unfolding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-16 16:54:03 -07:00
Nikolaj Bjorner 6b414ba5cf Add coalesce transformer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-16 08:21:32 -07:00
Nikolaj Bjorner d16db63e56 add rule unfolding transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-15 15:34:29 -07:00
Nikolaj Bjorner 2c24f25050 finish (inefficient) BMC for non-linear Horn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-15 10:49:19 -07:00
Nikolaj Bjorner b6e7d4ecc6 finish (inefficient) BMC for non-linear Horn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-15 10:48:42 -07:00
Leonardo de Moura f7f2a77504 Merge branch 'working' of //z3-1/z3 into working 2012-10-15 10:08:02 -07:00
Leonardo de Moura 4efe38a71d Added support for parsing negative numerals in the SMT 2.0 frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-15 10:02:52 -07:00