hasmtlib-1.2.0: A monad for interfacing with external SMT solvers
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Hasmtlib.Boolean

Synopsis

Documentation

class Boolean b where Source #

Minimal complete definition

bool, (&&), (||), not, xor

Methods

bool :: Bool -> b Source #

Lift a Bool

true :: b Source #

The true constant true = bool True

false :: b Source #

The false constant false = bool False

(&&) :: b -> b -> b infixr 3 Source #

Logical conjunction.

(||) :: b -> b -> b infixr 2 Source #

Logical disjunction (inclusive or).

(==>) :: b -> b -> b infixr 0 Source #

Logical implication.

not :: b -> b Source #

Logical negation

xor :: b -> b -> b Source #

Exclusive-or

Instances

Instances details
Boolean Bit Source # 
Instance details

Defined in Language.Hasmtlib.Boolean

Boolean Bool Source # 
Instance details

Defined in Language.Hasmtlib.Boolean

KnownNat n => Boolean (Bitvec n) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Bitvec

Boolean (Expr 'BoolSort) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Expr

KnownNat n => Boolean (Expr ('BvSort n)) Source # 
Instance details

Defined in Language.Hasmtlib.Internal.Expr

Methods

bool :: Bool -> Expr ('BvSort n) Source #

true :: Expr ('BvSort n) Source #

false :: Expr ('BvSort n) Source #

(&&) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source #

(||) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source #

(==>) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source #

not :: Expr ('BvSort n) -> Expr ('BvSort n) Source #

xor :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source #

KnownNat n => Boolean (Vector n Bit) Source #

Defined bitwise

Instance details

Defined in Language.Hasmtlib.Boolean

and :: (Foldable t, Boolean b) => t b -> b Source #

The logical conjunction of several values.

or :: (Foldable t, Boolean b) => t b -> b Source #

The logical disjunction of several values.

nand :: (Foldable t, Boolean b) => t b -> b Source #

The negated logical conjunction of several values.

nand = not . and

nor :: (Foldable t, Boolean b) => t b -> b Source #

The negated logical disjunction of several values.

nor = not . or

all :: (Foldable t, Boolean b) => (a -> b) -> t a -> b Source #

The logical conjunction of the mapping of a function over several values.

any :: (Foldable t, Boolean b) => (a -> b) -> t a -> b Source #

The logical disjunction of the mapping of a function over several values.