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 = DMap SSMTSort IntValueMap

A Solution is a dependent map DMap from SSMTSorts t to IntMap t.

newtype IntValueMap t

Newtype for IntMap Value so we can use it as right-hand-side of DMap.

Constructors

IntValueMap (IntMap (Value t))

Instances

Monoid (IntValueMap t)

Defined in Language.Hasmtlib.Type.Solution

Methods

mempty :: IntValueMap t

mappend :: IntValueMap t -> IntValueMap t -> IntValueMap t

mconcat :: [IntValueMap t] -> IntValueMap t

Semigroup (IntValueMap t)

Defined in Language.Hasmtlib.Type.Solution

Methods

(<>) :: IntValueMap t -> IntValueMap t -> IntValueMap t

sconcat :: NonEmpty (IntValueMap t) -> IntValueMap t

stimes :: Integral b => b -> IntValueMap t -> IntValueMap t

Show (IntValueMap t)

Defined in Language.Hasmtlib.Type.Solution

Methods

showsPrec :: Int -> IntValueMap t -> ShowS

show :: IntValueMap t -> String

showList :: [IntValueMap t] -> ShowS

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

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

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

class Ord (HaskellType t) => OrdHaskellType t

Alias class for constraint Ord (HaskellType t)

Instances

Ord (HaskellType t) => OrdHaskellType t

Defined in Language.Hasmtlib.Type.Solution

type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f

An existential wrapper that hides some known SMTSort with an Ord HaskellType

fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution

Create a Solution from some SMTVarSols.