| Portability | GHC only |
|---|---|
| Maintainer | Simon Meier <iridcode@gmail.com> |
| Safe Haskell | None |
Theory.Constraint.Solver.ProofMethod
Contents
Description
Proof methods and heuristics: the external small-step interface to the constraint solver.
- type CaseName = String
- data ProofMethod
- execProofMethod :: ProofContext -> ProofMethod -> System -> Maybe (Map CaseName System)
- data GoalRanking
- goalRankingName :: GoalRanking -> String
- rankProofMethods :: GoalRanking -> ProofContext -> System -> [(ProofMethod, (Map CaseName System, String))]
- data Heuristic
- roundRobinHeuristic :: [GoalRanking] -> Heuristic
- useHeuristic :: Heuristic -> Int -> GoalRanking
- prettyProofMethod :: HighlightDocument d => ProofMethod -> d
Proof methods
data ProofMethod Source
Sound transformations of sequents.
Constructors
| Sorry (Maybe String) | Proof was not completed |
| Solved | An attack was fond |
| Simplify | A simplification step. |
| SolveGoal Goal | A goal that was solved. |
| Contradiction (Maybe Contradiction) | A contradiction could be derived, possibly with a reason. |
| Induction | Use inductive strengthening on the single formula constraint in the system. |
execProofMethod :: ProofContext -> ProofMethod -> System -> Maybe (Map CaseName System)Source
Heuristics
data GoalRanking Source
The different available functions to rank goals with respect to their order of solving in a constraint system.
Constructors
| GoalNrRanking | |
| UsefulGoalNrRanking | |
| SmartRanking Bool |
goalRankingName :: GoalRanking -> StringSource
The name/explanation of a GoalRanking.
rankProofMethods :: GoalRanking -> ProofContext -> System -> [(ProofMethod, (Map CaseName System, String))]Source
Use a GoalRanking to generate the ranked, list of possible
ProofMethods and their corresponding results in this ProofContext and
for this System. If the resulting list is empty, then the constraint
system is solved.
roundRobinHeuristic :: [GoalRanking] -> HeuristicSource
Smart constructor for heuristics. Schedules the goal rankings in a round-robin fashion dependent on the proof depth.
useHeuristic :: Heuristic -> Int -> GoalRankingSource
Use a heuristic to schedule a GoalRanking according to the given
proof-depth.
Pretty Printing
prettyProofMethod :: HighlightDocument d => ProofMethod -> dSource
Pretty-print a proof method.