Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-10 10:58:03 -0800 (Wed, 10 Nov 2004)
Revision: 6258
Log message:

      My previous commit introduced a bug in SupInf which was causing "wrong" results in
      the inttestn. This commit fixes the problem.
      inttestn still can't be proved but this is alright because currently SupInf
      only makes one pass but full Shostak's SupInf does multi-pass.
      It might not be easy to implement multipass SupInf
      (not because of practical reasons but because of theoretical ones).
      Multipass version on n+1 pass takes the bounds [a;b] for variable v found on n-pass
      and replaces v with any integer from [a;b] then do SupInf again.
      Of course we can't do it in a tactic without proving it correct.
      what I'm going to do is instead of replacing v with some integer from [a;b]
      I'll add  ceiling(a) <= v <= floor(b).
      Though I'm not sure yet that this approach would give the same results as the original.
      

Changes	Path
+2 -2	metaprl/refiner/reflib/supinf.ml
+0 -0	metaprl/theories/itt/itt_supinf.ml