Safe Haskell	None
Language	Haskell2010

Z3.Tagged

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

Synopsis

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

Z3 monad

type Z3 s = ReaderT (Z3Env s) (ST s) Source #

module Z3.Opts

data Logic #

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
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Logic -> ShowS # show :: Logic -> String # showList :: [Logic] -> ShowS #

evalZ3 :: Z3 s a -> ST s a Source #

Eval a Z3 script with default configuration options.

evalZ3With :: Maybe Logic -> Opts -> Z3 s a -> ST s a Source #

Eval a Z3 script.

Z3 enviroments

data Z3Env s Source #

Z3 environment.

newEnv :: Maybe Logic -> Opts -> ST s (Z3Env s) Source #

Create a new Z3 environment.

Types

data Symbol s Source #

Instances

Instances details

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

data AST s Source #

Instances

Instances details

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

data Sort s Source #

Instances

Instances details

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

data FuncDecl s Source #

Instances

Instances details

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

data App s Source #

Instances

Instances details

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

data Pattern s Source #

Instances

Instances details

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

data Constructor s Source #

Instances

Instances details

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

data Model s Source #

Instances

Instances details

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

data Context #

A Z3 logical context.

Instances

Instances details

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

data FuncInterp s Source #

Instances

Instances details

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

data FuncEntry s Source #

Instances

Instances details

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

data Params s Source #

Instances

Instances details

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

data Solver s Source #

Instances

Instances details

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

data SortKind #

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
Instance details Defined in Z3.Base Methods (==) :: SortKind -> SortKind -> Bool # (/=) :: SortKind -> SortKind -> Bool #
Show SortKind
Instance details Defined in Z3.Base Methods showsPrec :: Int -> SortKind -> ShowS # show :: SortKind -> String # showList :: [SortKind] -> ShowS #

data ASTKind #

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
Instance details Defined in Z3.Base Methods (==) :: ASTKind -> ASTKind -> Bool # (/=) :: ASTKind -> ASTKind -> Bool #
Show ASTKind
Instance details Defined in Z3.Base Methods showsPrec :: Int -> ASTKind -> ShowS # show :: ASTKind -> String # showList :: [ASTKind] -> ShowS #

Satisfiability result

data Result #

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
Instance details Defined in Z3.Base Methods (==) :: Result -> Result -> Bool # (/=) :: Result -> Result -> Bool #
Ord Result
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
Instance details Defined in Z3.Base Methods readsPrec :: Int -> ReadS Result # readList :: ReadS [Result] # readPrec :: ReadPrec Result # readListPrec :: ReadPrec [Result] #
Show Result
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #
Marshal Result Z3_lbool
Instance details Defined in Z3.Base Methods c2h :: Context -> Z3_lbool -> IO Result h2c :: Result -> (Z3_lbool -> IO r) -> IO r

Parameters

mkParams :: Z3 s (Params s) 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 :: Params s -> Symbol s -> Bool -> Z3 s () Source #

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

paramsSetUInt :: Params s -> Symbol s -> Word -> Z3 s () Source #

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

paramsSetDouble :: Params s -> Symbol s -> Double -> Z3 s () Source #

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

paramsSetSymbol :: Params s -> Symbol s -> Symbol s -> Z3 s () Source #

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

paramsToString :: Params s -> Z3 s String Source #

Convert a parameter set into a string.

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

Symbols

mkIntSymbol :: forall i s. Integral i => i -> Z3 s (Symbol s) Source #

Create a Z3 symbol using an integer.

mkStringSymbol :: String -> Z3 s (Symbol s) Source #

Create a Z3 symbol using a string.

Reference: s/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae

Sorts

mkUninterpretedSort :: Symbol s -> Z3 s (Sort s) Source #

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

Reference: s/group__capi.html#ga736e88741af1c178cbebf94c49aa42de

mkBoolSort :: Z3 s (Sort s) Source #

Create the boolean type.

Reference: s/group__capi.html#gacdc73510b69a010b71793d429015f342

mkIntSort :: Z3 s (Sort s) Source #

Create the integer type.

Reference: s/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015

mkRealSort :: Z3 s (Sort s) Source #

Create the real type.

Reference: s/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0

