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

Z3.Monad

Contents

Z3 monad
- Z3 enviroments
Types
- Satisfiability result
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

A simple monadic interface to Z3 API.

Examples: https://bitbucket.org/iago/z3-haskell/src/tip/examples/Example/Monad

Synopsis

class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where
- getSolver :: m Solver
- getContext :: m Context
data Z3 a
module Z3.Opts
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
evalZ3 :: Z3 a -> IO a
evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
data Z3Env
newEnv :: Maybe Logic -> Opts -> IO Z3Env
evalZ3WithEnv :: Z3 a -> Z3Env -> IO a
data Symbol
data AST
data Sort
data FuncDecl
data App
data Pattern
data Constructor
data Model
data Context
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 Result
- = Sat
- | Unsat
- | Undef
mkParams :: MonadZ3 z3 => z3 Params
paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 ()
paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 ()
paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 ()
paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 ()
paramsToString :: MonadZ3 z3 => Params -> z3 String
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
mkBoolSort :: MonadZ3 z3 => z3 Sort
mkIntSort :: MonadZ3 z3 => z3 Sort
mkRealSort :: MonadZ3 z3 => z3 Sort
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort
mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
mkConstructor :: MonadZ3 z3 => Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> z3 Constructor
mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort
mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort]
mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort
mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl
mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST
mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST
mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST
mkBvVar :: MonadZ3 z3 => Symbol -> Int -> z3 AST
mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST
mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST
mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST
mkFreshBvVar :: MonadZ3 z3 => String -> Int -> z3 AST
mkTrue :: MonadZ3 z3 => z3 AST
mkFalse :: MonadZ3 z3 => z3 AST
mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
mkNot :: MonadZ3 z3 => AST -> z3 AST
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
mkOr :: MonadZ3 z3 => [AST] -> z3 AST
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
mkBool :: MonadZ3 z3 => Bool -> z3 AST
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
mkMul :: MonadZ3 z3 => [AST] -> z3 AST
mkSub :: MonadZ3 z3 => NonEmpty AST -> z3 AST
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
mkIsInt :: MonadZ3 z3 => AST -> z3 AST
mkBvnot :: MonadZ3 z3 => AST -> z3 AST
mkBvredand :: MonadZ3 z3 => AST -> z3 AST
mkBvredor :: MonadZ3 z3 => AST -> z3 AST
mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvneg :: MonadZ3 z3 => AST -> z3 AST
mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST
mkFullSet :: MonadZ3 z3 => Sort -> z3 AST
mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST
mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST
mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetComplement :: MonadZ3 z3 => AST -> z3 AST
mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST
mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST
mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST
mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST
mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST
mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST
mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST
mkRational :: MonadZ3 z3 => Rational -> z3 AST
mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST
mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST
mkInteger :: MonadZ3 z3 => Integer -> z3 AST
mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST
mkBitvector :: MonadZ3 z3 => Int -> Integer -> z3 AST
mkBvNum :: (MonadZ3 z3, Integral i) => Int -> i -> z3 AST
mkPattern :: MonadZ3 z3 => NonEmpty AST -> z3 Pattern
mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST
mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
getSymbolString :: MonadZ3 z3 => Symbol -> z3 String
getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
getDatatypeSortConstructors :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
getDatatypeSortRecognizers :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
getDatatypeSortConstructorAccessors :: MonadZ3 z3 => Sort -> z3 [[FuncDecl]]
getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol
getArity :: MonadZ3 z3 => FuncDecl -> z3 Int
getDomain :: MonadZ3 z3 => FuncDecl -> Int -> z3 Sort
getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort
appToAst :: MonadZ3 z3 => App -> z3 AST
getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl
getAppNumArgs :: MonadZ3 z3 => App -> z3 Int
getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST
getAppArgs :: MonadZ3 z3 => App -> z3 [AST]
getSort :: MonadZ3 z3 => AST -> z3 Sort
getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort
getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort
getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind
isApp :: MonadZ3 z3 => AST -> z3 Bool
toApp :: MonadZ3 z3 => AST -> z3 App
getNumeralString :: MonadZ3 z3 => AST -> z3 String
simplify :: MonadZ3 z3 => AST -> z3 AST
simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST
getIndexValue :: MonadZ3 z3 => AST -> z3 Int
isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool
isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool
getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int
getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol
getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort
getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST
getBool :: MonadZ3 z3 => AST -> z3 Bool
getInt :: MonadZ3 z3 => AST -> z3 Integer
getReal :: MonadZ3 z3 => AST -> z3 Rational
getBv :: MonadZ3 z3 => AST -> Bool -> z3 Integer
substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST
modelEval :: MonadZ3 z3 => Model -> AST -> Bool -> z3 (Maybe AST)
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST)
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool
numConsts :: MonadZ3 z3 => Model -> z3 Word
numFuncs :: MonadZ3 z3 => Model -> z3 Word
getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl]
getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl]
isAsArray :: MonadZ3 z3 => AST -> z3 Bool
addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp
addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 ()
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
modelToString :: MonadZ3 z3 => Model -> z3 String
showModel :: MonadZ3 z3 => Model -> z3 String
type EvalAst m a = Model -> AST -> m (Maybe a)
eval :: MonadZ3 z3 => EvalAst z3 AST
evalBool :: MonadZ3 z3 => EvalAst z3 Bool
evalInt :: MonadZ3 z3 => EvalAst z3 Integer
evalReal :: MonadZ3 z3 => EvalAst z3 Rational
evalBv :: MonadZ3 z3 => Bool -> EvalAst z3 Integer
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a))
data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
}
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
mkTactic :: MonadZ3 z3 => String -> z3 Tactic
andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
skipTactic :: MonadZ3 z3 => z3 Tactic
tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic
mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic
mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic
applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult
getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int
getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal
getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal]
mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal
goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 ()
getGoalSize :: MonadZ3 z3 => Goal -> z3 Int
getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST
getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST]
data ASTPrintMode
- = Z3_PRINT_SMTLIB_FULL
- | Z3_PRINT_LOW_LEVEL
- | Z3_PRINT_SMTLIB2_COMPLIANT
setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
astToString :: MonadZ3 z3 => AST -> z3 String
patternToString :: MonadZ3 z3 => Pattern -> z3 String
sortToString :: MonadZ3 z3 => Sort -> z3 String
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
parseSMTLib2String :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 AST
parseSMTLib2File :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 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 :: MonadZ3 z3 => z3 Version
data Fixedpoint
fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 ()
fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 ()
fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 ()
fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result
fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST
fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST]
solverGetHelp :: MonadZ3 z3 => z3 String
solverSetParams :: MonadZ3 z3 => Params -> z3 ()
solverPush :: MonadZ3 z3 => z3 ()
solverPop :: MonadZ3 z3 => Int -> z3 ()
solverReset :: MonadZ3 z3 => z3 ()
solverGetNumScopes :: MonadZ3 z3 => z3 Int
solverAssertCnstr :: MonadZ3 z3 => AST -> z3 ()
solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 ()
solverCheck :: MonadZ3 z3 => z3 Result
solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
solverGetModel :: MonadZ3 z3 => z3 Model
solverGetUnsatCore :: MonadZ3 z3 => z3 [AST]
solverGetReasonUnknown :: MonadZ3 z3 => z3 String
solverToString :: MonadZ3 z3 => z3 String
assert :: MonadZ3 z3 => AST -> z3 ()
check :: MonadZ3 z3 => z3 Result
checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
getUnsatCore :: MonadZ3 z3 => z3 [AST]
push :: MonadZ3 z3 => z3 ()
pop :: MonadZ3 z3 => Int -> z3 ()
local :: MonadZ3 z3 => z3 a -> z3 a
reset :: MonadZ3 z3 => z3 ()
getNumScopes :: MonadZ3 z3 => z3 Int

