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

4323 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 88f92660f0 Added param descrs collection to ackermannize_bv_tactic 2016-05-06 18:29:19 +01:00
Christoph M. Wintersteiger 4d11e57a33 Added param descrs collection to ackermannize_bv_tactic 2016-05-06 18:28:08 +01:00
Nikolaj Bjorner e4367803c1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-05 14:11:27 -07:00
Nikolaj Bjorner 5b31f54501 max/min 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-05 14:11:13 -07:00
Christoph M. Wintersteiger 50910e5b3b Merge branch 'master' of https://github.com/Z3Prover/z3 into new-mpf-rem 2016-05-05 12:24:29 +01:00
Nuno Lopes 0286cee450 simplify th_rewriter::mk_eq_value() 2016-05-05 11:00:21 +01:00
Nikolaj Bjorner 9e4b9ea98b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-04 11:17:18 -07:00
Nikolaj Bjorner 044e08a114 adding unit tests for qe_arith/mbo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-04 11:17:09 -07:00
Christoph M. Wintersteiger 40b9d0871a Merge branch 'master' of https://github.com/Z3Prover/z3 into new-mpf-rem 2016-05-04 16:24:56 +01:00
Nikolaj Bjorner d11d9bd1de avoid crash on quantifiers + sequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 16:24:12 -07:00
Nikolaj Bjorner 52e367417f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-03 11:09:14 -07:00
Nikolaj Bjorner 91af947863 adding checks for #570 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 11:09:05 -07:00
Christoph M. Wintersteiger a7c66356ae mpf partial remainder draft 2016-05-03 18:20:18 +01:00
Christoph M. Wintersteiger 107f50d41e Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-05-03 17:56:52 +01:00
Nikolaj Bjorner 6895cc7cc6 remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:21:15 -07:00
Nikolaj Bjorner e375be767d remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:20:20 -07:00
Christoph M. Wintersteiger 140f0bb794 ML API build fix 2016-05-03 13:34:20 +01:00
Christoph M. Wintersteiger 86126e2c01 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-05-03 11:52:21 +01:00
Nikolaj Bjorner 67e49b4adc fixing model-based-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-01 17:15:20 -07:00
Nikolaj Bjorner 22507281cf fix model generation in opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 12:23:46 -07:00
Nikolaj Bjorner 4b940bde11 fix compilation of unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 11:46:25 -07:00
Nikolaj Bjorner e29adbf304 fix issues #581: nested timeouts canceled each-other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-30 11:18:34 -07:00
Nikolaj Bjorner a020b13f10 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-29 19:08:29 -07:00
Nikolaj Bjorner 2428bf18f1 add model correction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-29 19:08:10 -07:00
Nikolaj Bjorner 121386779a Merge pull request #580 from yaqwsx/expr_operators_in_c++ 
Add srem, urem, shift, ext operators to c++ api
 2016-04-29 18:51:14 -07:00
Nikolaj Bjorner c75fd02c95 qsat-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-28 21:31:16 -07:00
xlauko ae2821dea1 Add srem, urem, shift, ext operators to c++ api 2016-04-28 21:58:05 +02:00
Nikolaj Bjorner c414c6b5fd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-28 09:48:04 -07:00
Nikolaj Bjorner 932ef442ae model based opt dev 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-28 09:47:55 -07:00
Christoph M. Wintersteiger 47ec3b1f87 Build fix for VS2012 2016-04-28 13:17:39 +01:00
Christoph M. Wintersteiger f3c74a06eb debug fix for mpf_manager 2016-04-28 12:54:10 +01:00
Christoph M. Wintersteiger deea4e92f2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-28 12:52:49 +01:00
Christoph M. Wintersteiger cba82325de Build fix for old systems that don't have a float remainder(...) function. 2016-04-28 12:52:36 +01:00
Nikolaj Bjorner 83d84dcedd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-27 15:09:12 -07:00
Nikolaj Bjorner 6aa6102891 factor out model-based-opt code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 15:08:10 -07:00
Christoph M. Wintersteiger 10cc8c3a75 Build fix for VS2012 and earlier. 2016-04-27 20:15:22 +01:00
Nikolaj Bjorner 68c7d64d00 adding model-based opt facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-27 11:18:20 -07:00
Christoph M. Wintersteiger bf49f81622 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-27 13:26:23 +01:00
Nikolaj Bjorner a1aa166ef5 adding local optimization to qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-26 17:15:24 -07:00
Christoph M. Wintersteiger 6455bf8114 New implementation for mpf_manager::rem. 
Relates to #561
 2016-04-26 21:13:02 +01:00
