Language.SMTLib2

Example usage: This program tries to find two numbers greater than zero which sum up to 5.

import Language.SMTLib2
import Language.SMTLib2.Solver

program :: SMT (Integer,Integer)
program = do
  x <- var
  y <- var
  assert $ (plus [x,y]) .==. (constant 5)
  assert $ x .>. (constant 0)
  assert $ y .>. (constant 0)
  checkSat
  vx <- getValue x
  vy <- getValue y
  return (vx,vy)

main = withZ3 program >>= print
     

SMT Monad

data Backend b => SMT b a

Instances

Backend b => Monad (SMT b)

Backend b => Functor (SMT b)

Backend b => Applicative (SMT b)

(Backend b, MonadIO (SMTMonad b)) => MonadIO (SMT b)

(Backend b, (~) (Type -> *) e (Expr b)) => Embed (SMT b) e

Backend b => MonadState (SMTState b) (SMT b)

type EmVar (SMT b) e = Var b

type EmQVar (SMT b) e = QVar b

type EmFun (SMT b) e = Fun b

type EmConstr (SMT b) e = Constr b

type EmField (SMT b) e = Field b

type EmFunArg (SMT b) e = FunArg b

type EmLVar (SMT b) e = LVar 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

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 Expr b :: Type -> *

type ClauseId b :: *

type Model b :: *

withBackend :: Backend b => SMTMonad b b -> SMT b a -> SMTMonad b a

withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a

Setting options

setOption :: Backend b => SMTOption -> SMT 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

Getting informations about the solver

getInfo :: Backend b => SMTInfo i -> SMT b i

data SMTInfo i where

Constructors

SMTSolverName :: SMTInfo String

SMTSolverVersion :: SMTInfo String

Expressions

expr :: QuasiQuoter

This quasiquoter can be used to generate SMTLib2 expressions or pattern matches. For example, to assert the fact that variable x is equal to variable y we can use

[expr| (= x y) |] >>= assert

To perform pattern matching against an expression e, we can use:

analyze e >>= \re -> case re of
  [expr| (+ x y) |] -> ...

Types can also be generated using for example:

myExpr :: Backend b => SMT b (Expr b [expr| (Array Int Bool) |])
myExpr = [expr| ((as const (Array Int Bool)) False) |]

Declaring variables

declare :: QuasiQuoter

declareVar :: Backend b => Repr t -> SMT b (Expr b t)

declareVarNamed :: Backend b => Repr t -> String -> SMT b (Expr b t)

Defining variables

define :: QuasiQuoter

defineVar :: Backend b => Expr b t -> SMT b (Expr b t)

defineVarNamed :: Backend b => String -> Expr b t -> SMT b (Expr b t)

defConst :: Backend b => Expr b t -> SMT b (Expr b t)

Declaring functions

declareFun :: Backend b => List Repr args -> Repr res -> SMT b (Fun b `(args, res)`)

declareFunNamed :: Backend b => List Repr args -> Repr res -> String -> SMT b (Fun b `(args, res)`)

Defining functions

defineFun :: Backend b => List Repr args -> (List (Expr b) args -> SMT b (Expr b res)) -> SMT b (Fun b `(args, res)`)

defineFunNamed :: Backend b => String -> List Repr args -> (List (Expr b) args -> SMT b (Expr b res)) -> SMT b (Fun b `(args, res)`)

Constants

constant :: Backend b => ConcreteValue t -> SMT b (Expr b t)

data ConcreteValue a where

Constructors

BoolValueC :: Bool -> ConcreteValue BoolType

IntValueC :: Integer -> ConcreteValue IntType

RealValueC :: Rational -> ConcreteValue RealType

BitVecValueC :: Integer -> Natural n -> ConcreteValue (BitVecType n)

ConstrValueC :: IsDatatype t => t -> ConcreteValue (DataType t)

Instances

GetType ConcreteValue

GCompare Type ConcreteValue

GEq Type ConcreteValue

GShow Type ConcreteValue

Show (ConcreteValue t)

Boolean constants

pattern ConstBool :: (~) Type rtp BoolType => Bool -> Expression v qv fun con field fv lv e rtp

cbool :: Embed m e => Bool -> m (e BoolType)

