twee-lib-2.4.2: An equational theorem prover

Twee.Constraints

Description

Solving constraints on variable ordering.

Synopsis

# Documentation

data Atom f Source #

Constructors

 Constant (Fun f) Variable Var

#### Instances

Instances details
 (Labelled f, Show f) => Show (Atom f) Source # Instance detailsDefined in Twee.Constraints MethodsshowsPrec :: Int -> Atom f -> ShowS #show :: Atom f -> String #showList :: [Atom f] -> ShowS # Eq (Atom f) Source # Instance detailsDefined in Twee.Constraints Methods(==) :: Atom f -> Atom f -> Bool #(/=) :: Atom f -> Atom f -> Bool # Ord (Atom f) Source # Instance detailsDefined in Twee.Constraints Methodscompare :: 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, PrettyTerm f) => Pretty (Atom f) Source # Instance detailsDefined in Twee.Constraints MethodspPrintPrec :: PrettyLevel -> Rational -> Atom f -> Doc #pPrint :: Atom f -> Doc #pPrintList :: PrettyLevel -> [Atom f] -> Doc #

atoms :: Term f -> [Atom f] Source #

toTerm :: Atom f -> Term f Source #

data Formula f Source #

Constructors

 Less (Atom f) (Atom f) LessEq (Atom f) (Atom f) And [Formula f] Or [Formula f]

#### Instances

Instances details
 (Labelled f, Show f) => Show (Formula f) Source # Instance detailsDefined in Twee.Constraints MethodsshowsPrec :: Int -> Formula f -> ShowS #show :: Formula f -> String #showList :: [Formula f] -> ShowS # Eq (Formula f) Source # Instance detailsDefined in Twee.Constraints Methods(==) :: Formula f -> Formula f -> Bool #(/=) :: Formula f -> Formula f -> Bool # Ord (Formula f) Source # Instance detailsDefined in Twee.Constraints Methodscompare :: 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, PrettyTerm f) => Pretty (Formula f) Source # Instance detailsDefined in Twee.Constraints MethodspPrintPrec :: PrettyLevel -> Rational -> Formula f -> Doc #pPrint :: Formula f -> Doc #pPrintList :: PrettyLevel -> [Formula f] -> Doc #

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

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

data Branch f Source #

Constructors

 Branch Fieldsfuns :: [Fun f] less :: [(Atom f, Atom f)] equals :: [(Atom f, Atom f)]

#### Instances

Instances details
 Eq (Branch f) Source # Instance detailsDefined in Twee.Constraints Methods(==) :: Branch f -> Branch f -> Bool #(/=) :: Branch f -> Branch f -> Bool # Ord (Branch f) Source # Instance detailsDefined in Twee.Constraints Methodscompare :: 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) Source # Instance detailsDefined in Twee.Constraints MethodspPrintPrec :: PrettyLevel -> Rational -> Branch f -> Doc #pPrint :: Branch f -> Doc #pPrintList :: PrettyLevel -> [Branch f] -> Doc #

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

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

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

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

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

newtype Model f Source #

Constructors

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

#### Instances

Instances details
 (Labelled f, Show f) => Show (Model f) Source # Instance detailsDefined in Twee.Constraints MethodsshowsPrec :: Int -> Model f -> ShowS #show :: Model f -> String #showList :: [Model f] -> ShowS # Eq (Model f) Source # Instance detailsDefined in Twee.Constraints Methods(==) :: Model f -> Model f -> Bool #(/=) :: Model f -> Model f -> Bool # (Labelled f, PrettyTerm f) => Pretty (Model f) Source # Instance detailsDefined in Twee.Constraints MethodspPrintPrec :: PrettyLevel -> Rational -> Model f -> Doc #pPrint :: Model f -> Doc #pPrintList :: PrettyLevel -> [Model f] -> Doc #

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

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

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

class Minimal f where Source #

Methods

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

class Ord f => Ordered f where Source #

Methods

lessEq :: Term f -> Term f -> Bool Source #

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 Source #

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 Source #

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

Instances details
 Source # Instance detailsDefined in Twee.Constraints MethodsshowList :: [Strictness] -> ShowS # Source # Instance detailsDefined in Twee.Constraints Methods

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

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 Source #

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.