Twee.Constraints

Solving constraints on variable ordering.

Documentation

data Atom f

Constructors

Constant (Fun f)

Variable Var

Instances

Eq (Atom f)

Defined in Twee.Constraints

Methods

(==) :: Atom f -> Atom f -> Bool

(/=) :: Atom f -> Atom f -> Bool

Ord (Atom f)

Defined in Twee.Constraints

Methods

compare :: Atom f -> Atom f -> Ordering

(<) :: Atom f -> Atom f -> Bool

(<=) :: Atom f -> Atom f -> Bool

(>) :: Atom f -> Atom f -> Bool

(>=) :: Atom f -> Atom f -> Bool

max :: Atom f -> Atom f -> Atom f

min :: Atom f -> Atom f -> Atom f

(Labelled f, Show f) => Show (Atom f)

Defined in Twee.Constraints

Methods

showsPrec :: Int -> Atom f -> ShowS

show :: Atom f -> String

showList :: [Atom f] -> ShowS

(Labelled f, PrettyTerm f) => Pretty (Atom f)

Defined in Twee.Constraints

Methods

pPrintPrec :: PrettyLevel -> Rational -> Atom f -> Doc

pPrint :: Atom f -> Doc

pPrintList :: PrettyLevel -> [Atom f] -> Doc

atoms :: Term f -> [Atom f]

toTerm :: Atom f -> Term f

fromTerm :: Term f -> Maybe (Atom f)

data Formula f

Constructors

Less (Atom f) (Atom f)

LessEq (Atom f) (Atom f)

And [Formula f]

Or [Formula f]

Instances

Eq (Formula f)

Defined in Twee.Constraints

Methods

(==) :: Formula f -> Formula f -> Bool

(/=) :: Formula f -> Formula f -> Bool

Ord (Formula f)

Defined in Twee.Constraints

Methods

compare :: Formula f -> Formula f -> Ordering

(<) :: Formula f -> Formula f -> Bool

(<=) :: Formula f -> Formula f -> Bool

(>) :: Formula f -> Formula f -> Bool

(>=) :: Formula f -> Formula f -> Bool

max :: Formula f -> Formula f -> Formula f

min :: Formula f -> Formula f -> Formula f

(Labelled f, Show f) => Show (Formula f)

Defined in Twee.Constraints

Methods

showsPrec :: Int -> Formula f -> ShowS

show :: Formula f -> String

showList :: [Formula f] -> ShowS

(Labelled f, PrettyTerm f) => Pretty (Formula f)

Defined in Twee.Constraints

Methods

pPrintPrec :: PrettyLevel -> Rational -> Formula f -> Doc

pPrint :: Formula f -> Doc

pPrintList :: PrettyLevel -> [Formula f] -> Doc

negateFormula :: Formula f -> Formula f

conj :: Foldable t => t (Formula f) -> Formula f

disj :: Foldable t => t (Formula f) -> Formula f

(&&&) :: Formula f -> Formula f -> Formula f

(|||) :: Formula f -> Formula f -> Formula f

true :: Formula f

false :: Formula f

data Branch f

Constructors

Branch

Fields

• funs :: [Fun f]
• less :: [(Atom f, Atom f)]
• equals :: [(Atom f, Atom f)]

Instances

Eq (Branch f)

Defined in Twee.Constraints

Methods

(==) :: Branch f -> Branch f -> Bool

(/=) :: Branch f -> Branch f -> Bool

Ord (Branch f)

Defined in Twee.Constraints

Methods

compare :: Branch f -> Branch f -> Ordering

(<) :: Branch f -> Branch f -> Bool

(<=) :: Branch f -> Branch f -> Bool

(>) :: Branch f -> Branch f -> Bool

(>=) :: Branch f -> Branch f -> Bool

max :: Branch f -> Branch f -> Branch f

min :: Branch f -> Branch f -> Branch f

(Labelled f, PrettyTerm f) => Pretty (Branch f)

Defined in Twee.Constraints

Methods

pPrintPrec :: PrettyLevel -> Rational -> Branch f -> Doc

pPrint :: Branch f -> Doc

pPrintList :: PrettyLevel -> [Branch f] -> Doc

trueBranch :: Branch f

norm :: Eq f => Branch f -> Atom f -> Atom f

contradictory :: (Minimal f, Ord f, Labelled f) => Branch f -> Bool

formAnd :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f] -> [Branch f]

branches :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f]

addLess :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]

addEquals :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]

addTerm :: (Minimal f, Ordered f, Labelled f) => Atom f -> Branch f -> Branch f

newtype Model f

Constructors

Model (Map (Atom f) (Int, Int))

Instances

Eq (Model f)

Defined in Twee.Constraints

Methods

(==) :: Model f -> Model f -> Bool

(/=) :: Model f -> Model f -> Bool

(Labelled f, Show f) => Show (Model f)

Defined in Twee.Constraints

Methods

showsPrec :: Int -> Model f -> ShowS

show :: Model f -> String

showList :: [Model f] -> ShowS

(Labelled f, PrettyTerm f) => Pretty (Model f)

Defined in Twee.Constraints

Methods

pPrintPrec :: PrettyLevel -> Rational -> Model f -> Doc

pPrint :: Model f -> Doc

pPrintList :: PrettyLevel -> [Model f] -> Doc

modelToLiterals :: Model f -> [Formula f]

modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f

weakenModel :: Model f -> [Model f]

varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool

varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]

class Minimal f where

Methods

minimal :: Fun f

lessEqInModel :: (Minimal f, Ordered f, Labelled f) => Model f -> Atom f -> Atom f -> Maybe Strictness

solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)

class Ord f => Ordered f where

Methods

lessEq :: Term f -> Term f -> Bool

Return True if the first term is less than or equal to the second, in the term ordering.

lessIn :: Model f -> Term f -> Term f -> Maybe Strictness

Check if the first term is less than or equal to the second in the given model, and decide whether the inequality is strict or nonstrict.

lessEqSkolem :: Term f -> Term f -> Bool

data Strictness

Describes whether an inequality is strict or nonstrict.

Constructors

Strict

The first term is strictly less than the second.

Nonstrict

The first term is less than or equal to the second.

Instances

Eq Strictness

Defined in Twee.Constraints

Methods

(==) :: Strictness -> Strictness -> Bool

(/=) :: Strictness -> Strictness -> Bool

Show Strictness

Defined in Twee.Constraints

Methods

showsPrec :: Int -> Strictness -> ShowS

show :: Strictness -> String

showList :: [Strictness] -> ShowS

lessThan :: Ordered f => Term f -> Term f -> Bool

Return True if the first argument is strictly less than the second, in the term ordering.

orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering

Return the direction in which the terms are oriented according to the term ordering, or Nothing if they cannot be oriented. A result of Just LT means that the first term is less than or equal to the second.