mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
978 commits 23 branches 48 tags 157 MiB
Commit graph

645 commits

Author SHA1 Message Date
Leonardo de Moura 711abc75fb Fix issue reported at http://z3.codeplex.com/workitem/14 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 13:22:28 -08:00
Leonardo de Moura 7e7927052e Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-24 12:51:11 -08:00
Leonardo de Moura 7eaa5562d8 Fix http://z3.codeplex.com/workitem/19 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 12:51:03 -08:00
Nikolaj Bjorner 521382e37f working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:50:19 -08:00
Nikolaj Bjorner d3025569c2 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:45:58 -08:00
Leonardo de Moura afaef63bfa Fix compilation error when using gcc. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 12:38:37 -08:00
Nikolaj Bjorner c89531bcf8 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 21:44:42 -08:00
Nikolaj Bjorner b61c1b0ded working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 19:05:38 -08:00
Nikolaj Bjorner 085ccf5eff working on tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 22:28:25 -08:00
Nikolaj Bjorner af4c09c8d3 update substitution routines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 21:59:20 -08:00
Nikolaj Bjorner b9cc7080e7 update substitution routines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 21:47:43 -08:00
Leonardo de Moura 7cad0b4a1f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-21 08:27:56 -08:00
Leonardo de Moura a3eb6d121f Merge branch 'cade24' into unstable 2013-01-21 08:27:32 -08:00
Nikolaj Bjorner 87e9015675 working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-20 18:41:41 -08:00
Leonardo de Moura 5d938a5fe2 Fix bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:41:24 -08:00
Leonardo de Moura 3344151aca Replace # with x in the definition of algebraic elements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:21:09 -08:00
Nikolaj Bjorner 99f5a5bddb working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 17:36:42 -08:00
Nikolaj Bjorner cab908bfef working on horn tab solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 09:56:35 -08:00
Nikolaj Bjorner 8daf100c65 working on tab Horn solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 18:03:34 -08:00
Christoph M. Wintersteiger 79dafcea81 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-17 19:31:24 +00:00
Christoph M. Wintersteiger 4b18c8f9c4 Java API: syntactic adjustments, getters, setters, 
... convenience parameters, etc.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:31:02 +00:00
Christoph M. Wintersteiger 3abf397560 Added Solver.AssertAndTrack 
Convenience fixes.
Renamed Context.Const to Context.ConstProbe

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:30:00 +00:00
Nikolaj Bjorner c0f22039e4 add back cooperate.h include (not used now, but will be) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 08:23:09 -08:00
Nikolaj Bjorner b19a47176b working on tab 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 08:17:21 -08:00
Nikolaj Bjorner 50bf845b40 add tabulation/subsumption engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-16 17:16:44 -08:00
Leonardo de Moura bb386c0f18 Fix problem in inv_rf 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 11:19:11 -08:00
Leonardo de Moura c9b7ea35b6 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 08:39:24 -08:00
Leonardo de Moura be266bdd56 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-15 17:44:18 -08:00
Leonardo de Moura eea3384106 Add lazy normalization for algebraic extension values. Increase default max_precision to 128. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 16:35:36 -08:00
Leonardo de Moura 217c8375ce Add new rational function normalization procedure. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 14:34:34 -08:00
Nikolaj Bjorner ca5eb5186d fix pretty printer for smt2 unary minus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-15 09:24:12 -08:00
Christoph M. Wintersteiger 5f0cb28ca3 .NET and Java APIs: added functions for global parameter management. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-15 17:05:31 +00:00
Leonardo de Moura f0737bdf7f Replace expensive_eval_sign_at with version that does not generate rational numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:30:36 -08:00
Leonardo de Moura 799fe073db Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:29:08 -08:00
Leonardo de Moura 991a1528cd Cache isolating interval for better pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:17:15 -08:00
Leonardo de Moura 025cb2a2a8 Avoid wasteful memory allocation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:03:22 -08:00
Leonardo de Moura 38e0b4a20a Fix bug. Add is_denominator_one macro. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:55:52 -08:00
Leonardo de Moura 742f2b07dd Add support for compact string representation in the RCF API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:08:32 -08:00
Leonardo de Moura 6c35e08e43 Make sure we do not use denominators != 1 when encoding values of algebraic extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 10:43:18 -08:00
Leonardo de Moura 39d5b850e8 Fix bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 12:59:39 -08:00
Leonardo de Moura 7312f49f88 Fix Visual Studio warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 09:06:07 -08:00
Leonardo de Moura 93f37bdf9f Merge branch 'realclosure' into unstable 2013-01-12 22:03:40 -08:00
Leonardo de Moura f747bde548 Add restore_interval for extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 21:59:41 -08:00
Leonardo de Moura be2bf861c7 Use clean_denominators before root isolation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 20:43:17 -08:00
Leonardo de Moura 2b5883454c Add support for prem_gcd in square_free 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:49:50 -08:00
Leonardo de Moura 551d0b7de0 Fix bug in sprem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:44:05 -08:00
Leonardo de Moura 7711146d23 Add prem_gcd based on pseudo-remainder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:36:07 -08:00
Leonardo de Moura 13d5c3e07a Add normalize_int_coeffs to control the coefficient growth in Sturm sequences 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 18:01:29 -08:00
Leonardo de Moura e6102a8260 Move clean_denominators code to the top 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 17:11:42 -08:00
Leonardo de Moura 1e362e6fec Add comments to mark sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 17:08:58 -08:00
Leonardo de Moura a9fa232f11 Fix bug in compare 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:45:24 -08:00
Leonardo de Moura ea9421bb38 Expose rcf module parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:40:45 -08:00
Leonardo de Moura e6a35c6241 Add prem to avoid rational function values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:27:56 -08:00
Leonardo de Moura 09d3686d58 Fix memory leak in realclosure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 15:54:07 -08:00
Leonardo de Moura 1d761ea9a5 Add clean_denominators procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 15:45:43 -08:00
Leonardo de Moura d60f2db116 Remove select method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 09:46:00 -08:00
Leonardo de Moura a03a6e9bf6 Add more tracing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 21:12:51 -08:00
Leonardo de Moura ef11ef61b5 Clean m_val field when switching to GMP bignum 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 17:55:52 -08:00
Leonardo de Moura 5ce70eb521 Fix bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 17:55:03 -08:00
Leonardo de Moura 3cc072f3a7 Add bisect_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 16:28:39 -08:00
Leonardo de Moura 5a9040a247 Replace is_real with depends_on_infinitesimals to avoid misunderstandings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 10:35:38 -08:00
Leonardo de Moura 0de6b4cc92 Complete the implementation of expensive_algebraic_poly_interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 10:11:03 -08:00
Christoph M. Wintersteiger 61b686f86f FPA: fixes for sbits < ebits 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-11 11:15:18 +00:00
Leonardo de Moura 714167a378 Add more tracing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 18:36:47 -08:00
Leonardo de Moura 2f5c7c9ba9 Add determine_algebraic_sign 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 17:07:32 -08:00
Leonardo de Moura 619e597174 Add normalize_algebraic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 13:38:51 -08:00
Leonardo de Moura 4cd2998743 Add power operator to C and Python RCF APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 13:05:47 -08:00
Leonardo de Moura 191e503418 Fix bug. Improve nl_nz_sqf_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:51:54 -08:00
Leonardo de Moura 71ab7759d1 Add root method (syntax sugar for isolate_roots) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:23:37 -08:00
Leonardo de Moura 1a7d39f9a0 Add refine_algebraic_interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:09:07 -08:00
Leonardo de Moura 4a0b431cf4 Add mk_algebraic method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 11:13:21 -08:00
Christoph M. Wintersteiger dd127c2f71 Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:16:29 +00:00
Christoph M. Wintersteiger 3482b8f4f1 .NET API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:08:56 +00:00
Leonardo de Moura 872165fa55 Add more tracing to sign_det_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 09:17:22 -08:00
Leonardo de Moura eca78aa9c6 Fix incorrect assertions and bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 08:52:25 -08:00
Leonardo de Moura 191de6f7b5 Fix test program 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 08:01:42 -08:00
Leonardo de Moura d644b37ac1 Add non naive sign determination algorithm 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 22:35:39 -08:00
Leonardo de Moura 1712f0a33b Add goodies 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 18:43:32 -08:00
Leonardo de Moura 81807c7001 Add procedure for computing TaQ(Q, P; a, b) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 13:37:10 -08:00
Leonardo de Moura b662bc8dc7 Add lower and upper bounds for negative and positive roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 11:16:04 -08:00
Leonardo de Moura 9c8b428ffb Add matrix operations needed for implementing non-naive sign determination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-08 17:58:34 -08:00
Leonardo de Moura ff809db16d Add get_int and get_uint to mpz_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-08 15:40:19 -08:00
Leonardo de Moura e01a7b6268 Fix memory management bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 17:31:53 -08:00
Leonardo de Moura 5873a59769 Add root upper bounds estimation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 16:23:30 -08:00
Leonardo de Moura 4ea06b8040 Fix Z3_enable_trace API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 16:22:47 -08:00
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