mirror of
https://github.com/Z3Prover/z3
synced 2025-10-26 17:29:21 +00:00
use fold_left instead of filteri because it is not available on old
OCaml versions
This commit is contained in:
parent
b1b61c9d57
commit
2c89a49ba8
1 changed files with 8 additions and 1 deletions
|
|
@ -2086,7 +2086,14 @@ struct
|
||||||
|
|
||||||
let mk_roots (ctx:context) (a:rcf_num list) =
|
let mk_roots (ctx:context) (a:rcf_num list) =
|
||||||
let n, r = Z3native.rcf_mk_roots ctx (List.length a) a in
|
let n, r = Z3native.rcf_mk_roots ctx (List.length a) a in
|
||||||
List.filteri (fun i _v -> i < n) r
|
let _i, l =
|
||||||
|
(* keep only the first `n` elements of the list `r` *)
|
||||||
|
List.fold_left (fun (i, acc) x ->
|
||||||
|
if i = 0 then i, acc
|
||||||
|
else (i - 1, x :: acc)
|
||||||
|
) (n, []) r
|
||||||
|
in
|
||||||
|
List.rev l
|
||||||
|
|
||||||
let add (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_add ctx a b
|
let add (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_add ctx a b
|
||||||
let sub (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_sub ctx a b
|
let sub (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_sub ctx a b
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue