| Copyright | (c) Iago Abal, 2012-2013 (c) David Castro, 2012-2013 |
|---|---|
| License | BSD3 |
| Maintainer | Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> |
| Safe Haskell | None |
| Language | Haskell98 |
Z3.Base
Contents
Description
Low-level bindings to Z3 API.
- data Config
- data Context
- data Symbol
- data AST
- data Sort
- data FuncDecl
- data App
- data Pattern
- data Model
- data Params
- data Solver
- data Result
- mkConfig :: IO Config
- delConfig :: Config -> IO ()
- withConfig :: (Config -> IO a) -> IO a
- setParamValue :: Config -> String -> String -> IO ()
- mkContext :: Config -> IO Context
- delContext :: Context -> IO ()
- withContext :: Config -> (Context -> IO a) -> IO a
- mkStringSymbol :: Context -> String -> IO Symbol
- mkBoolSort :: Context -> IO Sort
- mkIntSort :: Context -> IO Sort
- mkRealSort :: Context -> IO Sort
- mkBvSort :: Context -> Int -> IO Sort
- mkArraySort :: Context -> Sort -> Sort -> IO Sort
- mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
- mkApp :: Context -> FuncDecl -> [AST] -> IO AST
- mkConst :: Context -> Symbol -> Sort -> IO AST
- mkTrue :: Context -> IO AST
- mkFalse :: Context -> IO AST
- mkEq :: Context -> AST -> AST -> IO AST
- mkNot :: Context -> AST -> IO AST
- mkIte :: Context -> AST -> AST -> AST -> IO AST
- mkIff :: Context -> AST -> AST -> IO AST
- mkImplies :: Context -> AST -> AST -> IO AST
- mkXor :: Context -> AST -> AST -> IO AST
- mkAnd :: Context -> [AST] -> IO AST
- mkOr :: Context -> [AST] -> IO AST
- mkDistinct :: Context -> [AST] -> IO AST
- mkAdd :: Context -> [AST] -> IO AST
- mkMul :: Context -> [AST] -> IO AST
- mkSub :: Context -> [AST] -> IO AST
- mkUnaryMinus :: Context -> AST -> IO AST
- mkDiv :: Context -> AST -> AST -> IO AST
- mkMod :: Context -> AST -> AST -> IO AST
- mkRem :: Context -> AST -> AST -> IO AST
- mkLt :: Context -> AST -> AST -> IO AST
- mkLe :: Context -> AST -> AST -> IO AST
- mkGt :: Context -> AST -> AST -> IO AST
- mkGe :: Context -> AST -> AST -> IO AST
- mkInt2Real :: Context -> AST -> IO AST
- mkReal2Int :: Context -> AST -> IO AST
- mkIsInt :: Context -> AST -> IO AST
- mkBvnot :: Context -> AST -> IO AST
- mkBvredand :: Context -> AST -> IO AST
- mkBvredor :: Context -> AST -> IO AST
- mkBvand :: Context -> AST -> AST -> IO AST
- mkBvor :: Context -> AST -> AST -> IO AST
- mkBvxor :: Context -> AST -> AST -> IO AST
- mkBvnand :: Context -> AST -> AST -> IO AST
- mkBvnor :: Context -> AST -> AST -> IO AST
- mkBvxnor :: Context -> AST -> AST -> IO AST
- mkBvneg :: Context -> AST -> IO AST
- mkBvadd :: Context -> AST -> AST -> IO AST
- mkBvsub :: Context -> AST -> AST -> IO AST
- mkBvmul :: Context -> AST -> AST -> IO AST
- mkBvudiv :: Context -> AST -> AST -> IO AST
- mkBvsdiv :: Context -> AST -> AST -> IO AST
- mkBvurem :: Context -> AST -> AST -> IO AST
- mkBvsrem :: Context -> AST -> AST -> IO AST
- mkBvsmod :: Context -> AST -> AST -> IO AST
- mkBvult :: Context -> AST -> AST -> IO AST
- mkBvslt :: Context -> AST -> AST -> IO AST
- mkBvule :: Context -> AST -> AST -> IO AST
- mkBvsle :: Context -> AST -> AST -> IO AST
- mkBvuge :: Context -> AST -> AST -> IO AST
- mkBvsge :: Context -> AST -> AST -> IO AST
- mkBvugt :: Context -> AST -> AST -> IO AST
- mkBvsgt :: Context -> AST -> AST -> IO AST
- mkConcat :: Context -> AST -> AST -> IO AST
- mkExtract :: Context -> Int -> Int -> AST -> IO AST
- mkSignExt :: Context -> Int -> AST -> IO AST
- mkZeroExt :: Context -> Int -> AST -> IO AST
- mkRepeat :: Context -> Int -> AST -> IO AST
- mkBvshl :: Context -> AST -> AST -> IO AST
- mkBvlshr :: Context -> AST -> AST -> IO AST
- mkBvashr :: Context -> AST -> AST -> IO AST
- mkRotateLeft :: Context -> Int -> AST -> IO AST
- mkRotateRight :: Context -> Int -> AST -> IO AST
- mkExtRotateLeft :: Context -> AST -> AST -> IO AST
- mkExtRotateRight :: Context -> AST -> AST -> IO AST
- mkInt2bv :: Context -> Int -> AST -> IO AST
- mkBv2int :: Context -> AST -> Bool -> IO AST
- mkBvnegNoOverflow :: Context -> AST -> IO AST
- mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
- mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
- mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
- mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
- mkSelect :: Context -> AST -> AST -> IO AST
- mkStore :: Context -> AST -> AST -> AST -> IO AST
- mkConstArray :: Context -> Sort -> AST -> IO AST
- mkMap :: Context -> FuncDecl -> Int -> [AST] -> IO AST
- mkArrayDefault :: Context -> AST -> IO AST
- mkNumeral :: Context -> String -> Sort -> IO AST
- mkInt :: Integral a => Context -> a -> IO AST
- mkReal :: Real r => Context -> r -> IO AST
- mkPattern :: Context -> [AST] -> IO Pattern
- mkBound :: Context -> Int -> Sort -> IO AST
- mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
- mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
- getBvSortSize :: Context -> Sort -> IO Int
- getSort :: Context -> AST -> IO Sort
- getBool :: Context -> AST -> IO (Maybe Bool)
- getInt :: Context -> AST -> IO Integer
- getReal :: Context -> AST -> IO Rational
- eval :: Context -> Model -> AST -> IO (Maybe AST)
- evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
- showModel :: Context -> Model -> IO String
- showContext :: Context -> IO String
- assertCnstr :: Context -> AST -> IO ()
- check :: Context -> IO Result
- getModel :: Context -> IO (Result, Maybe Model)
- delModel :: Context -> Model -> IO ()
- push :: Context -> IO ()
- pop :: Context -> Int -> IO ()
- mkParams :: Context -> IO Params
- paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
- paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()
- paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
- paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
- paramsToString :: Context -> Params -> IO String
- data Logic
- mkSolver :: Context -> IO Solver
- mkSimpleSolver :: Context -> IO Solver
- mkSolverForLogic :: Context -> Logic -> IO Solver
- solverSetParams :: Context -> Solver -> Params -> IO ()
- solverPush :: Context -> Solver -> IO ()
- solverPop :: Context -> Solver -> Int -> IO ()
- solverReset :: Context -> Solver -> IO ()
- solverAssertCnstr :: Context -> Solver -> AST -> IO ()
- solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
- solverCheck :: Context -> Solver -> IO Result
- solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)
- solverGetReasonUnknown :: Context -> Solver -> IO String
- data ASTPrintMode
- setASTPrintMode :: Context -> ASTPrintMode -> IO ()
- astToString :: Context -> AST -> IO String
- patternToString :: Context -> Pattern -> IO String
- sortToString :: Context -> Sort -> IO String
- funcDeclToString :: Context -> FuncDecl -> IO String
- data Z3Error = Z3Error {
- errCode :: Z3ErrorCode
- errMsg :: String
- data Z3ErrorCode
Types
Kind of AST used to represent function symbols.
A kind of Z3 AST used to represent constant and function declarations.
A kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.
A Z3 parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
Satisfiability result
Result of a satisfiability check.
Configuration
Create a configuration.
withConfig :: (Config -> IO a) -> IO a Source
Run a computation using a temporally created configuration.
setParamValue :: Config -> String -> String -> IO () Source
Set a configuration parameter.
See: http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html
Context
delContext :: Context -> IO () Source
Delete the given logical context.
withContext :: Config -> (Context -> IO a) -> IO a Source
Run a computation using a temporally created context.
Symbols
Sorts
mkBoolSort :: Context -> IO Sort Source
Create the Boolean type.
mkRealSort :: Context -> IO Sort Source
Create a real type.
mkBvSort :: Context -> Int -> IO Sort Source
Create a bit-vector type of the given size.
This type can also be seen as a machine integer.
Constants and Applications
mkIte :: Context -> AST -> AST -> AST -> IO AST Source
Create an AST node representing an if-then-else: ite(t1, t2, t3).
mkAnd :: Context -> [AST] -> IO AST Source
Create an AST node representing args[0] and ... and args[num_args-1].
mkOr :: Context -> [AST] -> IO AST Source
Create an AST node representing args[0] or ... or args[num_args-1].
mkDistinct :: Context -> [AST] -> IO AST Source
The distinct construct is used for declaring the arguments pairwise distinct.
mkAdd :: Context -> [AST] -> IO AST Source
Create an AST node representing args[0] + ... + args[num_args-1].
mkMul :: Context -> [AST] -> IO AST Source
Create an AST node representing args[0] * ... * args[num_args-1].
mkSub :: Context -> [AST] -> IO AST Source
Create an AST node representing args[0] - ... - args[num_args - 1].
Bit-vectors
mkBvredand :: Context -> AST -> IO AST Source
Take conjunction of bits in vector, return vector of length 1.
mkBvredor :: Context -> AST -> IO AST Source
Take disjunction of bits in vector, return vector of length 1.
mkBvsrem :: Context -> AST -> AST -> IO AST Source
Two's complement signed remainder (sign follows dividend).
mkBvsmod :: Context -> AST -> AST -> IO AST Source
Two's complement signed remainder (sign follows divisor).
mkExtract :: Context -> Int -> Int -> AST -> IO AST Source
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.
mkSignExt :: Context -> Int -> AST -> IO AST Source
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
mkZeroExt :: Context -> Int -> AST -> IO AST Source
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
mkInt2bv :: Context -> Int -> AST -> IO AST Source
Create an n bit bit-vector from the integer argument t1.
mkBv2int :: Context -> AST -> Bool -> IO AST Source
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.
mkBvnegNoOverflow :: Context -> AST -> IO AST Source
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST Source
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST Source
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST Source
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST Source
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST Source
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Arrays
mkSelect :: Context -> AST -> AST -> IO AST Source
Array read. The argument a is the array and i is the index of the array that gets read.
mkArrayDefault :: Context -> AST -> IO AST Source
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Numerals
Quantifiers
Accessors
getBool :: Context -> AST -> IO (Maybe Bool) Source
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
Models
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST)) Source
Evaluate a collection of AST nodes in the given model.
showContext :: Context -> IO String Source
Convert the given logical context into a string.
Constraints
assertCnstr :: Context -> AST -> IO () Source
Assert a constraing into the logical context.
Parameters
Solvers
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
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!
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. |
mkSolver :: Context -> IO Solver Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
mkSimpleSolver :: Context -> IO Solver Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
mkSolverForLogic :: Context -> Logic -> IO Solver Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverSetParams :: Context -> Solver -> Params -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverPush :: Context -> Solver -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverPop :: Context -> Solver -> Int -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverReset :: Context -> Solver -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverAssertCnstr :: Context -> Solver -> AST -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO () Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverCheck :: Context -> Solver -> IO Result Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model) Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
solverGetReasonUnknown :: Context -> Solver -> IO String Source
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
String Conversion
data ASTPrintMode Source
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.
setASTPrintMode :: Context -> ASTPrintMode -> IO () Source
Set the pretty-printing mode for converting ASTs to strings.
Error Handling
Z3 exceptions.
Constructors
| Z3Error | |
Fields
| |