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 =