Copyright	(C) 2017-18 Jakub Daniel
License	BSD-style (see the file LICENSE)
Maintainer	Jakub Daniel <jakub.daniel@protonmail.com>
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.Expression

Description

Usage:

You can build expressions in predefined languages (QFLogic, QFLia, QFALia, Lia, ALia) using the smart constructors such as var, and, or, not, forall, exists (or operators .&., .|., .->., .<-., .<->.) or you can define your own sorted language as a fixpoint (IFix) of a sum (:+:) of indexed functors (IFunctor).

Synopsis

Documentation

module Data.Expression.Arithmetic

module Data.Expression.Array

module Data.Expression.Equality

module Data.Expression.IfThenElse

module Data.Expression.Parser

module Data.Expression.Sort

module Data.Expression.Utils.Indexed.Eq

module Data.Expression.Utils.Indexed.Foldable

module Data.Expression.Utils.Indexed.Functor

module Data.Expression.Utils.Indexed.Show

module Data.Expression.Utils.Indexed.Sum

module Data.Expression.Utils.Indexed.Traversable

type QFLogicF = EqualityF :+: (ConjunctionF :+: (DisjunctionF :+: (NegationF :+: VarF))) Source #

A functor representing propositional logic embedded in first order logic (quantifier-free, boolean variables aka propositions, logical connectives and, or, not, equality of propositions)

type QFLiaF = ArithmeticF :+: (IfThenElseF :+: QFLogicF) Source #

A functor representing the language of quantifier-free linear integer arithmetic theory in first order logic (integer constants, integer variables, addition, multiplication, divisibility, ordering)

type LiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFLiaF))) Source #

A functor much like QFLiaF with quantifiers over booleans and integers

type QFALiaF = ArrayF :+: QFLiaF Source #

A functor representing the language of quantifier-free linear integer arithmetic and array theories in first order logic (much like QFLiaF with additional array variables, select, and store)

type ALiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFALiaF))) Source #

A functor much like QFALiaF with quantifiers over booleans and integers

type Var = IFix VarF Source #

A language consisting solely of variables (useful for listing variables outside of any particular context, such as bound variables of quantified formula)

type QFLogic = IFix QFLogicF Source #

A language obtained as fixpoint of QFLogicF

type QFLia = IFix QFLiaF Source #

A language obtained as fixpoint of QFLiaF

type Lia = IFix LiaF Source #

A language obtained as fixpoint of LiaF

type QFALia = IFix QFALiaF Source #

A language obtained as fixpoint of QFALiaF

type ALia = IFix ALiaF Source #

A language obtained as fixpoint of ALiaF

class BoundedLattice a => ComplementedLattice a where Source #

Bounded lattices that support complementing elements

complement . complement = id

Minimal complete definition

complement

Methods

complement :: a -> a Source #

Instances

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #

type VariableName = String Source #

Type of names assigned to variables

data VarF a s where Source #

A functor representing a sorted variable, each variable is identified by its name and sort

Constructors

Var :: VariableName -> Sing s -> VarF a s

Instances

