Copyright	(c) Iago Abal 2012-2015 (c) David Castro 2012-2015
License	BSD3
Maintainer	Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Safe Haskell	None
Language	Haskell98

Z3.Base

Contents

Types
- Satisfiability result
Create configuration
- Helpers
Create context
Parameters
Symbols
Sorts
Constants and Applications
- Helpers
Propositional Logic and Equality
- Helpers
Arithmetic: Integers and Reals
Bit-vectors
Arrays
Sets
Numerals
- Helpers
Quantifiers
Accessors
- Helpers
Modifiers
Models
- Helpers
Tactics
String Conversion
Parser interface
Error Handling
Miscellaneous
Fixedpoint
Solvers
- Helpers

Description

Low-level bindings to Z3 API.

There is (mostly) a one-to-one correspondence with Z3 C API, thus see http://z3prover.github.io/api/html/group__capi.html for further details.

Synopsis

data Config
data Context
data Symbol
data AST
data Sort
data FuncDecl
data App
data Pattern
data Constructor
data Model
data FuncInterp
data FuncEntry
data Params
data Solver
data SortKind
- = Z3_UNINTERPRETED_SORT
- | Z3_BOOL_SORT
- | Z3_INT_SORT
- | Z3_REAL_SORT
- | Z3_BV_SORT
- | Z3_ARRAY_SORT
- | Z3_DATATYPE_SORT
- | Z3_RELATION_SORT
- | Z3_FINITE_DOMAIN_SORT
- | Z3_FLOATING_POINT_SORT
- | Z3_ROUNDING_MODE_SORT
- | Z3_UNKNOWN_SORT
data ASTKind
- = Z3_NUMERAL_AST
- | Z3_APP_AST
- | Z3_VAR_AST
- | Z3_QUANTIFIER_AST
- | Z3_SORT_AST
- | Z3_FUNC_DECL_AST
- | Z3_UNKNOWN_AST
data Tactic
data ApplyResult
data Goal
data Result
- = Sat
- | Unsat
- | Undef
mkConfig :: IO Config
delConfig :: Config -> IO ()
setParamValue :: Config -> String -> String -> IO ()
withConfig :: (Config -> IO a) -> IO a
mkContext :: Config -> IO Context
withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r
mkParams :: Context -> IO Params
paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO ()
paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
paramsToString :: Context -> Params -> IO String
mkIntSymbol :: Integral int => Context -> int -> IO Symbol
mkStringSymbol :: Context -> String -> IO Symbol
mkUninterpretedSort :: Context -> Symbol -> IO Sort
mkBoolSort :: Context -> IO Sort
mkIntSort :: Context -> IO Sort
mkRealSort :: Context -> IO Sort
mkBvSort :: Integral int => Context -> int -> IO Sort
mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort
mkArraySort :: Context -> Sort -> Sort -> IO Sort
mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
mkConstructor :: Context -> Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> IO Constructor
mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort
mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort]
mkSetSort :: Context -> Sort -> IO Sort
mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
mkApp :: Context -> FuncDecl -> [AST] -> IO AST
mkConst :: Context -> Symbol -> Sort -> IO AST
mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl
mkFreshConst :: Context -> String -> Sort -> IO AST
mkVar :: Context -> Symbol -> Sort -> IO AST
mkBoolVar :: Context -> Symbol -> IO AST
mkRealVar :: Context -> Symbol -> IO AST
mkIntVar :: Context -> Symbol -> IO AST
mkBvVar :: Context -> Symbol -> Int -> IO AST
mkFreshVar :: Context -> String -> Sort -> IO AST
mkFreshBoolVar :: Context -> String -> IO AST
mkFreshRealVar :: Context -> String -> IO AST
mkFreshIntVar :: Context -> String -> IO AST
mkFreshBvVar :: Context -> String -> Int -> IO AST
mkTrue :: Context -> IO AST
mkFalse :: Context -> IO AST
mkEq :: Context -> AST -> AST -> IO AST
mkNot :: Context -> AST -> IO AST
mkIte :: Context -> AST -> AST -> AST -> IO AST
mkIff :: Context -> AST -> AST -> IO AST
mkImplies :: Context -> AST -> AST -> IO AST
mkXor :: Context -> AST -> AST -> IO AST
mkAnd :: Context -> [AST] -> IO AST
mkOr :: Context -> [AST] -> IO AST
mkDistinct :: Context -> [AST] -> IO AST
mkBool :: Context -> Bool -> IO AST
mkAdd :: Context -> [AST] -> IO AST
mkMul :: Context -> [AST] -> IO AST
mkSub :: Context -> NonEmpty AST -> IO AST
mkUnaryMinus :: Context -> AST -> IO AST
mkDiv :: Context -> AST -> AST -> IO AST
mkMod :: Context -> AST -> AST -> IO AST
mkRem :: Context -> AST -> AST -> IO AST
mkLt :: Context -> AST -> AST -> IO AST
mkLe :: Context -> AST -> AST -> IO AST
mkGt :: Context -> AST -> AST -> IO AST
mkGe :: Context -> AST -> AST -> IO AST
mkInt2Real :: Context -> AST -> IO AST
mkReal2Int :: Context -> AST -> IO AST
mkIsInt :: Context -> AST -> IO AST
mkBvnot :: Context -> AST -> IO AST
mkBvredand :: Context -> AST -> IO AST
mkBvredor :: Context -> AST -> IO AST
mkBvand :: Context -> AST -> AST -> IO AST
mkBvor :: Context -> AST -> AST -> IO AST
mkBvxor :: Context -> AST -> AST -> IO AST
mkBvnand :: Context -> AST -> AST -> IO AST
mkBvnor :: Context -> AST -> AST -> IO AST
mkBvxnor :: Context -> AST -> AST -> IO AST
mkBvneg :: Context -> AST -> IO AST
mkBvadd :: Context -> AST -> AST -> IO AST
mkBvsub :: Context -> AST -> AST -> IO AST
mkBvmul :: Context -> AST -> AST -> IO AST
mkBvudiv :: Context -> AST -> AST -> IO AST
mkBvsdiv :: Context -> AST -> AST -> IO AST
mkBvurem :: Context -> AST -> AST -> IO AST
mkBvsrem :: Context -> AST -> AST -> IO AST
mkBvsmod :: Context -> AST -> AST -> IO AST
mkBvult :: Context -> AST -> AST -> IO AST
mkBvslt :: Context -> AST -> AST -> IO AST
mkBvule :: Context -> AST -> AST -> IO AST
mkBvsle :: Context -> AST -> AST -> IO AST
mkBvuge :: Context -> AST -> AST -> IO AST
mkBvsge :: Context -> AST -> AST -> IO AST
mkBvugt :: Context -> AST -> AST -> IO AST
mkBvsgt :: Context -> AST -> AST -> IO AST
mkConcat :: Context -> AST -> AST -> IO AST
mkExtract :: Context -> Int -> Int -> AST -> IO AST
mkSignExt :: Context -> Int -> AST -> IO AST
mkZeroExt :: Context -> Int -> AST -> IO AST
mkRepeat :: Context -> Int -> AST -> IO AST
mkBvshl :: Context -> AST -> AST -> IO AST
mkBvlshr :: Context -> AST -> AST -> IO AST
mkBvashr :: Context -> AST -> AST -> IO AST
mkRotateLeft :: Context -> Int -> AST -> IO AST
mkRotateRight :: Context -> Int -> AST -> IO AST
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
mkExtRotateRight :: Context -> AST -> AST -> IO AST
mkInt2bv :: Context -> Int -> AST -> IO AST
mkBv2int :: Context -> AST -> Bool -> IO AST
mkBvnegNoOverflow :: Context -> AST -> IO AST
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
mkSelect :: Context -> AST -> AST -> IO AST
mkStore :: Context -> AST -> AST -> AST -> IO AST
mkConstArray :: Context -> Sort -> AST -> IO AST
mkMap :: Context -> FuncDecl -> [AST] -> IO AST
mkArrayDefault :: Context -> AST -> IO AST
mkEmptySet :: Context -> Sort -> IO AST
mkFullSet :: Context -> Sort -> IO AST
mkSetAdd :: Context -> AST -> AST -> IO AST
mkSetDel :: Context -> AST -> AST -> IO AST
mkSetUnion :: Context -> [AST] -> IO AST
mkSetIntersect :: Context -> [AST] -> IO AST
mkSetDifference :: Context -> AST -> AST -> IO AST
mkSetComplement :: Context -> AST -> IO AST
mkSetMember :: Context -> AST -> AST -> IO AST
mkSetSubset :: Context -> AST -> AST -> IO AST
mkNumeral :: Context -> String -> Sort -> IO AST
mkReal :: Context -> Int -> Int -> IO AST
mkInt :: Context -> Int -> Sort -> IO AST
mkUnsignedInt :: Context -> Word -> Sort -> IO AST
mkInt64 :: Context -> Int64 -> Sort -> IO AST
mkUnsignedInt64 :: Context -> Word64 -> Sort -> IO AST
mkIntegral :: Integral a => Context -> a -> Sort -> IO AST
mkRational :: Context -> Rational -> IO AST
mkFixed :: HasResolution a => Context -> Fixed a -> IO AST
mkRealNum :: Real r => Context -> r -> IO AST
mkInteger :: Context -> Integer -> IO AST
mkIntNum :: Integral a => Context -> a -> IO AST
mkBitvector :: Context -> Int -> Integer -> IO AST
mkBvNum :: Integral i => Context -> Int -> i -> IO AST
mkPattern :: Context -> NonEmpty AST -> IO Pattern
mkBound :: Context -> Int -> Sort -> IO AST
mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkForallConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
mkExistsConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
getSymbolString :: Context -> Symbol -> IO String
getSortKind :: Context -> Sort -> IO SortKind
getBvSortSize :: Context -> Sort -> IO Int
getDatatypeSortConstructors :: Context -> Sort -> IO [FuncDecl]
getDatatypeSortRecognizers :: Context -> Sort -> IO [FuncDecl]
getDatatypeSortConstructorAccessors :: Context -> Sort -> IO [[FuncDecl]]
getDeclName :: Context -> FuncDecl -> IO Symbol
getArity :: Context -> FuncDecl -> IO Int
getDomain :: Context -> FuncDecl -> Int -> IO Sort
getRange :: Context -> FuncDecl -> IO Sort
appToAst :: Context -> App -> IO AST
getAppDecl :: Context -> App -> IO FuncDecl
getAppNumArgs :: Context -> App -> IO Int
getAppArg :: Context -> App -> Int -> IO AST
getAppArgs :: Context -> App -> IO [AST]
getSort :: Context -> AST -> IO Sort
getArraySortDomain :: Context -> Sort -> IO Sort
getArraySortRange :: Context -> Sort -> IO Sort
getBoolValue :: Context -> AST -> IO (Maybe Bool)
getAstKind :: Context -> AST -> IO ASTKind
isApp :: Context -> AST -> IO Bool
toApp :: Context -> AST -> IO App
getNumeralString :: Context -> AST -> IO String
simplify :: Context -> AST -> IO AST
simplifyEx :: Context -> AST -> Params -> IO AST
getIndexValue :: Context -> AST -> IO Int
isQuantifierForall :: Context -> AST -> IO Bool
isQuantifierExists :: Context -> AST -> IO Bool
getQuantifierWeight :: Context -> AST -> IO Int
getQuantifierNumPatterns :: Context -> AST -> IO Int
getQuantifierPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierPatterns :: Context -> AST -> IO [AST]
getQuantifierNumNoPatterns :: Context -> AST -> IO Int
getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierNoPatterns :: Context -> AST -> IO [AST]
getQuantifierNumBound :: Context -> AST -> IO Int
getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol
getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort
getQuantifierBoundVars :: Context -> AST -> IO [AST]
getQuantifierBody :: Context -> AST -> IO AST
getBool :: Context -> AST -> IO Bool
getInt :: Context -> AST -> IO Integer
getReal :: Context -> AST -> IO Rational
getBv :: Context -> AST -> Bool -> IO Integer
substituteVars :: Context -> AST -> [AST] -> IO AST
modelEval :: Context -> Model -> AST -> Bool -> IO (Maybe AST)
evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)
getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
hasInterp :: Context -> Model -> FuncDecl -> IO Bool
numConsts :: Context -> Model -> IO Word
numFuncs :: Context -> Model -> IO Word
getConstDecl :: Context -> Model -> Word -> IO FuncDecl
getFuncDecl :: Context -> Model -> Word -> IO FuncDecl
getConsts :: Context -> Model -> IO [FuncDecl]
getFuncs :: Context -> Model -> IO [FuncDecl]
isAsArray :: Context -> AST -> IO Bool
addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp
addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
funcInterpGetElse :: Context -> FuncInterp -> IO AST
funcInterpGetArity :: Context -> FuncInterp -> IO Int
funcEntryGetValue :: Context -> FuncEntry -> IO AST
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
modelToString :: Context -> Model -> IO String
showModel :: Context -> Model -> IO String
type EvalAst a = Model -> AST -> IO (Maybe a)
eval :: Context -> EvalAst AST
evalBool :: Context -> EvalAst Bool
evalInt :: Context -> EvalAst Integer
evalReal :: Context -> EvalAst Rational
evalBv :: Context -> Bool -> EvalAst Integer
mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
}
evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
mkTactic :: Context -> String -> IO Tactic
andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic
orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic
skipTactic :: Context -> IO Tactic
tryForTactic :: Context -> Tactic -> Int -> IO Tactic
mkQuantifierEliminationTactic :: Context -> IO Tactic
mkAndInverterGraphTactic :: Context -> IO Tactic
applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult
getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int
getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal
getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]
mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal
goalAssert :: Context -> Goal -> AST -> IO ()
getGoalSize :: Context -> Goal -> IO Int
getGoalFormula :: Context -> Goal -> Int -> IO AST
getGoalFormulas :: Context -> Goal -> IO [AST]
data ASTPrintMode
- = Z3_PRINT_SMTLIB_FULL
- | Z3_PRINT_LOW_LEVEL
- | Z3_PRINT_SMTLIB2_COMPLIANT
setASTPrintMode :: Context -> ASTPrintMode -> IO ()
astToString :: Context -> AST -> IO String
patternToString :: Context -> Pattern -> IO String
sortToString :: Context -> Sort -> IO String
funcDeclToString :: Context -> FuncDecl -> IO String
benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String
parseSMTLib2String :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
parseSMTLib2File :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
data Z3Error = Z3Error {
- errCode :: Z3ErrorCode
- errMsg :: String
}
data Z3ErrorCode
- = SortError
- | IOB
- | InvalidArg
- | ParserError
- | NoParser
- | InvalidPattern
- | MemoutFail
- | FileAccessError
- | InternalFatal
- | InvalidUsage
- | DecRefError
- | Z3Exception
data Version = Version {
- z3Major :: !Int
- z3Minor :: !Int
- z3Build :: !Int
- z3Revision :: !Int
}
getVersion :: IO Version
newtype Fixedpoint = Fixedpoint {
- unFixedpoint :: ForeignPtr Z3_fixedpoint
}
mkFixedpoint :: Context -> IO Fixedpoint
fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO ()
fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()
fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()
fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result
fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST
fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]
data Logic
- = AUFLIA
- | AUFLIRA
- | AUFNIRA
- | LRA
- | QF_ABV
- | QF_AUFBV
- | QF_AUFLIA
- | QF_AX
- | QF_BV
- | QF_IDL
- | QF_LIA
- | QF_LRA
- | QF_NIA
- | QF_NRA
- | QF_RDL
- | QF_UF
- | QF_UFBV
- | QF_UFIDL
- | QF_UFLIA
- | QF_UFLRA
- | QF_UFNRA
- | UFLRA
- | UFNIA
mkSolver :: Context -> IO Solver
mkSimpleSolver :: Context -> IO Solver
mkSolverForLogic :: Context -> Logic -> IO Solver
solverGetHelp :: Context -> Solver -> IO String
solverSetParams :: Context -> Solver -> Params -> IO ()
solverPush :: Context -> Solver -> IO ()
solverPop :: Context -> Solver -> Int -> IO ()
solverReset :: Context -> Solver -> IO ()
solverGetNumScopes :: Context -> Solver -> IO Int
solverAssertCnstr :: Context -> Solver -> AST -> IO ()
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
solverCheck :: Context -> Solver -> IO Result
solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result
solverGetModel :: Context -> Solver -> IO Model
solverGetUnsatCore :: Context -> Solver -> IO [AST]
solverGetReasonUnknown :: Context -> Solver -> IO String
solverToString :: Context -> Solver -> IO String
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)

