# lrs-checkpred - Man Page

### Name

checkpred - utility to create and verify logical formulas for determining whether a given inequality is redundant after eliminating variables, without eliminating the variables.

### Synopsis

**checkpred** *[input-file]*

### Description

The input file is a list of inequalities defining a polyhedron P in *lrs* format along with a list of variables for a projection of P and an inequality I to test. The question is whether we have the same projection when I is deleted from P. If so we say I is redundant for the projection, otherwise it is non-redundant. *checkpred* is a utility for determining this without performing the projection. It produces logical formulas in *SMT-LIB* 2.6 format that are satisfiable iff the I is non-redundant for the projection. In addition, *checkpred* can produce *lrs* inputs that verify witnesses of non-redundancy produced by an SMT solver.

### File formats

The input file is in *lrs* format (see lrs(1)**)** consisting of (a) an H-representation of a polyhedron, (b) a projection to a subset of variables given by the *project* or *eliminate* options, and (c) an inequality to test given by the *redund* or *redund_list* options. Note that only "linearity", "redund", "redund_list", "project" and "eliminate" options are supported, and the combination of redund/redund_list and project/eliminate options is both unique to checkpred and required.

The output is in *SMT-LIB* 2.6 format using logic *LRA*. Solvers such as *z3* or *cvc4* support this logic. See The SMT-LIB Standard: Version 2.6 for details.

### Options

**checkpred** [input-file] produces a logical formula satisfiable iff the first inequality given in a redund/redund_list option is redundant after projection according to a project/eliminate option. The solver can produce witnesses for non-redundant inequalities, i.e. an assignment to the variables whose image is in the projection only if the inequality is removed. No witness is produced if the inequality is redundant.

A witness of non-redundancy can be verified using two certificates. The first certificate specifies that the assignment to the variables is feasible when the inequality in question is removed. The second certificate asserts that when this inequality is added, no feasible assignment has the same projection. Certificates are produced using the following options.

**checkpred** -c 1 [input-file] reads a witness of non-redundancy on standard input and produces an lrs input file that should be feasible. The options in the input file should be the same as when the formula was produced.

**checkpred** -c 2 [input-file] reads a witness of non-redundancy on standard input and produces an lrs input file that should be infeasible. The options in the input file should be the same as when the formula was produced.

### Examples

(1) Check if the first inequality in cp4.ine is redundant for projections.

(a) To check for redunancy after the first variable is eliminated, add options "redund_list 1 1" and "eliminate 1 1" to cp4.ine. Then:

% checkpred cp4.ine > cp4-11.smt

% z3 cp4-11.smt > cp4-11.out

or

% cvc4 -L smt --produce-models cp4-11.smt > cp4-11.out

The first line of cp4-11.out reads "sat" indicating that inequality 1 is non-redundant for eliminating variable 1. We can check the witness:

% checkpred -c 1 cp4.ine < cp4-11.out | lrs

% checkpred -c 2 cp4.ine < cp4-11.out | lrs

The first certificate is feasible and second infeasible, so the witness proves non-redundancy for the projection.

(b) To check for redunancy after variables 1 and 2 are eliminated, add options "redund_list 1 1" and "eliminate 2 1 2" to cp4.ine. Then

% checkpred cp4.ine > cp4-112.smt

% z3 cp4-112.smt > cp4-112.out

or

% cvc4 -L smt --produce-models cp4-112.smt > cp4-112.out

The first line of cp4-112.out reads "unsat" indicating that inequality 1 is redundant for eliminating variables 1 and 2. In this case there is no witness.

### Notes

### Author

Charles Jordan <skip at res dot otaru-uc dot ac dot jp >