Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-02-13 14:18:44 -0800 (Sun, 13 Feb 2005)
Revision: 6669
Log message:

      Certain conditions (like <>) doubles number of problems omega
      has to be applied to. We want to normalize polynoms before
      these problems multiply but we don't know which constraints
      will actually be useful.
      That's why omega is launched twice per constraint set now:
      first time to establish which hypotheses are actually used
      second time (after all constraints are converted to >=) to construct
      proofs.
      time in itt_int_bench/test6 dropped to 2 seconds
      total time in itt_int_bench dropped to 20 seconds
      itt_int_test is only 3 seconds (vs 2 seconds using arithT).
      

Changes	Path
+13 -5	metaprl/theories/itt/itt_int_arith.ml
+142 -4	metaprl/theories/itt/itt_omega.ml