Types

data Config Source #

A Z3 configuration object.

Instances

Instances details

Eq Config Source #
Instance details Defined in Z3.Base Methods (==) :: Config -> Config -> Bool # (/=) :: Config -> Config -> Bool #

data Context Source #

A Z3 logical context.

Instances

Instances details

Eq Context Source #
Instance details Defined in Z3.Base Methods (==) :: Context -> Context -> Bool # (/=) :: Context -> Context -> Bool #

data Symbol Source #

A Z3 symbol.

Used to name types, constants and functions.

Instances

Instances details

Eq Symbol Source #
Instance details Defined in Z3.Base Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol Source #
Instance details Defined in Z3.Base Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #
Show Symbol Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
Storable Symbol Source #
Instance details Defined in Z3.Base Methods sizeOf :: Symbol -> Int # alignment :: Symbol -> Int # peekElemOff :: Ptr Symbol -> Int -> IO Symbol # pokeElemOff :: Ptr Symbol -> Int -> Symbol -> IO () # peekByteOff :: Ptr b -> Int -> IO Symbol # pokeByteOff :: Ptr b -> Int -> Symbol -> IO () # peek :: Ptr Symbol -> IO Symbol # poke :: Ptr Symbol -> Symbol -> IO () #

data AST Source #

A Z3 AST node.

