3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Commit graph

75 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 68a2c08d5e
Add Z3_get_estimated_alloc_size to OCaml API (#7068) 2023-12-21 12:54:30 -08:00
Christoph M. Wintersteiger 16753e43f1
Add accessors for RCF numeral internals (#7013) 2023-11-23 17:54:23 +01:00
Christoph M. Wintersteiger 23de8056d7
Add RCF functions to OCaml API (#6932) 2023-10-06 11:49:22 +09: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 47c7ed3b17 update ml example to 64 bit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-24 04:33:52 -08:00
Kartik Singhal 1dcbd2d86c
Correct capitalization of package (#5569)
See https://stackoverflow.com/a/50004273/1167061
2021-09-25 09:04:06 -07:00
Kiwamu Okabe 81b8f397b3
Need -thread option to compile OCaml example (#5440)
I can compile the OCaml example with `-thread` option at Linux.

```
$ ocaml --version
The OCaml toplevel, version 4.05.0
```
2021-07-28 16:57:26 -07:00
Bruce Mitchener a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +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
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Christoph M. Wintersteiger b99fcb9c8a More new OCaml API 2016-02-14 19:56:22 +00:00
Christoph M. Wintersteiger 7e3676e24a bugfix for ML example 2016-01-08 13:25:14 +00:00
Christoph M. Wintersteiger 134b93b43e ML API build fixes for Windows. 2015-12-14 14:41:19 +00:00
Christoph M. Wintersteiger 771caba9db update ML example readme 2015-12-13 17:44:50 +00:00
Christoph M. Wintersteiger b92bdaeebe ML API readme fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-24 18:51:47 +00:00
Christoph M. Wintersteiger e29abefb12 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng
Conflicts:
	scripts/mk_util.py

+ Cosmetics

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-24 18:44:59 +00:00
Christoph M. Wintersteiger 5c7d0380d3 Fixes in the OCaml FPA API and example 2015-01-24 18:29:52 +00:00
Christoph M. Wintersteiger 65ccc9a8ea added FPA ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-23 19:36:47 +00:00
Christoph M. Wintersteiger ed0fa93245 Minor adjustments after rebase
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:35:19 +00:00
Christoph M. Wintersteiger 10c153bfe4 ML API: build fix 2015-01-19 17:17:13 +00:00
Christoph M. Wintersteiger 05af33ac7d ML API: ocamlfind installation fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:13:52 +00:00
Christoph M. Wintersteiger 555a3883b9 ML example doc fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:11:18 +00:00
Christoph M. Wintersteiger 0465ad3ce6 ML example; or' is deprecated, changed to ||'
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:11:16 +00:00
Christoph M. Wintersteiger 9dc8021995 Added facilities for ocamlfind in the ML API build
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:11:15 +00:00
Christoph M. Wintersteiger 54b7f8eec3 ML API bugfix (Codeplex issue 102)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:09:39 +00:00
Christoph M. Wintersteiger b889b225a0 ML cleanup; makefile removed. The example is built by running make examples in the build directory.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:09:36 +00:00
Christoph M. Wintersteiger c1e29dabe7 ML API: renamed assert_ to add
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:15 +00:00
Christoph M. Wintersteiger 050629536a ML API: bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:14 +00:00
Christoph M. Wintersteiger eea13a087f ML API savegame
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:14 +00:00
Christoph M. Wintersteiger d293b579f3 ML API: flat & rich layer in place.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:13 +00:00
Christoph M. Wintersteiger 79d0c32c91 ML API: replaced arrays with lists.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:12 +00:00
Christoph M. Wintersteiger 6842acbea8 ML API: Cleanup
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:10 +00:00
Christoph M. Wintersteiger 9142901efe ML API: bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:08 +00:00
Christoph M. Wintersteiger 9ed926498f ML API: updated example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:06:20 +00:00
Christoph M. Wintersteiger 3347d7ca8c ML API: moved more objects into normal types.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger 6257c56901 ML API: bugfixes; starting to replace objects with normal types.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger 1e2b546b03 ML API: changed context from object to normal type. Removed optional array parameters.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:06:17 +00:00
Christoph M. Wintersteiger e2f6b10e32 ML API bugfixes
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:02:17 +00:00
Christoph M. Wintersteiger c03d5277bc more ML
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger 25498345e5 New ML API bugfixes and first example.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger c2ff90720e ML API: mk_context added.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:35 +00:00
Christoph M. Wintersteiger 49a4e77a6d More new ML API.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:34 +00:00
Christoph M. Wintersteiger c28f0e7c8a ML API bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:31 +00:00
Christoph M. Wintersteiger 7ae90f0b20 More ML API:
Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:01:29 +00:00
Christoph M. Wintersteiger 1685e3dd6f ML API bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:57:10 +00:00
Christoph M. Wintersteiger 0e98d26721 ML API and example compilation.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:56:42 +00:00
Christoph M. Wintersteiger c9cca119c5 File renamed
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:55:24 +00:00
Christoph M. Wintersteiger f7b3529f01 More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:55:22 +00:00
Christoph M. Wintersteiger ccffea2bc9 ML API: build fix 2015-01-19 16:08:38 +00:00
Christoph M. Wintersteiger 1e4b14af67 ML API: ocamlfind installation fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 16:07:00 +00:00