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

Portability GHC only Benedikt Schmidt None

Theory.Tools.EquationStore

Description

Support for reasoning with and about disjunctions of substitutions.

Synopsis

# Equations

newtype SplitId Source

Index of disjunction in equation store

Constructors

 SplitId FieldsunSplitId :: Integer

Instances

 Enum SplitId Eq SplitId Ord SplitId Show SplitId Binary SplitId NFData SplitId Apply SplitId HasFrees SplitId

data EqStore Source

Constructors

 EqStore Fields_eqsSubst :: LNSubst _eqsConj :: Conj (SplitId, Set LNSubstVFresh) _eqsNextSplitId :: SplitId

Instances

 Eq EqStore Ord EqStore Show EqStore Binary EqStore NFData EqStore HasFrees EqStore

`emptyEqStore` is the empty equation store.

eqsSubst :: forall arr. Arrow arr => Lens arr EqStore LNSubstSource

eqsConj :: forall arr. Arrow arr => Lens arr EqStore (Conj (SplitId, Set LNSubstVFresh))Source

## Equalitiy constraint conjunctions

The false conjunction. It is always identified with split number -1.

## Queries

`True` iff the `EqStore` is contradictory.

addEqs :: MonadFresh m => MaudeHandle -> [Equal LNTerm] -> EqStore -> m (EqStore, Maybe SplitId)Source

Add a list of term equalities to the equation store. Returns the split identifier of the disjunction in resulting equation store.

Add a disjunction to the equation store at the beginning

## Case splitting

`performSplit eqs i` performs a case-split on the first disjunction with the given `SplitId`.

splits :: EqStore -> [SplitId]Source

Returns the list of all `SplitId`s valid for the given equation store sorted by the size of the disjunctions.

Returns the number of cases for a given `SplitId`.

Returns `True` if the `SplitId` is valid.

# Simplification

simp :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> EqStore -> m EqStoreSource

`simp eqStore` simplifies the equation store.

simpDisjunction :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> Disj LNSubstVFresh -> m (LNSubst, Maybe [LNSubstVFresh])Source

Simplify given disjunction via EqStore simplification. Obtains fresh names for variables from the underlying `MonadFresh`.

## Pretty printing

Pretty print an `EqStore`.