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

1126 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura 56db84a0e5 Fix RCF API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 15:10:16 -08:00
Leonardo de Moura 09b5724d82 Simplify RCF C API. Add Z3_rcf_mk_roots (C API) and MkRoots (Python API). Implement basic root isolation support. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 12:25:28 -08:00
Leonardo de Moura 3c1f1a3b65 Fix bug in realclosure::compare function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:50:36 -08:00
Leonardo de Moura 3e19df0441 Fix API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:25:46 -08:00
Leonardo de Moura 4d578b418f Fix bug in approx_div 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:15:37 -08:00
Leonardo de Moura 1c8101419b Add Python API for RCF module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:59:00 -08:00
Leonardo de Moura 9fbbdb56e4 Implement RCF external C API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:06:27 -08:00
Leonardo de Moura f1d47f35b2 Add refine interval infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 18:30:41 -08:00
Leonardo de Moura c01f27fe13 Add small interval caching infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 10:46:38 -08:00
Leonardo de Moura 47c6a73e19 Add RCF external API skeletons 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 22:24:56 -08:00
Leonardo de Moura ecb58091f7 Add support for transcendental values such as pi and e, and the power operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 21:26:12 -08:00
Leonardo de Moura ae1da72cb7 Implement compare 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 20:21:49 -08:00
Leonardo de Moura 3ffda25350 Implement add, sub, mul, div, inv, neg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 18:43:57 -08:00
Leonardo de Moura 322d355290 Simplify data-structures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 11:51:58 -08:00
Leonardo de Moura 14827e94f0 Fix typos and bugs. Add tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 15:01:27 -08:00
Leonardo de Moura ff62948d90 Add div and inv for binary rational intervals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 12:31:28 -08:00
Leonardo de Moura c430fe26aa Add ite operator to the C++ API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:29:25 -08:00
Leonardo de Moura 0203fa56d2 Add tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:11:33 -08:00
Leonardo de Moura 9ede98a029 Fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:09:20 -08:00
Leonardo de Moura 15ed819fbd Implement mk_transcendental. Replace extension_ref with extension *. Remove m_to_delete 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 22:09:43 -08:00
Leonardo de Moura 1ed275b801 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 22:08:32 -08:00
Leonardo de Moura 6160b2891b Change representation for values in the module for encoding infinitesimals, algebraic extensions and transcendal extensions. Implement basic polynomial operations for polynomials in this field 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:47:23 -08:00
Leonardo de Moura ed5b106574 Add support for ref_buffers with different initial sizes. Add shrink and operator= methods. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:45:28 -08:00
Leonardo de Moura f324724abc Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:43:48 -08:00
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
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 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