This is the data-structure used in Z3 to represent terms, formulas and types.

Instances

Instances details

Eq AST Source #
Instance details Defined in Z3.Base Methods (==) :: AST -> AST -> Bool # (/=) :: AST -> AST -> Bool #
Ord AST Source #
Instance details Defined in Z3.Base Methods compare :: AST -> AST -> Ordering # (<) :: AST -> AST -> Bool # (<=) :: AST -> AST -> Bool # (>) :: AST -> AST -> Bool # (>=) :: AST -> AST -> Bool # max :: AST -> AST -> AST # min :: AST -> AST -> AST #
Show AST Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> AST -> ShowS # show :: AST -> String # showList :: [AST] -> ShowS #

data Sort Source #

A kind of AST representing types.

Instances

Instances details

Eq Sort Source #
Instance details Defined in Z3.Base Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Ord Sort Source #
Instance details Defined in Z3.Base Methods compare :: Sort -> Sort -> Ordering # (<) :: Sort -> Sort -> Bool # (<=) :: Sort -> Sort -> Bool # (>) :: Sort -> Sort -> Bool # (>=) :: Sort -> Sort -> Bool # max :: Sort -> Sort -> Sort # min :: Sort -> Sort -> Sort #
Show Sort Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #

data FuncDecl Source #

A kind of AST representing function symbols.

