Language.SMTLib2.Internals.Backend

Documentation

type SMTAction b r = b -> SMTMonad b (r, b)

class (Typeable b, Functor (SMTMonad b), Monad (SMTMonad b), GetType (Expr b), GetType (Var b), GetType (QVar b), GetFunType (Fun b), GetConType (Constr b), GetFieldType (Field b), GetType (FunArg b), GetType (LVar b), Typeable (Expr b), Typeable (Var b), Typeable (QVar b), Typeable (Fun b), Typeable (Constr b), Typeable (Field b), Typeable (FunArg b), Typeable (LVar b), Typeable (ClauseId b), GCompare (Expr b), GShow (Expr b), GCompare (Var b), GShow (Var b), GCompare (QVar b), GShow (QVar b), GCompare (Fun b), GShow (Fun b), GCompare (Constr b), GShow (Constr b), GCompare (Field b), GShow (Field b), GCompare (FunArg b), GShow (FunArg b), GCompare (LVar b), GShow (LVar b), Ord (ClauseId b), Show (ClauseId b), Ord (Proof b), Show (Proof b), Show (Model b)) => Backend b where

Minimal complete definition

setOption, getInfo, push, pop, declareVar, createQVar, createFunArg, defineVar, declareFun, defineFun, assert, assertId, assertPartition, checkSat, getUnsatCore, getValue, getModel, modelEvaluate, getProof, analyzeProof, simplify, toBackend, fromBackend, declareDatatypes, interpolate, exit

Associated Types

type SMTMonad b :: * -> *

type Expr b :: Type -> *

type Var b :: Type -> *

type QVar b :: Type -> *

type Fun b :: ([Type], Type) -> *

type Constr b :: ([Type], *) -> *

type Field b :: (*, Type) -> *

type FunArg b :: Type -> *

type LVar b :: Type -> *

type ClauseId b :: *

type Model b :: *

type Proof b :: *

Methods

setOption :: SMTOption -> SMTAction b ()

getInfo :: SMTInfo i -> SMTAction b i

comment :: String -> SMTAction b ()

push :: SMTAction b ()

pop :: SMTAction b ()

declareVar :: Repr t -> Maybe String -> SMTAction b (Var b t)

createQVar :: Repr t -> Maybe String -> SMTAction b (QVar b t)

createFunArg :: Repr t -> Maybe String -> SMTAction b (FunArg b t)

defineVar :: Maybe String -> Expr b t -> SMTAction b (Var b t)

declareFun :: List Repr arg -> Repr t -> Maybe String -> SMTAction b (Fun b `(arg, t)`)

defineFun :: Maybe String -> List (FunArg b) arg -> Expr b r -> SMTAction b (Fun b `(arg, r)`)

assert :: Expr b BoolType -> SMTAction b ()

assertId :: Expr b BoolType -> SMTAction b (ClauseId b)

assertPartition :: Expr b BoolType -> Partition -> SMTAction b ()

checkSat :: Maybe Tactic -> CheckSatLimits -> SMTAction b CheckSatResult

getUnsatCore :: SMTAction b [ClauseId b]

getValue :: Expr b t -> SMTAction b (Value (Constr b) t)

getModel :: SMTAction b (Model b)

modelEvaluate :: Model b -> Expr b t -> SMTAction b (Value (Constr b) t)

getProof :: SMTAction b (Proof b)

analyzeProof :: b -> Proof b -> Proof String (Expr b) (Proof b)

simplify :: Expr b t -> SMTAction b (Expr b t)

toBackend :: Expression (Var b) (QVar b) (Fun b) (Constr b) (Field b) (FunArg b) (LVar b) (Expr b) t -> SMTAction b (Expr b t)

fromBackend :: b -> Expr b t -> Expression (Var b) (QVar b) (Fun b) (Constr b) (Field b) (FunArg b) (LVar b) (Expr b) t

declareDatatypes :: TypeCollection sigs -> SMTAction b (BackendTypeCollection (Constr b) (Field b) sigs)

interpolate :: SMTAction b (Expr b BoolType)

exit :: SMTAction b ()

type BackendTypeCollection con field sigs = Datatypes (BackendDatatype con field) sigs

newtype BackendDatatype con field sig

Constructors

BackendDatatype

Fields

bconstructors :: Constrs (BackendConstr con field) (Fst sig) (Snd sig)

data BackendConstr con field sig

Constructors

BackendConstr

Fields

bconName :: String

bconRepr :: con sig

bconFields :: List (BackendField field (Snd sig)) (Fst sig)

bconstruct :: List ConcreteValue (Fst sig) -> Snd sig

bconTest :: Snd sig -> Bool

data BackendField field dt t

Constructors

