Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-02-12 20:40:05 -0800 (Sat, 12 Feb 2005)
Revision: 6665
Log message:

      Variables that have only lower or only upper bounds can be removed
      with all constraints that contain them.
      Constraints are stored in a hashtable now (instead of list).
      This allows to eliminate redundant constraints.
      At this moment itt_int_bench/test6 takes 100secs to prove,
      at least 90% of which is "ttca".
      

Changes  Path
+131 -58 metaprl/theories/itt/itt_omega.ml