Language.Hasmtlib.Boolean

This module provides a more generic version of bool-like algebras than what the Prelude does for Bool.

The class Boolean therefore overloads most of the Preludes operators like (&&).

However, as Bool also features an instance of Boolean, you can simply hide the Prelude ones - not having to import either qualified.

Example

import Prelude hiding (not, any, all, (&&), (||), and, or)
import Language.Hasmtlib

problem :: MonadSMT s m => StateT s m (Expr BoolSort, Expr BoolSort)
problem = do
  x <- var @BoolSort
  y <- var
  let b = False || True
  assert $ x && y <==> and [x, y, true] && encode b ==> x && y
  return (x,y)

Class

class Boolean b where

Minimal complete definition

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

Methods

bool :: Bool -> b

Lift a Bool.

true :: b

The true constant. true = bool True

false :: b

The false constant. false = bool False

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

Logical conjunction.

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

Logical disjunction (inclusive or).

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

Logical implication.

(<==) :: b -> b -> b infixl 0

Logical implication with arrow reversed.

forall x y. (x ==> y) === (y <== x)

(<==>) :: b -> b -> b infixr 4

Logical equivalence.

not :: b -> b

Logical negation.

xor :: b -> b -> b infix 4

Exclusive-or.

Instances

Boolean Bit

Defined in Language.Hasmtlib.Boolean

Methods

bool :: Bool -> Bit

true :: Bit

false :: Bit

(&&) :: Bit -> Bit -> Bit

(||) :: Bit -> Bit -> Bit

(==>) :: Bit -> Bit -> Bit

(<==) :: Bit -> Bit -> Bit

(<==>) :: Bit -> Bit -> Bit

not :: Bit -> Bit

xor :: Bit -> Bit -> Bit

Boolean Bool

Defined in Language.Hasmtlib.Boolean

Methods

bool :: Bool -> Bool

true :: Bool

false :: Bool

(&&) :: Bool -> Bool -> Bool

(||) :: Bool -> Bool -> Bool

(==>) :: Bool -> Bool -> Bool

(<==) :: Bool -> Bool -> Bool

(<==>) :: Bool -> Bool -> Bool

not :: Bool -> Bool

xor :: Bool -> Bool -> Bool

Boolean (Expr 'BoolSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

bool :: Bool -> Expr 'BoolSort

true :: Expr 'BoolSort

false :: Expr 'BoolSort

(&&) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

(||) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

(==>) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

(<==) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

(<==>) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

not :: Expr 'BoolSort -> Expr 'BoolSort

xor :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

(KnownBvEnc enc, KnownNat n) => Boolean (Expr ('BvSort enc n))

Defined in Language.Hasmtlib.Type.Expr

Methods

bool :: Bool -> Expr ('BvSort enc n)

true :: Expr ('BvSort enc n)

false :: Expr ('BvSort enc n)

(&&) :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

(||) :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

(==>) :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

(<==) :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

(<==>) :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

not :: Expr ('BvSort enc n) -> Expr ('BvSort enc n)

xor :: Expr ('BvSort enc n) -> Expr ('BvSort enc n) -> Expr ('BvSort enc n)

Boolean (Value 'BoolSort)

Defined in Language.Hasmtlib.Type.Value

Methods

bool :: Bool -> Value 'BoolSort

true :: Value 'BoolSort

false :: Value 'BoolSort

(&&) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(||) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(==>) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(<==) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(<==>) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

not :: Value 'BoolSort -> Value 'BoolSort

xor :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

KnownNat n => Boolean (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

bool :: Bool -> Bitvec enc n

true :: Bitvec enc n

false :: Bitvec enc n

(&&) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(||) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(==>) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(<==) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(<==>) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

not :: Bitvec enc n -> Bitvec enc n

xor :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

KnownNat n => Boolean (Vector n Bit)

Defined bitwise

Defined in Language.Hasmtlib.Boolean

Methods

bool :: Bool -> Vector n Bit

true :: Vector n Bit

false :: Vector n Bit

(&&) :: Vector n Bit -> Vector n Bit -> Vector n Bit

(||) :: Vector n Bit -> Vector n Bit -> Vector n Bit

(==>) :: Vector n Bit -> Vector n Bit -> Vector n Bit

(<==) :: Vector n Bit -> Vector n Bit -> Vector n Bit

(<==>) :: Vector n Bit -> Vector n Bit -> Vector n Bit

not :: Vector n Bit -> Vector n Bit

xor :: Vector n Bit -> Vector n Bit -> Vector n Bit

Operators

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

The logical conjunction of several values.

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

The logical disjunction of several values.

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

The negated logical conjunction of several values.

nand = not . and

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

The negated logical disjunction of several values.

nor = not . or

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

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

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

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