Instances

Instances details

Eq FuncDecl Source #
Instance details Defined in Z3.Base Methods (==) :: FuncDecl -> FuncDecl -> Bool # (/=) :: FuncDecl -> FuncDecl -> Bool #
Ord FuncDecl Source #
Instance details Defined in Z3.Base Methods compare :: FuncDecl -> FuncDecl -> Ordering # (<) :: FuncDecl -> FuncDecl -> Bool # (<=) :: FuncDecl -> FuncDecl -> Bool # (>) :: FuncDecl -> FuncDecl -> Bool # (>=) :: FuncDecl -> FuncDecl -> Bool # max :: FuncDecl -> FuncDecl -> FuncDecl # min :: FuncDecl -> FuncDecl -> FuncDecl #
Show FuncDecl Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> FuncDecl -> ShowS # show :: FuncDecl -> String # showList :: [FuncDecl] -> ShowS #

data App Source #

A kind of AST representing constant and function declarations.

Instances

Instances details

Eq App Source #
Instance details Defined in Z3.Base Methods (==) :: App -> App -> Bool # (/=) :: App -> App -> Bool #
Ord App Source #
Instance details Defined in Z3.Base Methods compare :: App -> App -> Ordering # (<) :: App -> App -> Bool # (<=) :: App -> App -> Bool # (>) :: App -> App -> Bool # (>=) :: App -> App -> Bool # max :: App -> App -> App # min :: App -> App -> App #
Show App Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> App -> ShowS # show :: App -> String # showList :: [App] -> ShowS #