true :: Embed m e => m (e BoolType)

false :: Embed m e => m (e BoolType)

Integer constants

pattern ConstInt :: (~) Type rtp IntType => Integer -> Expression v qv fun con field fv lv e rtp

cint :: Embed m e => Integer -> m (e IntType)

Real constants

pattern ConstReal :: (~) Type rtp RealType => Rational -> Expression v qv fun con field fv lv e rtp

creal :: Embed m e => Rational -> m (e RealType)

Bitvector constants

pattern ConstBV :: (~) Type rtp (BitVecType bw) => Integer -> Natural bw -> Expression v qv fun con field fv lv e rtp

cbv :: Embed m e => Integer -> Natural bw -> m (e (BitVecType bw))

Functions

pattern Fun :: (~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type arg res) => t ((,) [Type] Type arg res) -> List Type t arg -> Expression t t t t t t t t t

fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e `(args, res)` -> a -> m (e res)

Equality

pattern EqLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp

pattern Eq :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:==:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

pattern DistinctLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp

pattern Distinct :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:/=:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

Map

map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e), GetFieldType (EmField m e), GetConType (EmConstr m e)) => Function (EmFun m e) (EmConstr m e) (EmField m e) `(tps, res)` -> arg -> m (e (ArrayType idx res))

Comparison

pattern Ord :: ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:>=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:>:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:<=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:<:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType)

(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

Arithmetic

pattern ArithLst :: IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun con field fv lv e tp

pattern Arith :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun con field fv lv e tp

arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp)

pattern PlusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Plus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:+:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6

pattern MultLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Mult :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:*:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 7

pattern MinusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Minus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:-:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

pattern Neg :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> Expression v qv fun con field fv lv e tp

minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6

neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

pattern Div :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

pattern Mod :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

pattern Rem :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

pattern (:/:) :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType) infixl 7

pattern Abs :: IsSMTNumber tp => e tp -> Expression v qv fun con field fv lv e tp

abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

Logic

pattern Not :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)

pattern LogicLst :: (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Logic :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun con field fv lv e rtp

logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)

pattern AndLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern And :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:&:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 3

pattern OrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Or :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:|:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2

pattern XOrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern XOr :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

pattern ImpliesLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Implies :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:=>:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2

Conversion

pattern ToReal :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

pattern ToInt :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType)

toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType)

If-then-else

pattern ITE :: () => GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun con field fv lv e tp

ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp)

Bitvectors

pattern BVComp :: (~) Type rtp BoolType => GetType e => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVULE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVULT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSLE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSLT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType)

bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

pattern BVBin :: (~) Type rtp (BitVecType bw) => GetType e => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVAdd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSub :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVMul :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVURem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSRem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSHL :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVLSHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVASHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVXor :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVAnd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVOr :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw))

bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

pattern BVUn :: (~) Type rtp (BitVecType bw) => GetType e => BVUnOp -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVNot :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVNeg :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw))

bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))

bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))

pattern Concat :: (~) Type rtp (BitVecType ((+) n1 n2)) => GetType e => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun con field fv lv e rtp

pattern Extract :: ((~) Type rtp (BitVecType len), (~) Bool ((<=) ((+) start len) bw) True) => GetType e => Natural start -> Natural len -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2)))

extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), ((start + len) <= bw) ~ True) => Natural start -> Natural len -> a -> m (e (BitVecType len))

Arrays

pattern Select :: (~) Type rtp val => GetType e => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun con field fv lv e rtp

pattern Store :: (~) Type rtp (ArrayType idx val) => GetType e => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun con field fv lv e rtp

pattern ConstArray :: (~) Type rtp (ArrayType idx val) => GetType e => List Type Repr idx -> e val -> Expression v qv fun con field fv lv e rtp

select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el)

select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType `[idx']` el), MonadResult idx ~ e idx') => arr -> idx -> m (e el)

store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el))

store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType `[idx']` el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType `[idx']` el'))

constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))

Misc

pattern Divisible :: (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun con field fv lv e rtp

divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)

Analyzation

data AnalyzedExpr i e tp

analyze :: Backend b => Expr b tp -> SMT b (AnalyzedExpr (BackendInfo b) (Expr b) tp)

