mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
4122 commits 49 branches 53 tags 182 MiB
Commit graph

4122 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f8f23382dc bug fix: unsound pruning of assumptions. remove deprecated reduce() feature from smt_kernel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-03 17:36:21 -08:00
Leonardo de Moura
70baa3c8c9 Add nlsat.factor option. This is a workaround for the slow factorization procedure. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-02 21:18:02 -08:00
Leonardo de Moura
8a69e8a283 Merge 2013-01-02 21:15:51 -08:00
Leonardo de Moura
2cc3e3745e Fix gcc compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-02 21:14:22 -08:00
Nikolaj Bjorner
eee4b1a37b fix g++ build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 20:17:33 -08:00
Leonardo de Moura
edf62481e9 Add skeleton for the realclosure package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-02 18:08:42 -08:00
Nikolaj Bjorner
51a5d22f23 experiments wtih QHC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 09:50:31 -08:00
Nikolaj Bjorner
d318aab7d1 experiments wtih QHC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 09:49:27 -08:00
Leonardo de Moura
1235b3ea24 Fix header 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-31 14:40:52 -08:00
Leonardo de Moura
4681281765 Add example sent by Ganesh 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-31 14:37:54 -08:00
Leonardo de Moura
6a6015e335 Merge branch 'unstable' into contrib 2012-12-31 13:48:44 -08:00
Nikolaj Bjorner
63b7f7ecd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-28 16:40:36 -08:00
Nikolaj Bjorner
9f2743309f fix to proof hypothesis removal facility reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-28 16:40:29 -08:00
Leonardo de Moura
a51c6d125d Add support for Python Fraction object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-28 13:39:34 -08:00
Leonardo de Moura
d0d48c7ce2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-28 09:13:26 -08:00
Leonardo de Moura
9a523defa2 Add pp (debugging function) for params_ref 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-28 09:13:18 -08:00
Leonardo de Moura
8515044f8b Add option bvnot2arith 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-27 20:28:42 -08:00
Leonardo de Moura
1a09523c99 Fix mk_make bug introduced yesterday 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-27 09:10:13 -08:00
Leonardo de Moura
6e468e84e7 Update installation instructions in the README file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 17:37:18 -08:00
Leonardo de Moura
1b35668eb7 Improve Z3Py installation in non-standard prefix. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 17:24:26 -08:00
Leonardo de Moura
7c886fb7dd Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-26 15:50:54 -08:00
Leonardo de Moura
71aec11a04 Ignore callgrind files and Python pyo files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 15:50:09 -08:00
Nikolaj Bjorner
00b5d9e014 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-26 15:45:11 -08:00
Nikolaj Bjorner
c513f7e9c2 fixed slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-26 15:44:54 -08:00
Leonardo de Moura
53df82c314 Add arith_decls for underspecified operators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 11:35:00 -08:00
Nikolaj Bjorner
8b8fb74fd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-26 11:31:09 -08:00
Nikolaj Bjorner
bc77a97e92 qe lite checks 2012-12-26 11:28:05 -08:00
Leonardo de Moura
2a286541e0 Fix crash reported at http://z3.codeplex.com/workitem/11. Fix array rewriter bug, rewriter was producing sort incorrect expression. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-26 08:36:25 -08:00
Leonardo de Moura
fbce816025 Merge branch 'unstable' into contrib 2012-12-22 14:36:30 -08:00
Leonardo de Moura
3cc9d57438 Fix pytest, it should work with Python 2.7.x and 3.x 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-21 16:58:10 -08:00
Leonardo de Moura
a0a505e1b8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-20 17:48:30 -08:00
Leonardo de Moura
6602803850 Add Python 3.x support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-20 17:47:38 -08:00
Leonardo de Moura
7d97f407c2 Remove non-ascii characters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-20 11:22:03 -08:00
Josh Berdine
d7b8110cc8 Regenerate ml api 2012-12-20 12:58:21 +00:00
Josh Berdine
a7f89dcdd2 Move Z3_get_implied_equalities from v3 to v4 ml api as it now needs Z3_solver type 2012-12-20 12:54:44 +00:00
Josh Berdine
fd5372d7a2 Z3_search_failure type not needed in v4 ml api 2012-12-20 12:53:05 +00:00
Josh Berdine
32896a15e6 Fix for compiling ml api 2012-12-20 12:49:17 +00:00
Josh Berdine
27438b0fc9 Fix newlines 2012-12-20 12:48:49 +00:00
Leonardo de Moura
7b1fac11e6 Add new C++ examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-19 12:33:14 -08:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 17:14:25 -08:00
Leonardo de Moura
3ddb1a85f1 Add basic_recognizers and array_recognizers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 15:00:16 -08:00
Leonardo de Moura
cec328cfdc Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 14:44:51 -08:00
Leonardo de Moura
4f0d5a5756 Add thanks to Etienne Kneuss 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 07:27:20 -08:00
Leonardo de Moura
83f7b294cc Update RELEASE_NOTES with latest bug fix 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 21:05:04 -08:00
Leonardo de Moura
08789b69d4 Fix warning on FreeBSD 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 20:56:20 -08:00
Leonardo de Moura
9674f511b3 Fix scoped_timer for Linux. Nested timers were misbehaving, and it was not possible to create timers in more than one thread 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 20:46:04 -08:00
Leonardo de Moura
607fab486c Fix incorrect uses of set_cancel() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 18:48:10 -08:00
Leonardo de Moura
f8014f54c1 Fix bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 15:13:05 -08:00
Leonardo de Moura
8c211dd4fc Fix bug reported by Philippe Suter, see RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 14:07:21 -08:00
Leonardo de Moura
143b829488 Fix literal duplication bug that was introduced after v4.3.1 release 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 13:42:01 -08:00