data Pattern Source #

A kind of AST representing pattern and multi-patterns to guide quantifier instantiation.

Instances

Instances details

Eq Pattern Source #
Instance details Defined in Z3.Base Methods (==) :: Pattern -> Pattern -> Bool # (/=) :: Pattern -> Pattern -> Bool #
Ord Pattern Source #
Instance details Defined in Z3.Base Methods compare :: Pattern -> Pattern -> Ordering # (<) :: Pattern -> Pattern -> Bool # (<=) :: Pattern -> Pattern -> Bool # (>) :: Pattern -> Pattern -> Bool # (>=) :: Pattern -> Pattern -> Bool # max :: Pattern -> Pattern -> Pattern # min :: Pattern -> Pattern -> Pattern #
Show Pattern Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #

data Constructor Source #

A type contructor for a (recursive) datatype.

Instances

Instances details

Eq Constructor Source #
Instance details Defined in Z3.Base Methods (==) :: Constructor -> Constructor -> Bool # (/=) :: Constructor -> Constructor -> Bool #
Ord Constructor Source #
Instance details Defined in Z3.Base Methods compare :: Constructor -> Constructor -> Ordering # (<) :: Constructor -> Constructor -> Bool # (<=) :: Constructor -> Constructor -> Bool # (>) :: Constructor -> Constructor -> Bool # (>=) :: Constructor -> Constructor -> Bool # max :: Constructor -> Constructor -> Constructor # min :: Constructor -> Constructor -> Constructor #
Show Constructor Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Constructor -> ShowS # show :: Constructor -> String # showList :: [Constructor] -> ShowS #

data Model Source #

A model for the constraints asserted into the logical context.

Instances

Instances details

Eq Model Source #
Instance details Defined in Z3.Base Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #

data FuncInterp Source #

An interpretation of a function in a model.

Instances

Instances details

Eq FuncInterp Source #
Instance details Defined in Z3.Base Methods (==) :: FuncInterp -> FuncInterp -> Bool # (/=) :: FuncInterp -> FuncInterp -> Bool #

data FuncEntry Source #

Representation of the value of a Z3_func_interp at a particular point.

Instances

Instances details

Eq FuncEntry Source #
Instance details Defined in Z3.Base Methods (==) :: FuncEntry -> FuncEntry -> Bool # (/=) :: FuncEntry -> FuncEntry -> Bool #

data Params Source #

A Z3 parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

Instances

Instances details

Eq Params Source #
Instance details Defined in Z3.Base Methods (==) :: Params -> Params -> Bool # (/=) :: Params -> Params -> Bool #

data Solver Source #

A Z3 solver engine.

A(n) (incremental) solver, possibly specialized by a particular tactic or logic.

Instances

Instances details

Eq Solver Source #
Instance details Defined in Z3.Base Methods (==) :: Solver -> Solver -> Bool # (/=) :: Solver -> Solver -> Bool #

data SortKind Source #

Different kinds of Z3 types.

Constructors

Z3_UNINTERPRETED_SORT
Z3_BOOL_SORT
Z3_INT_SORT
Z3_REAL_SORT
Z3_BV_SORT
Z3_ARRAY_SORT
Z3_DATATYPE_SORT
Z3_RELATION_SORT
Z3_FINITE_DOMAIN_SORT
Z3_FLOATING_POINT_SORT
Z3_ROUNDING_MODE_SORT
Z3_UNKNOWN_SORT

Instances

Instances details

Eq SortKind Source #
Instance details Defined in Z3.Base Methods (==) :: SortKind -> SortKind -> Bool # (/=) :: SortKind -> SortKind -> Bool #
Show SortKind Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> SortKind -> ShowS # show :: SortKind -> String # showList :: [SortKind] -> ShowS #

data ASTKind Source #

Different kinds of Z3 AST nodes.

Constructors

Z3_NUMERAL_AST
Z3_APP_AST
Z3_VAR_AST
Z3_QUANTIFIER_AST
Z3_SORT_AST
Z3_FUNC_DECL_AST
Z3_UNKNOWN_AST

Instances

Instances details

