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.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 :+: 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.