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 |