mkBvSort :: forall i s. Integral i => i -> Z3 s (Sort s) Source #

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

Reference: s/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688

mkFiniteDomainSort :: Symbol s -> Word64 -> Z3 s (Sort s) Source #

Create a finite domain type.

mkArraySort :: Sort s -> Sort s -> Z3 s (Sort s) Source #

Create an array type

Reference: s/group__capi.html#gafe617994cce1b516f46128e448c84445

mkTupleSort Source #

Arguments

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

Create a tuple type

Reference: s/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1

mkConstructor Source #

Arguments

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

Create a contructor

Reference: s/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0

mkDatatype :: Symbol s -> [Constructor s] -> Z3 s (Sort s) Source #

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

Reference s/group__capi.html#gab6809d53327d807da9158abdf75df387

mkDatatypes :: [Symbol s] -> [[Constructor s]] -> Z3 s [Sort s] Source #

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

Returns the datatype sorts

mkSetSort :: Sort s -> Z3 s (Sort s) Source #

Create a set type

Reference: s/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b

Constants and Applications

mkFuncDecl :: Symbol s -> [Sort s] -> Sort s -> Z3 s (FuncDecl s) Source #

A Z3 function

mkApp :: FuncDecl s -> [AST s] -> Z3 s (AST s) Source #

Create a constant or function application.

Reference: s/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe

mkConst :: Symbol s -> Sort s -> Z3 s (AST s) Source #

Declare and create a constant.

Reference: s/group__capi.html#ga093c9703393f33ae282ec5e8729354ef

mkFreshConst :: String -> Sort s -> Z3 s (AST s) Source #

Declare and create a constant.

Reference: s/group__capi.html#ga093c9703393f33ae282ec5e8729354ef

mkFreshFuncDecl :: String -> [Sort s] -> Sort s -> Z3 s (FuncDecl s) Source #

Declare a fresh constant or function.

Reference: s/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec

Helpers

mkVar :: Symbol s -> Sort s -> Z3 s (AST s) Source #

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: Symbol s -> Z3 s (AST s) Source #

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: Symbol s -> Z3 s (AST s) Source #

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: Symbol s -> Z3 s (AST s) Source #

Declarate and create a variable of sort int.

See mkVar.

mkBvVar Source #

Arguments

:: Symbol s
-> Int	bit-width
-> Z3 s (AST s)

Declarate and create a variable of sort bit-vector.

See mkVar.

mkFreshVar :: String -> Sort s -> Z3 s (AST s) Source #

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: String -> Z3 s (AST s) Source #

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: String -> Z3 s (AST s) Source #

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: String -> Z3 s (AST s) Source #

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar Source #

Arguments

:: String
-> Int	bit-width
-> Z3 s (AST s)

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

See mkFreshVar.

Propositional Logic and Equality

mkTrue :: Z3 s (AST s) Source #

Create an (AST s) node representing true.

Reference: s/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7

mkFalse :: Z3 s (AST s) Source #

Create an (AST s) node representing false.

Reference: s/group__capi.html#ga5952ac17671117a02001fed6575c778d

mkEq :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing l = r.

Reference: s/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c

mkNot :: AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing not(a).

Reference: s/group__capi.html#ga3329538091996eb7b3dc677760a61072

mkIte :: AST s -> AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547

mkIff :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing t1 iff t2.

Reference: s/group__capi.html#ga930a8e844d345fbebc498ac43a696042

mkImplies :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing t1 implies t2.

Reference: s/group__capi.html#gac829c0e25bbbd30343bf073f7b524517

mkXor :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing t1 xor t2.

Reference: s/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec

mkAnd :: [AST s] -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61

mkOr :: [AST s] -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga00866d16331d505620a6c515302021f9

mkDistinct :: NonEmpty (AST s) -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7

Helpers

mkBool :: Bool -> Z3 s (AST s) Source #

Create an (AST s) node representing the given boolean.

Arithmetic: Integers and Reals

mkAdd :: [AST s] -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5

mkMul :: [AST s] -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gab9affbf8401a18eea474b59ad4adc890

mkSub :: NonEmpty (AST s) -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9

mkUnaryMinus :: AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing -arg.

Reference: s/group__capi.html#gadcd2929ad732937e25f34277ce4988ea

