Copyright | (c) Junaid Rasheed 2021-2022 |
---|---|
License | MPL |
Maintainer | jrasheed178@gmail.com |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Module defining algorithms that can decide DNFs of ESafe
terms.
Synopsis
- setupBestFirstCheckDNF :: [(ESafe, BoxFun)] -> TypedVarMap -> Integer -> Rational -> Precision -> (Maybe Bool, Maybe TypedVarMap)
- checkEDNFDepthFirstWithSimplex :: [[ESafe]] -> TypedVarMap -> Integer -> Rational -> Precision -> (Maybe Bool, Maybe TypedVarMap)
- checkEDNFBestFirstWithSimplexCE :: [[ESafe]] -> TypedVarMap -> Integer -> Rational -> Precision -> (Maybe Bool, Maybe TypedVarMap)
- decideConjunctionWithApply :: [(ESafe, BoxFun)] -> Box -> Maybe Bool
- decideConjunctionBestFirst :: MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool) -> Integer -> Integer -> Rational -> Precision -> (Maybe Bool, Maybe TypedVarMap)
- decideConjunctionDepthFirstWithSimplex :: [(ESafe, BoxFun)] -> TypedVarMap -> TypedVarMap -> Integer -> Integer -> Rational -> Precision -> (Maybe Bool, Maybe TypedVarMap)
- decideConjunctionWithSimplexCE :: [(ESafe, BoxFun)] -> TypedVarMap -> TypedVarMap -> Rational -> Precision -> Bool -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
Documentation
setupBestFirstCheckDNF Source #
:: [(ESafe, BoxFun)] | Each item is a term in the conjunction.
The first item of each pair is the |
-> 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 |
|
-> (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 Source #
:: [[ESafe]] | Each item is a term in the conjunction.
The first item of each pair is the |
-> 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 |
|
-> (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 Source #
:: [[ESafe]] | Each item is a term in the conjunction.
The first item of each pair is the |
-> 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 |
|
-> (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 Source #
:: [(ESafe, BoxFun)] | Each item is a term in the conjunction.
The first item of each pair is the |
-> Box | |
-> Maybe Bool |
Attempt to decide a conjunction over some given box using basic interval evaluation via apply
decideConjunctionBestFirst Source #
:: 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 |
-> 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 |
|
-> (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 Source #
:: [(ESafe, BoxFun)] | Each item is a term in the conjunction.
The first item of each pair is the |
-> 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 |
|
-> (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 Source #
:: [(ESafe, BoxFun)] | Each item is a term in the conjunction.
The first item of each pair is the |
-> 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 |
|
-> Bool | A boolean used to determine the |
-> (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.