-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Bindings for the Z3 Theorem Prover
--
@package z3
@version 0.3.2
-- | Low-level bindings to Z3 API.
--
-- There is (mostly) a one-to-one correspondence with Z3 C API, thus see
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html
-- for further details.
--
-- Note that these bindings still focus on the old Z3 3.x API, and will
-- not handle reference counting for you if you decide to use Z3 4.x API
-- functions. Mixing both API is known to cause some segmentation faults!
--
-- Supporting Z3 4.x API (and removing support for 3.x) is planned for
-- the 0.4 version of these bindings.
module Z3.Base
-- | A Z3 configuration object.
data Config
-- | A Z3 logical context.
data Context
-- | A Z3 symbol.
--
-- Used to name types, constants and functions.
data Symbol
-- | A Z3 AST node.
--
-- This is the data-structure used in Z3 to represent terms, formulas and
-- types.
data AST
-- | A kind of AST representing types.
data Sort
-- | A kind of AST representing function symbols.
data FuncDecl
-- | A kind of AST representing constant and function declarations.
data App
-- | A kind of AST representing pattern and multi-patterns to guide
-- quantifier instantiation.
data Pattern
-- | A model for the constraints asserted into the logical context.
data Model
-- | An interpretation of a function in a model.
data FuncInterp
-- | Representation of the value of a Z3_func_interp at a particular
-- point.
data FuncEntry
-- | A Z3 parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many
-- components such as: simplifiers, tactics, solvers, etc.
data Params
-- | A Z3 solver engine.
--
-- A(n) (incremental) solver, possibly specialized by a particular tactic
-- or logic.
data Solver
-- | Result of a satisfiability check.
--
-- This corresponds to the z3_lbool type in the C API.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result
-- | Create a configuration.
mkConfig :: IO Config
-- | Delete a configuration.
delConfig :: Config -> IO ()
-- | Run a computation using a temporally created configuration.
--
-- Note that the configuration object can be thrown away once it has been
-- used to create the Z3 Context.
withConfig :: (Config -> IO a) -> IO a
-- | Set a configuration parameter.
setParamValue :: Config -> String -> String -> IO ()
-- | Create a context using the given configuration.
mkContext :: Config -> IO Context
-- | Delete the given logical context.
delContext :: Context -> IO ()
-- | Run a computation using a temporally created context.
withContext :: Config -> (Context -> IO a) -> IO a
-- | Convert the given logical context into a string.
contextToString :: Context -> IO String
-- | Alias for contextToString.
-- | Deprecated: Use contextToString instead.
showContext :: Context -> IO String
-- | Create a Z3 symbol using an integer.
--
-- mkIntSymbol c i requires 0 <= i < 2^30
mkIntSymbol :: Integral int => Context -> int -> IO Symbol
-- | Create a Z3 symbol using a string.
mkStringSymbol :: Context -> String -> IO Symbol
-- | Create a free (uninterpreted) type using the given name (symbol).
--
-- Two free types are considered the same iff the have the same name.
mkUninterpretedSort :: Context -> Symbol -> IO Sort
-- | Create the boolean type.
--
-- This type is used to create propositional variables and predicates.
mkBoolSort :: Context -> IO Sort
-- | Create an integer type.
--
-- This is the type of arbitrary precision integers. A machine integer
-- can be represented using bit-vectors, see mkBvSort.
mkIntSort :: Context -> IO Sort
-- | Create a real type.
--
-- This type is not a floating point number. Z3 does not have support for
-- floating point numbers yet.
mkRealSort :: Context -> IO Sort
-- | Create a bit-vector type of the given size.
--
-- This type can also be seen as a machine integer.
--
-- mkBvSort c sz requires sz >= 0
mkBvSort :: Context -> Int -> IO Sort
-- | Create an array type
--
-- We usually represent the array type as: [domain -> range]. Arrays
-- are usually used to model the heap/memory in software verification.
mkArraySort :: Context -> Sort -> Sort -> IO Sort
-- | Create a tuple type
--
-- A tuple with n fields has a constructor and n projections. This
-- function will also declare the constructor and projection functions.
mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
-- | Declare a constant or function.
mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
-- | Create a constant or function application.
mkApp :: Context -> FuncDecl -> [AST] -> IO AST
-- | Declare and create a constant.
--
-- This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c
-- xd []
mkConst :: Context -> Symbol -> Sort -> IO AST
-- | Create an AST node representing true.
mkTrue :: Context -> IO AST
-- | Create an AST node representing false.
mkFalse :: Context -> IO AST
-- | Create an AST node representing l = r.
mkEq :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing not(a).
mkNot :: Context -> AST -> IO AST
-- | Create an AST node representing an if-then-else: ite(t1, t2,
-- t3).
mkIte :: Context -> AST -> AST -> AST -> IO AST
-- | Create an AST node representing t1 iff t2.
mkIff :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing t1 implies t2.
mkImplies :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing t1 xor t2.
mkXor :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing args[0] and ... and args[num_args-1].
mkAnd :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] or ... or args[num_args-1].
mkOr :: Context -> [AST] -> IO AST
-- | The distinct construct is used for declaring the arguments pairwise
-- distinct.
--
-- That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j
-- <- [i+1..length(args)-1] ]
mkDistinct :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] + ... + args[num_args-1].
mkAdd :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] * ... * args[num_args-1].
mkMul :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] - ... - args[num_args - 1].
mkSub :: Context -> [AST] -> IO AST
-- | Create an AST node representing -arg.
mkUnaryMinus :: Context -> AST -> IO AST
-- | Create an AST node representing arg1 div arg2.
mkDiv :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing arg1 mod arg2.
mkMod :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing arg1 rem arg2.
mkRem :: Context -> AST -> AST -> IO AST
-- | Create less than.
mkLt :: Context -> AST -> AST -> IO AST
-- | Create less than or equal to.
mkLe :: Context -> AST -> AST -> IO AST
-- | Create greater than.
mkGt :: Context -> AST -> AST -> IO AST
-- | Create greater than or equal to.
mkGe :: Context -> AST -> AST -> IO AST
-- | Coerce an integer to a real.
mkInt2Real :: Context -> AST -> IO AST
-- | Coerce a real to an integer.
mkReal2Int :: Context -> AST -> IO AST
-- | Check if a real number is an integer.
mkIsInt :: Context -> AST -> IO AST
-- | Bitwise negation.
mkBvnot :: Context -> AST -> IO AST
-- | Take conjunction of bits in vector, return vector of length 1.
mkBvredand :: Context -> AST -> IO AST
-- | Take disjunction of bits in vector, return vector of length 1.
mkBvredor :: Context -> AST -> IO AST
-- | Bitwise and.
mkBvand :: Context -> AST -> AST -> IO AST
-- | Bitwise or.
mkBvor :: Context -> AST -> AST -> IO AST
-- | Bitwise exclusive-or.
mkBvxor :: Context -> AST -> AST -> IO AST
-- | Bitwise nand.
mkBvnand :: Context -> AST -> AST -> IO AST
-- | Bitwise nor.
mkBvnor :: Context -> AST -> AST -> IO AST
-- | Bitwise xnor.
mkBvxnor :: Context -> AST -> AST -> IO AST
-- | Standard two's complement unary minus.
mkBvneg :: Context -> AST -> IO AST
-- | Standard two's complement addition.
mkBvadd :: Context -> AST -> AST -> IO AST
-- | Standard two's complement subtraction.
mkBvsub :: Context -> AST -> AST -> IO AST
-- | Standard two's complement multiplication.
mkBvmul :: Context -> AST -> AST -> IO AST
-- | Unsigned division.
mkBvudiv :: Context -> AST -> AST -> IO AST
-- | Two's complement signed division.
mkBvsdiv :: Context -> AST -> AST -> IO AST
-- | Unsigned remainder.
mkBvurem :: Context -> AST -> AST -> IO AST
-- | Two's complement signed remainder (sign follows dividend).
mkBvsrem :: Context -> AST -> AST -> IO AST
-- | Two's complement signed remainder (sign follows divisor).
mkBvsmod :: Context -> AST -> AST -> IO AST
-- | Unsigned less than.
mkBvult :: Context -> AST -> AST -> IO AST
-- | Two's complement signed less than.
mkBvslt :: Context -> AST -> AST -> IO AST
-- | Unsigned less than or equal to.
mkBvule :: Context -> AST -> AST -> IO AST
-- | Two's complement signed less than or equal to.
mkBvsle :: Context -> AST -> AST -> IO AST
-- | Unsigned greater than or equal to.
mkBvuge :: Context -> AST -> AST -> IO AST
-- | Two's complement signed greater than or equal to.
mkBvsge :: Context -> AST -> AST -> IO AST
-- | Unsigned greater than.
mkBvugt :: Context -> AST -> AST -> IO AST
-- | Two's complement signed greater than.
mkBvsgt :: Context -> AST -> AST -> IO AST
-- | Concatenate the given bit-vectors.
mkConcat :: Context -> AST -> AST -> IO AST
-- | 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.
mkExtract :: Context -> Int -> Int -> AST -> IO AST
-- | 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.
mkSignExt :: Context -> Int -> AST -> IO AST
-- | 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.
mkZeroExt :: Context -> Int -> AST -> IO AST
-- | Repeat the given bit-vector up length i.
mkRepeat :: Context -> Int -> AST -> IO AST
-- | Shift left.
mkBvshl :: Context -> AST -> AST -> IO AST
-- | Logical shift right.
mkBvlshr :: Context -> AST -> AST -> IO AST
-- | Arithmetic shift right.
mkBvashr :: Context -> AST -> AST -> IO AST
-- | Rotate bits of t1 to the left i times.
mkRotateLeft :: Context -> Int -> AST -> IO AST
-- | Rotate bits of t1 to the right i times.
mkRotateRight :: Context -> Int -> AST -> IO AST
-- | Rotate bits of t1 to the left t2 times.
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
-- | Rotate bits of t1 to the right t2 times.
mkExtRotateRight :: Context -> AST -> AST -> IO AST
-- | Create an n bit bit-vector from the integer argument t1.
mkInt2bv :: Context -> Int -> AST -> IO AST
-- | 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.
mkBv2int :: Context -> AST -> Bool -> IO AST
-- | Check that bit-wise negation does not overflow when t1 is
-- interpreted as a signed bit-vector.
mkBvnegNoOverflow :: Context -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise addition of t1
-- and t2 does not overflow.
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-- | Create a predicate that checks that the bit-wise signed addition of
-- t1 and t2 does not underflow.
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise signed subtraction of
-- t1 and t2 does not overflow.
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise subtraction of
-- t1 and t2 does not underflow.
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise multiplication of
-- t1 and t2 does not overflow.
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-- | Create a predicate that checks that the bit-wise signed multiplication
-- of t1 and t2 does not underflow.
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise signed division of
-- t1 and t2 does not overflow.
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
-- | Array read. The argument a is the array and i is the index of the
-- array that gets read.
mkSelect :: Context -> AST -> AST -> IO AST
-- | Array update.
--
-- The result of this function is an array that is equal to the input
-- array (with respect to select) on all indices except for i, where it
-- maps to v.
--
-- The semantics of this function is given by the theory of arrays
-- described in the SMT-LIB standard. See http://smtlib.org for
-- more details.
mkStore :: Context -> AST -> AST -> AST -> IO AST
-- | Create the constant array.
--
-- The resulting term is an array, such that a select on an arbitrary
-- index produces the value v.
mkConstArray :: Context -> Sort -> AST -> IO AST
-- | Map a function f on the the argument arrays.
--
-- The n nodes args must be of array sorts [domain -> range_i].
-- The function declaration f must have type range_1 .. range_n
-- -> range. The sort of the result is [domain -> range].
mkMap :: Context -> FuncDecl -> [AST] -> IO AST
-- | Access the array default value.
--
-- Produces the default range value, for arrays that can be represented
-- as finite maps with a default range value.
mkArrayDefault :: Context -> AST -> IO AST
-- | Create a numeral of a given sort.
mkNumeral :: Context -> String -> Sort -> IO AST
-- | Create a numeral of sort int.
mkInt :: Integral a => Context -> a -> IO AST
-- | Create a numeral of sort real.
mkReal :: Real r => Context -> r -> IO AST
-- | Create a pattern for quantifier instantiation.
--
-- Z3 uses pattern matching to instantiate quantifiers. If a pattern is
-- not provided for a quantifier, then Z3 will automatically compute a
-- set of patterns for it. However, for optimal performance, the user
-- should provide the patterns.
--
-- Patterns comprise a list of terms. The list should be non-empty. If
-- the list comprises of more than one term, it is a called a
-- multi-pattern.
--
-- In general, one can pass in a list of (multi-)patterns in the
-- quantifier constructor.
mkPattern :: Context -> [AST] -> IO Pattern
-- | Create a bound variable.
--
-- Bound variables are indexed by de-Bruijn indices.
--
-- See
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e
mkBound :: Context -> Int -> Sort -> IO AST
-- | Create a forall formula.
--
-- The bound variables are de-Bruijn indices created using
-- mkBound.
--
-- Z3 applies the convention that the last element in xs refers to
-- the variable with index 0, the second to last element of xs
-- refers to the variable with index 1, etc.
mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
-- | Create an exists formula.
--
-- Similar to mkForall.
mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
-- | Create a universal quantifier using a list of constants that will form
-- the set of bound variables.
mkForallConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
-- | Create a existential quantifier using a list of constants that will
-- form the set of bound variables.
mkExistsConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
-- | Return the size of the given bit-vector sort.
getBvSortSize :: Context -> Sort -> IO Int
-- | Return the sort of an AST node.
getSort :: Context -> AST -> IO Sort
-- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and
-- Z3_L_UNDEF otherwise.
getBool :: Context -> AST -> IO (Maybe Bool)
-- | Return Z3Int value
getInt :: Context -> AST -> IO Integer
-- | Return Z3Real value
getReal :: Context -> AST -> IO Rational
-- | Convert an ast into an APP_AST. This is just type casting.
toApp :: Context -> AST -> IO App
-- | The interpretation of a function.
data FuncModel
FuncModel :: [([AST], AST)] -> AST -> FuncModel
-- | Mapping from arguments to values.
interpMap :: FuncModel -> [([AST], AST)]
-- | Default value.
interpElse :: FuncModel -> AST
-- | Evaluate an AST node in the given model.
--
-- The evaluation may fail for the following reasons:
--
--
-- - t contains a quantifier.
-- - the model m is partial.
-- - t is type incorrect.
--
eval :: Context -> Model -> AST -> IO (Maybe AST)
-- | Evaluate a collection of AST nodes in the given model.
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
-- | Evaluate a function declaration to a list of argument/value pairs.
evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
-- | Evaluate an array as a function, if possible.
evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
-- | Return the interpretation of the function f in the model m. Return
-- NULL, if the model does not assign an interpretation for f. That
-- should be interpreted as: the f does not matter.
getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
-- | The (_ as-array f) AST node is a construct for assigning
-- interpretations for arrays in Z3. It is the array such that forall
-- indices i we have that (select (_ as-array f) i) is equal to (f i).
-- This procedure returns Z3_TRUE if the a is an as-array AST node.
isAsArray :: Context -> AST -> IO Bool
-- | Return the function declaration f associated with a (_ as_array f)
-- node.
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
-- | Return the number of entries in the given function interpretation.
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
-- | Return a _point_ of the given function intepretation. It represents
-- the value of f in a particular point.
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
-- | Return the 'else' value of the given function interpretation.
funcInterpGetElse :: Context -> FuncInterp -> IO AST
-- | Return the arity (number of arguments) of the given function
-- interpretation.
funcInterpGetArity :: Context -> FuncInterp -> IO Int
-- | Return the value of this point.
funcEntryGetValue :: Context -> FuncEntry -> IO AST
-- | Return the number of arguments in a Z3_func_entry object.
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
-- | Return an argument of a Z3_func_entry object.
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
-- | Convert the given model into a string.
modelToString :: Context -> Model -> IO String
-- | Alias for modelToString.
-- | Deprecated: Use modelToString instead.
showModel :: Context -> Model -> IO String
-- | Assert a constraing into the logical context.
assertCnstr :: Context -> AST -> IO ()
-- | Check whether the given logical context is consistent or not.
check :: Context -> IO Result
-- | Check whether the given logical context is consistent or not.
--
-- If the logical context is not unsatisfiable and model construction is
-- enabled (via mkConfig), then a model is returned. The caller is
-- responsible for deleting the model using the function delModel.
checkAndGetModel :: Context -> IO (Result, Maybe Model)
-- | Check whether the given logical context is consistent or not.
-- | Deprecated: Use checkAndGetModel instead.
getModel :: Context -> IO (Result, Maybe Model)
-- | Delete a model object.
delModel :: Context -> Model -> IO ()
-- | Create a backtracking point.
push :: Context -> IO ()
-- | Backtrack n backtracking points.
pop :: Context -> Int -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
mkParams :: Context -> IO Params
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
paramsToString :: Context -> Params -> IO String
-- | Solvers available in Z3.
--
-- These are described at http://smtlib.cs.uiowa.edu/logics.html
--
-- WARNING: Support for solvers is fragile, you may experience
-- segmentation faults!
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
data Logic
-- | 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.
AUFLIA :: Logic
-- | Closed linear formulas with free sort and function symbols over one-
-- and two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Closed formulas with free function and predicate symbols over a theory
-- of arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Closed linear formulas in linear real arithmetic.
LRA :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays.
QF_ABV :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Closed quantifier-free linear formulas over the theory of integer
-- arrays extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Closed quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Closed quantifier-free formulas over the theory of fixed-size
-- bitvectors.
QF_BV :: Logic
-- | 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_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | 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_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
mkSolver :: Context -> IO Solver
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
mkSimpleSolver :: Context -> IO Solver
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
mkSolverForLogic :: Context -> Logic -> IO Solver
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverSetParams :: Context -> Solver -> Params -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverPush :: Context -> Solver -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverPop :: Context -> Solver -> Int -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverReset :: Context -> Solver -> IO ()
-- | Number of backtracking points.
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverGetNumScopes :: Context -> Solver -> IO Int
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverAssertCnstr :: Context -> Solver -> AST -> IO ()
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
-- | Check whether the assertions in a given solver are consistent or not.
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverCheck :: Context -> Solver -> IO Result
solverGetModel :: Context -> Solver -> IO Model
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
solverGetReasonUnknown :: Context -> Solver -> IO String
-- | Convert the given solver into a string.
solverToString :: Context -> Solver -> IO String
-- | Pretty-printing mode for converting ASTs to strings. The mode can be
-- one of the following:
--
--
-- - Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
-- format.
-- - Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
-- - Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
-- format.
-- - Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
-- compliant format.
--
data ASTPrintMode
Z3_PRINT_SMTLIB_FULL :: ASTPrintMode
Z3_PRINT_LOW_LEVEL :: ASTPrintMode
Z3_PRINT_SMTLIB_COMPLIANT :: ASTPrintMode
Z3_PRINT_SMTLIB2_COMPLIANT :: ASTPrintMode
-- | Set the pretty-printing mode for converting ASTs to strings.
setASTPrintMode :: Context -> ASTPrintMode -> IO ()
-- | Convert an AST to a string.
astToString :: Context -> AST -> IO String
-- | Convert a pattern to a string.
patternToString :: Context -> Pattern -> IO String
-- | Convert a sort to a string.
sortToString :: Context -> Sort -> IO String
-- | Convert a FuncDecl to a string.
funcDeclToString :: Context -> FuncDecl -> IO String
-- | Convert the given benchmark into SMT-LIB formatted string.
--
-- The output format can be configured via setASTPrintMode.
benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String
data Version
Version :: !Int -> !Int -> !Int -> !Int -> Version
z3Major :: Version -> !Int
z3Minor :: Version -> !Int
z3Build :: Version -> !Int
z3Revision :: Version -> !Int
-- | Return Z3 version number information.
getVersion :: IO Version
-- | Z3 exceptions.
data Z3Error
Z3Error :: Z3ErrorCode -> String -> Z3Error
errCode :: Z3Error -> Z3ErrorCode
errMsg :: Z3Error -> String
data Z3ErrorCode
SortError :: Z3ErrorCode
IOB :: Z3ErrorCode
InvalidArg :: Z3ErrorCode
ParserError :: Z3ErrorCode
NoParser :: Z3ErrorCode
InvalidPattern :: Z3ErrorCode
MemoutFail :: Z3ErrorCode
FileAccessError :: Z3ErrorCode
InternalFatal :: Z3ErrorCode
InvalidUsage :: Z3ErrorCode
DecRefError :: Z3ErrorCode
Z3Exception :: Z3ErrorCode
instance Typeable AST
instance Typeable FuncDecl
instance Typeable Z3ErrorCode
instance Typeable Z3Error
instance Eq Config
instance Eq Context
instance Eq Symbol
instance Ord Symbol
instance Show Symbol
instance Storable Symbol
instance Eq AST
instance Ord AST
instance Show AST
instance Storable AST
instance Eq Sort
instance Ord Sort
instance Show Sort
instance Storable Sort
instance Eq FuncDecl
instance Ord FuncDecl
instance Show FuncDecl
instance Storable FuncDecl
instance Eq App
instance Ord App
instance Show App
instance Storable App
instance Eq Pattern
instance Ord Pattern
instance Show Pattern
instance Storable Pattern
instance Eq Model
instance Eq FuncInterp
instance Eq FuncEntry
instance Eq Params
instance Eq Solver
instance Eq Result
instance Ord Result
instance Read Result
instance Show Result
instance Show Z3ErrorCode
instance Eq Version
instance Ord Version
instance Marshal Solver (Ptr Z3_solver)
instance Marshal Pattern (Ptr Z3_pattern)
instance Marshal Model (Ptr Z3_model)
instance Marshal FuncInterp (Ptr Z3_func_interp)
instance Marshal FuncEntry (Ptr Z3_func_entry)
instance Marshal FuncDecl (Ptr Z3_func_decl)
instance Marshal Sort (Ptr Z3_sort)
instance Marshal AST (Ptr Z3_ast)
instance Marshal Symbol (Ptr Z3_symbol)
instance Marshal Params (Ptr Z3_params)
instance Marshal App (Ptr Z3_app)
instance Marshal String CString
instance Marshal Double CDouble
instance Integral h => Marshal h CULLong
instance Integral h => Marshal h CLLong
instance Integral h => Marshal h CUInt
instance Integral h => Marshal h CInt
instance Marshal Result Z3_lbool
instance Marshal Bool Z3_bool
instance Marshal () ()
instance Marshal h (Ptr x) => Marshal (Maybe h) (Ptr x)
instance Show Version
instance Exception Z3Error
instance Show Z3Error
instance Show Logic
-- | Configuring Z3.
--
-- Z3 has plenty of configuration options and these vary quite a lot
-- across Z3 versions, being hard to design a proper abstraction. We
-- decided to keep this simple.
module Z3.Opts
-- | Z3 configuration.
data Opts
-- | Set configuration.
--
-- If you are using Lang or Monad interfaces, you don't
-- need to call this function directly, just pass your Opts to
-- evalZ3*.
setOpts :: Config -> Opts -> IO ()
-- | Default configuration.
stdOpts :: Opts
-- | Append configurations.
(+?) :: Opts -> Opts -> Opts
-- | Set a configuration option.
opt :: OptValue val => String -> val -> Opts
-- | Values for Z3 options.
class OptValue val
instance OptValue [Char]
instance OptValue Double
instance OptValue Integer
instance OptValue Int
instance OptValue Bool
instance Monoid Opts
-- | A simple monadic wrapper for Base.
module Z3.Monad
class (Monad m, MonadIO m) => MonadZ3 m
getSolver :: MonadZ3 m => m (Maybe Solver)
getContext :: MonadZ3 m => m Context
data Z3 a
-- | Solvers available in Z3.
--
-- These are described at http://smtlib.cs.uiowa.edu/logics.html
--
-- WARNING: Support for solvers is fragile, you may experience
-- segmentation faults!
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
data Logic
-- | 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.
AUFLIA :: Logic
-- | Closed linear formulas with free sort and function symbols over one-
-- and two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Closed formulas with free function and predicate symbols over a theory
-- of arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Closed linear formulas in linear real arithmetic.
LRA :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays.
QF_ABV :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Closed quantifier-free linear formulas over the theory of integer
-- arrays extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Closed quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Closed quantifier-free formulas over the theory of fixed-size
-- bitvectors.
QF_BV :: Logic
-- | 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_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | 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_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
-- | Eval a Z3 script with default configuration options.
evalZ3 :: Z3 a -> IO a
-- | Eval a Z3 script.
evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
-- | Z3 environment.
data Z3Env
-- | Create a new Z3 environment.
--
-- Until we move to Z3 API 4.0 you need to manually freed this
-- environment using delEnv.
newEnv :: Maybe Logic -> Opts -> IO Z3Env
-- | Free a Z3 environment.
delEnv :: Z3Env -> IO ()
-- | 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).
evalZ3WithEnv :: Z3 a -> Z3Env -> IO a
-- | A Z3 symbol.
--
-- Used to name types, constants and functions.
data Symbol
-- | A Z3 AST node.
--
-- This is the data-structure used in Z3 to represent terms, formulas and
-- types.
data AST
-- | A kind of AST representing types.
data Sort
-- | A kind of AST representing function symbols.
data FuncDecl
-- | A kind of AST representing constant and function declarations.
data App
-- | A kind of AST representing pattern and multi-patterns to guide
-- quantifier instantiation.
data Pattern
-- | A model for the constraints asserted into the logical context.
data Model
-- | A Z3 logical context.
data Context
-- | An interpretation of a function in a model.
data FuncInterp
-- | Representation of the value of a Z3_func_interp at a particular
-- point.
data FuncEntry
-- | The interpretation of a function.
data FuncModel
FuncModel :: [([AST], AST)] -> AST -> FuncModel
-- | Mapping from arguments to values.
interpMap :: FuncModel -> [([AST], AST)]
-- | Default value.
interpElse :: FuncModel -> AST
-- | A Z3 solver engine.
--
-- A(n) (incremental) solver, possibly specialized by a particular tactic
-- or logic.
data Solver
-- | Result of a satisfiability check.
--
-- This corresponds to the z3_lbool type in the C API.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result
-- | Convert Z3's logical context into a string.
contextToString :: MonadZ3 z3 => z3 String
-- | Alias for contextToString.
showContext :: MonadZ3 z3 => z3 String
-- | Create a Z3 symbol using an integer.
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
-- | Create a Z3 symbol using a string.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
-- | 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
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
-- | Create the boolean type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342
mkBoolSort :: MonadZ3 z3 => z3 Sort
-- | Create the integer type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015
mkIntSort :: MonadZ3 z3 => z3 Sort
-- | Create the real type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0
mkRealSort :: MonadZ3 z3 => z3 Sort
-- | 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
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
-- | Create an array type
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445
mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
-- | Create a tuple type
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1
mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
-- | A Z3 function
mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
-- | Create a constant or function application.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
-- | Declare and create a constant.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef
mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
-- | Create an AST node representing true.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7
mkTrue :: MonadZ3 z3 => z3 AST
-- | Create an AST node representing false.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d
mkFalse :: MonadZ3 z3 => z3 AST
-- | Create an AST node representing l = r.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c
mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing not(a).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072
mkNot :: MonadZ3 z3 => AST -> z3 AST
-- | 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
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
-- | Create an AST node representing t1 iff t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042
mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing t1 implies t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing t1 xor t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec
mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
-- | 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
mkOr :: MonadZ3 z3 => [AST] -> z3 AST
-- | 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
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
-- | 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
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
-- | 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
mkMul :: MonadZ3 z3 => [AST] -> z3 AST
-- | 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#ga4f5fea9b683f9e674fd8f14d676cc9a9
mkSub :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing -arg.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
-- | Create an AST node representing arg1 div arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3
mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing arg1 mod arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713
mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing arg1 rem arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff
mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534
mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf
mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3
mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942
mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Coerce an integer to a real.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
-- | Coerce a real to an integer.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
-- | Check if a real number is an integer.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3
mkIsInt :: MonadZ3 z3 => AST -> z3 AST
-- | Bitwise negation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080
mkBvnot :: MonadZ3 z3 => AST -> z3 AST
-- | 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
mkBvredand :: MonadZ3 z3 => AST -> z3 AST
-- | 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
mkBvredor :: MonadZ3 z3 => AST -> z3 AST
-- | Bitwise and.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d
mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise or.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5
mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise exclusive-or.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8
mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise nand.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61
mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise nor.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb
mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise xnor.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6
mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement unary minus.
--
-- Reference:
-- <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
mkBvneg :: MonadZ3 z3 => AST -> z3 AST
-- | Standard two's complement addition.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158
mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement subtraction.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e
mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement multiplication.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c
mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned division.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544
mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed division.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0
mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned remainder.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d
mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed remainder (sign follows dividend).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed remainder (sign follows divisor).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4
mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a
mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87
mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d
mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df
mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3
mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0
mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Concatenate the given bit-vectors.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa
mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
-- | 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
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | 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
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Repeat the given bit-vector up length i.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d
mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Shift left.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1
mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Logical shift right.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512
mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Arithmetic shift right.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4
mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Rotate bits of t1 to the left i times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda
mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Rotate bits of t1 to the right i times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c
mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Rotate bits of t1 to the left t2 times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7
mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Rotate bits of t1 to the right t2 times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | 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
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
-- | 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
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
-- | 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
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
-- | 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
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
-- | 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
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | 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
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Array update.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593
mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
-- | Create the constant array.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d
mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
-- | map f on the the argument arrays.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d
mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
-- | Access the array default value. Produces the default range value, for
-- arrays that can be represented as finite maps with a default range
-- value.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
-- | Create a numeral of a given sort.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c
mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
-- | Create a numeral of sort int.
mkInt :: (MonadZ3 z3, Integral a) => a -> z3 AST
-- | Create a numeral of sort real.
mkReal :: (MonadZ3 z3, Real r) => r -> z3 AST
mkPattern :: MonadZ3 z3 => [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
-- | Return the size of the given bit-vector sort.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
-- | Returns Just True, Just False, or Nothing
-- for undefined.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4
getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
-- | Return the integer value
getInt :: MonadZ3 z3 => AST -> z3 Integer
-- | Return rational value
getReal :: MonadZ3 z3 => AST -> z3 Rational
-- | Cast AST into an App.
toApp :: MonadZ3 z3 => AST -> z3 App
-- | Evaluate an AST node in the given model.
eval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST)
-- | Evaluate a collection of AST nodes in the given model.
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
-- | Get function as a list of argument/value pairs.
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
-- | Get array as a list of argument/value pairs, if it is represented as a
-- function (ie, using as-array).
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
-- | Return the interpretation of the function f in the model m. Return
-- NULL, if the model does not assign an interpretation for f. That
-- should be interpreted as: the f does not matter.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
-- | The (_ as-array f) AST node is a construct for assigning
-- interpretations for arrays in Z3. It is the array such that forall
-- indices i we have that (select (_ as-array f) i) is equal to (f i).
-- This procedure returns Z3_TRUE if the a is an as-array AST node.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa
isAsArray :: MonadZ3 z3 => AST -> z3 Bool
-- | Return the function declaration f associated with a (_ as_array f)
-- node.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
-- | Return the number of entries in the given function interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
-- | Return a "point" of the given function intepretation. It represents
-- the value of f in a particular point.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
-- | Return the 'else' value of the given function interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
-- | Return the arity (number of arguments) of the given function
-- interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
-- | Return the value of this point.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
-- | Return the number of arguments in a Z3_func_entry object.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
-- | Return an argument of a Z3_func_entry object.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
-- | Convert the given model into a string.
modelToString :: MonadZ3 z3 => Model -> z3 String
-- | Alias for modelToString.
showModel :: MonadZ3 z3 => Model -> z3 String
-- | Assert a constraing into the logical context.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a
assertCnstr :: MonadZ3 z3 => AST -> z3 ()
-- | Check whether the given logical context is consistent or not.
check :: MonadZ3 z3 => z3 Result
-- | Get model.
--
-- Reference :
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
-- | Delete a model object.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee
delModel :: MonadZ3 z3 => Model -> z3 ()
withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
-- | Create a backtracking point.
push :: MonadZ3 z3 => z3 ()
-- | Backtrack n backtracking points.
pop :: MonadZ3 z3 => Int -> z3 ()
-- | Run a query and restore the initial logical context.
--
-- This is a shorthand for push, run the query, and pop.
local :: MonadZ3 z3 => z3 a -> z3 a
-- | Backtrack all the way.
reset :: MonadZ3 z3 => z3 ()
-- | Get number of backtracking points.
getNumScopes :: MonadZ3 z3 => z3 Int
-- | Pretty-printing mode for converting ASTs to strings. The mode can be
-- one of the following:
--
--
-- - Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
-- format.
-- - Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
-- - Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
-- format.
-- - Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
-- compliant format.
--
data ASTPrintMode
Z3_PRINT_SMTLIB_FULL :: ASTPrintMode
Z3_PRINT_LOW_LEVEL :: ASTPrintMode
Z3_PRINT_SMTLIB_COMPLIANT :: ASTPrintMode
Z3_PRINT_SMTLIB2_COMPLIANT :: ASTPrintMode
-- | Set the mode for converting expressions to strings.
setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
-- | Convert an AST to a string.
astToString :: MonadZ3 z3 => AST -> z3 String
-- | Convert a pattern to a string.
patternToString :: MonadZ3 z3 => Pattern -> z3 String
-- | Convert a sort to a string.
sortToString :: MonadZ3 z3 => Sort -> z3 String
-- | Convert a FuncDecl to a string.
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
-- | Convert the solver to a string.
solverToString :: MonadZ3 z3 => z3 String
-- | Convert the given benchmark into SMT-LIB formatted string.
--
-- The output format can be configured via setASTPrintMode.
benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
data Version
Version :: !Int -> !Int -> !Int -> !Int -> Version
z3Major :: Version -> !Int
z3Minor :: Version -> !Int
z3Build :: Version -> !Int
z3Revision :: Version -> !Int
-- | Return Z3 version number information.
getVersion :: MonadZ3 z3 => z3 Version
instance Functor Z3
instance Applicative Z3
instance Monad Z3
instance MonadIO Z3
instance MonadZ3 Z3
-- | Deprecated: The Z3.Lang interface will be moved to a dedicated
-- package.
module Z3.Lang.Prelude
-- | Z3 monad.
data Z3 a
-- | Result of a satisfiability check.
--
-- This corresponds to the z3_lbool type in the C API.
data Result
-- | Eval a Z3 script.
evalZ3 :: Z3 a -> IO a
data Args
Args :: Maybe Logic -> Maybe Int -> Opts -> Args
-- | the logic to use; see http://smtlib.cs.uiowa.edu/logics.html
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
logic :: Args -> Maybe Logic
-- | soft timeout (in milliseconds)
softTimeout :: Args -> Maybe Int
-- | Z3 options
options :: Args -> Opts
stdArgs :: Args
-- | Solvers available in Z3.
--
-- These are described at http://smtlib.cs.uiowa.edu/logics.html
--
-- WARNING: Support for solvers is fragile, you may experience
-- segmentation faults!
-- | Warning: New Z3 API support is still incomplete and fragile: you
-- may experience segmentation faults!
data Logic
-- | 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.
AUFLIA :: Logic
-- | Closed linear formulas with free sort and function symbols over one-
-- and two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Closed formulas with free function and predicate symbols over a theory
-- of arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Closed linear formulas in linear real arithmetic.
LRA :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays.
QF_ABV :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Closed quantifier-free linear formulas over the theory of integer
-- arrays extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Closed quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Closed quantifier-free formulas over the theory of fixed-size
-- bitvectors.
QF_BV :: Logic
-- | 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_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | 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_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
-- | Eval a Z3 script.
evalZ3With :: Args -> Z3 a -> IO a
-- | Declare skolem variables.
var :: IsTy a => Z3 (Expr a)
-- | Declare skolem variables with a user specified name.
namedVar :: IsTy a => String -> Z3 (Expr a)
-- | Declare uninterpreted function of arity 1.
fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b)
-- | Declare uninterpreted function of arity 2.
fun2 :: (IsTy a, IsTy b, IsTy c) => Z3 (Expr a -> Expr b -> Expr c)
-- | Declare uninterpreted function of arity 3.
fun3 :: (IsTy a, IsTy b, IsTy c, IsTy d) => Z3 (Expr a -> Expr b -> Expr c -> Expr d)
-- | Declare uninterpreted function of arity 4.
fun4 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e) => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e)
-- | Declare uninterpreted function of arity 5.
fun5 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e, IsTy f) => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e -> Expr f)
-- | Make assertion in current context.
assert :: Expr Bool -> Z3 ()
-- | Introduce an auxiliary declaration to name a given expression.
--
-- If you really want sharing use this instead of Haskell's let.
let_ :: IsTy a => Expr a -> Z3 (Expr a)
-- | Check whether the given logical context is consistent or not.
check :: MonadZ3 z3 => z3 Result
-- | Alias for contextToString.
showContext :: MonadZ3 z3 => z3 String
-- | Convert an Expr to a string.
exprToString :: Compilable (Expr a) => Expr a -> Z3 String
-- | Create a backtracking point.
push :: MonadZ3 z3 => z3 ()
-- | Backtrack n backtracking points.
pop :: MonadZ3 z3 => Int -> z3 ()
-- | Return Z3 version number information.
getVersion :: MonadZ3 z3 => z3 Version
-- | A computation derived from a model.
data Model a
-- | Check satisfiability and evaluate a model if some exists.
checkModel :: Model a -> Z3 (Maybe a)
-- | Check satisfiability and evaluate a model if some exists.
checkModelWith :: (Result -> Maybe a -> b) -> Model a -> Z3 b
-- | Check satisfiability and evaluate a model if some exists, also
-- returning a Result to the reason for any failure.
checkModelWithResult :: Model a -> Z3 (Result, Maybe a)
-- | Show Z3's internal model.
showModel :: Model String
-- | Evaluate an expression within a model.
eval :: IsTy a => Expr a -> Model a
-- | Evaluate a collection of expressions within a model.
evalT :: (IsTy a, Traversable t) => t (Expr a) -> Model (t a)
-- | Expressions.
data Expr :: * -> *
-- | Quantifier pattern.
data Pattern
Pat :: Expr a -> Pattern
-- | Types for expressions.
class (Eq a, Show a, Typeable a, Compilable (Expr a)) => IsTy a
-- | Numeric types.
class (IsTy a, Num a) => IsNum a
-- | Typeclass for Haskell Z3 numbers of int sort in Z3.
class (IsNum a, Integral a) => IsInt a
-- | Typeclass for Haskell Z3 numbers of real sort in Z3.
class (IsNum a, Fractional a, Real a) => IsReal a
-- | Convertible types.
class (IsTy a, IsTy b) => Castable a b
-- | literal constructor.
literal :: IsTy a => a -> Expr a
-- | Boolean literals.
true :: Expr Bool
-- | Boolean literals.
false :: Expr Bool
-- | Boolean negation
not_ :: Expr Bool -> Expr Bool
-- | Boolean variadic and.
and_ :: [Expr Bool] -> Expr Bool
-- | Boolean binary and.
(&&*) :: Expr Bool -> Expr Bool -> Expr Bool
-- | Boolean variadic or.
or_ :: [Expr Bool] -> Expr Bool
-- | Boolean binary or.
(||*) :: Expr Bool -> Expr Bool -> Expr Bool
-- | Boolean variadic distinct.
distinct :: IsTy a => [Expr a] -> Expr Bool
-- | Boolean binary xor.
xor :: Expr Bool -> Expr Bool -> Expr Bool
-- | Boolean implication
implies :: Expr Bool -> Expr Bool -> Expr Bool
-- | An alias for implies.
(==>) :: Expr Bool -> Expr Bool -> Expr Bool
-- | Boolean if and only if.
iff :: Expr Bool -> Expr Bool -> Expr Bool
-- | An alias for iff.
(<=>) :: Expr Bool -> Expr Bool -> Expr Bool
-- | Universally quantified formula.
forall :: QExpr t => t -> Expr Bool
-- | Existentially quantified formula.
exists :: QExpr t => t -> Expr Bool
-- | Pattern-based instantiation.
instanceWhen :: Expr Bool -> [Pattern] -> QBody
-- | Integer division.
(//) :: IsInt a => Expr a -> Expr a -> Expr a
-- | Integer modulo.
(%*) :: IsInt a => Expr a -> Expr a -> Expr a
-- | Integer remainder.
(%%) :: IsInt a => Expr a -> Expr a -> Expr a
-- |
-- k divides n == n %* k ==* 0
--
divides :: IsInt a => Expr a -> Expr a -> Expr Bool
-- | Equals.
(==*) :: IsTy a => Expr a -> Expr a -> Expr Bool
-- | Not equals.
(/=*) :: IsTy a => Expr a -> Expr a -> Expr Bool
-- | Less or equals than.
(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool
-- | Less than.
(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool
-- | Greater or equals than.
(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool
-- | Greater than.
(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool
-- | Minimum.
min_ :: IsNum a => Expr a -> Expr a -> Expr a
-- | Maximum.
max_ :: IsNum a => Expr a -> Expr a -> Expr a
-- | if-then-else.
ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a
-- | Casting between compatible types
cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b
instance [incoherent] Typeable Expr
instance [incoherent] Applicative Model
instance [incoherent] Functor Model
instance [incoherent] Monad Model
instance [incoherent] Compilable Pattern
instance [incoherent] IsTy a => Compilable (FunApp a)
instance [incoherent] (IsTy a, IsFun (b -> c)) => IsFun (a -> b -> c)
instance [incoherent] (IsTy a, IsTy b) => IsFun (a -> b)
instance [incoherent] IsReal Rational
instance [incoherent] IsNum Rational
instance [incoherent] IsTy Rational
instance [incoherent] Compilable (Expr Rational)
instance [incoherent] IsInt Integer
instance [incoherent] IsNum Integer
instance [incoherent] IsTy Integer
instance [incoherent] Compilable (Expr Integer)
instance [incoherent] (IsTy a, QExpr t) => QExpr (Expr a -> t)
instance [incoherent] IsTy a => QExpr (Expr a -> QBody)
instance [incoherent] IsTy a => QExpr (Expr a -> Expr Bool)
instance [incoherent] IsTy Bool
instance [incoherent] Compilable (Expr Bool)
instance [incoherent] Castable Rational Integer
instance [incoherent] Castable Integer Rational
instance [incoherent] IsReal a => Fractional (Expr a)
instance [incoherent] IsNum a => Num (Expr a)
-- | Deprecated: The Z3.Lang interface will be moved to a dedicated
-- package.
module Z3.Lang.Lg2
-- | Ceiling logarithm base two. Axiomatization of the lg2 function.
-- Most likely Z3 is going to diverge if you use lg2 to specify a
-- satisfiable problem since it cannot construct a recursive definition
-- for lg2, but it should work fine for unsatisfiable instances.
declareLg2 :: IsInt a => Z3 (Expr a -> Expr a)
-- | Deprecated: The Z3.Lang interface will be moved to a dedicated
-- package.
module Z3.Lang.Pow2
-- | Raise to the power of 2. Axiomatization of the 2^n function.
-- Most likely Z3 is going to diverge if you use 2^n to specify a
-- satisfiable problem, since it cannot construct a recursive definition
-- for 2^n, but it should work fine for unsatisfiable instances.
declarePow2 :: IsInt a => Z3 (Expr a -> Expr a)
-- | Deprecated: The Z3.Lang interface will be moved to a dedicated
-- package.
module Z3.Lang.Nat
-- | This type allows to reason about natural numbers.
--
-- Naturals are just integers plus a (>= 0) invariant, and we
-- ensure that this invariant is always preserved by transparently adding
-- new assertions to the context.
--
-- Note that arithmetic on naturals must result in natural numbers,
-- otherwise the problem becomes unsatisfiable.
data Nat
instance Typeable Nat
instance Eq Nat
instance Ord Nat
instance Enum Nat
instance Real Nat
instance Castable Nat Integer
instance IsInt Nat
instance IsNum Nat
instance IsTy Nat
instance Compilable (Expr Nat)
instance Integral Nat
instance Num Nat
instance Show Nat
-- | Deprecated: The Z3.Lang interface will be moved to a dedicated
-- package.
module Z3.Lang