Term.Unification

AC unification based on maude and free unification.

Unification modulo AC

unifyLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude [SubstVFresh c LVar]

unifyLNTerm eqs returns a complete set of unifiers for eqs modulo AC.

unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]

unifyLNTerm eqs returns a complete set of unifiers for eqs modulo AC.

unifiableLNTerms :: LNTerm -> LNTerm -> WithMaude Bool

True iff the terms are unifiable.

unifyLTermFactored :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude (LSubst c, [SubstVFresh c LVar])

unifyLTerm sortOf eqs returns a complete set of unifiers for eqs modulo AC.

unifyLNTermFactored :: [Equal LNTerm] -> WithMaude (LNSubst, [SubstVFresh Name LVar])

unifyLTerm sortOf eqs returns a complete set of unifiers for eqs modulo AC.

matching modulo AC

Constructing matching problems

matchLVar :: LVar -> LVar -> Match (LTerm c)

Match an LVar term to an LVar pattern.

Solving matching problems

solveMatchLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> Match (LTerm c) -> WithMaude [Subst c LVar]

solveMatchLNTerm sortOf eqs returns a complete set of matchers for eqs modulo AC.

solveMatchLNTerm :: Match LNTerm -> WithMaude [Subst Name LVar]

solveMatchLNTerm eqs returns a complete set of matchers for eqs modulo AC.

Handles to a Maude process

data MaudeHandle

A handle to a Maude process. It requires the Maude path for Signatures to be serializable. If we also add the string for the Maude config file, then it would even be serializable on its own.

type WithMaude = Reader MaudeHandle

Values that depend on a MaudeHandle.

startMaude :: FilePath -> MaudeSig -> IO MaudeHandle

startMaude starts a new instance of Maude and returns a Handle to it.

getMaudeStats :: MaudeHandle -> IO String

getMaudeStats returns the maude stats formatted as a string.

mhMaudeSig :: MaudeHandle -> MaudeSig

mhFilePath :: MaudeHandle -> FilePath

Maude signatures

data MaudeSig

The required information to define a Maude functional module.

Instances

Eq MaudeSig

Ord MaudeSig

Show MaudeSig

Monoid MaudeSig

A monoid instance to combine maude signatures.

Binary MaudeSig

NFData MaudeSig

enableDH :: MaudeSig -> Bool

enableBP :: MaudeSig -> Bool

enableMSet :: MaudeSig -> Bool

minimalMaudeSig :: MaudeSig

The minimal maude signature.

dhMaudeSig :: MaudeSig

Maude signatures for the AC symbols.

bpMaudeSig :: MaudeSig

Maude signatures for the AC symbols.

msetMaudeSig :: MaudeSig

Maude signatures for the AC symbols.

pairMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

symEncMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

asymEncMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

signatureMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

hashMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)

Returns all rewriting rules including the rules for DH, BP, and multiset.

stFunSyms :: MaudeSig -> Set NoEqSym

function signature for subterm theory

funSyms :: MaudeSig -> FunSig

function signature including the function symbols for DH, BP, and Multiset can be computed from enableX and stFunSyms

stRules :: MaudeSig -> Set StRule

rewriting rules for subterm theory

irreducibleFunSyms :: MaudeSig -> FunSig

irreducible function symbols (can be computed)

noEqFunSyms :: MaudeSig -> NoEqFunSig

Non-AC function symbols.

addFunSym :: NoEqSym -> MaudeSig -> MaudeSig

Add function symbol to given maude signature.

addStRule :: StRule -> MaudeSig -> MaudeSig

Add subterm rule to given maude signature.

Convenience exports

module Term.Substitution

module Term.Rewriting.Definitions