Ошибка при использовании модуля Z3 в OCaml

Question

Я новичок в OCaml. Я установил модуль Z3, как указано в этом link

Я звоню Z3 с помощью команды:

ocamlc -custom -o ml_example.byte -I ~/Downloads/z3-unstable/build/api/ml -cclib "-L ~/Downloads/z3-unstable/build/ -lz3" nums.cma z3ml.cma $1 

где $ 1 заменяется на имя файла.

type loc = int 

type var = string 

type exp = 
| Mul of int * exp 
| Add of exp * exp 
| Sub of exp * exp 
| Const of int 
| Var of var 

type formula = 
    | Eq of exp * exp 
    | Geq of exp 
    | Gt of exp 

type stmt = 
    | Assign of var * exp 
    | Assume of formula 

    type transition = loc * stmt * loc 

module OrdVar = 
struct 
    type t = var 
    let compare = Pervasives.compare 
end 
module VarSets = Set.Make(OrdVar) 

type vars = VarSets.t 

module OrdTrans = 
struct 
    type t = transition 
    let compare = Pervasives.compare 
end 
module TransitionSets = Set.Make(OrdTrans) 

type transitionSet = TransitionSets.t 

type program = vars * loc * transitionSet * loc 

let ex1() : program = 
    let vset = VarSets.empty in 
    let vset = VarSets.add "x" vset in 
    let vset = VarSets.add "y" vset in 
    let vset = VarSets.add "z" vset in 
    let ts = TransitionSets.empty in 
    (* 0 X' = X + 1 *) 
    let stmt1 = Assign("x", Add(Var("x"), Const(1))) in 
    let tr1 = (0,stmt1,1) in 
    let ts = TransitionSets.add tr1 ts in 
    (vset,0,ts,10) 

В приведенном выше коде я определяю некоторые типы. Теперь, если я включаю команду «открыть Z3», я получаю сообщение «Ошибка: Unbound module Set.Make».

Я могу запустить тестовый код, который использует Z3-модуль без каких-либо трудностей, но не может работать с указанным выше кодом.

Answer 1

Сообщение об ошибке в этом случае немного запутанно. Проблема в том, что Z3 также предоставляет модуль под названием Set, который не имеет функции make. Это можно преодолеть, просто не импортируя все из Z3, так как есть ряд модуллов, которые могут столкнуться с другими. Например,

open Z3.Expr 
open Z3.Boolean 

будет работать нормально и открывает только Z3.Expr и Z3.Boolean модулей, но не Z3.Set модуля. так что мы можем написать пример функции:

let myfun (ctx:Z3.context) (args:expr list) = 
    mk_and ctx args 

Если Z3.Boolean не открыт, мы должны были бы написать Z3.Boolean.mk_and вместо этого, а так же мы все еще можем получить доступ к Set функций модуля Z3 в предваряя их Z3.Set.