getExpr :: Backend b => Expr b tp -> SMT b (Expression (Var b) (QVar b) (Fun b) (Constr b) (Field b) (FunArg b) (LVar b) (Expr b) tp)

Satisfiability

assert :: Backend b => Expr b BoolType -> SMT b ()

Asserts a boolean expression to be true. A successive successful checkSat calls mean that the generated model is consistent with the assertion.

checkSat :: Backend b => SMT b CheckSatResult

Checks if the set of asserted expressions is satisfiable.

checkSatWith :: Backend b => Maybe Tactic -> CheckSatLimits -> SMT b CheckSatResult

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

noLimits :: CheckSatLimits

Unsatisfiable core

assertId :: Backend b => Expr b BoolType -> SMT b (ClauseId b)

Works like assert, but additionally allows the user to find the unsatisfiable core of a set of assignments using getUnsatCore.

getUnsatCore :: Backend b => SMT b [ClauseId b]

Interpolation

assertPartition :: Backend b => Expr b BoolType -> Partition -> SMT b ()

data Partition

The interpolation partition

Constructors

PartitionA

PartitionB

Instances

Eq Partition

Ord Partition

Show Partition

getInterpolant :: Backend b => SMT b (Expr b BoolType)

Proofs

getProof :: Backend b => SMT b (Proof b)

analyzeProof :: Backend b => Proof b -> SMT b (Proof String (Expr b) (Proof b))

Stack

push :: Backend b => SMT b ()

pop :: Backend b => SMT b ()

stack :: Backend b => SMT b a -> SMT b a

Models

getValue :: Backend b => Expr b t -> SMT b (ConcreteValue t)

getModel :: Backend b => SMT b (Model b)

After a successful checkSat query, return a satisfying assignment that makes all asserted formula true.

modelEvaluate :: Backend b => Model b -> Expr b t -> SMT b (ConcreteValue t)

Evaluate an expression in a model, yielding a concrete value.

Types

registerDatatype :: (Backend b, IsDatatype dt) => Proxy dt -> SMT b ()

data Type

Describes the kind of all SMT types. It is only used in promoted form, for a concrete representation see Repr.

Constructors

BoolType

IntType

RealType

BitVecType Nat

ArrayType [Type] Type

forall a . DataType a

Instances

GCompare Type NumRepr

GCompare Type Repr

GCompare Type ConcreteValue

GCompare Type NoVar

GEq Type NumRepr

GEq Type Repr

GEq Type ConcreteValue

GEq Type NoVar

GShow Type NumRepr

GShow Type Repr

GShow Type ConcreteValue

GShow Type NoVar

GCompare ((,) [Type] *) con => GCompare Type (Value con)

Ord v => GCompare Type (UntypedVar v)

GEq ((,) [Type] *) con => GEq Type (Value con)

Eq v => GEq Type (UntypedVar v)

GShow ((,) [Type] *) con => GShow Type (Value con)

Show v => GShow Type (UntypedVar v)

(GCompare Type v, GCompare Type e) => GCompare Type (LetBinding v e)

(GEq Type v, GEq Type e) => GEq Type (LetBinding v e)

(GCompare Type v, GCompare Type qv, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type fv, GCompare Type lv, GCompare Type e) => GCompare Type (Expression v qv fun con field fv lv e)

(GEq Type v, GEq Type qv, GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field, GEq Type fv, GEq Type lv, GEq Type e) => GEq Type (Expression v qv fun con field fv lv e)

(GShow Type v, GShow Type qv, GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field, GShow Type fv, GShow Type lv, GShow Type e) => GShow Type (Expression v qv fun con field fv lv e)

HasMonad (m (List Type e tp))

GCompare ((,) [Type] *) NoCon

GCompare ((,) [Type] Type) FunRepr

GCompare ((,) [Type] Type) NoFun

GCompare ((,) * Type) NoField

GEq ((,) [Type] *) NoCon

GEq ((,) [Type] Type) FunRepr

GEq ((,) [Type] Type) NoFun

GEq ((,) * Type) NoField

GShow ((,) [[Type]] *) Datatype

GShow ((,) [Type] *) NoCon

