Z3.Painless

A facade for Monad.

Documentation

class Z3Symbol a where

Methods

symbol :: MonadZ3 z3 => a -> z3 Symbol

Instances

Z3Symbol Int

Z3Symbol Integer

Z3Symbol [Char]

data Ty

Constructors

TyBool

TyInt

TyReal

TyBv !Int

TyUn !Symbol

Sort !Sort

ty2sort :: MonadZ3 z3 => Ty -> z3 Sort

const :: (MonadZ3 z3, Z3Symbol n) => Ty -> n -> z3 AST

script :: Z3 ()