tamarin-prover-theory- Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone



The constraint reduction rules, which are not enforced as invariants in Theory.Constraint.Solver.Reduction.

A goal represents a possible application of a rule that may result in multiple cases or even non-termination (if applied repeatedly). These goals are computed as the list of openGoals. See Theory.Constraint.Solver.ProofMethod for the public interface to solving goals and the implementation of heuristics.



data Usefulness Source



A goal that is likely to result in progress.


A goal that is delayed to avoid immediate termination.


A goal that is likely to be constructible by the adversary.


A message that is deducible for the current solution.

type AnnotatedGoal = (Goal, (Integer, Usefulness))Source

Goals annotated with their number and usefulness.

openGoals :: System -> [AnnotatedGoal]Source

The list of goals that must be solved before a solution can be extracted. Each goal is annotated with its age and an indicator for its usefulness.

solveGoal :: Goal -> Reduction StringSource

solveGoal rules goal enumerates all possible cases of how this goal could be solved in the context of the given rules. For each case, a sensible case-name is returned.