Z3 monad

class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where Source #

Methods

getSolver :: m Solver Source #

getContext :: m Context Source #

Instances

Instances details

MonadZ3 Z3 Source #
Instance details Defined in Z3.Monad Methods getSolver :: Z3 Solver Source # getContext :: Z3 Context Source #

data Z3 a Source #

Instances

Instances details

Monad Z3 Source #
Instance details Defined in Z3.Monad Methods (>>=) :: Z3 a -> (a -> Z3 b) -> Z3 b # (>>) :: Z3 a -> Z3 b -> Z3 b # return :: a -> Z3 a #
Functor Z3 Source #
Instance details Defined in Z3.Monad Methods fmap :: (a -> b) -> Z3 a -> Z3 b # (<$) :: a -> Z3 b -> Z3 a #
MonadFix Z3 Source #
Instance details Defined in Z3.Monad Methods mfix :: (a -> Z3 a) -> Z3 a #
MonadFail Z3 Source #
Instance details Defined in Z3.Monad Methods fail :: String -> Z3 a #
Applicative Z3 Source #
Instance details Defined in Z3.Monad Methods pure :: a -> Z3 a # (<>) :: Z3 (a -> b) -> Z3 a -> Z3 b # liftA2 :: (a -> b -> c) -> Z3 a -> Z3 b -> Z3 c # (>) :: Z3 a -> Z3 b -> Z3 b # (<*) :: Z3 a -> Z3 b -> Z3 a #
MonadIO Z3 Source #
Instance details Defined in Z3.Monad Methods liftIO :: IO a -> Z3 a #
MonadZ3 Z3 Source #
Instance details Defined in Z3.Monad Methods getSolver :: Z3 Solver Source # getContext :: Z3 Context Source #

