1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
module E = Dolmen.Std.Expr
module B = Dolmen.Std.Builtin
let rec all_equals = function
| [] | [_] -> Bool.mk true
| x :: ((y :: _) as r) ->
if Value.compare x y = 0 then all_equals r else Bool.mk false
let rec distinct = function
| [] | [_] -> Bool.mk true
| x :: r ->
if List.for_all (fun y -> Value.compare x y <> 0) r
then distinct r else Bool.mk false
let builtins _ (cst : E.Term.Const.t) =
match cst.builtin with
| B.Equal -> Some (Fun.fun_n ~cst all_equals)
| B.Distinct -> Some (Fun.fun_n ~cst distinct)
| B.Ite ->
Some (Fun.fun_lazy ~cst (fun env eval args ->
match args with
| [cond; then_; else_] ->
if Value.extract_exn ~ops:Bool.ops (eval env cond)
then eval env then_
else eval env else_
| _ -> assert false
))
| _ -> None