mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity
18223 commits 23 branches 48 tags 156 MiB
Commit graph

208 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 36382ccb57
Fix memory and concurrency issues in OCaml API (#6992) 
* Fix memory and concurrency issues in OCaml API

* Undo locking changes
 2023-11-16 18:28:12 -08:00
Christoph M. Wintersteiger 3af2b36cd7
Add Z3_solver_interrupt to OCaml API (#6976) 2023-10-31 08:48:06 -07:00
Christoph M. Wintersteiger 23de8056d7
Add RCF functions to OCaml API (#6932) 2023-10-06 11:49:22 +09:00
권승완 6670807103
update ocaml binding to support more string apis (#6656) 2023-03-29 05:49:33 -07:00
Patrick LaFontaine 0a59617bac
Fix Ocaml bindings FuncEntry to_string (#6639) 
Hello, I was looking at the different api string conversions for FuncEntry and I believe that the ml version is incorrect? Clearly we want the argument(`c`) to be comma separated from the accumulated string `p`. The current implementation just so happens to have most of the arguments separated, but the order is flipped and one of the commas is misplaced.
 2023-03-27 13:04:32 -07:00
Nikolaj Bjorner 63c0f35978 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:27:17 -08:00
Nikolaj Bjorner d51d518f96 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:24:45 -08:00
Nikolaj Bjorner 4c6d44f974 add ocaml signature for simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 18:58:18 -08:00
Nikolaj Bjorner fa72ec5405 switch to expose fresh function instead of changing legacy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:05:34 -08:00
Nikolaj Bjorner 3f1b7866ca convert caml mk_real to int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:53:42 -08:00
Nikolaj Bjorner aefd336c18 set OCaml default behaivor to enable concurrent dec ref #6160 
Add Z3_enable_concurrent_dec_ref to the API.
It is enables behavior of dec_ref functions that are exposed over the API to work with concurrent GC. The API calls to dec_ref are queued and processed in the main thread where context operations take place (in a way that is assumed thread safe as context operations are only allowed to be serialized on one thread at a time).
 2022-07-16 16:49:39 -07:00
Sacha Ayoun ffbabf251d
enhance ocaml seq api (#6010) 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
 2022-05-04 12:03:22 -07:00
Ryan Goulden 99e299b90c
ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003) 2022-04-27 12:36:09 +02:00
Anton Kochkov f3af2193d0
Use Stdlib. instead of Pervasives. due to deprecation (#5730) 2021-12-22 07:53:47 -08:00
Gabriel Radanne 0c7625cd26
Remove size argument in OCaml's Z3.mk_re_intersect (#5383) 
* Remove size argument in OCaml's `Z3.mk_re_intersect`

Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.

* Enable the ocaml documentation in Seq.

Turn all the comments into proper documentation comments.
 2021-07-06 01:21:04 -07:00
Nikolaj Bjorner 04a1d4245c fix #4801 2021-02-12 20:20:00 -08:00
Nikolaj Bjorner 006418e027 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 23:34:21 -07:00
Nikolaj Bjorner 74eb401c3b addrecdef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:18:25 -07:00
Nikolaj Bjorner 2bb712c9da ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:09:08 -07:00
Nikolaj Bjorner 5ea145ce26 ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:08:22 -07:00
Nikolaj Bjorner 10d0404175 add rec decl/def to ML #4563 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:38:32 -07:00
Nicola Mometto 77c3f1fb82 fix ocaml build by moving to Zarith methods 2019-10-14 09:48:51 -07:00
philzook58 ea8ef3edf8 edited error message string 2019-10-03 17:06:14 -07:00
philzook58 0321312c8d Changed to get_const_interp to match Java and C# bindings 2019-10-03 17:06:14 -07:00
Nikolaj Bjorner 40e329fc92 remove push/pop for fixedpoint objects from API #2249 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 10:13:15 -07:00
Nicola Mometto fa97f4a626 fix name clash in ocaml api 2019-03-26 14:16:31 +00:00
Nicola Mometto f18227bf2d Add Memory.reset to OCaml API 2018-11-26 17:24:51 +00:00
Nikolaj Bjorner b1ab473035 add arguments to optimize_check fix #1866 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 20:44:46 -07:00
Nikolaj Bjorner 09e40f6e23 add arguments to optimize_check fix #1866 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 20:43:35 -07:00
Nikolaj Bjorner 0457b5a73f add arguments to optimize_check fix #1866 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 20:39:54 -07:00
Nikolaj Bjorner 3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00
Nikolaj Bjorner 80d0c5cf82 fix #1836 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-24 16:52:25 -07:00
Nikolaj Bjorner 382bce4bb7 fix #1836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 19:19:40 -07:00
Nikolaj Bjorner 94ffa3963e fix #1800 by converting large integers to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-24 16:54:22 +02:00
Nikolaj Bjorner 6dc9c3a587 fix ml build breakd #1659, #1660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-29 07:37:27 -07:00
Nikolaj Bjorner 2b2aee3c18 remove unused operators #1530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-14 07:29:26 -07:00
Nikolaj Bjorner a875d3e491 fix #1429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-02 07:54:31 -08:00
Nikolaj Bjorner 8e1ab23c3d remove deprecated functions from ML API. #1393 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 18:43:29 +05:30
Sangwoo Joh 5845958986 Bugfix: get_objectives in ML API 2017-08-24 18:17:47 +09:00
Nikolaj Bjorner 6feb7ba795 :q 
add sequences to ML API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 14:28:05 -07:00
Christoph M. Wintersteiger 9053e6eba6 Resolved merge conflicts. Added FPA API input validity checks. 2016-11-15 20:19:40 +00:00
Christoph M. Wintersteiger 9ebea09d05 added is_numeral_negative to ML API. 2016-11-07 10:28:39 +00:00
Christoph M. Wintersteiger 81fce55d78 Updated optimization ML API. Addresses #776. 2016-11-04 21:22:01 +00:00
Christoph M. Wintersteiger 23c58a1ef6 Added FPA numeral predicates to ML API 2016-10-26 18:53:20 +01:00
Christoph M. Wintersteiger 7517cf485e ML API bugfixes for FPA numeral accessors 2016-10-24 13:32:37 +01:00
Christoph M. Wintersteiger 6b474adc8a Added accessors to extract sign/exponent/significand BV numerals from FP numerals. 2016-10-24 12:50:05 +01:00
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +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 bd9d13279a Pretty printing 2016-04-06 12:39:19 +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