Safe Haskell | None |
---|---|
Language | Haskell2010 |
Solving constraints on variable ordering.
- data Atom f
- atoms :: Term f -> [Atom f]
- toTerm :: Atom f -> Term f
- fromTerm :: Term f -> Maybe (Atom f)
- data Formula f
- 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 = Branch {}
- trueBranch :: Branch f
- norm :: Eq f => Branch f -> Atom f -> Atom f
- contradictory :: (Minimal f, Ord f) => Branch f -> Bool
- formAnd :: (Minimal f, Ordered f) => Formula f -> [Branch f] -> [Branch f]
- branches :: (Minimal f, Ordered f) => Formula f -> [Branch f]
- addLess :: (Minimal f, Ordered f) => Atom f -> Atom f -> Branch f -> [Branch f]
- addEquals :: (Minimal f, Ordered f) => Atom f -> Atom f -> Branch f -> [Branch f]
- addTerm :: (Minimal f, Ordered f) => Atom f -> Branch f -> Branch f
- newtype Model f = Model (Map (Atom f) (Int, Int))
- 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
- lessEqInModel :: (Minimal f, Ordered f) => Model f -> Atom f -> Atom f -> Maybe Strictness
- solve :: (Minimal f, Ordered f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
- class Ord f => Ordered f where
- data Strictness
- lessThan :: Ordered f => Term f -> Term f -> Bool
- orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
Documentation
negateFormula :: Formula f -> Formula f Source #
trueBranch :: Branch f Source #
modelToLiterals :: Model f -> [Formula f] Source #
weakenModel :: Model f -> [Model f] Source #
lessEqInModel :: (Minimal f, Ordered f) => Model f -> Atom f -> Atom f -> Maybe Strictness Source #
solve :: (Minimal f, Ordered f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f) Source #
class Ord f => Ordered f where Source #
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.
data Strictness Source #
Describes whether an inequality is strict or nonstrict.