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

Language.Hasmtlib.Type.Solution

Description

This module provides the types Solution and Result.

External SMT-Solvers responses are parsed into these types.

Synopsis

Result

data Result Source #

Results of check-sat commands.

Constructors

Unsat 
Unknown 
Sat 

Instances

Instances details
Show Result Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Eq Result Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Methods

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

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

Ord Result Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Solution

class Ord (HaskellType t) => OrdHaskellType t Source #

Alias class for constraint Ord (HaskellType t)

Instances

Instances details
Ord (HaskellType t) => OrdHaskellType t Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

type SomeKnownOrdSMTSort f = Somes1 '[(~) f] '[KnownSMTSort, OrdHaskellType] Source #

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

IntValueMap

newtype IntValueMap t Source #

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

Constructors

IntValueMap (IntMap (Value t)) 

Instances

Instances details
Monoid (IntValueMap t) Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Semigroup (IntValueMap t) Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Show (Value t) => Show (IntValueMap t) Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

SMTVarVol

Type

data SMTVarSol (t :: SMTSort) Source #

A solution for a single variable.

Constructors

SMTVarSol 

Fields

Instances

Instances details
Show (Value t) => Show (SMTVarSol t) Source # 
Instance details

Defined in Language.Hasmtlib.Type.Solution

Lens

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

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