module Z3.Opts

data Logic Source #

Solvers available in Z3.

These are described at http://smtlib.cs.uiowa.edu/logics.html

Constructors

AUFLIA	Closed formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.
AUFLIRA	Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.
AUFNIRA	Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.
LRA	Closed linear formulas in linear real arithmetic.
QF_ABV	Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays.
QF_AUFBV	Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.
QF_AUFLIA	Closed quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.
QF_AX	Closed quantifier-free formulas over the theory of arrays with extensionality.
QF_BV	Closed quantifier-free formulas over the theory of fixed-size bitvectors.
QF_IDL	Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.
QF_LIA	Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.
QF_LRA	Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
QF_NIA	Quantifier-free integer arithmetic.
QF_NRA	Quantifier-free real arithmetic.
QF_RDL	Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.
QF_UF	Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.
QF_UFBV	Unquantified formulas over bitvectors with uninterpreted sort function and symbols.
QF_UFIDL	Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.
QF_UFLIA	Unquantified linear integer arithmetic with uninterpreted sort and function symbols.
QF_UFLRA	Unquantified linear real arithmetic with uninterpreted sort and function symbols.
QF_UFNRA	Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.
UFLRA	Linear real arithmetic with uninterpreted sort and function symbols.
UFNIA	Non-linear integer arithmetic with uninterpreted sort and function symbols.

Instances

Instances details

Show Logic Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Logic -> ShowS # show :: Logic -> String # showList :: [Logic] -> ShowS #

evalZ3 :: Z3 a -> IO a Source #

Eval a Z3 script with default configuration options.

evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a Source #

Eval a Z3 script.

Z3 enviroments

data Z3Env Source #

Z3 environment.

newEnv :: Maybe Logic -> Opts -> IO Z3Env Source #

Create a new Z3 environment.

evalZ3WithEnv :: Z3 a -> Z3Env -> IO a Source #

Eval a Z3 script with a given environment.

Environments may facilitate running many queries under the same logical context.

Note that an environment may change after each query. If you want to preserve the same environment then use local, as in evalZ3WithEnv env (local query).

Types

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 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 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 #

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 #

Parameters

mkParams :: MonadZ3 z3 => z3 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 :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 () Source #

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

paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 () Source #

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

paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 () Source #

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

paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 () Source #

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

paramsToString :: MonadZ3 z3 => Params -> z3 String Source #

Convert a parameter set into a string.

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

Symbols

mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol Source #

Create a Z3 symbol using an integer.

mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol Source #

Create a Z3 symbol using a string.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae

Sorts

mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de

mkBoolSort :: MonadZ3 z3 => z3 Sort Source #

Create the boolean type.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342

mkIntSort :: MonadZ3 z3 => z3 Sort Source #

Create the integer type.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015

mkRealSort :: MonadZ3 z3 => z3 Sort Source #

Create the real type.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0

mkBvSort :: MonadZ3 z3 => Int -> z3 Sort Source #

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688

mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort Source #

Create a finite-domain type.

mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort Source #

Create an array type

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445

mkTupleSort Source #

Arguments

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

Create a tuple type

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1

mkConstructor Source #

Arguments

:: MonadZ3 z3
=> Symbol	Name of the sonstructor
-> Symbol	Name of recognizer function
-> [(Symbol, Maybe Sort, Int)]	Name, sort option, and sortRefs
-> z3 Constructor

Create a contructor

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0

mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort Source #

Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

Reference http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab6809d53327d807da9158abdf75df387

mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort] Source #

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

Returns the datatype sorts

mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort Source #

Create a set type

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b

Constants and Applications

mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl Source #

A Z3 function

mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST Source #

Create a constant or function application.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe

mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST Source #

Declare and create a constant.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef

mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST Source #

Declare and create a constant.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef

mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl Source #

Declare a fresh constant or function.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec

Helpers

mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST Source #

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST Source #

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST Source #

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST Source #

Declarate and create a variable of sort int.

See mkVar.

mkBvVar Source #

Arguments

:: MonadZ3 z3
=> Symbol
-> Int	bit-width
-> z3 AST