Nikolaj Bjorner 271b56aa1b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-24 09:21:10 -07:00
Nikolaj Bjorner d97bddc3b5 revert to legacy syntax to enable older versions of .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-24 09:21:05 -07:00
Christoph M. Wintersteiger be424d9cbb Bugfixes for fp.roundToIntegral and fp.rem. 
Relates to #561
 2016-04-24 15:14:16 +01:00
Christoph M. Wintersteiger 952e3afb90 bugfix for hwf_manager::rem 2016-04-24 15:11:24 +01:00
Christoph M. Wintersteiger 3131f29816 whitespace 2016-04-24 15:11:03 +01:00
Nikolaj Bjorner 643a87cb5b overloading support for C# expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-23 22:03:27 -07:00
Nikolaj Bjorner 662e43d264 overloading support for C# expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-23 15:50:30 -07:00
Nikolaj Bjorner e4b7ac37f3 add overloading for arithmetical expressions in C# to handle common cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-22 13:58:02 -07:00
Nikolaj Bjorner 8ee49d16df Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-21 10:49:22 -07:00
Nikolaj Bjorner 20a6b41c5c coalescing is-int check for python 2.x, issue #572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-21 10:49:16 -07:00
Nikolaj Bjorner d0175b96b8 guarding against null symbols creeping in. Issue #571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-20 14:07:45 -07:00
Nuno Lopes 417c80edbc fix mem leak in quantifier_info::insert_qinfo on timeout 2016-04-19 02:17:12 -07:00
Nikolaj Bjorner b512212d41 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:31:36 -07:00
Nikolaj Bjorner 3a6218ac21 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:30:52 -07:00
Nikolaj Bjorner cff843ca59 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-18 17:22:54 -07:00
Nikolaj Bjorner 4cb57cd4da fix regression introduced by using ref-vectors on non-ref'ed output parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:22:47 -07:00
Nikolaj Bjorner c3f4124a9f trace down recent exposed regression in goal2sat, incorporate Scott's suggestion on making vector<std::string inaccessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 14:50:10 -07:00
Nikolaj Bjorner 81232808ba add handling for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 11:17:33 -07:00
Nikolaj Bjorner 4761f4f191 add handling for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 11:14:40 -07:00
Christoph M. Wintersteiger 5d0db6d256 Fixed memory leak in goal::update. 
Fixes #567
 2016-04-18 17:18:16 +01:00
Christoph M. Wintersteiger 6db0a15d29 Fixed potential memory leakage issues in fpa2bv_converfter 2016-04-18 17:17:31 +01:00
Christoph M. Wintersteiger 3ffcea0fe4 whitespace 2016-04-18 16:52:12 +01:00
Martin R. Neuhaeusser 67ac1a003e Avoid conversion between mutable arrays and lists in OCaml API. 
This patch eliminates the conversion between OCaml arrays and lists
from Z3's OCaml API.
 2016-04-18 17:20:27 +02:00
martin-neuhaeusser 34bf4b1d3c Fix installation of custom error handler during context creation in OCaml bindings 
This patch fixes a bug detected by valgrind, where a custom error handler
did not get installed correctly.
 2016-04-18 17:20:12 +02:00
