假设我想检查公式 x+y=z（x,y,z 整数）是否可满足。使用 Z3 我可以输入如下内容：
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= z (+ x y)))
(check-sat)
我可以等效地使用 OCaml api 并编写以下代码：
let ctx=Z3.mk_context [("model", "true"); ("proof", "false")] in
let v1=(Z3.Arithmetic.Integer.mk_const_s ctx "x") in
let v2=(Z3.Arithmetic.Integer.mk_const_s ctx "y") in
let res=(Z3.Arithmetic.Integer.mk_const_s ctx "z") in
let sum=Z3.Arithmetic.mk_add ctx [ v1 ; v2] in
let phi=Z3.Boolean.mk_eq ctx sum res in
let solver = (Z3.Solver.mk_solver ctx None) in
let _= Z3.Solver.add solver [phi] in
let is_sat=Z3.Solver.check solver …我在 OCaml 中操作二维数组。我有一些问题：
如何声明一个长度为类型int64而不是类型的数组int？例如，Array.make : int -> 'a -> 'a array如果我需要一个索引类型为 的更大数组int64怎么办？
我可以写如下内容吗：
let array = Array.make_matrix 10 10 0 in array.(1).(2) <- 5; 数组。(3).(4) <- 20; (* where I modify a part of values in array) f array ... ... 上面的代码在我看来不自然，因为我们修改了array里面的值let，是不是非得这样，或者有没有更自然的方法去做这个？
有人可以帮忙吗？非常感谢！
在 emacs 中，当我输入文件名的开头，然后按Tab进行自动完成时，这就是我得到的：
可能的完成有：
dummy.cmi dummy.cmx
dummy.ml dummy.o
我想让 emacs 忽略目标文件（.o、.cmx、.cmi）并直接用dummy.ml完成
有没有办法在 emacs 中指定该行为？某种类似于git 的.emacsignore 机制？
我如何引用 OCaml 的顶级 repl 中最后一个评估的表达式？
即 JavaScript 使用$_，python 使用_，haskell ghci 使用it。
我正在通过或多或少的方式下载某些目录的所有“.htm”文件：
wget http://some/url/ -r --accept="*.htm" -nv --show-progress
其中我关闭了 wget 的打印，但保留了对我有用的进度条 ( -nv --show-progress)
这很好用，但会为每个下载的文件输出一个进度条。它是一个可能有一个单一的，将考虑到所有文件的大小之和进度条？
我查看了该progress=TYPE选项，但这似乎只是设置了进度条的样式，而不是下载的数据总量
我对 OCaml 很陌生。我尝试在两台不同的计算机上从头开始安装它——都是 Linux Mint——并且两次都遇到了这个问题。
当我使用 opam 安装一个包（特别是 Base，但它也发生在 Core 中）时，OCaml 找不到它。
$ opam install Base
[NOTE] Package base is already installed (current version is v0.11.1).
$ ocaml -open Base
OCaml version 4.05.0
File "command line", line 1:
Error: Unbound module Base
ocaml 似乎在 /usr/lib/ocaml 中，它的二进制文件在 /usr/bin/ 中，而 opam 似乎把所有东西都放在 ~/.opam/packages 中。
如何让 OCaml 查看使用 opam 安装的软件包？我发现了许多涉及未绑定模块的问答错误，但似乎没有一个可以为我修复它，或者它们似乎已经过时。另外，我知道我的包管理器 OCaml 不是完全最新的，但是我也从源代码安装了 4.10.0 并且仍然有问题。