The% time ./slfq examples/Ex5 -q -a "beta4 > 0 /\ nu > 0" 511000 beta4 - 60850 nu - 1217 > 0 316.020u 3.010s 10:43.80 49.5% 0+0k 0+0io 276pf+0w %
-aoption has been used to add the assumptions that
nuare both positive. Thus, the equivalent formula is really:
beta4 > 0 /\ nu > 0 /\ 60850 nu - 511000 beta4 + 1217 < 0In the original formula as I recieved it, the contents of examples/Ex5 were actually conjoined with
beta4 > 0 /\ nu > 0. The user, not the system, must recognize that such constraints are actually fundamental to the problem and should be made explicit assumptions. Without this assumption, SLFQ spends a lot of time trying to find a simple way of expressing sets in the plane that are outside of
beta4 > 0 /\ nu > 0, which is wasted effort.
-q option asks the program to run in a "quiet" mode,
where intermediate information is not printed out.