LPPaver.Decide.Linearisation

Module defining linearisations for conjunctions of ESafe terms.

Documentation

removeConjunctionUnsatAreaWithSimplex

Arguments

:: [(CN MPBall, CN MPBall, Box)]

A list of values needed to linearise each term in the conjunction. In each triple, the first item is the value of the term from the extreme left corner of a VarMap, the second item is the value of the term from the extreme right corner of a VarMap, and the third item are partial derivatives of the term over a VarMap.

-> VarMap

The VarMap over which we are examining the conjunction.

-> (Maybe Bool, Maybe VarMap)

The result of the simplex method on the resulting linear system. (Just False, Nothing) is returned if the system is infeasible. (Nothing, Just newArea) is returned if the system is feasible: newArea is an optimisation of the given VarMap.

Remove unsat areas from a conjunction arising from a DNF by weakening the conjunction using createConstraintsToRemoveConjunctionUnsatArea. The resulting linear system is solved and optimised by the two-phase simplex method. If the linear system is infeasible, the entire conjunction was unsatisfiable.

findConjunctionSatAreaWithSimplex

Arguments

:: [(CN MPBall, CN MPBall, Box)]

A list of values needed to linearise each term in the conjunction. In each triple, the first item is the value of the term from the extreme left corner of a VarMap, the second item is the value of the term from the extreme right corner of a VarMap, and the third item are partial derivatives of the term over a VarMap.

-> VarMap

The VarMap over which we are examining the conjunction.

-> Bool

A boolean used to determine which extreme corner to strengthen the conjunction from. If true, linearise from the extreme left corner and vice versa.

-> Maybe VarMap

The result. If this is Nothing, no satisfiable point was found.

Find a satisfiable point from a conjunction arising from a DNF by strengthening the conjunction using createConstraintsToFindSatSolution. The resulting linear system is solved by the first phase of the two-phase simplex method.

createConstraintsToRemoveConjunctionUnsatArea

Arguments

:: [(CN MPBall, CN MPBall, Box)]

A list of values needed to linearise each term in the conjunction. In each triple, the first item is the value of the term from the extreme left corner of a VarMap, the second item is the value of the term from the extreme right corner of a VarMap, and the third item are partial derivatives of the term over a VarMap.

-> VarMap

The VarMap over which we are examining the conjunction.

-> [Constraint]

An implicit linear system that is a weakening of the conjunction.

Linearisations that weaken a conjunction of terms over some box.

createConstraintsToFindSatSolution

Arguments

:: [(CN MPBall, CN MPBall, Box)]

A list of values needed to linearise each term in the conjunction. In each triple, the first item is the value of the term from the extreme left corner of a VarMap, the second item is the value of the term from the extreme right corner of a VarMap, and the third item are partial derivatives of the term over a VarMap.

-> VarMap

The VarMap over which we are examining the conjunction.

-> Bool

A boolean used to determine which extreme corner to strengthen the conjunction from. If true, linearise from the extreme left corner and vice versa.

-> [Constraint]

An implicit linear system that is a weakening of the conjunction.

Linearisations that strengthen a conjunction of terms over some box.