Language.Hasmtlib.Type.Solution

Documentation

type Solver s m = s -> m (Result, Solution)

Function that turns a state into a result and a solution.

data Result

Results of check-sat commands.

Constructors

Unsat

Unknown

Sat

Instances

Show Result

Defined in Language.Hasmtlib.Type.Solution

Methods

showsPrec :: Int -> Result -> ShowS

show :: Result -> String

showList :: [Result] -> ShowS

Eq Result

Defined in Language.Hasmtlib.Type.Solution

Methods

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

(/=) :: Result -> Result -> Bool

Ord Result

Defined in Language.Hasmtlib.Type.Solution

Methods

compare :: Result -> Result -> Ordering

(<) :: Result -> Result -> Bool

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

(>) :: Result -> Result -> Bool

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

max :: Result -> Result -> Result

min :: Result -> Result -> Result

type Solution = IntMap (SomeKnownSMTSort SMTVarSol)

A Solution is a Map from the variable-identifier to some solution for it.

data SMTVarSol (t :: SMTSort)

A solution for a single variable.

Constructors

SMTVarSol

Fields

• _solVar :: SMTVar t

  A variable in the SMT-Problem

• _solVal :: Value t

  An assignment for this variable in a solution

Instances

Show (SMTVarSol t)

Defined in Language.Hasmtlib.Type.Solution

Methods

showsPrec :: Int -> SMTVarSol t -> ShowS

show :: SMTVarSol t -> String

showList :: [SMTVarSol t] -> ShowS

Eq (SMTVarSol t)

Defined in Language.Hasmtlib.Type.Solution

Methods

(==) :: SMTVarSol t -> SMTVarSol t -> Bool

(/=) :: SMTVarSol t -> SMTVarSol t -> Bool

Ord (SMTVarSol t)

Defined in Language.Hasmtlib.Type.Solution

Methods

compare :: SMTVarSol t -> SMTVarSol t -> Ordering

(<) :: SMTVarSol t -> SMTVarSol t -> Bool

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

(>) :: SMTVarSol t -> SMTVarSol t -> Bool

(>=) :: SMTVarSol t -> SMTVarSol t -> Bool

max :: SMTVarSol t -> SMTVarSol t -> SMTVarSol t

min :: SMTVarSol t -> SMTVarSol t -> SMTVarSol t

solVar :: forall t. Lens' (SMTVarSol t) (SMTVar t)

solVal :: forall t. Lens' (SMTVarSol t) (Value t)