LPPaver.Decide.Algorithm

Module defining algorithms that can decide DNFs of ESafe terms.

Documentation

setupBestFirstCheckDNF

Arguments

:: [(ESafe, BoxFun)]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> TypedVarMap

The area over which we are checking the conjunction.

-> Integer

The maximum number of boxes that should be examined before giving up.

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method. 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> (Maybe Bool, Maybe TypedVarMap)

The return result. (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area. (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area. (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

Start initial call to decideConjunctionBestFirst for some conjunction in a DNF.

checkEDNFDepthFirstWithSimplex

Arguments

:: [[ESafe]]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> TypedVarMap

The area over which we are checking the conjunction.

-> Integer

The maximum depth that we can reach before giving up.

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method. 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> (Maybe Bool, Maybe TypedVarMap)

The return result. (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area. (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area. (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

Check a DNF of ESafe terms using a depth-first branch-and-prune algorithm which tends to perform well when the problem is unsatisfiable.

checkEDNFBestFirstWithSimplexCE

Arguments

:: [[ESafe]]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> TypedVarMap

The area over which we are checking the conjunction.

-> Integer

The maximum number of boxes that should be examined before giving up.

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method. 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> (Maybe Bool, Maybe TypedVarMap)

The return result. (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area. (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area. (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

Check a DNF of ESafe terms using a best-first branch-and-prune algorithm which tends to perform well when the problem is satisfiable.

decideConjunctionWithApply

Arguments

:: [(ESafe, BoxFun)]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> Box

-> Maybe Bool

Attempt to decide a conjunction over some given box using basic interval evaluation via apply

decideConjunctionBestFirst

Arguments

:: MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)

The priority queue. Maximal minimals are represented using CN MPBall. Each element in the queue is a triple. The first item is a pair where fst is an ESafe representation of the term and the snd is a BoxFun equivalent of the same term. The second item is the area over which the previous conjunction should be examined. The third item is a boolean used to determine from which extreme corner to linearise the conjunction.

-> Integer

The number of boxes that have been examined.

-> Integer

The maximum number of boxes that should be examined before giving up.

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> (Maybe Bool, Maybe TypedVarMap)

The return result. (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area. (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area. (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

Decide a conjunction in a best-first manner using a priority queue. Maximal minimums over conjunctions are used to order them, with larger maximal minimums taking priority.

decideConjunctionDepthFirstWithSimplex

Arguments

:: [(ESafe, BoxFun)]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> TypedVarMap

The initial area over which the box is being examined. This remains unchanged during recursive calls to this function.

-> TypedVarMap

The current area over which the box is being examined.

-> Integer

The current depth.

-> Integer

The maximum allowed depth before giving up

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method. 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> (Maybe Bool, Maybe TypedVarMap)

The return result. (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area. (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area. (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

Decide a conjunction arising from a DNF over a given box using a depth-first branch-and-prune algorithm which tends to work well when the problem is unsatisfiable.

decideConjunctionWithSimplexCE

Arguments

:: [(ESafe, BoxFun)]

Each item is a term in the conjunction. The first item of each pair is the ESafe representation of the term and the second item is a BoxFun equivalent of the same term.

-> TypedVarMap

The initial area over which the box is being examined. This remains unchanged during recursive calls to this function.

-> TypedVarMap

The current area over which the box is being examined.

-> Rational

A rational number used as a heuristic to determine when to recurse when pruning with the simplex method. 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%

-> Precision

Precision used for MPBalls. prec 100 is the recommended default.

-> Bool

A boolean used to determine the extreme corner to linearise the conjunction from.

-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)

The return result For the first item, Nothing means the algorithm could not decide, Just False means unsatisfiable and Just True means satisfiable. The second item gives a counter-example/indeterminate area if appropriate. The third item is a filtered conjunction: terms which interval evaluate to true are filtered out. A boolean specifying the last corner from which the conjunction was linearised.

Decide a conjunction arising from a DNF over a given box using a best-first branch-and-prune algorithm which tends to work well when the problem is satisfiable.