Eq ASTKind Source #
Instance details Defined in Z3.Base Methods (==) :: ASTKind -> ASTKind -> Bool # (/=) :: ASTKind -> ASTKind -> Bool #
Show ASTKind Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> ASTKind -> ShowS # show :: ASTKind -> String # showList :: [ASTKind] -> ShowS #

data Tactic Source #

A tactic

Instances

Instances details

Eq Tactic Source #
Instance details Defined in Z3.Base Methods (==) :: Tactic -> Tactic -> Bool # (/=) :: Tactic -> Tactic -> Bool #

data ApplyResult Source #

A result of applying a tactic

Instances

Instances details

Eq ApplyResult Source #
Instance details Defined in Z3.Base Methods (==) :: ApplyResult -> ApplyResult -> Bool # (/=) :: ApplyResult -> ApplyResult -> Bool #

data Goal Source #

A goal (aka problem)

Instances

Instances details

Eq Goal Source #
Instance details Defined in Z3.Base Methods (==) :: Goal -> Goal -> Bool # (/=) :: Goal -> Goal -> Bool #

Satisfiability result

data Result Source #

Result of a satisfiability check.

This corresponds to the z3_lbool type in the C API.

Constructors

Sat
Unsat
Undef

Instances

Instances details

Eq Result Source #
Instance details Defined in Z3.Base Methods (==) :: Result -> Result -> Bool # (/=) :: Result -> Result -> Bool #
Ord Result Source #
Instance details Defined in Z3.Base Methods compare :: Result -> Result -> Ordering # (<) :: Result -> Result -> Bool # (<=) :: Result -> Result -> Bool # (>) :: Result -> Result -> Bool # (>=) :: Result -> Result -> Bool # max :: Result -> Result -> Result # min :: Result -> Result -> Result #
Read Result Source #
Instance details Defined in Z3.Base Methods readsPrec :: Int -> ReadS Result # readList :: ReadS [Result] # readPrec :: ReadPrec Result # readListPrec :: ReadPrec [Result] #
Show Result Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #

Create configuration

mkConfig :: IO Config Source #

Create a configuration.

See withConfig.

delConfig :: Config -> IO () Source #

Delete a configuration.

See withConfig.

setParamValue :: Config -> String -> String -> IO () Source #

Set a configuration parameter.

Helpers

withConfig :: (Config -> IO a) -> IO a Source #

Run a computation using a temporally created configuration.

Note that the configuration object can be thrown away once it has been used to create the Z3 Context.

Create context

mkContext :: Config -> IO Context Source #

Create a context using the given configuration.

Z3_del_context is called by Haskell's garbage collector before freeing the Context object.

withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r Source #

Parameters

mkParams :: Context -> IO Params Source #

Create a Z3 (empty) parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO () Source #

Add a Boolean parameter k with value v to the parameter set p.

paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO () Source #

Add a unsigned parameter k with value v to the parameter set p.

paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO () Source #

Add a double parameter k with value v to the parameter set p.

paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () Source #

Add a symbol parameter k with value v to the parameter set p.

paramsToString :: Context -> Params -> IO String Source #

Convert a parameter set into a string.

This function is mainly used for printing the contents of a parameter set.

Symbols

mkIntSymbol :: Integral int => Context -> int -> IO Symbol Source #

Create a Z3 symbol using an integer.

mkIntSymbol c i requires 0 <= i < 2^30

mkStringSymbol :: Context -> String -> IO Symbol Source #

Create a Z3 symbol using a String.

Sorts

mkUninterpretedSort :: Context -> Symbol -> IO Sort Source #

Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

mkBoolSort :: Context -> IO Sort Source #

Create the boolean type.

This type is used to create propositional variables and predicates.

mkIntSort :: Context -> IO Sort Source #

Create the integer type.

This is the type of arbitrary precision integers. A machine integer can be represented using bit-vectors, see mkBvSort.

mkRealSort :: Context -> IO Sort Source #

Create the real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

mkBvSort :: Integral int => Context -> int -> IO Sort Source #

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

mkBvSort c sz requires sz >= 0

mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort Source #

Create a finite-domain type.

mkArraySort :: Context -> Sort -> Sort -> IO Sort Source #

Create an array type

We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.

mkTupleSort Source #

Arguments

:: Context	Context
-> Symbol	Name of the sort
-> [(Symbol, Sort)]	Name and sort of each field
-> IO (Sort, FuncDecl, [FuncDecl])	Resulting sort, and function declarations for the constructor and projections.

Create a tuple type

A tuple with n fields has a constructor and n projections. This function will also declare the constructor and projection functions.

mkConstructor Source #

Arguments

:: Context	Context
-> Symbol	Name of the constructor
-> Symbol	Name of recognizer function
-> [(Symbol, Maybe Sort, Int)]	Name, sort option, and sortRefs
-> IO Constructor

Create a contructor

mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort Source #

Create datatype, such as lists, trees, records, enumerations or unions of records.

The datatype may be recursive. Returns the datatype sort.

mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort] Source #

Create mutually recursive datatypes, such as a tree and forest.

Returns the datatype sorts

mkSetSort :: Context -> Sort -> IO Sort Source #

Create an set type with a given domain type

