diff options
| author | Alasdair Armstrong | 2017-12-13 18:48:39 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-12-13 18:48:39 +0000 |
| commit | b37a6de931c71a3d1136fee74885b5864c24c5c9 (patch) | |
| tree | 23d156248a51ca9d2e194ea03a10ac821e477859 /src/constraint.ml | |
| parent | 69fd2187cf4a09bb0954d481c6ce8fb3b5863ab8 (diff) | |
Use big_nums from Lem
Diffstat (limited to 'src/constraint.ml')
| -rw-r--r-- | src/constraint.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 3d5a3689..ae72d956 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Big_int +module Big_int = Nat_big_num open Util (* ===== Integer Constraints ===== *) @@ -58,13 +58,13 @@ type nexp_op = string type nexp = | NFun of (nexp_op * nexp list) | N2n of nexp - | NConstant of big_int + | NConstant of Big_int.num | NVar of int -let big_int_op : nexp_op -> (big_int -> big_int -> big_int) option = function - | "+" -> Some add_big_int - | "-" -> Some sub_big_int - | "*" -> Some mult_big_int +let big_int_op : nexp_op -> (Big_int.num -> Big_int.num -> Big_int.num) option = function + | "+" -> Some Big_int.add + | "-" -> Some Big_int.sub + | "*" -> Some Big_int.mul | _ -> None let rec arith constr = @@ -80,7 +80,7 @@ let rec arith constr = | Some op -> NConstant (op x y) | None -> c end - | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x) + | N2n (NConstant x) -> NConstant (Big_int.pow_int_positive 2 (Big_int.to_int x)) | c -> c (* ===== Boolean Constraints ===== *) @@ -157,7 +157,7 @@ let cop_sexpr op x y = let rec sexpr_of_nexp = function | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs) | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x] - | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *) + | NConstant c -> Atom (Big_int.to_string c) (* CHECK: do we do negative constants right? *) | NVar var -> Atom ("v" ^ string_of_int var) let rec sexpr_of_constraint = function @@ -303,6 +303,6 @@ let mult x y : nexp = NFun ("*", [x; y]) let app f xs : nexp = NFun (f, xs) -let constant (x : big_int) : nexp = NConstant x +let constant (x : Big_int.num) : nexp = NConstant x let variable (v : int) : nexp = NVar v |