mlrs: simple interface to mplrs(1) that is similar to lrs(1) and in addition does automatic checkpoint/restart for long runs. procs (if specified) is the number of processors to use (assigned according to the default-hostfile), otherwise all available processors on the current machine are used. cptime (if specified) is the time in seconds until a checkpoint/restart is made, default 86400 secs (1 day). Checkpoint data is written into a file named input-file.cpN, where N=0,1,2,... is assigned consecutively. cpindex (if specified) is a valid value of N and causes a restart from checkpoint file input-file.cpN. Other mplrs(1) command line parameters are default values.
plotV(requires gnuplot be installed): produces a PDF file named <lrs-output-file>V.pdf that gives a plot of each vertex or facet along with its height in the reverse search tree. lrs-output-file should be an lrs/mplrs output file produced when the printcobasis is included in the input file for the run.
plotR(requires gnuplot be installed): performs a similar task to plotV for cones producing the file <lrs-output-file>H.pdf where the height of each ray is plotted.
plotL(requires gnuplot be installed): plotL produces a realtime view of an mplrs run that uses the command line option "-hist <histogram-file>". If histogram-file is not specified hist is the assumed file name. A PDF file named <histogram-file>.pdf is produced. The first plot has 3 graphs showing the number of processors working, the size of the job queue L, and message requests pending, all versus elapsed time on the x-axis. The second histogram shows the size of the subtrees explored by producers. The root of the subtree is not counted in this size. Note that a producer stops after (possibly scaled) maxc nodes are explored, but in backtracking some additional leaves may be discovered. So the size of the largest subtree may be slightly larger than maxc.
projred(requires inedel, checkpred(1) and external SMT solver be installed): simple wrapper for checkpred(1) that tests and greedily removes inequalities that are redundant after a projection, without doing the projection. Repeatedly calls checkpred(1) and the specified SMT solver (z3 by default), removing inequalities determined to be redundant for the given projection. The output is produced in [output file] or on standard output if no output file is specified. The output file will produce the same projection as the original input. Inequalities and projection to test are given as options in the input file, see checkpred(1) for details.
User's guide for lrslib