Constants and Applications

mkFuncDecl Source #

Arguments

:: Context	Logical context.
-> Symbol	Name of the function (or constant).
-> [Sort]	Function domain (empty for constants).
-> Sort	Return sort of the function.
-> IO FuncDecl

Declare a constant or function.

mkApp :: Context -> FuncDecl -> [AST] -> IO AST Source #

Create a constant or function application.

mkConst :: Context -> Symbol -> Sort -> IO AST Source #

Declare and create a constant.

This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c xd []

mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl Source #

Declare a fresh constant or function.

mkFreshConst Source #

Arguments

:: Context	Logical context.
-> String	Prefix.
-> Sort	Sort of the constant.
-> IO AST

Declare and create a fresh constant.

Helpers

mkVar :: Context -> Symbol -> Sort -> IO AST Source #

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort int.

See mkVar.

mkBvVar Source #

Arguments

:: Context
-> Symbol
-> Int	bit-width
-> IO AST

Declarate and create a variable of sort bit-vector.

See mkVar.

mkFreshVar :: Context -> String -> Sort -> IO AST Source #

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar Source #

Arguments

:: Context
-> String
-> Int	bit-width
-> IO AST

Declarate and create a fresh variable of sort bit-vector.

See mkFreshVar.

Propositional Logic and Equality

mkTrue :: Context -> IO AST Source #

Create an AST node representing true.

mkFalse :: Context -> IO AST Source #

Create an AST node representing false.

mkEq :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing l = r.

mkNot :: Context -> AST -> IO AST Source #

Create an AST node representing not(a).

mkIte :: Context -> AST -> AST -> AST -> IO AST Source #

Create an AST node representing an if-then-else: ite(t1, t2, t3).

mkIff :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 iff t2.

mkImplies :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 implies t2.

mkXor :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 xor t2.

mkAnd :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] and ... and args[num_args-1].

mkOr :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] or ... or args[num_args-1].

mkDistinct :: Context -> [AST] -> IO AST Source #

The distinct construct is used for declaring the arguments pairwise distinct.

That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]

Helpers

mkBool :: Context -> Bool -> IO AST Source #

Create an AST node representing the given boolean.

Arithmetic: Integers and Reals

mkAdd :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] + ... + args[num_args-1].

mkMul :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] * ... * args[num_args-1].

mkSub :: Context -> NonEmpty AST -> IO AST Source #

Create an AST node representing args[0] - ... - args[num_args - 1].

mkUnaryMinus :: Context -> AST -> IO AST Source #

Create an AST node representing -arg.

mkDiv :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 div arg2.

mkMod :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 mod arg2.

mkRem :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 rem arg2.

mkLt :: Context -> AST -> AST -> IO AST Source #

Create less than.

mkLe :: Context -> AST -> AST -> IO AST Source #

Create less than or equal to.

mkGt :: Context -> AST -> AST -> IO AST Source #

Create greater than.

mkGe :: Context -> AST -> AST -> IO AST Source #

Create greater than or equal to.

mkInt2Real :: Context -> AST -> IO AST Source #

Coerce an integer to a real.

mkReal2Int :: Context -> AST -> IO AST Source #

Coerce a real to an integer.

mkIsInt :: Context -> AST -> IO AST Source #

Check if a real number is an integer.

Bit-vectors

mkBvnot :: Context -> AST -> IO AST Source #

Bitwise negation.

mkBvredand :: Context -> AST -> IO AST Source #

Take conjunction of bits in vector, return vector of length 1.

mkBvredor :: Context -> AST -> IO AST Source #

Take disjunction of bits in vector, return vector of length 1.

mkBvand :: Context -> AST -> AST -> IO AST Source #

Bitwise and.

mkBvor :: Context -> AST -> AST -> IO AST Source #

Bitwise or.

mkBvxor :: Context -> AST -> AST -> IO AST Source #

Bitwise exclusive-or.

mkBvnand :: Context -> AST -> AST -> IO AST Source #

Bitwise nand.

mkBvnor :: Context -> AST -> AST -> IO AST Source #

Bitwise nor.

mkBvxnor :: Context -> AST -> AST -> IO AST Source #

Bitwise xnor.

mkBvneg :: Context -> AST -> IO AST Source #

Standard two's complement unary minus.

mkBvadd :: Context -> AST -> AST -> IO AST Source #

Standard two's complement addition.

mkBvsub :: Context -> AST -> AST -> IO AST Source #

Standard two's complement subtraction.

mkBvmul :: Context -> AST -> AST -> IO AST Source #

Standard two's complement multiplication.

mkBvudiv :: Context -> AST -> AST -> IO AST Source #

Unsigned division.

mkBvsdiv :: Context -> AST -> AST -> IO AST Source #

Two's complement signed division.

mkBvurem :: Context -> AST -> AST -> IO AST Source #

Unsigned remainder.

mkBvsrem :: Context -> AST -> AST -> IO AST Source #

Two's complement signed remainder (sign follows dividend).

mkBvsmod :: Context -> AST -> AST -> IO AST Source #

