Language.Hasmtlib.Type.Relation

This module provides the data-type Relation for encoding binary relations as SMT-problems.

Example

problem :: MonadSMT s m => StateT s m (Relation Int Int)
    setLogic "QF_LIA"

    r <- relation ((2,1), (6,5))

    forM_ (image r <$> domain r) (assert . exactly @IntSort 1)
    forM_ (preimage r <$> codomain r) (assert . exactly @IntSort 1)

    assertMaybe $ do
      item <- r^?ix (3,3)
      return $ item === true

    return r

Type

newtype Relation a b

Relation a b represents a binary relation \(R \subseteq A \times B \), where the domain \(A\) is a finite subset of the type a, and the codomain \(B\) is a finite subset of the type b.

A relation is stored internally as Array (a,b) Expr BoolSort, so a and b have to be instances of Ix, and both \(A\) and \(B\) are intervals.

Constructors

Relation (Array (a, b) (Expr BoolSort))

Instances

(Ix a, Ix b) => Codec (Relation a b)

Defined in Language.Hasmtlib.Type.Relation

Associated Types

type Decoded (Relation a b)

Methods

decode :: Solution -> Relation a b -> Maybe (Decoded (Relation a b))

encode :: Decoded (Relation a b) -> Relation a b

(Ix a, Ix b) => Ixed (Relation a b)

Defined in Language.Hasmtlib.Type.Relation

Methods

ix :: Index (Relation a b) -> Traversal' (Relation a b) (IxValue (Relation a b))

(Ix a, Ix b, a ~ c, b ~ d) => Each (Relation a b) (Relation c d) (Expr 'BoolSort) (Expr 'BoolSort)

Defined in Language.Hasmtlib.Type.Relation

Methods

each :: Traversal (Relation a b) (Relation c d) (Expr 'BoolSort) (Expr 'BoolSort)

type Decoded (Relation a b)

Defined in Language.Hasmtlib.Type.Relation

type Decoded (Relation a b) = Array (a, b) Bool

type Index (Relation a b)

Defined in Language.Hasmtlib.Type.Relation

type Index (Relation a b) = (a, b)

type IxValue (Relation a b)

Defined in Language.Hasmtlib.Type.Relation

type IxValue (Relation a b) = Expr 'BoolSort

Construction

relation :: (Ix a, Ix b, MonadSMT s m) => ((a, b), (a, b)) -> m (Relation a b)

relation ((amin,bmin),(amax,mbax)) constructs an indeterminate relation \(R \subseteq A \times B \) where \(A\) is {amin .. amax} and \(B\) is {bmin .. bmax}.

symmetric_relation

Arguments

:: (MonadSMT s m, Ix b)

=> ((b, b), (b, b))

Since a symmetric relation must be homogeneous, the domain must equal the codomain. Therefore, given bounds ((p,q),(r,s)), it must hold that p=q and r=s.

-> m (Relation b b)

Constructs an indeterminate relation \(R \subseteq B \times B \) that is symmetric, i.e., \(\forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).

build

Arguments

:: (Ix a, Ix b)

=> ((a, b), (a, b))

-> [((a, b), Expr BoolSort)]

A list of tuples, where the first element represents an element \((x,y) \in A \times B \) and the second element is a positive Expr BoolSort if \((x,y) \in R \), or a negative Expr BoolSort if \((x,y) \notin R \).

-> Relation a b

Constructs a relation \(R \subseteq A \times B \) from a list.

buildFrom

Arguments

:: (Ix a, Ix b)

=> ((a, b), (a, b))

-> ((a, b) -> Expr BoolSort)

A function that assigns a Expr BoolSort-value to each element \((x,y) \in A \times B \).

-> Relation a b

Constructs a relation \(R \subseteq A \times B \) from a function.

buildFromM :: (Ix a, Ix b, MonadSMT s m) => ((a, b), (a, b)) -> ((a, b) -> m (Expr BoolSort)) -> m (Relation a b)

Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.

identity

Arguments

:: Ix a

=> ((a, a), (a, a))

Since the identity relation is homogeneous, the domain must equal the codomain. Therefore, given bounds ((p,q),(r,s)), it must hold that p=q and r=s.

-> Relation a a

Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\).

Accessors

(!?) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Maybe (Expr BoolSort)

Maybe (Expr BoolSort) for a given element \((x,y) \in A \times B \) and a given relation \(R \subseteq A \times B \) that indicates if \((x,y) \in R \) or not.

Just if given element is in bounds of the relation. Nothing otherwise.

(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Expr BoolSort

Unsafe version of (!?). Produces an array-indexing-error if given element is not within the bounds of the relation.

bounds :: Relation a b -> ((a, b), (a, b))

The bounds of the array that correspond to the matrix representation of the given relation.

indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]

The list of indices, where each index represents an element \((x,y) \in A \times B \) that may be contained in the given relation \(R \subseteq A \times B \).

elems :: Relation a b -> [Expr BoolSort]

The list of elements of the array that correspond to the matrix representation of the given relation.

assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Expr BoolSort)]

The list of tuples for the given relation \(R \subseteq A \times B \), where the first element represents an element \((x,y) \in A \times B \) and the second element indicates via a Expr BoolSort , if \((x,y) \in R \) or not.

domain :: Ix a => Relation a b -> [a]

The domain \(A\) of a relation \(R \subseteq A \times B\).

codomain :: Ix b => Relation a b -> [b]

The codomain \(B\) of a relation \(R \subseteq A \times B\).

image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort]

Returns a list of Expr BoolSort indicating whether the projection on given element \( x \in A \) holds for every element in the codomain:

\( \{ (x,y) \in R \mid y \in codomain(R) \} \)

preimage :: (Ix a, Ix b) => Relation a b -> b -> [Expr BoolSort]

Returns a list of Expr BoolSort indicating whether the projection on given element \( y \in B \) holds for every element in the domain:

\( \{ (x,y) \in R \mid x \in domain(R) \} \)

Pretty printing

table :: (Ix a, Ix b) => Array (a, b) Bool -> String

Print a satisfying assignment from an SMT solver, where the assignment is interpreted as a relation. putStrLn $ table <assignment> corresponds to the matrix representation of this relation.