mkDiv :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing arg1 div arg2.

Reference: s/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3

mkMod :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing arg1 mod arg2.

Reference: s/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713

mkRem :: AST s -> AST s -> Z3 s (AST s) Source #

Create an (AST s) node representing arg1 rem arg2.

Reference: s/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff

mkLt :: AST s -> AST s -> Z3 s (AST s) Source #

Create less than.

Reference: s/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534

mkLe :: AST s -> AST s -> Z3 s (AST s) Source #

Create less than or equal to.

Reference: s/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf

mkGt :: AST s -> AST s -> Z3 s (AST s) Source #

Create greater than.

Reference: s/group__capi.html#ga46167b86067586bb742c0557d7babfd3

mkGe :: AST s -> AST s -> Z3 s (AST s) Source #

Create greater than or equal to.

Reference: s/group__capi.html#gad9245cbadb80b192323d01a8360fb942

mkInt2Real :: AST s -> Z3 s (AST s) Source #

Coerce an integer to a real.

Reference: s/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21

mkReal2Int :: AST s -> Z3 s (AST s) Source #

Coerce a real to an integer.

Reference: s/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d

mkIsInt :: AST s -> Z3 s (AST s) Source #

Check if a real number is an integer.

Reference: s/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3

Bit-vectors

mkBvnot :: AST s -> Z3 s (AST s) Source #

Bitwise negation.

Reference: s/group__capi.html#ga36cf75c92c54c1ca633a230344f23080

mkBvredand :: AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8

mkBvredor :: AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2

mkBvand :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise and.

Reference: s/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d

mkBvor :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise or.

Reference: s/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5

mkBvxor :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise exclusive-or.

Reference: s/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8

mkBvnand :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise nand.

Reference: s/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61

mkBvnor :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise nor.

Reference: s/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb

mkBvxnor :: AST s -> AST s -> Z3 s (AST s) Source #

Bitwise xnor.

Reference: s/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6

mkBvneg :: AST s -> Z3 s (AST s) Source #

Standard two's complement unary minus.

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

mkBvadd :: AST s -> AST s -> Z3 s (AST s) Source #

Standard two's complement addition.

Reference: s/group__capi.html#ga819814e33573f3f9948b32fdc5311158

mkBvsub :: AST s -> AST s -> Z3 s (AST s) Source #

Standard two's complement subtraction.

Reference: s/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e

mkBvmul :: AST s -> AST s -> Z3 s (AST s) Source #

Standard two's complement multiplication.

Reference: s/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c

mkBvudiv :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned division.

Reference: s/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544

mkBvsdiv :: AST s -> AST s -> Z3 s (AST s) Source #

Two's complement signed division.

Reference: s/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0

mkBvurem :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned remainder.

Reference: s/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d

mkBvsrem :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga46c18a3042fca174fe659d3185693db1

mkBvsmod :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879

mkBvult :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned less than.

Reference: s/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4

mkBvslt :: AST s -> AST s -> Z3 s (AST s) Source #

Two's complement signed less than.

Reference: s/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a

mkBvule :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned less than or equal to.

Reference: s/group__capi.html#gab738b89de0410e70c089d3ac9e696e87

mkBvsle :: AST s -> AST s -> Z3 s (AST s) Source #

Two's complement signed less than or equal to.

Reference: s/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d

mkBvuge :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned greater than or equal to.

Reference: s/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df

mkBvsge :: AST s -> AST s -> Z3 s (AST s) Source #

Two's complement signed greater than or equal to.

Reference: s/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5

mkBvugt :: AST s -> AST s -> Z3 s (AST s) Source #

Unsigned greater than.

Reference: s/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3

mkBvsgt :: AST s -> AST s -> Z3 s (AST s) Source #

Two's complement signed greater than.

Reference: s/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0

mkConcat :: AST s -> AST s -> Z3 s (AST s) Source #

Concatenate the given bit-vectors.

Reference: s/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa

mkExtract :: Int -> Int -> AST s -> Z3 s (AST s) 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: s/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317

mkSignExt :: Int -> AST s -> Z3 s (AST s) 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: s/group__capi.html#gad29099270b36d0680bb54b560353c10e