GShow ((,) [Type] Type) NoFun

GShow ((,) * Type) NoField

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

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

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

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

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

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

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

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

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

(GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field) => GCompare ((,) [Type] Type) (Function fun con field)

(GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field) => GEq ((,) [Type] Type) (Function fun con field)

(GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field) => GShow ((,) [Type] Type) (Function fun con field)

HasMonad (List Type e tp)

(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps))

Same ((:) Type tp ([] Type))

Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx

Unlift ((:) Type tp ([] Type)) idx

type MonadResult (m (List Type e tp)) = List Type e tp

type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'

type MonadResult (List Type e tp) = List Type e tp

type MatchMonad (List Type e tp) m = ()

data Repr t where

A concrete representation of an SMT type. For aesthetic reasons, it's recommended to use the functions bool, int, real, bitvec or array.

Constructors

BoolRepr :: Repr BoolType

IntRepr :: Repr IntType

RealRepr :: Repr RealType

BitVecRepr :: Natural n -> Repr (BitVecType n)

ArrayRepr :: List Repr idx -> Repr val -> Repr (ArrayType idx val)

DataRepr :: IsDatatype dt => Datatype `(DatatypeSig dt, dt)` -> Repr (DataType dt)

Instances

GetType Repr

GCompare Type Repr

GEq Type Repr

GShow Type Repr

Eq (Repr tp)

Ord (Repr tp)

Show (Repr t)

class GetType v where

Methods

getType :: v tp -> Repr tp

Instances

GetType Repr

GetType ConcreteValue

GetType NoVar

GetType (Value con)

GetType (UntypedVar v)

(GetType var, GetType qvar, GetFunType fun, GetConType con, GetFieldType field, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun con field farg lvar)

(GetType v, GetType qv, GetFunType fun, GetConType con, GetFieldType field, GetType fv, GetType lv, GetType e) => GetType (Expression v qv fun con field fv lv e)

reifyType :: Type -> (forall tp. Repr tp -> a) -> a

Get a concrete representation for a type.

bool :: Repr BoolType

A representation of the SMT Bool type. Holds the values true or false.

int :: Repr IntType

real :: Repr RealType

bitvec :: Natural bw -> Repr (BitVecType bw)

array :: List Repr idx -> Repr el -> Repr (ArrayType idx el)

Numbers

data Nat

Constructors

Z

S Nat

Instances

Enum Nat

Eq Nat

Integral Nat

Num Nat

Ord Nat

Real Nat

GCompare Nat Natural

GEq Nat Natural

GShow Nat Natural

data Natural n where

Constructors

Zero :: Natural Z

Succ :: Natural n -> Natural (S n)

Instances

GCompare Nat Natural

GEq Nat Natural

GShow Nat Natural

Eq (Natural n)

Ord (Natural n)

Show (Natural n)

nat :: (Num a, Ord a) => a -> ExpQ

reifyNat :: Nat -> (forall n. Natural n -> r) -> r

Lists

data List e tp where

Constructors

Nil :: List e `[]`

(:::) :: e x -> List e xs -> List e (x : xs) infixr 9

Instances

HasMonad (m (List Type e tp))

GCompare k e => GCompare [k] (List k e)

GEq k e => GEq [k] (List k e)

GShow k e => GShow [k] (List k e)

GEq k e => Eq (List k e lst)

GCompare k e => Ord (List k e lst)

GShow k e => Show (List k e lst)

HasMonad (List Type e tp)

type MonadResult (m (List Type e tp)) = List Type e tp

type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'

type MonadResult (List Type e tp) = List Type e tp

type MatchMonad (List Type e tp) m = ()

list :: [ExpQ] -> ExpQ

reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r

list1 :: e t1 -> List e `[t1]`

list2 :: e t1 -> e t2 -> List e `[t1, t2]`

list3 :: e t1 -> e t2 -> e t3 -> List e `[t1, t2, t3]`

(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Monad m) => a -> m (List e tps) -> m (List e (tp : tps)) infixr 5

nil :: Monad m => m (List e `[]`)

Misc

comment :: Backend b => String -> SMT b ()

simplify :: Backend b => Expr b tp -> SMT b (Expr b tp)

Use the SMT solver to simplify a given expression.