Language.SMTLib2.Internals.Backend

Documentation

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

mapAction :: Backend b => (r -> r') -> SMTAction b r -> SMTAction b r'

class (Typeable b, Functor (SMTMonad b), Monad (SMTMonad b), GetType (Expr b), GetType (Var b), GetType (QVar b), GetFunType (Fun b), GetType (FunArg b), GetType (LVar b), Typeable (Expr b), Typeable (Var b), Typeable (QVar b), Typeable (Fun 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 (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

A backend represents a specific type of SMT solver.

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 :: * -> *

The monad in which the backend executes queries.

data Expr b :: Type -> *

The internal type of expressions.

type Var b :: Type -> *

The internal type of variables.

type QVar b :: Type -> *

The internal type of quantified variables.

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

The internal type of user-defined functions.

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 t)

getModel :: SMTAction b (Model b)

modelEvaluate :: Model b -> Expr b t -> SMTAction b (Value 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) (FunArg b) (LVar b) (Expr b) t -> SMTAction b (Expr b t)

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

declareDatatypes :: [AnyDatatype] -> SMTAction b ()

interpolate :: SMTAction b (Expr b BoolType)

exit :: SMTAction b ()

data Partition

The interpolation partition

Constructors

PartitionA

PartitionB

Instances

Eq Partition

Methods

(==) :: Partition -> Partition -> Bool

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

Ord Partition

Methods

compare :: Partition -> Partition -> Ordering

(<) :: Partition -> Partition -> Bool

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

(>) :: Partition -> Partition -> Bool

(>=) :: Partition -> Partition -> Bool

max :: Partition -> Partition -> Partition

min :: Partition -> Partition -> Partition

Show Partition

Methods

showsPrec :: Int -> Partition -> ShowS

show :: Partition -> String

showList :: [Partition] -> ShowS

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

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

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

Ord CheckSatResult

Methods

compare :: CheckSatResult -> CheckSatResult -> Ordering

(<) :: CheckSatResult -> CheckSatResult -> Bool

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

(>) :: CheckSatResult -> CheckSatResult -> Bool

(>=) :: CheckSatResult -> CheckSatResult -> Bool

max :: CheckSatResult -> CheckSatResult -> CheckSatResult

min :: CheckSatResult -> CheckSatResult -> CheckSatResult

Show CheckSatResult

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

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

Methods

(==) :: CheckSatLimits -> CheckSatLimits -> Bool

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

Ord CheckSatLimits

Methods

compare :: CheckSatLimits -> CheckSatLimits -> Ordering

(<) :: CheckSatLimits -> CheckSatLimits -> Bool

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

(>) :: CheckSatLimits -> CheckSatLimits -> Bool

(>=) :: CheckSatLimits -> CheckSatLimits -> Bool

max :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

min :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

Show CheckSatLimits

Methods

showsPrec :: Int -> CheckSatLimits -> ShowS

show :: CheckSatLimits -> String

showList :: [CheckSatLimits] -> ShowS

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)

Methods

showsPrec :: Int -> AssignmentModel b -> ShowS

show :: AssignmentModel b -> String

showList :: [AssignmentModel b] -> ShowS

data Assignment b

Constructors

VarAssignment (Var b t) (Expr b 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)

Methods

showsPrec :: Int -> Assignment b -> ShowS

show :: Assignment b -> String

showList :: [Assignment b] -> ShowS

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

Methods

(==) :: SMTOption -> SMTOption -> Bool

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

Ord SMTOption

Methods

compare :: SMTOption -> SMTOption -> Ordering

(<) :: SMTOption -> SMTOption -> Bool

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

(>) :: SMTOption -> SMTOption -> Bool

(>=) :: SMTOption -> SMTOption -> Bool

max :: SMTOption -> SMTOption -> SMTOption

min :: SMTOption -> SMTOption -> SMTOption

Show SMTOption

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS

data SMTInfo i where

Solver information query type. Used with getInfo.

Constructors

SMTSolverName :: SMTInfo String

SMTSolverVersion :: SMTInfo String

data UntypedVar v t

Constructors

UntypedVar v (Repr t)

Instances

Ord v => GCompare Type (UntypedVar v)

Methods

gcompare :: f a -> f b -> GOrdering (UntypedVar v) a b

Eq v => GEq Type (UntypedVar v)

Methods

geq :: f a -> f b -> Maybe ((UntypedVar v := a) b)

Show v => GShow Type (UntypedVar v)

Methods

gshowsPrec :: Int -> t a -> ShowS

GetType (UntypedVar v)

Methods

getType :: UntypedVar v tp -> Repr tp

Eq v => Eq (UntypedVar v t)

Methods

(==) :: UntypedVar v t -> UntypedVar v t -> Bool

(/=) :: UntypedVar v t -> UntypedVar v t -> Bool

Ord v => Ord (UntypedVar v t)

Methods

compare :: UntypedVar v t -> UntypedVar v t -> Ordering

(<) :: UntypedVar v t -> UntypedVar v t -> Bool

(<=) :: UntypedVar v t -> UntypedVar v t -> Bool

(>) :: UntypedVar v t -> UntypedVar v t -> Bool

(>=) :: UntypedVar v t -> UntypedVar v t -> Bool

max :: UntypedVar v t -> UntypedVar v t -> UntypedVar v t

min :: UntypedVar v t -> UntypedVar v t -> UntypedVar v t

Show v => Show (UntypedVar v t)

Methods

showsPrec :: Int -> UntypedVar v t -> ShowS

show :: UntypedVar v t -> String

showList :: [UntypedVar v t] -> ShowS

data UntypedFun v sig where

Constructors

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

Instances

GetFunType (UntypedFun v)

Methods

getFunType :: UntypedFun v (([Type], Type) arg res) -> (List Type Repr arg, Repr res)

Eq v => Eq (UntypedFun v sig)

Methods

(==) :: UntypedFun v sig -> UntypedFun v sig -> Bool

(/=) :: UntypedFun v sig -> UntypedFun v sig -> Bool

Ord v => Ord (UntypedFun v sig)

Methods

compare :: UntypedFun v sig -> UntypedFun v sig -> Ordering

(<) :: UntypedFun v sig -> UntypedFun v sig -> Bool

(<=) :: UntypedFun v sig -> UntypedFun v sig -> Bool

(>) :: UntypedFun v sig -> UntypedFun v sig -> Bool

(>=) :: UntypedFun v sig -> UntypedFun v sig -> Bool

max :: UntypedFun v sig -> UntypedFun v sig -> UntypedFun v sig

min :: UntypedFun v sig -> UntypedFun v sig -> UntypedFun v sig

Show v => Show (UntypedFun v sig)

Methods

showsPrec :: Int -> UntypedFun v sig -> ShowS

show :: UntypedFun v sig -> String

showList :: [UntypedFun v sig] -> ShowS

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

Methods

gcompare :: f a -> f b -> GOrdering (UntypedFun v) a b

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

Methods

geq :: f a -> f b -> Maybe ((UntypedFun v := a) b)

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

Methods

gshowsPrec :: Int -> t a -> ShowS

data RenderedSubExpr t

Constructors

RenderedSubExpr (Int -> ShowS)

Instances

GShow k (RenderedSubExpr k)

Methods

gshowsPrec :: Int -> t a -> ShowS

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