rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
why/why-num.patch
Jerry James 88002a4073 New upstream release. 
Add -num patch to fix incomplete num to zarith conversion.
2018-02-12 20:20:06 -07:00

596 lines
23 KiB
Diff
Raw Permalink Blame History

--- atp/cooper.ml.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/cooper.ml 2018-02-11 20:48:48.754907226 -0700
@@ -38,10 +38,10 @@
(* Lift operations up to numerals. *)
(* ------------------------------------------------------------------------- *)
-let mk_numeral n = Fn(string_of_num n,[]);;
+let mk_numeral n = Fn(Z.to_string n,[]);;
let dest_numeral =
- function (Fn(ns,[])) -> num_of_string ns
+ function (Fn(ns,[])) -> Z.of_string ns
| _ -> failwith "dest_numeral";;
let is_numeral = can dest_numeral;;
@@ -59,12 +59,12 @@ let numeral2 fn m n = mk_numeral(fn (des
(* ------------------------------------------------------------------------- *)
let rec linear_cmul n tm =
- if n =/ Int 0 then Fn("0",[]) else
+ if Z.equal n Z.zero then Fn("0",[]) else
match tm with
Fn("+",[Fn("*",[c1; x1]); rest]) ->
- Fn("+",[Fn("*",[numeral1 (( */ ) n) c1; x1]);
+ Fn("+",[Fn("*",[numeral1 (Z.mul n) c1; x1]);
linear_cmul n rest])
- | k -> numeral1 (( */ ) n) k;;
+ | k -> numeral1 (Z.mul n) k;;
let earlierv vars (Var x) (Var y) = earlier vars x y;;
@@ -73,7 +73,7 @@ let rec linear_add vars tm1 tm2 =
(Fn("+",[Fn("*",[c1; x1]); rest1]),
Fn("+",[Fn("*",[c2; x2]); rest2])) ->
if x1 = x2 then
- let c = numeral2 (+/) c1 c2 in
+ let c = numeral2 Z.add c1 c2 in
if c = Fn("0",[]) then linear_add vars rest1 rest2
else Fn("+",[Fn("*",[c; x1]); linear_add vars rest1 rest2])
else if earlierv vars x1 x2 then
@@ -84,9 +84,9 @@ let rec linear_add vars tm1 tm2 =
Fn("+",[Fn("*",[c1; x1]); linear_add vars rest1 tm2])
| (_,Fn("+",[Fn("*",[c2; x2]); rest2])) ->
Fn("+",[Fn("*",[c2; x2]); linear_add vars tm1 rest2])
- | _ -> numeral2 (+/) tm1 tm2;;
+ | _ -> numeral2 Z.add tm1 tm2;;
-let linear_neg tm = linear_cmul (Int(-1)) tm;;
+let linear_neg tm = linear_cmul Z.minus_one tm;;
let linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);;
@@ -116,7 +116,7 @@ let mkatom vars p t = Atom(R(p,[Fn("0",[
let linform vars fm =
match fm with
Atom(R("divides",[c;t])) ->
- let c' = mk_numeral(abs_num(dest_numeral c)) in
+ let c' = mk_numeral(Z.abs(dest_numeral c)) in
Atom(R("divides",[c';lint vars t]))
| Atom(R("=",[s;t])) -> mkatom vars "=" (Fn("-",[t;s]))
| Atom(R("<",[s;t])) -> mkatom vars "<" (Fn("-",[t;s]))
@@ -144,11 +144,11 @@ let rec posineq fm =
let rec formlcm x fm =
match fm with
Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
- abs_num(dest_numeral c)
+ Z.abs(dest_numeral c)
| Not(p) -> formlcm x p
| And(p,q) -> lcm_num (formlcm x p) (formlcm x q)
| Or(p,q) -> lcm_num (formlcm x p) (formlcm x q)
- | _ -> Int 1;;
+ | _ -> Z.one;;
(* ------------------------------------------------------------------------- *)
(* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *)
@@ -157,10 +157,10 @@ let rec formlcm x fm =
let rec adjustcoeff x l fm =
match fm with
Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
- let m = l // dest_numeral c in
- let n = if p = "<" then abs_num(m) else m in
- let xtm = Fn("*",[mk_numeral(m // n); x]) in
- Atom(R(p,[linear_cmul (abs_num m) d;
+ let m = Z.div l (dest_numeral c) in
+ let n = if p = "<" then Z.abs(m) else m in
+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
+ Atom(R(p,[linear_cmul (Z.abs m) d;
Fn("+",[xtm; linear_cmul n z])]))
| Not(p) -> Not(adjustcoeff x l p)
| And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
@@ -174,7 +174,7 @@ let rec adjustcoeff x l fm =
let unitycoeff x fm =
let l = formlcm x fm in
let fm' = adjustcoeff x l fm in
- if l =/ Int 1 then fm' else
+ if Z.equal l Z.one then fm' else
let xp = Fn("+",[Fn("*",[Fn("1",[]);x]); Fn("0",[])]) in
And(Atom(R("divides",[mk_numeral l; xp])),adjustcoeff x l fm);;
@@ -204,7 +204,7 @@ let rec divlcm x fm =
| Not(p) -> divlcm x p
| And(p,q) -> lcm_num (divlcm x p) (divlcm x q)
| Or(p,q) -> lcm_num (divlcm x p) (divlcm x q)
- | _ -> Int 1;;
+ | _ -> Z.one;;
(* ------------------------------------------------------------------------- *)
(* Construct the B-set. *)
@@ -242,8 +242,8 @@ let rec linrep vars x t fm =
(* ------------------------------------------------------------------------- *)
let operations =
- ["=",(=/); "<",(</); ">",(>/); "<=",(<=/); ">=",(>=/);
- "divides",(fun x y -> mod_num y x =/ Int 0)];;
+ ["=",(Z.equal); "<",(Z.lt); ">",(Z.gt); "<=",(Z.leq); ">=",(Z.geq);
+ "divides",(fun x y -> Z.equal (Z.rem y x) Z.zero)];;
let evalc_atom at =
match at with
@@ -265,7 +265,7 @@ let cooper vars fm =
let x = Var x0 in
let p = unitycoeff x p0 in
let p_inf = simplify(minusinf x p) and bs = bset x p
- and js = Int 1 --- divlcm x p in
+ and js = Z.one --- divlcm x p in
let p_element j b =
linrep vars x (linear_add vars b (mk_numeral j)) p in
let stage j = list_disj
--- atp/defcnf.ml.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/defcnf.ml 2018-02-11 14:00:03.159892859 -0700
@@ -55,7 +55,7 @@ let rec nenf fm =
(* Make a stylized variable and update the index. *)
(* ------------------------------------------------------------------------- *)
-let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;;
+let mkprop n = Atom(P("p_"^(Z.to_string n))),Z.succ n;;
(* ------------------------------------------------------------------------- *)
(* Make n large enough that "v_m" won't clash with s for any m >= n *)
@@ -67,7 +67,7 @@ let max_varindex pfx =
let l = String.length s in
if l <= m or String.sub s 0 m <> pfx then n else
let s' = String.sub s m (l - m) in
- if forall numeric (explode s') then max_num n (num_of_string s')
+ if forall numeric (explode s') then Z.max n (Z.of_string s')
else n;;
(* ------------------------------------------------------------------------- *)
@@ -90,7 +90,7 @@ and defstep op (p,q) (fm,defs,n) =
let defcnf fm =
let fm' = nenf(psimplify fm) in
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
let (fm'',defs,_) = maincnf (fm',undefined,n) in
let deflist = map (snd ** snd) (funset defs) in
let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in
@@ -130,7 +130,7 @@ let rec andcnf (fm,defs,n as trip) =
let defcnfs fm =
let fm' = nenf(psimplify fm) in
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
let (fm'',defs,_) = andcnf (fm',undefined,n) in
let deflist = map (snd ** snd) (funset defs) in
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
@@ -181,7 +181,7 @@ let rec andcnf pos (fm,defs,n as trip) =
let defcnfs imps fm =
let fm' = nenf(psimplify fm) in
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
let (fm'',defs,_) = andcnf imps (fm',undefined,n) in
let deflist = map (snd ** snd) (funset defs) in
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
@@ -209,7 +209,7 @@ let rec andcnf3 pos (fm,defs,n as trip)
let defcnf3s imps fm =
let fm' = nenf(psimplify fm) in
- let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+ let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in
let deflist = map (snd ** snd) (funset defs) in
setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
--- atp/fourier_motzkin.ml.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/fourier_motzkin.ml 2018-02-11 20:34:13.822886848 -0700
@@ -71,10 +71,10 @@ let rec posineq fm =
let rec adjustcoeff x l fm =
match fm with
Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
- let m = l // dest_numeral c in
- let n = if p = "<=" then abs_num(m) else m in
- let xtm = Fn("*",[mk_numeral(m // n); x]) in
- Atom(R(p,[linear_cmul (abs_num m) d;
+ let m = Z.div l (dest_numeral c) in
+ let n = if p = "<=" then Z.abs(m) else m in
+ let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
+ Atom(R(p,[linear_cmul (Z.abs m) d;
Fn("+",[xtm; linear_cmul n z])]))
| Not(p) -> Not(adjustcoeff x l p)
| And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
@@ -88,7 +88,7 @@ let rec adjustcoeff x l fm =
let unitycoeff x fm =
let l = formlcm x fm in
let fm' = adjustcoeff x l fm in
- if l =/ Int 1 then fm' else
+ if Z.equal l Z.one then fm' else
adjustcoeff x l fm;;
(* ------------------------------------------------------------------------- *)
@@ -98,10 +98,10 @@ let unitycoeff x fm =
let isolate x fm =
match fm with
Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
- let c = mk_numeral (Int 0 -/ dest_numeral c) in
+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
Atom(R(p,[Fn("*",[c;y]);z]))
| Atom(R(p,[zero;Fn("*",[c;y])])) when y = x ->
- let c = mk_numeral (Int 0 -/ dest_numeral c) in
+ let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
Atom(R(p,[Fn("*",[c;y]);zero]))
| _ ->
printer fm;
@@ -110,7 +110,7 @@ let isolate x fm =
let replace vars x t fm =
match fm with
Atom(R(p,[Fn("*",[c;y]);z])) when y = x ->
- let t = if dest_numeral c >/ Int 0 then t else linear_neg t in
+ let t = if Z.gt (dest_numeral c) Z.zero then t else linear_neg t in
linform vars (Atom(R(p,[t;z])))
| _ -> assert false
@@ -128,13 +128,13 @@ let fourier vars fm =
(function (Atom(R("=",_))) -> true | _ -> false) cjs in
let (Atom(R("=",[s;t]))) = eqn in
let (Fn("*",[c;_])) = s in
- let y = if dest_numeral c =/ Int 1 then t else linear_neg t in
+ let y = if Z.equal (dest_numeral c) Z.one then t else linear_neg t in
list_conj(map (replace vars x y) (subtract cjs [eqn]))
with Failure _ ->
let l,r =
partition
(fun (Atom(R("<=",[Fn("*",[c;_]);t]))) ->
- dest_numeral c =/ Int (-1)) cjs
+ Z.equal (dest_numeral c) Z.minus_one) cjs
in
let lefts = map (fun (Atom(R("<=",[_;l]))) -> linear_neg l) l
and rights = map (fun (Atom(R("<=",[_;r]))) -> r) r in
--- atp/lib.ml.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/lib.ml 2018-02-11 13:26:57.020559495 -0700
@@ -46,11 +46,9 @@ let ( ** ) = fun f g x -> f(g x);;
(* GCD and LCM on arbitrary-precision numbers. *)
(* ------------------------------------------------------------------------- *)
-let gcd_num n1 n2 =
- abs_num(num_of_big_int
- (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));;
+let gcd_num n1 n2 = Z.gcd n1 n2;;
-let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;;
+let lcm_num n1 n2 = Z.lcm n1 n2;;
(* ------------------------------------------------------------------------- *)
(* A useful idiom for "non contradictory" etc. *)
@@ -73,7 +71,7 @@ let can f x = try f x; true with Failure
let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
-let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);;
+let rec (---) = fun m n -> if Z.gt m n then [] else m::((Z.succ m) --- n);;
let rec map2 f l1 l2 =
match (l1,l2) with
@@ -596,4 +594,4 @@ let equated (Partition f) = dom f;;
(* First number starting at n for which p succeeds. *)
(* ------------------------------------------------------------------------- *)
-let rec first n p = if p(n) then n else first (n +/ Int 1) p;;
+let rec first n p = if p(n) then n else first (Z.succ n) p;;
--- atp/Makefile.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/Makefile 2018-02-11 13:14:15.311777144 -0700
@@ -8,6 +8,8 @@
# many.ml (Example relevant to many-sorted logic)
# hol.ml (Simple higher order logic setup)
+ZARITHLIB=$(shell ocamlfind query zarith)
+
#MLFILES = lib.ml intro.ml formulas.ml prop.ml propexamples.ml \
defcnf.ml dp.ml stal.ml bdd.ml fol.ml skolem.ml \
herbrand.ml unif.ml tableaux.ml resolution.ml prolog.ml \
@@ -33,9 +35,9 @@ compiled: example.ml atp.cmx; ocamlopt -
# Make the appropriate object for the main body of code
-atp.cmx: atp.ml; ocamlopt -w ax -c atp.ml
+atp.cmx: atp.ml; ocamlopt -I $(ZARITHLIB) -w ax -c atp.ml
-atp.cmo: atp.ml; ocamlc -w ax -c atp.ml
+atp.cmo: atp.ml; ocamlc -I $(ZARITHLIB) -w ax -c atp.ml
# Make the camlp4 quotation expander
--- atp/make.ml.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/make.ml 2018-02-11 14:37:48.178019612 -0700
@@ -44,10 +44,9 @@
Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; (* Up the stack size *)
Format.set_margin 72;; (* Reduce margins *)
open Format;; (* Open formatting *)
-open Num;; (* Open bignums *)
let imperative_assign = (:=);; (* Preserve this *)
-let print_num n = print_string(string_of_num n);; (* Avoid range limit *)
+let print_num n = print_string(Z.to_string n);; (* Avoid range limit *)
#install_printer print_num;; (* when printing nums *)
(* ------------------------------------------------------------------------- *)
--- atp/Mk_ml_file.orig 2018-01-23 03:07:35.000000000 -0700
+++ atp/Mk_ml_file 2018-02-10 22:01:01.925304810 -0700
@@ -1,4 +1,3 @@
-echo "open Num;;"
echo "open Format;;"
cat $@ | sed 's/START_INTERACTIVE;;/(\*/' | sed 's/END_INTERACTIVE;;/\*)/'
--- jc/jc_annot_inference.ml.orig 2018-02-10 16:03:04.338379961 -0700
+++ jc/jc_annot_inference.ml 2018-02-11 13:13:48.313855743 -0700
@@ -49,7 +49,6 @@ open Apron
open Coeff
open Interval
open Lincons1
-open Num
(*****************************************************************************)
@@ -1120,7 +1119,7 @@ let linearize t =
try match t#node with
| JCTconst c ->
begin match c with
- | JCCinteger s -> (TermMap.empty, num_of_string s)
+ | JCCinteger s -> (TermMap.empty, Z.of_string s)
| JCCboolean _ | JCCvoid | JCCnull | JCCreal _ | JCCstring _ ->
err ()
end
@@ -1133,7 +1132,7 @@ let linearize t =
(fun vt1 c1 acc ->
try
let c2 = TermMap.find vt1 coeffs2 in
- TermMap.add vt1 (c1 +/ c2) acc
+ TermMap.add vt1 (Z.add c1 c2) acc
with Not_found -> TermMap.add vt1 c1 acc
) coeffs1 TermMap.empty
in
@@ -1143,55 +1142,55 @@ let linearize t =
else TermMap.add vt2 c2 acc
) coeffs2 coeffs
in
- (coeffs, cst1 +/ cst2)
+ (coeffs, (Z.add cst1 cst2))
| `Bsub ->
let coeffs = TermMap.fold
(fun vt1 c1 acc ->
try
let c2 = TermMap.find vt1 coeffs2 in
- TermMap.add vt1 (c1 -/ c2) acc
+ TermMap.add vt1 (Z.sub c1 c2) acc
with Not_found -> TermMap.add vt1 c1 acc
) coeffs1 TermMap.empty
in
let coeffs = TermMap.fold
(fun vt2 c2 acc ->
if TermMap.mem vt2 coeffs then acc
- else TermMap.add vt2 (minus_num c2) acc
+ else TermMap.add vt2 (Z.neg c2) acc
) coeffs2 coeffs
in
- (coeffs, cst1 -/ cst2)
+ (coeffs, (Z.sub cst1 cst2))
| `Bmul when TermMap.is_empty coeffs1 || TermMap.is_empty coeffs2 ->
let coeffs =
if TermMap.is_empty coeffs1 then
- TermMap.map (fun c -> c */ cst1) coeffs2
+ TermMap.map (fun c -> Z.mul c cst1) coeffs2
else
- TermMap.map (fun c -> c */ cst2) coeffs1
+ TermMap.map (fun c -> Z.mul c cst2) coeffs1
in
- (coeffs, cst1 */ cst2)
+ (coeffs, (Z.mul cst1 cst2))
| `Bmul
| `Bdiv
| `Bmod -> err ()
end
| JCTbinary(t1,(#bitwise_op as bop,`Integer),t2) ->
let coeffs1, cst1 = aux t1 in
- if coeffs1 = TermMap.empty && cst1 =/ Int 0 then
+ if coeffs1 = TermMap.empty && Z.equal cst1 Z.zero then
match bop with
| `Bbw_and
| `Bshift_left
| `Blogical_shift_right
- | `Barith_shift_right -> TermMap.empty, Int 0
+ | `Barith_shift_right -> TermMap.empty, Z.zero
| `Bbw_or
| `Bbw_xor -> aux t2
| _ -> err ()
else
(* Consider non-linear term as abstract variable. *)
- (TermMap.add t (Int 1) TermMap.empty, Int 0)
+ (TermMap.add t Z.one TermMap.empty, Z.zero)
| JCTunary((uop,`Integer),t1) ->
let coeffs1,cst1 = aux t1 in
begin match uop with
| `Uminus ->
- let coeffs = TermMap.map (fun c -> minus_num c) coeffs1 in
- (coeffs, minus_num cst1)
+ let coeffs = TermMap.map (fun c -> Z.neg c) coeffs1 in
+ (coeffs, Z.neg cst1)
| _ -> err ()
end
| JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _
@@ -1201,13 +1200,16 @@ let linearize t =
| JCTrange _ | JCTif _ | JCTlet _ ->
err ()
with Failure "linearize" ->
- (TermMap.add t (Int 1) TermMap.empty, Int 0)
+ (TermMap.add t Z.one TermMap.empty, Z.zero)
in aux t
let linstr_of_term env t =
+(*
let mkmulstr = function
- | (_va, Int 0) -> ""
- | (va, c) -> string_of_num c ^ " * " ^ va
+ | (_va, Z.zero) -> ""
+ | (va, c) -> (Z.to_string c) ^ " * " ^ va
+*)
+ let mkmulstr = (fun (va,c) -> if Z.equal Z.zero c then "" else (Z.to_string c) ^ " * " ^ va)
in
let rec mkaddstr = function
| [] -> ""
@@ -1286,33 +1288,33 @@ let rec linstr_of_assertion env a =
in
let env,str,cst = linstr_of_term env subt in
if str = "" then
- let ncst = minus_num cst in
+ let ncst = Z.neg cst in
let is_true = match bop with
- | `Blt -> Int 0 </ ncst
- | `Bgt -> Int 0 >/ ncst
- | `Ble -> Int 0 <=/ ncst
- | `Bge -> Int 0 >=/ ncst
- | `Beq -> Int 0 =/ ncst
- | `Bneq -> Int 0 <>/ ncst
+ | `Blt -> Z.lt Z.zero ncst
+ | `Bgt -> Z.gt Z.zero ncst
+ | `Ble -> Z.leq Z.zero ncst
+ | `Bge -> Z.geq Z.zero ncst
+ | `Beq -> Z.equal Z.zero ncst
+ | `Bneq -> not (Z.equal Z.zero ncst)
in
env, if is_true then Dnf.true_ else Dnf.false_
else
- let cstr = string_of_num (minus_num cst) in
+ let cstr = Z.to_string (Z.neg cst) in
(* Do not use < and > with APRON, due to bugs in some versions.
Convert to equivalent non-strict. *)
let str = match bop with
| `Blt -> [[str ^ " <= " ^
- (string_of_num (pred_num (minus_num cst)))]]
+ (Z.to_string (Z.pred (Z.neg cst)))]]
| `Bgt -> [[str ^ " >= " ^
- (string_of_num (succ_num (minus_num cst)))]]
+ (Z.to_string (Z.succ (Z.neg cst)))]]
| `Ble -> [[str ^ " <= " ^ cstr]]
| `Bge -> [[str ^ " >= " ^ cstr]]
| `Beq -> [[str ^ " = " ^ cstr]]
| `Bneq ->
[[str ^ " <= " ^
- (string_of_num (pred_num (minus_num cst)))];
+ (Z.to_string (Z.pred (Z.neg cst)))];
[str ^ " >= " ^
- (string_of_num (succ_num (minus_num cst)))]]
+ (Z.to_string (Z.succ (Z.neg cst)))]]
in
env, str
| JCAnot a ->
@@ -1330,8 +1332,8 @@ let rec linstr_of_assertion env a =
let linstr_of_expr env e =
match Jc_effect.term_of_expr e with None -> None | Some t ->
let env,str,cst = linstr_of_term env t in
- if str = "" then Some (env, string_of_num cst)
- else Some (env, str ^ " + " ^ (string_of_num cst))
+ if str = "" then Some (env, Z.to_string cst)
+ else Some (env, str ^ " + " ^ (Z.to_string cst))
let offset_linstr_of_expr env ok e =
match e#node with
@@ -1340,15 +1342,15 @@ let offset_linstr_of_expr env ok e =
else
begin match Jc_effect.term_of_expr e with None -> None | Some t ->
let env,str,cst = linstr_of_term env t in
- if str = "" then Some (env,string_of_num cst)
- else Some (env,str ^ " + " ^ (string_of_num cst))
+ if str = "" then Some (env,Z.to_string cst)
+ else Some (env,str ^ " + " ^ (Z.to_string cst))
end
| _ ->
if is_nonnull_pointer_type e#typ then
match Jc_effect.term_of_expr e with None -> None | Some t ->
let env,str,cst = offset_linstr_of_term env ok t in
- if str = "" then Some (env,string_of_num cst)
- else Some (env,str ^ " + " ^ (string_of_num cst))
+ if str = "" then Some (env,Z.to_string cst)
+ else Some (env,str ^ " + " ^ (Z.to_string cst))
else None
@@ -1419,13 +1421,13 @@ let mkassertion lincons =
let rec linterms_of_term t =
let mkmulterm (t,c) =
- if c =/ Int 0 then None
- else if c =/ Int 1 then Some t
- else if c =/ Int (-1) then
+ if Z.equal c Z.zero then None
+ else if Z.equal c Z.one then Some t
+ else if Z.equal c Z.minus_one then
Some(new term ~typ:integer_type (JCTunary((`Uminus,`Integer),t)))
else
let c =
- new term ~typ:integer_type (JCTconst(JCCinteger(string_of_num c)))
+ new term ~typ:integer_type (JCTconst(JCCinteger(Z.to_string c)))
in
Some(new term ~typ:integer_type (JCTbinary(c,(`Bmul,`Integer),t)))
in
@@ -1443,30 +1445,30 @@ let rec linterms_of_term t =
let coeffs,cst = linearize t in
let posl,negl =
TermMap.fold (fun t c (pl,nl) ->
- if c >/ Int 0 then (t,c) :: pl, nl
- else if c </ Int 0 then pl, (t,minus_num c) :: nl
+ if Z.gt c Z.zero then (t,c) :: pl, nl
+ else if Z.lt c Z.zero then pl, (t,Z.neg c) :: nl
else pl, nl
) coeffs ([],[])
in
let cstt =
new term ~typ:integer_type
- (JCTconst(JCCinteger(string_of_num(abs_num cst))))
+ (JCTconst(JCCinteger(Z.to_string(Z.abs cst))))
in
let post = match mkaddterm posl with
| None ->
- if cst >/ Int 0 then cstt
+ if Z.gt cst Z.zero then cstt
else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
| Some t ->
- if cst >/ Int 0 then
+ if Z.gt cst Z.zero then
new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
else t
in
let negt = match mkaddterm negl with
| None ->
- if cst </ Int 0 then cstt
+ if Z.lt cst Z.zero then cstt
else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
| Some t ->
- if cst </ Int 0 then
+ if Z.lt cst Z.zero then
new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
else t
in
@@ -1518,8 +1520,8 @@ let mkconsistent a =
let posl,negl =
TermMap.fold
(fun t c (pl,nl) ->
- if c >/ Int 0 then t :: pl, nl
- else if c </ Int 0 then pl, t :: nl
+ if Z.gt c Z.zero then t :: pl, nl
+ else if Z.lt c Z.zero then pl, t :: nl
else pl, nl
) coeffs ([],[])
in
@@ -2497,10 +2499,10 @@ let collect_expr_targets e =
let collect_integer_overflow ei e1 =
match Jc_effect.term_of_expr e1 with None -> [] | Some t1 ->
let mint = new term ~typ:integer_type
- (JCTconst (JCCinteger (Num.string_of_num ei.jc_enum_info_min)))
+ (JCTconst (JCCinteger (Z.to_string ei.jc_enum_info_min)))
in
let maxt = new term ~typ:integer_type
- (JCTconst(JCCinteger (Num.string_of_num ei.jc_enum_info_max)))
+ (JCTconst(JCCinteger (Z.to_string ei.jc_enum_info_max)))
in
let mina = new assertion (JCArelation (mint, (`Ble,`Integer), t1)) in
let maxa = new assertion (JCArelation (t1, (`Ble,`Integer), maxt)) in
Reference in a new issue View git blame Copy permalink