BackendField

Fields

bfieldName :: String

bfieldRepr :: field `(dt, t)`

bfieldType :: Repr t

bfieldGet :: dt -> ConcreteValue t

data Partition

The interpolation partition

Constructors

PartitionA

PartitionB

Instances

Eq Partition

Ord Partition

Show Partition

data CheckSatResult

The result of a check-sat query

Constructors

Sat

The formula is satisfiable

Unsat

The formula is unsatisfiable

Unknown

The solver cannot determine the satisfiability of a formula

Instances

Eq CheckSatResult

Ord CheckSatResult

Show CheckSatResult

data CheckSatLimits

Describe limits on the ressources that an SMT-solver can use

Constructors

CheckSatLimits

Fields

limitTime :: Maybe Integer

A limit on the amount of time the solver can spend on the problem (in milliseconds)

limitMemory :: Maybe Integer

A limit on the amount of memory the solver can use (in megabytes)

Instances

Eq CheckSatLimits

Ord CheckSatLimits

Show CheckSatLimits

newtype AssignmentModel b

Constructors

AssignmentModel

Fields

assignments :: [Assignment b]

Instances

(GShow Type (Var b), GShow Type (Expr b), GShow ((,) [Type] Type) (Fun b), GShow Type (FunArg b)) => Show (AssignmentModel b)

data Assignment b

Constructors

forall t . VarAssignment (Var b t) (Expr b t)

forall arg t . FunAssignment (Fun b `(arg, t)`) (List (FunArg b) arg) (Expr b t)

Instances

(GShow Type (Var b), GShow Type (Expr b), GShow ((,) [Type] Type) (Fun b), GShow Type (FunArg b)) => Show (Assignment b)

data SMTOption

Options controling the behaviour of the SMT solver

Constructors

PrintSuccess Bool

Whether or not to print "success" after each operation

ProduceModels Bool

Produce a satisfying assignment after each successful checkSat

ProduceProofs Bool

Produce a proof of unsatisfiability after each failed checkSat

ProduceUnsatCores Bool

Enable the querying of unsatisfiable cores after a failed checkSat

ProduceInterpolants Bool

Enable the generation of craig interpolants

SMTLogic String

Instances

Eq SMTOption

Ord SMTOption

Show SMTOption

data SMTInfo i where

Constructors

SMTSolverName :: SMTInfo String

SMTSolverVersion :: SMTInfo String

data UntypedVar v t

Constructors

UntypedVar v (Repr t)

Instances

Ord v => GCompare Type (UntypedVar v)

Eq v => GEq Type (UntypedVar v)

Show v => GShow Type (UntypedVar v)

GetType (UntypedVar v)

Eq v => Eq (UntypedVar v t)

Ord v => Ord (UntypedVar v t)

Show v => Show (UntypedVar v t)

data UntypedFun v sig where

Constructors

UntypedFun :: v -> List Repr arg -> Repr ret -> UntypedFun v `(arg, ret)`

Instances

GetFunType (UntypedFun v)

Eq v => Eq (UntypedFun v sig)

Ord v => Ord (UntypedFun v sig)

Show v => Show (UntypedFun v sig)

Ord v => GCompare ((,) [Type] Type) (UntypedFun v)

Eq v => GEq ((,) [Type] Type) (UntypedFun v)

Show v => GShow ((,) [Type] Type) (UntypedFun v)

data UntypedCon v sig where

Constructors

UntypedCon :: IsDatatype dt => v -> List Repr arg -> Proxy dt -> UntypedCon v `(arg, dt)`

Instances

GetConType (UntypedCon v)

Eq v => Eq (UntypedCon v sig)

Ord v => Ord (UntypedCon v sig)

Show v => Show (UntypedCon v sig)

Ord v => GCompare ((,) [Type] *) (UntypedCon v)

Eq v => GEq ((,) [Type] *) (UntypedCon v)

Show v => GShow ((,) [Type] *) (UntypedCon v)

data UntypedField v sig where

Constructors

UntypedField :: IsDatatype dt => v -> Proxy dt -> Repr t -> UntypedField v `(dt, t)`

Instances

GetFieldType (UntypedField v)

Eq v => Eq (UntypedField v sig)

Ord v => Ord (UntypedField v sig)

Show v => Show (UntypedField v sig)

Ord v => GCompare ((,) * Type) (UntypedField v)

Eq v => GEq ((,) * Type) (UntypedField v)

Show v => GShow ((,) * Type) (UntypedField v)

data RenderedSubExpr t

Constructors

RenderedSubExpr (Int -> ShowS)

Instances

GShow k (RenderedSubExpr k)

showsBackendExpr :: Backend b => b -> Int -> Expr b t -> ShowS