Nikolaj Bjorner 0094b36636 fix bounds check to fix segfault reported in issue #565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 12:25:29 -07:00
Nikolaj Bjorner 1c8e0918d8 move to std::vector in replayer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 10:08:29 -07:00
Nikolaj Bjorner d383fd851a move vector<std::string to std::vector<std::string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:34:27 -07:00
Nikolaj Bjorner 4ebf392da7 Fixes #564: use std::vector on std::strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-16 09:26:13 -07:00
Nikolaj Bjorner 0f93853a4c remove labels from evaluation result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 13:17:10 -07:00
Nikolaj Bjorner aa7b5d80fe extract array terms for evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-12 09:41:50 -07:00
Nikolaj Bjorner 2033719c14 fix optimization pre-processing reported by Gereon Kremer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-09 20:58:57 -07:00
Nikolaj Bjorner 6e57015a12 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-09 16:51:42 -07:00
Nikolaj Bjorner cc6f72aba7 fix handing of ite conditions that have to be included in projection, thanks to bug report by Zak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-10 01:48:35 +02:00
Christoph M. Wintersteiger 16e487b32a Bugfix for ackermann helper 2016-04-08 17:20:09 +01:00
Christoph M. Wintersteiger bd0bd08ecf add is_considered_uninterpreted checks into acker_helper 2016-04-08 16:58:11 +01:00
Christoph M. Wintersteiger 0597b579b1 Bugfixes for bvarray2uf conversion. 2016-04-07 19:10:31 +01:00
Christoph M. Wintersteiger 5971c20653 Bugfixes for bv_trailing. 2016-04-07 13:08:17 +01:00
Christoph M. Wintersteiger 3a532c08a6 Bugfix for func_interp else-case compression 2016-04-06 19:24:08 +01:00
Christoph M. Wintersteiger 324fcc6a13 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-04-06 15:40:13 +01:00
Christoph M. Wintersteiger e662427060 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 15:39:37 +01:00
Christoph M. Wintersteiger e527aca296 Bugfix for unspecified else-case in func_interps. 2016-04-06 15:39:32 +01:00
Nuno Lopes e2b7ad246a bv_trailing: fix compiler warning + use of ast_manager 2016-04-06 15:34:31 +01:00
Christoph M. Wintersteiger 7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01:00
martin-neuhaeusser 95454679e2 Another round of pretty printing 2016-04-06 12:45:21 +02:00
martin-neuhaeusser bd9d13279a Pretty printing 2016-04-06 12:39:19 +02:00
martin-neuhaeusser 1662ba8353 Add more comments on comparison functions in the C layer of the OCaml bindings 2016-04-06 12:36:11 +02:00
martin-neuhaeusser b873c6b508 Simplify OCaml API 
This patch simplifies the implementation of the OCaml bindings. For example,
the applyX wrapper functions have become unnecessary in the new OCaml API.
It also removes the internal ML2C structure that was used as an intermediate
layer between the C and the OCaml layer.
 2016-04-06 12:10:59 +02:00
Mikolas Janota dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas 9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota 248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas 78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00
mikolas c7f1746321 Starting to work on trailing 0 analysis. 2016-04-06 11:04:03 +01:00
Nikolaj Bjorner 493b86eca7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-05 22:27:11 +02:00
Nikolaj Bjorner b97d694e5e undo model evaluation to BR_FULL pending regression in assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 22:26:57 +02:00
mikolas 05ce886afe Avoiding adding spurious +0 in poly_rewriter::cancel_monomials. 2016-04-05 17:26:48 +01:00
martin-neuhaeusser 71f991c5df Avoid using physical equality checks in OCaml bindings (z3.ml) 
This patch avoids the use of physical equality wherever possible
and improves some details of the OCaml implementation.
 2016-04-05 12:51:03 +02:00
Nikolaj Bjorner c454b81b2c special case branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 11:57:49 +02:00
Nikolaj Bjorner ed1a5797fb check that a clause was not removed to fix issue #551 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 20:15:49 +02:00