Two's complement signed remainder (sign follows divisor).

mkBvult :: Context -> AST -> AST -> IO AST Source #

Unsigned less than.

mkBvslt :: Context -> AST -> AST -> IO AST Source #

Two's complement signed less than.

mkBvule :: Context -> AST -> AST -> IO AST Source #

Unsigned less than or equal to.

mkBvsle :: Context -> AST -> AST -> IO AST Source #

Two's complement signed less than or equal to.

mkBvuge :: Context -> AST -> AST -> IO AST Source #

Unsigned greater than or equal to.

mkBvsge :: Context -> AST -> AST -> IO AST Source #

Two's complement signed greater than or equal to.

mkBvugt :: Context -> AST -> AST -> IO AST Source #

Unsigned greater than.

mkBvsgt :: Context -> AST -> AST -> IO AST Source #

Two's complement signed greater than.

mkConcat :: Context -> AST -> AST -> IO AST Source #

Concatenate the given bit-vectors.

mkExtract :: Context -> Int -> Int -> AST -> IO AST Source #

Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.

mkSignExt :: Context -> Int -> AST -> IO AST Source #

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

mkZeroExt :: Context -> Int -> AST -> IO AST Source #

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

mkRepeat :: Context -> Int -> AST -> IO AST Source #

Repeat the given bit-vector up length i.

mkBvshl :: Context -> AST -> AST -> IO AST Source #

Shift left.

mkBvlshr :: Context -> AST -> AST -> IO AST Source #

Logical shift right.

mkBvashr :: Context -> AST -> AST -> IO AST Source #

Arithmetic shift right.

mkRotateLeft :: Context -> Int -> AST -> IO AST Source #

Rotate bits of t1 to the left i times.

mkRotateRight :: Context -> Int -> AST -> IO AST Source #

Rotate bits of t1 to the right i times.

mkExtRotateLeft :: Context -> AST -> AST -> IO AST Source #

Rotate bits of t1 to the left t2 times.

mkExtRotateRight :: Context -> AST -> AST -> IO AST Source #

Rotate bits of t1 to the right t2 times.

mkInt2bv :: Context -> Int -> AST -> IO AST Source #

Create an n bit bit-vector from the integer argument t1.

mkBv2int :: Context -> AST -> Bool -> IO AST Source #

Create an integer from the bit-vector argument t1.

If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

mkBvnegNoOverflow :: Context -> AST -> IO AST Source #

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Arrays

mkSelect Source #

Arguments

:: Context
-> AST	Array.
-> AST	Index of the array to read.
-> IO AST

Array read. The argument a is the array and i is the index of the array that gets read.

mkStore Source #

Arguments

:: Context
-> AST	Array.
-> AST	Index i of the array.
-> AST	New value for i.
-> IO AST

Array update.

The result of this function is an array that is equal to the input array (with respect to select) on all indices except for i, where it maps to v.

The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details.

mkConstArray Source #

Arguments

:: Context
-> Sort	Domain sort of the array.
-> AST	Value v that the array maps to.
-> IO AST

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

mkMap Source #

Arguments

:: Context
-> FuncDecl	Function f.
-> [AST]	List of arrays.
-> IO AST

Map a function f on the the argument arrays.

The n nodes args must be of array sorts [domain -> range_i]. The function declaration f must have type range_1 .. range_n -> range. The sort of the result is [domain -> range].

mkArrayDefault Source #

Arguments

:: Context
-> AST	Array.
-> IO AST

Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Sets

mkEmptySet Source #

Arguments

:: Context
-> Sort	Domain sort of the set.
-> IO AST

Create the empty set.

mkFullSet Source #

Arguments

:: Context
-> Sort	Domain sort of the set.
-> IO AST

Create the full set.

mkSetAdd Source #

Arguments

:: Context
-> AST	Set.
-> AST	Element.
-> IO AST

Add an element to a set.

mkSetDel Source #

Arguments

:: Context
-> AST	Set.
-> AST	Element.
-> IO AST

Remove an element from a set.

mkSetUnion :: Context -> [AST] -> IO AST Source #

Take the union of a list of sets.

mkSetIntersect :: Context -> [AST] -> IO AST Source #

Take the intersection of a list of sets.

mkSetDifference Source #

Arguments

:: Context
-> AST	First set.
-> AST	Second set.
-> IO AST

Take the set difference between two sets.

mkSetComplement Source #

Arguments

:: Context
-> AST	Set.
-> IO AST

Take the complement of a set.

mkSetMember Source #

Arguments

:: Context
-> AST	Element.
-> AST	Set.
-> IO AST

Check for set membership.

mkSetSubset Source #

Arguments

:: Context
-> AST	First set.
-> AST	Second set.
-> IO AST

Check if the first set is a subset of the second set.

Numerals

mkNumeral :: Context -> String -> Sort -> IO AST Source #

Create a numeral of a given sort.

mkReal Source #

Arguments

:: Context
-> Int	numerator
-> Int	denominator (/= 0)
-> IO AST

Create a real from a fraction.

mkInt :: Context -> Int -> Sort -> IO AST Source #