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

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

Theory.Constraint.Solver.Simplify

Description

This module implements all rules that do not result in case distinctions and equation solving. Some additional cases may although result from splitting over multiple AC-unifiers. Note that a few of these rules are implemented directly in the methods for inserting constraints to the constraint system. These methods are provided by Theory.Constraint.Solver.Reduction.

Synopsis

Documentation

simplifySystem :: Reduction ()Source

Apply CR-rules that don't result in case splitting until the constraint system does not change anymore.