From 77c3f1fb822035ef4de04685cabcaa4da3f0a456 Mon Sep 17 00:00:00 2001 From: Nicola Mometto Date: Mon, 14 Oct 2019 17:18:24 +0100 Subject: [PATCH] fix ocaml build by moving to Zarith methods --- src/api/ml/z3.ml | 4 ++-- src/api/ml/z3.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index b4e35c6b3..47dd487ee 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1039,7 +1039,7 @@ struct let get_big_int (x:expr) = if is_int_numeral x then let s = (Z3native.get_numeral_string (Expr.gc x) x) in - Big_int.big_int_of_string s + Z.of_string s else raise (Error "Conversion failed.") @@ -1063,7 +1063,7 @@ struct let get_ratio x = if is_rat_numeral x then let s = Z3native.get_numeral_string (Expr.gc x) x in - Ratio.ratio_of_string s + Q.of_string s else raise (Error "Conversion failed.") diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 678f99443..6c367f10c 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1159,7 +1159,7 @@ sig val mk_sort : context -> Sort.sort (** Get a big_int from an integer numeral *) - val get_big_int : Expr.expr -> Big_int.big_int + val get_big_int : Expr.expr -> Z.t (** Returns a string representation of a numeral. *) val numeral_to_string : Expr.expr -> string @@ -1217,7 +1217,7 @@ sig val get_denominator : Expr.expr -> Expr.expr (** Get a ratio from a real numeral *) - val get_ratio : Expr.expr -> Ratio.ratio + val get_ratio : Expr.expr -> Q.t (** Returns a string representation in decimal notation. The result has at most as many decimal places as indicated by the int argument.*)