mkZeroExt :: Int -> AST s -> Z3 s (AST s) 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: s/group__capi.html#gac9322fae11365a78640baf9078c428b3

mkRepeat :: Int -> AST s -> Z3 s (AST s) Source #

Repeat the given bit-vector up length i.

Reference: s/group__capi.html#ga03e81721502ea225c264d1f556c9119d

mkBvshl :: AST s -> AST s -> Z3 s (AST s) Source #

Shift left.

Reference: s/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1

mkBvlshr :: AST s -> AST s -> Z3 s (AST s) Source #

Logical shift right.

Reference: s/group__capi.html#gac59645a6edadad79a201f417e4e0c512

mkBvashr :: AST s -> AST s -> Z3 s (AST s) Source #

Arithmetic shift right.

Reference: s/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4

mkRotateLeft :: Int -> AST s -> Z3 s (AST s) Source #

Rotate bits of t1 to the left i times.

Reference: s/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda

mkRotateRight :: Int -> AST s -> Z3 s (AST s) Source #

Rotate bits of t1 to the right i times.

Reference: s/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c

mkExtRotateLeft :: AST s -> AST s -> Z3 s (AST s) Source #

Rotate bits of t1 to the left t2 times.

Reference: s/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7

mkExtRotateRight :: AST s -> AST s -> Z3 s (AST s) Source #

Rotate bits of t1 to the right t2 times.

Reference: s/group__capi.html#gabb227526c592b523879083f12aab281f

mkInt2bv :: Int -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5

mkBv2int :: AST s -> Bool -> Z3 s (AST s) 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: s/group__capi.html#gac87b227dc3821d57258d7f53a28323d4

mkBvnegNoOverflow :: AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7

mkBvaddNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f

mkBvaddNoUnderflow :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947

mkBvsubNoOverflow :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c

mkBvsubNoUnderflow :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4

mkBvmulNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df

mkBvmulNoUnderflow :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga501ccc01d737aad3ede5699741717fda

mkBvsdivNoOverflow :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e

Arrays

mkSelect :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67

mkStore :: AST s -> AST s -> AST s -> Z3 s (AST s) Source #

Array update.

Reference: s/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593

mkConstArray :: Sort s -> AST s -> Z3 s (AST s) Source #

Create the constant array.

Reference: s/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d

mkMap :: FuncDecl s -> [AST s] -> Z3 s (AST s) Source #

map f on the the argument arrays.

Reference: s/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d

mkArrayDefault :: AST s -> Z3 s (AST s) 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: s/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d

Sets

mkEmptySet :: Sort s -> Z3 s (AST s) Source #

Create the empty set.

Reference: s/group__capi.html#ga358b6b80509a567148f1c0ca9252118c

mkFullSet :: Sort s -> Z3 s (AST s) Source #

Create the full set.

Reference: s/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2

mkSetAdd :: AST s -> AST s -> Z3 s (AST s) Source #

Add an element to a set.

Reference: s/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175

mkSetDel :: AST s -> AST s -> Z3 s (AST s) Source #

Remove an element from a set.

Reference: s/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d

mkSetUnion :: [AST s] -> Z3 s (AST s) Source #

Take the union of a list of sets.

Reference: s/group__capi.html#ga4050162a13d539b8913200963bb4743c

mkSetIntersect :: [AST s] -> Z3 s (AST s) Source #

Take the intersection of a list of sets.

Reference: s/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d

mkSetDifference :: AST s -> AST s -> Z3 s (AST s) Source #

Take the set difference between two sets.

Reference: s/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1

mkSetComplement :: AST s -> Z3 s (AST s) Source #

Take the complement of a set.

Reference: s/group__capi.html#ga5c57143c9229cdf730c5103ff696590f

mkSetMember :: AST s -> AST s -> Z3 s (AST s) Source #

Check for set membership.

Reference: s/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063

mkSetSubset :: AST s -> AST s -> Z3 s (AST s) Source #

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

Reference: s/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a

Numerals

mkNumeral :: String -> Sort s -> Z3 s (AST s) Source #

Create a numeral of a given sort.

Reference: s/group__capi.html#gac8aca397e32ca33618d8024bff32948c

mkInt :: Int -> Sort s -> Z3 s (AST s) Source #