Declarate and create a variable of sort bit-vector.

See mkVar.

mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST Source #

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST Source #

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST Source #

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST Source #

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar Source #

Arguments

:: MonadZ3 z3
=> String
-> Int	bit-width
-> z3 AST

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

See mkFreshVar.

Propositional Logic and Equality

mkTrue :: MonadZ3 z3 => z3 AST Source #

Create an AST node representing true.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7

mkFalse :: MonadZ3 z3 => z3 AST Source #

Create an AST node representing false.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d

mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing l = r.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c

mkNot :: MonadZ3 z3 => AST -> z3 AST Source #

Create an AST node representing not(a).

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072

mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547

mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing t1 iff t2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042

mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing t1 implies t2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517

mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing t1 xor t2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec

mkAnd :: MonadZ3 z3 => [AST] -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61

mkOr :: MonadZ3 z3 => [AST] -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9

mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7

Helpers

mkBool :: MonadZ3 z3 => Bool -> z3 AST Source #

Create an AST node representing the given boolean.

Arithmetic: Integers and Reals

mkAdd :: MonadZ3 z3 => [AST] -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5

mkMul :: MonadZ3 z3 => [AST] -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890

mkSub :: MonadZ3 z3 => NonEmpty AST -> z3 AST Source #

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

Requires a non-empty list.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9

mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST Source #

Create an AST node representing -arg.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea

mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing arg1 div arg2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3

mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing arg1 mod arg2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713

mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create an AST node representing arg1 rem arg2.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff

mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create less than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534

mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create less than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf

mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create greater than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3

mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Create greater than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942

mkInt2Real :: MonadZ3 z3 => AST -> z3 AST Source #

Coerce an integer to a real.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21

mkReal2Int :: MonadZ3 z3 => AST -> z3 AST Source #

Coerce a real to an integer.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d

mkIsInt :: MonadZ3 z3 => AST -> z3 AST Source #

Check if a real number is an integer.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3

Bit-vectors

mkBvnot :: MonadZ3 z3 => AST -> z3 AST Source #

Bitwise negation.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080

mkBvredand :: MonadZ3 z3 => AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8

mkBvredor :: MonadZ3 z3 => AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2

mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise and.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d

mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise or.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5

mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise exclusive-or.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8

mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise nand.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61

mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise nor.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb

mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Bitwise xnor.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6

mkBvneg :: MonadZ3 z3 => AST -> z3 AST Source #

Standard two's complement unary minus.

Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7

mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Standard two's complement addition.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158

mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Standard two's complement subtraction.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e

mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Standard two's complement multiplication.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c

mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned division.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544

mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Two's complement signed division.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0

mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned remainder.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d

mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1

mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879

mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned less than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4

mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Two's complement signed less than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a

mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned less than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87

mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Two's complement signed less than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d

mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned greater than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df

mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Two's complement signed greater than or equal to.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5

mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Unsigned greater than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3

mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Two's complement signed greater than.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0

mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Concatenate the given bit-vectors.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa

mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 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.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317

mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 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.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e

mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 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.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3

mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST Source #

Repeat the given bit-vector up length i.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d

mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Shift left.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1

mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Logical shift right.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512

mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Arithmetic shift right.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4

mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST Source #

Rotate bits of t1 to the left i times.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda

mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST Source #

Rotate bits of t1 to the right i times.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c

mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Rotate bits of t1 to the left t2 times.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7

mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Rotate bits of t1 to the right t2 times.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f

mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5

mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 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.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4

mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7

mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f

mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947

mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c

mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4

mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df

mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda

mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e

Arrays

mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67

mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST Source #

Array update.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593

mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST Source #

Create the constant array.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d

mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST Source #

map f on the the argument arrays.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d

mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d

Sets

mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST Source #

Create the empty set.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga358b6b80509a567148f1c0ca9252118c

mkFullSet :: MonadZ3 z3 => Sort -> z3 AST Source #

Create the full set.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2

mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Add an element to a set.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175

mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Remove an element from a set.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d

mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST Source #

Take the union of a list of sets.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4050162a13d539b8913200963bb4743c

mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST Source #

Take the intersection of a list of sets.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d

mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Take the set difference between two sets.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1

mkSetComplement :: MonadZ3 z3 => AST -> z3 AST Source #

Take the complement of a set.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5c57143c9229cdf730c5103ff696590f

mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

Check for set membership.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063

mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST Source #

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

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a

Numerals

mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST Source #

Create a numeral of a given sort.

Reference: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c

mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST Source #