From: Marko Kääramees <Marko.K<aaramees@tt...>  20091116 16:47:18

Hi, I use Reduce and its package Redlog for simplifying the boolean combination of linear inequalities. I found that some quite obvious simplifications work only one way in the redlog. An example script load_package redlog; rlset pasf; c := (x = 1 or x >= 2) and (x = 6 or x <= 5); rlsimpl c; simplifies to x  1 >= 0 and (x  5 <= 0 or x  6 = 0) The first disjunction with >= is simplified, but the other with <= is not. Could somebody explain the reasons please or guide if it can be tuned somehow. I am working in the finite domains (bounded integers) and generate lots of combinations of linear inequalities automatically, which should be simplified and converted to a normal form to handle complexity. Although Redlog seems to do exactly what I need, it is not too difficult to get to the situation where the system eats up all the memory or does not seem to finish the computation any time soon. Redlog seems to be quite general tool accepting more complex arithmetics and formulas. Could anybody point to some other tool which seems to be more suitable for such tasks? Best regards, marko 