IShow Sort k (VarF (k -> *)) Source #
Methods ishow :: f (Const k String) i -> Const (VarF (k -> *)) String i Source #
IFoldable Sort (VarF (Sort -> *)) Source #
Methods ifold :: Monoid m => f (Const (VarF (Sort -> )) m) i' -> Const (VarF (Sort -> )) m i' Source #
IEq1 Sort (VarF (Sort -> *)) Source #
Methods ieq1 :: IEq (VarF (Sort -> *)) a => f a j -> f a j -> Bool Source #
IFunctor Sort (VarF (Sort -> *)) Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing (VarF (Sort -> *)) i' Source #
ITraversable Sort (VarF (Sort -> *)) Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
MaybeQuantified Sort (VarF (Sort -> *)) Source #
Methods isQuantified' :: MaybeQuantified (VarF (Sort -> )) g => f (IFix (VarF (Sort -> )) g) s -> Const (VarF (Sort -> )) Any s freevars' :: f (Const (VarF (Sort -> )) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (VarF (Sort -> )) [DynamicallySorted (VarF (Sort -> *))] s
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (QFALia BooleanSort) Source #
Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
JoinSemiLattice (QFLia BooleanSort) Source #
Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
JoinSemiLattice (QFLogic BooleanSort) Source #
Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (QFALia BooleanSort) Source #
Methods (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (QFLia BooleanSort) Source #
Methods (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
MeetSemiLattice (QFLogic BooleanSort) Source #
Methods (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (QFALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

Lattice (QFLia BooleanSort) Source #

Lattice (QFLogic BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (QFALia BooleanSort) Source #
Methods bottom :: QFALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedJoinSemiLattice (QFLia BooleanSort) Source #
Methods bottom :: QFLia BooleanSort #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Methods bottom :: QFLogic BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (QFALia BooleanSort) Source #
Methods top :: QFALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedMeetSemiLattice (QFLia BooleanSort) Source #
Methods top :: QFLia BooleanSort #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Methods top :: QFLogic BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (QFALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

BoundedLattice (QFLia BooleanSort) Source #

BoundedLattice (QFLogic BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
(:<:) Sort (VarF (Sort -> )) f => Parseable (k -> Sort -> ) (VarF k) f Source #
Methods parser :: Proxy (VarF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data ConjunctionF a s where Source #

A functor representing a logical connective for conjunction

Constructors

And :: [a BooleanSort] -> ConjunctionF a BooleanSort

Instances

IFoldable Sort ConjunctionF Source #
Methods ifold :: Monoid m => f (Const ConjunctionF m) i' -> Const ConjunctionF m i' Source #
IEq1 Sort ConjunctionF Source #
Methods ieq1 :: IEq ConjunctionF a => f a j -> f a j -> Bool Source #
IFunctor Sort ConjunctionF Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing ConjunctionF i' Source #
ITraversable Sort ConjunctionF Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
IShow Sort Sort ConjunctionF Source #
Methods ishow :: f (Const k String) i -> Const ConjunctionF String i Source #
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (QFALia BooleanSort) Source #
Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
JoinSemiLattice (QFLia BooleanSort) Source #
Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
JoinSemiLattice (QFLogic BooleanSort) Source #
Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (QFALia BooleanSort) Source #
Methods (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (QFLia BooleanSort) Source #
Methods (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
MeetSemiLattice (QFLogic BooleanSort) Source #
Methods (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (QFALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

Lattice (QFLia BooleanSort) Source #

Lattice (QFLogic BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (QFALia BooleanSort) Source #
Methods bottom :: QFALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedJoinSemiLattice (QFLia BooleanSort) Source #
Methods bottom :: QFLia BooleanSort #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Methods bottom :: QFLogic BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (QFALia BooleanSort) Source #
Methods top :: QFALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedMeetSemiLattice (QFLia BooleanSort) Source #
Methods top :: QFLia BooleanSort #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Methods top :: QFLogic BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (QFALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

BoundedLattice (QFLia BooleanSort) Source #

BoundedLattice (QFLogic BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
(:<:) Sort ConjunctionF f => Parseable ((Sort -> ) -> Sort -> ) ConjunctionF f Source #
Methods parser :: Proxy ConjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data DisjunctionF a s where Source #

A functor representing a logical connective for disjunction

Constructors

Or :: [a BooleanSort] -> DisjunctionF a BooleanSort

Instances

IFoldable Sort DisjunctionF Source #
Methods ifold :: Monoid m => f (Const DisjunctionF m) i' -> Const DisjunctionF m i' Source #
IEq1 Sort DisjunctionF Source #
Methods ieq1 :: IEq DisjunctionF a => f a j -> f a j -> Bool Source #
IFunctor Sort DisjunctionF Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing DisjunctionF i' Source #
ITraversable Sort DisjunctionF Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
IShow Sort Sort DisjunctionF Source #
Methods ishow :: f (Const k String) i -> Const DisjunctionF String i Source #
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (QFALia BooleanSort) Source #
Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
JoinSemiLattice (QFLia BooleanSort) Source #
Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
JoinSemiLattice (QFLogic BooleanSort) Source #
Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (QFALia BooleanSort) Source #
Methods (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (QFLia BooleanSort) Source #
Methods (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
MeetSemiLattice (QFLogic BooleanSort) Source #
Methods (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (QFALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

Lattice (QFLia BooleanSort) Source #

Lattice (QFLogic BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (QFALia BooleanSort) Source #
Methods bottom :: QFALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedJoinSemiLattice (QFLia BooleanSort) Source #
Methods bottom :: QFLia BooleanSort #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Methods bottom :: QFLogic BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (QFALia BooleanSort) Source #
Methods top :: QFALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedMeetSemiLattice (QFLia BooleanSort) Source #
Methods top :: QFLia BooleanSort #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Methods top :: QFLogic BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (QFALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

BoundedLattice (QFLia BooleanSort) Source #

BoundedLattice (QFLogic BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
(:<:) Sort DisjunctionF f => Parseable ((Sort -> ) -> Sort -> ) DisjunctionF f Source #
Methods parser :: Proxy DisjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data NegationF a s where Source #

A functor representing a logical connective for negation

Constructors

Not :: a BooleanSort -> NegationF a BooleanSort

Instances

IFoldable Sort NegationF Source #
Methods ifold :: Monoid m => f (Const NegationF m) i' -> Const NegationF m i' Source #
IEq1 Sort NegationF Source #
Methods ieq1 :: IEq NegationF a => f a j -> f a j -> Bool Source #
IFunctor Sort NegationF Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing NegationF i' Source #
ITraversable Sort NegationF Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
IShow Sort Sort NegationF Source #
Methods ishow :: f (Const k String) i -> Const NegationF String i Source #
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (QFALia BooleanSort) Source #
Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
JoinSemiLattice (QFLia BooleanSort) Source #
Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
JoinSemiLattice (QFLogic BooleanSort) Source #
Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (QFALia BooleanSort) Source #
Methods (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (QFLia BooleanSort) Source #
Methods (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
MeetSemiLattice (QFLogic BooleanSort) Source #
Methods (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (QFALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

Lattice (QFLia BooleanSort) Source #

Lattice (QFLogic BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (QFALia BooleanSort) Source #
Methods bottom :: QFALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedJoinSemiLattice (QFLia BooleanSort) Source #
Methods bottom :: QFLia BooleanSort #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Methods bottom :: QFLogic BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (QFALia BooleanSort) Source #
Methods top :: QFALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedMeetSemiLattice (QFLia BooleanSort) Source #
Methods top :: QFLia BooleanSort #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Methods top :: QFLogic BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (QFALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

BoundedLattice (QFLia BooleanSort) Source #

BoundedLattice (QFLogic BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
(:<:) Sort NegationF f => Parseable ((Sort -> ) -> Sort -> ) NegationF f Source #
Methods parser :: Proxy NegationF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data UniversalF v a s where Source #

A functor representing a mono-sorted universal quantifier binding a number of variables within a formula

Constructors

Forall :: [Var v] -> a BooleanSort -> UniversalF v a BooleanSort

Instances

IShow Sort Sort (UniversalF v) Source #
Methods ishow :: f (Const k String) i -> Const (UniversalF v) String i Source #
IFoldable Sort (UniversalF v) Source #
Methods ifold :: Monoid m => f (Const (UniversalF v) m) i' -> Const (UniversalF v) m i' Source #
IEq1 Sort (UniversalF v) Source #
Methods ieq1 :: IEq (UniversalF v) a => f a j -> f a j -> Bool Source #
IFunctor Sort (UniversalF v) Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing (UniversalF v) i' Source #
ITraversable Sort (UniversalF v) Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
MaybeQuantified Sort (UniversalF v) Source #
Methods isQuantified' :: MaybeQuantified (UniversalF v) g => f (IFix (UniversalF v) g) s -> Const (UniversalF v) Any s freevars' :: f (Const (UniversalF v) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (UniversalF v) [DynamicallySorted (VarF (Sort -> ))] s
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> ) -> Sort -> ) (UniversalF v) f Source #
Methods parser :: Proxy (UniversalF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data ExistentialF v a s where Source #

A functor representing a mono-sorted existential quantifier binding a number of variables within a formula

Constructors

Exists :: [Var v] -> a BooleanSort -> ExistentialF v a BooleanSort

Instances

IShow Sort Sort (ExistentialF v) Source #
Methods ishow :: f (Const k String) i -> Const (ExistentialF v) String i Source #
IFoldable Sort (ExistentialF v) Source #
Methods ifold :: Monoid m => f (Const (ExistentialF v) m) i' -> Const (ExistentialF v) m i' Source #
IEq1 Sort (ExistentialF v) Source #
Methods ieq1 :: IEq (ExistentialF v) a => f a j -> f a j -> Bool Source #
IFunctor Sort (ExistentialF v) Source #
Methods imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source # index :: f a i' -> Sing (ExistentialF v) i' Source #
ITraversable Sort (ExistentialF v) Source #
Methods itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #
MaybeQuantified Sort (ExistentialF v) Source #
Methods isQuantified' :: MaybeQuantified (ExistentialF v) g => f (IFix (ExistentialF v) g) s -> Const (ExistentialF v) Any s freevars' :: f (Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> ))] s
JoinSemiLattice (ALia BooleanSort) Source #
Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
Lattice (ALia BooleanSort) Source #

Lattice (Lia BooleanSort) Source #

BoundedJoinSemiLattice (ALia BooleanSort) Source #
Methods bottom :: ALia BooleanSort #
BoundedJoinSemiLattice (Lia BooleanSort) Source #
Methods bottom :: Lia BooleanSort #
BoundedMeetSemiLattice (ALia BooleanSort) Source #
Methods top :: ALia BooleanSort #
BoundedMeetSemiLattice (Lia BooleanSort) Source #
Methods top :: Lia BooleanSort #
BoundedLattice (ALia BooleanSort) Source #

BoundedLattice (Lia BooleanSort) Source #

ComplementedLattice (ALia BooleanSort) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> ) -> Sort -> ) (ExistentialF v) f Source #
Methods parser :: Proxy (ExistentialF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

newtype Substitution f Source #

Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.

Constructors

Substitution
Fields runSubstitution :: forall s. IFix f s -> Maybe (IFix f s)

Instances

Monoid (Substitution f) Source #
Methods mempty :: Substitution f # mappend :: Substitution f -> Substitution f -> Substitution f # mconcat :: [Substitution f] -> Substitution f #

substitute :: (IFunctor f, IEq1 f) => IFix f s -> Substitution f -> IFix f s Source #

Executes a substitution.

for :: forall f s. (IFunctor f, IEq1 f) => IFix f s -> IFix f s -> Substitution f Source #

A simple constructor of substitutions that replaces the latter expression with the former.

var :: forall f s. (VarF :<: f, SingI s) => VariableName -> IFix f s Source #

A smart constructor for variables of any sort in any language Takes the variable name and infers the target language and sort from context.

var "a" :: Lia 'IntegralSort

true :: ConjunctionF :<: f => IFix f BooleanSort Source #

Logical tautology

false :: DisjunctionF :<: f => IFix f BooleanSort Source #

Logical contradiction

and :: ConjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort Source #

A smart constructor for variadic conjunction

or :: DisjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort Source #

A smart constructor for variadic disjunction

not :: NegationF :<: f => IFix f BooleanSort -> IFix f BooleanSort Source #

A smart constructor for negation

forall :: UniversalF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort Source #

A smart constructor for universally quantified formulae

exists :: ExistentialF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort Source #

A smart constructor for existentially quantified formulae

(.&.) :: ConjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 6 Source #

A smart constructor for binary conjunction

(.|.) :: DisjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 5 Source #

A smart constructor for binary disjunction

(.->.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 4 Source #

A smart constructor for implication (an abbreviation for not a .|. b)

(.<-.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixl 4 Source #

A smart constructor for reversed implication (an abbreviation for a .|. not b)

(.<->.) :: (ConjunctionF :<: f, DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infix 3 Source #

A smart constructor for if-and-only-if connective

(./=.) :: forall f s. (NegationF :<: f, EqualityF :<: f, SingI s) => IFix f s -> IFix f s -> IFix f BooleanSort infix 7 Source #

A smart constructor for disequality

literals :: (ConjunctionF :<: f, DisjunctionF :<: f) => IFix f BooleanSort -> [IFix f BooleanSort] Source #

literals decomposes a boolean combination (formed with conjunctions and disjunctions, preferably in negation normal form) into its constituents.

conjuncts :: ConjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort] Source #

conjuncts decomposes a conjunction into conjuncts.

disjuncts :: DisjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort] Source #

disjuncts decomposes a disjunction into disjuncts.

vars :: (VarF :<: f, IFoldable f, IFunctor f) => IFix f s -> [DynamicallySorted VarF] Source #

Collects a list of all variables occurring in an expression (bound or free).

freevars :: (IFunctor f, MaybeQuantified f) => IFix f s -> [DynamicallySorted VarF] Source #

Collects a list of all free variables occurring in an expression.

class MaybeQuantified f Source #

Minimal complete definition

isQuantified', freevars'

Instances

(IFunctor k f, IFoldable k f) => MaybeQuantified k f Source #
Methods isQuantified' :: MaybeQuantified f g => f (IFix f g) s -> Const f Any s freevars' :: f (Const f [DynamicallySorted (VarF (Sort -> ))]) s -> Const f [DynamicallySorted (VarF (Sort -> ))] s
MaybeQuantified Sort (ExistentialF v) Source #
Methods isQuantified' :: MaybeQuantified (ExistentialF v) g => f (IFix (ExistentialF v) g) s -> Const (ExistentialF v) Any s freevars' :: f (Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> ))] s
MaybeQuantified Sort (UniversalF v) Source #
Methods isQuantified' :: MaybeQuantified (UniversalF v) g => f (IFix (UniversalF v) g) s -> Const (UniversalF v) Any s freevars' :: f (Const (UniversalF v) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (UniversalF v) [DynamicallySorted (VarF (Sort -> ))] s
MaybeQuantified Sort (VarF (Sort -> *)) Source #
Methods isQuantified' :: MaybeQuantified (VarF (Sort -> )) g => f (IFix (VarF (Sort -> )) g) s -> Const (VarF (Sort -> )) Any s freevars' :: f (Const (VarF (Sort -> )) [DynamicallySorted (VarF (Sort -> ))]) s -> Const (VarF (Sort -> )) [DynamicallySorted (VarF (Sort -> *))] s
(MaybeQuantified k f, MaybeQuantified k g) => MaybeQuantified k ((:+:) k (k -> *) f g) Source #
Methods isQuantified' :: MaybeQuantified ((k :+: (k -> )) f g) g => f (IFix ((k :+: (k -> )) f g) g) s -> Const ((k :+: (k -> )) f g) Any s freevars' :: f (Const ((k :+: (k -> )) f g) [DynamicallySorted (VarF (Sort -> ))]) s -> Const ((k :+: (k -> )) f g) [DynamicallySorted (VarF (Sort -> *))] s

isQuantified :: MaybeQuantified f => IFix f s -> Bool Source #

Test whether an expression contains a quantifier.

isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool Source #

Tests whether an expression is free of any quantifier.

class (NegationF :<: f, HasDual f f) => NNF f Source #

Instances

((:<:) Sort NegationF f, HasDual f f) => NNF f Source #

nnf :: forall f. NNF f => IFix f BooleanSort -> IFix f BooleanSort Source #

Propagates negation toward boolean atoms (across conjunction, disjunction, quantifiers).

class (VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f) => Prenex f Source #

Instances

((:<:) Sort (VarF (Sort -> *)) f, (:<:) Sort NegationF f, IFunctor Sort f, IFoldable Sort f, ITraversable Sort f, HasDual f f, MaybeQuantified' f f) => Prenex f Source #

prenex :: forall f. Prenex f => IFix f BooleanSort -> IFix f BooleanSort Source #

Puts an expression into prenex form (quantifier prefix and a quantifier-free formula).

class (VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f) => Flatten f Source #

Instances

((:<:) Sort (VarF (Sort -> )) f, Bind ((Sort -> ) -> Sort -> *) f f, Bind' f f, MaybeQuantified'' f f, IFoldable Sort f, ITraversable Sort f) => Flatten f Source #

flatten :: forall f. Flatten f => IFix f BooleanSort -> IFix f BooleanSort Source #

Replaces non-variable and non-constant arguments to uninterpreted functions (such as select and store) with a fresh bound (universally or existentially) variable that is bound to the original term.

class (VarF :<: f, EqualityF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f) => Unstore f Source #

Instances

((:<:) Sort (VarF (Sort -> )) f, (:<:) Sort (EqualityF Sort) f, Bind ((Sort -> ) -> Sort -> ) f f, Bind' f f, MaybeQuantified'' f f, Forall ((Sort -> ) -> Sort -> *) f f, Axiomatized f f, IFoldable Sort f, ITraversable Sort f) => Unstore f Source #

unstore :: forall f. Unstore f => IFix f BooleanSort -> IFix f BooleanSort Source #

Replaces store with an instance of its axiomatization.