src/Provers/Arith/fast_lin_arith.ML
 changeset 15965 f422f8283491 parent 15922 7ef183f3fc98 child 16358 2e2a506553a3
```     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 09:35:05 2005 +0200
1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 10:29:15 2005 +0200
1.3 @@ -15,6 +15,8 @@
1.4
1.5  Only take premises and conclusions into account that are already (negated)
1.6  (in)equations. lin_arith_prover tries to prove or disprove the term.
1.7 +
1.8 +FIXME: convert to IntInf.int throughout.
1.9  *)
1.10
1.11  (* Debugging: set Fast_Arith.trace *)
1.12 @@ -189,15 +191,15 @@
1.13  val ratrelmax = foldr1 ratrelmax2;
1.14
1.15  fun ratroundup r = let val (p,q) = rep_rat r
1.16 -                   in if q=1 then r else rat_of_int((p div q) + 1) end
1.17 +                   in if q=1 then r else rat_of_intinf((p div q) + 1) end
1.18
1.19  fun ratrounddown r = let val (p,q) = rep_rat r
1.20 -                     in if q=1 then r else rat_of_int((p div q) - 1) end
1.21 +                     in if q=1 then r else rat_of_intinf((p div q) - 1) end
1.22
1.23  fun ratexact up (r,exact) =
1.24    if exact then r else
1.25    let val (p,q) = rep_rat r
1.26 -      val nth = ratinv(rat_of_int q)
1.27 +      val nth = ratinv(rat_of_intinf q)
1.28    in ratadd(r,if up then nth else ratneg nth) end;
1.29
1.30  fun ratmiddle(r,s) = ratmul(ratadd(r,s),ratinv(rat_of_int 2));
1.31 @@ -299,7 +301,7 @@
1.32
1.33  fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
1.34    let val c1 = el v l1 and c2 = el v l2
1.35 -      val m = lcm(abs c1,abs c2)
1.36 +      val m = IntInf.toInt (lcm(IntInf.fromInt (abs c1), IntInf.fromInt(abs c2)))
1.37        val m1 = m div (abs c1) and m2 = m div (abs c2)
1.38        val (n1,n2) =
1.39          if (c1 >= 0) = (c2 >= 0)
1.40 @@ -497,12 +499,15 @@
1.41
1.42  fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i;
1.43
1.44 -fun lcms is = Library.foldl lcm (1,is);
1.45 +fun lcms_intinf is = Library.foldl lcm (1, is);
1.46 +fun lcms is = IntInf.toInt (lcms_intinf (map IntInf.fromInt is));
1.47
1.48  fun integ(rlhs,r,rel,rrhs,s,d) =
1.49 -let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s
1.50 -    val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs))
1.51 -    fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end
1.52 +let val (rn,rd) = pairself IntInf.toInt (rep_rat r) and (sn,sd) = pairself IntInf.toInt (rep_rat s)
1.53 +    val m = IntInf.toInt (lcms_intinf(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)))
1.54 +    fun mult(t,r) =
1.55 +        let val (i,j) =  pairself IntInf.toInt (rep_rat r)
1.56 +        in (t,i * (m div j)) end
1.57  in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
1.58
1.59  fun mklineq n atoms =
1.60 @@ -533,9 +538,9 @@
1.61
1.62  fun print_atom((a,d),r) =
1.63    let val (p,q) = rep_rat r
1.64 -      val s = if d then string_of_int p else
1.65 +      val s = if d then IntInf.toString p else
1.66                if p = 0 then "0"
1.67 -              else string_of_int p ^ "/" ^ string_of_int q
1.68 +              else IntInf.toString p ^ "/" ^ IntInf.toString q
1.69    in a ^ " = " ^ s end;
1.70
1.71  fun print_ex sds =
```