mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity
19510 commits 22 branches 48 tags 156 MiB
Commit graph

19510 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner bdad4e3bcb optimize model pruning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-14 11:19:02 -07:00
Nikolaj Bjorner f27c9b9d3d optimize model pruning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-14 11:17:05 -07:00
Nikolaj Bjorner bf0481c4d0 working on pdr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-14 11:13:36 -07:00
Nikolaj Bjorner 990b93c2fd working on pdr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-14 00:24:17 -07:00
Nikolaj Bjorner 16cfb3895d optimize model pruning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-13 20:09:12 -07:00
Nikolaj Bjorner 95fbf073f8 Merge branch 'working' of https://z3-1/gw/git/z3 into working 2012-10-13 20:09:04 -07:00
Leonardo de Moura 6a7d180e69 goodies for gdb 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-13 18:13:39 -07:00
Nikolaj Bjorner 72809843d5 Merge branch 'working' of https://z3-1/gw/git/z3 into working 2012-10-13 17:55:12 -07:00
Nikolaj Bjorner 148416122f optimize model pruning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-13 17:52:37 -07:00
Nikolaj Bjorner 0a8be25149 optimize model pruning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-13 16:15:42 -07:00
Leonardo de Moura a159943669 cygwin support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-13 14:07:39 -07:00
Leonardo de Moura 3cf96f7475 Merge branch 'working' of ssh://localhost:22/home/leo/projects-bare/z3 into working 2012-10-13 14:03:44 -07:00
Leonardo de Moura 42572ec93a added missing script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-13 14:03:03 -07:00
Nikolaj Bjorner 9828a29b68 better proof mining for Farkas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-13 10:13:14 -07:00
Nikolaj Bjorner 8121386d5e Merge branch 'working' of https://z3-1/gw/git/z3 into working 2012-10-13 10:13:02 -07:00
Leonardo de Moura bccf07be0b fixed bug in unsat core generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-13 09:11:54 -07:00
Leonardo de Moura 6145ccc077 Added tactic for qfnra purely based on nlsat 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 17:34:23 -07:00
Nikolaj Bjorner af469f82ec better proof mining for Farkas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-12 17:20:55 -07:00
Nikolaj Bjorner 9ad4b5bc0f Merge branch 'working' of https://z3-1/gw/git/z3 into working 2012-10-12 17:15:53 -07:00
Nikolaj Bjorner 2087c59084 better proof mining for Farkas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-12 17:12:43 -07:00
Leonardo de Moura 5c0d82d555 Updated Release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 16:42:28 -07:00
Leonardo de Moura af13e22f99 Merge branch 'working' of //z3-1/z3 into working 2012-10-12 16:38:06 -07:00
Leonardo de Moura 75457e1393 int<->real coercions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 16:34:54 -07:00
Christoph M. Wintersteiger c2623e15c3 Switched ParamDescrs.ToString to native implementation 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-10-12 21:05:32 +01:00
Leonardo de Moura c48bd1e8de updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 12:16:20 -07:00
Leonardo de Moura 44db8c083d exposed solver object param descrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 09:42:45 -07:00
Leonardo de Moura f7bcd40137 Added API Z3_param_descrs_to_string 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 09:13:04 -07:00
Christoph M. Wintersteiger 42c27b7a46 Added ParamDescr.ToString() 
Formatting

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-10-12 16:44:46 +01:00
Leonardo de Moura 4d70722769 Merge branch 'working' of //z3-1/z3 into working 2012-10-12 07:48:45 -07:00
Leonardo de Moura b0a2d8488d added repr method to ParamDescrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 07:47:55 -07:00
Christoph M. Wintersteiger c11e134aae Formatting and build configuration fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-10-12 15:13:38 +01:00
Christoph M. Wintersteiger 6c475660d8 Removed support for signed assemblies. 
Users are advised to build their own assemblies from the source code,
which they can sign using their own private keys.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-10-12 15:12:21 +01:00
Leonardo de Moura 1f61381172 trying to compile Z3 using cygwin/gcc... 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-12 00:07:16 -07:00
Leonardo de Moura 4dc834d5ee making sure that Z3 can be compiled with cygwin/g++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-11 21:59:09 -07:00
Leonardo de Moura ad107bfc42 fixed typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-11 21:47:46 -07:00
Leonardo de Moura 44a98920d1 improved z3py installation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-11 21:34:36 -07:00
Leonardo de Moura 12882f865f Fixed z3test.py. Execute z3test.py during Z3Py installation. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-11 21:06:07 -07:00
Leonardo de Moura db8782e7e7 New default behavior in the strategic_solver: invoke tactics when incremental solver returns unknown. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-11 19:27:19 -07:00
Nikolaj Bjorner 89ca9aa5bd bmc/farkas/smt2 pattern printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-11 09:34:15 -07:00
unknown 27a5bd5b83 working on bmc and bug fixes 
Signed-off-by: unknown <nbjorner@NBJORNER-X200.redmond.corp.microsoft.com>
 2012-10-11 09:11:56 -07:00
unknown 3e810ca74f working on bmc and bug fixes 
Signed-off-by: unknown <nbjorner@NBJORNER-X200.redmond.corp.microsoft.com>
 2012-10-11 09:05:12 -07:00