mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-02 00:00:41 +00:00
Code Activity
16307 commits 65 branches 52 tags 179 MiB
Commit graph

95 commits

Author SHA1 Message Date
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
49dfaeb406 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-12 13:11:46 -07:00
Nikolaj Bjorner
dd5e2e8930 check for 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 10:44:00 -07:00
Nikolaj Bjorner
006418e027 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 23:34:21 -07:00
Nikolaj Bjorner
f3b51db891 ml build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 16:22:01 -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
Nikolaj Bjorner
a432fd71d3 update ocaml doc per #2843 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 20:26:06 -08:00
Nicola Mometto
77c3f1fb82 fix ocaml build by moving to Zarith methods 2019-10-14 09:48:51 -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
9008beeb01 fix mk_quantifier signature 2019-03-26 14:33:20 +00:00
Nicola Mometto
fa97f4a626 fix name clash in ocaml api 2019-03-26 14:16:31 +00:00
Bruce Mitchener
7fb0106ead Fix typo in OCaml API docs. 2018-11-27 22:14:41 +07:00
Nicola Mometto
f18227bf2d Add Memory.reset to OCaml API 2018-11-26 17:24:51 +00: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
a5762a78e9 change to ast-vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-30 17:39:18 -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
Bruce Mitchener
a3facc82fb Update OCaml docs for changes made elsewhere. 
This removes references to the PROOF_MODE that have been removed
elsewhere.
 2018-05-23 23:55:17 +07:00
Nikolaj Bjorner
b1f05d8271 fix #1539 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-14 18:14:29 -07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Christoph M. Wintersteiger
c3c06d756c Documentation fixes. 2017-12-18 20:12:19 +00: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
Christoph M. Wintersteiger
ed5058d225 Fixed typo in ML API. Relates to #1214. 2017-08-21 18:21:31 +01:00
Nikolaj Bjorner
aa81d58bb0 add sequences to ML API #1214 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-18 14:29:53 -07: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-neuhaeusser
bd9d13279a Pretty printing 2016-04-06 12:39:19 +02: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
Christoph M. Wintersteiger
824169da0a New OCaml API 2016-02-13 22:09:45 +00:00
Christoph M. Wintersteiger
689ed9fa12 Added Z3_mk_array_ext to ML API. 
Relates to #292
 2015-11-09 13:49:37 +00:00
Christoph M. Wintersteiger
cffff18373 -whitespace 2015-11-09 13:22:33 +00:00
Christoph M. Wintersteiger
6625f7a749 Added Z3_solver_translate to ML API. 2015-11-09 13:19:10 +00:00
Christoph M. Wintersteiger
cab42d2c66 Clarified documentation of par-or tactic. 
Relates to #269.
 2015-10-28 18:50:22 +00:00
Paul Phillips
64a5247813 Changed references to help-tactics to help-tactic. 2015-10-25 11:45:46 -07:00
Christoph M. Wintersteiger
18a0314f6b Fix for ast_map in ML API 2015-10-02 15:52:33 +01:00
Christoph M. Wintersteiger
9ad065a538 Bugfixes for the optimization module in the ML API 2015-08-15 23:51:43 +01:00
Nikolaj Bjorner
76ca64b93b add consistency per request from Gabriel R 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-09 18:56:42 +02:00
Nikolaj Bjorner
eb5af100bd adding optimize bindings for ML, adding get_reason_unknown to optimize, mentioned in pull request issue #188, second edition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-09 17:49:20 +02:00
Christoph M. Wintersteiger
004bf1471f Added conversion function for Goal to Expr conversion in .NET, Java, ML 2015-06-10 13:17:34 +01:00
Christoph M. Wintersteiger
98f2de3216 Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java, and ML APIs. 2015-06-09 12:57:19 +01:00
Christoph M. Wintersteiger
d8f6d84217 Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. 
Fixes #103
 2015-05-23 16:53:47 +01:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger
1c77ad00c3 Added accessors to enumeration sorts. Thanks to codeplex user steimann for suggesting this. 
(http://z3.codeplex.com/workitem/195)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-24 21:42:05 +00:00