Copyright | (c) Iago Abal, 2013 (c) David Castro, 2013 |
---|---|
License | BSD3 |
Maintainer | Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> |
Safe Haskell | None |
Language | Haskell98 |
A simple monadic wrapper for Base
.
- class (Monad m, MonadIO m) => MonadZ3 m where
- getSolver :: m (Maybe Solver)
- getContext :: m Context
- data Z3 a
- module Z3.Opts
- data Logic
- evalZ3 :: Z3 a -> IO a
- evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
- data Symbol
- data AST
- data Sort
- data FuncDecl
- data App
- data Pattern
- data Model
- data FuncInterp
- data FuncEntry
- data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
- data Result
- contextToString :: MonadZ3 z3 => z3 String
- showContext :: MonadZ3 z3 => z3 String
- mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
- mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
- mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
- mkBoolSort :: MonadZ3 z3 => z3 Sort
- mkIntSort :: MonadZ3 z3 => z3 Sort
- mkRealSort :: MonadZ3 z3 => z3 Sort
- mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
- mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
- mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
- mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
- mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
- mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
- mkTrue :: MonadZ3 z3 => z3 AST
- mkFalse :: MonadZ3 z3 => z3 AST
- mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkNot :: MonadZ3 z3 => AST -> z3 AST
- mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
- mkOr :: MonadZ3 z3 => [AST] -> z3 AST
- mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
- mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
- mkMul :: MonadZ3 z3 => [AST] -> z3 AST
- mkSub :: MonadZ3 z3 => [AST] -> z3 AST
- mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
- mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
- mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
- mkIsInt :: MonadZ3 z3 => AST -> z3 AST
- mkBvnot :: MonadZ3 z3 => AST -> z3 AST
- mkBvredand :: MonadZ3 z3 => AST -> z3 AST
- mkBvredor :: MonadZ3 z3 => AST -> z3 AST
- mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvneg :: MonadZ3 z3 => AST -> z3 AST
- mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
- mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
- mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
- mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
- mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
- mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
- mkMap :: MonadZ3 z3 => FuncDecl -> Int -> [AST] -> z3 AST
- mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
- mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
- mkInt :: (MonadZ3 z3, Integral a) => a -> z3 AST
- 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
- getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
- getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
- getInt :: MonadZ3 z3 => AST -> z3 Integer
- getReal :: MonadZ3 z3 => AST -> z3 Rational
- eval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST)
- evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
- evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
- evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
- getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
- isAsArray :: MonadZ3 z3 => AST -> z3 Bool
- getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
- funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
- funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
- funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
- funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
- funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
- funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
- funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
- modelToString :: MonadZ3 z3 => Model -> z3 String
- showModel :: MonadZ3 z3 => Model -> z3 String
- assertCnstr :: MonadZ3 z3 => AST -> z3 ()
- check :: MonadZ3 z3 => z3 Result
- getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
- delModel :: MonadZ3 z3 => Model -> z3 ()
- withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
- push :: MonadZ3 z3 => z3 ()
- pop :: MonadZ3 z3 => Int -> z3 ()
- data ASTPrintMode
- setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
- astToString :: MonadZ3 z3 => AST -> z3 String
- patternToString :: MonadZ3 z3 => Pattern -> z3 String
- sortToString :: MonadZ3 z3 => Sort -> z3 String
- funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
- benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
Documentation
module Z3.Opts
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!
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. |
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.
The interpretation of a function is a mapping part (arguments to values) and an 'else' part.
Satisfiability result
Result of a satisfiability check.
Context
contextToString :: MonadZ3 z3 => z3 String Source
Convert Z3's logical context into a string.
showContext :: MonadZ3 z3 => z3 String Source
Alias for contextToString
.
Symbols
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol Source
Create a Z3 symbol using an integer.
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol Source
Create a Z3 symbol using a string.
Sorts
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort Source
Create a free (uninterpreted) type using the given name (symbol).
mkBoolSort :: MonadZ3 z3 => z3 Sort Source
Create the boolean type.
mkRealSort :: MonadZ3 z3 => z3 Sort Source
Create the real type.
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort Source
Create a bit-vector type of the given size.
This type can also be seen as a machine integer.
:: MonadZ3 z3 | |
=> Symbol | Name of the sort |
-> [(Symbol, Sort)] | Name and sort of each field |
-> z3 (Sort, FuncDecl, [FuncDecl]) | Resulting sort, and function declarations for the constructor and projections. |
Create a tuple type
Constants and Applications
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST Source
Create an AST node representing an if-then-else: ite(t1, t2, t3).
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create an AST node representing t1 implies t2.
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST Source
Create an AST node representing args[0] and ... and args[num_args-1].
mkOr :: MonadZ3 z3 => [AST] -> z3 AST Source
Create an AST node representing args[0] or ... or args[num_args-1].
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST Source
The distinct construct is used for declaring the arguments pairwise distinct.
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST Source
Create an AST node representing args[0] + ... + args[num_args-1].
mkMul :: MonadZ3 z3 => [AST] -> z3 AST Source
Create an AST node representing args[0] * ... * args[num_args-1].
mkSub :: MonadZ3 z3 => [AST] -> z3 AST Source
Create an AST node representing args[0] - ... - args[num_args - 1].
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST Source
Create an AST node representing -arg.
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST Source
Coerce an integer to a real.
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST Source
Coerce a real to an integer.
Bit-vectors
mkBvredand :: MonadZ3 z3 => AST -> z3 AST Source
Take conjunction of bits in vector, return vector of length 1.
mkBvredor :: MonadZ3 z3 => AST -> z3 AST Source
Take disjunction of bits in vector, return vector of length 1.
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Two's complement signed remainder (sign follows dividend).
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Two's complement signed remainder (sign follows divisor).
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Two's complement signed greater than or equal to.
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST Source
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST Source
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST Source
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Rotate bits of t1 to the right t2 times.
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST Source
Create an n bit bit-vector from the integer argument t1.
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST Source
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST Source
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Arrays
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST Source
Array read. The argument a is the array and i is the index of the array that gets read.
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST Source
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Numerals
Quantifiers
Accessors
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int Source
Return the size of the given bit-vector sort.
getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool) Source
Returns Just True
, Just False
, or Nothing
for undefined.
Models
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) Source
Evaluate a collection of AST nodes in the given model.
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel) Source
Get function as a list of argument/value pairs.
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel) Source
Get array as a list of argument/value pairs, if it is represented as a function (ie, using as-array).
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp) Source
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.
isAsArray :: MonadZ3 z3 => AST -> z3 Bool Source
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.
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl Source
Return the function declaration f associated with a (_ as_array f) node.
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int Source
Return the number of entries in the given function interpretation.
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry Source
Return a "point" of the given function intepretation. It represents the value of f in a particular point.
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST Source
Return the 'else' value of the given function interpretation.
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int Source
Return the arity (number of arguments) of the given function interpretation.
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST Source
Return the value of this point.
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int Source
Return the number of arguments in a Z3_func_entry object.
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST Source
Return an argument of a Z3_func_entry object.
modelToString :: MonadZ3 z3 => Model -> z3 String Source
Convert the given model into a string.
Constraints
assertCnstr :: MonadZ3 z3 => AST -> z3 () Source
Assert a constraing into the logical context.
check :: MonadZ3 z3 => z3 Result Source
Check whether the given logical context is consistent or not.
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 :: MonadZ3 z3 => ASTPrintMode -> z3 () Source
Set the mode for converting expressions to strings.
astToString :: MonadZ3 z3 => AST -> z3 String Source
Convert an AST to a string.
patternToString :: MonadZ3 z3 => Pattern -> z3 String Source
Convert a pattern to a string.
sortToString :: MonadZ3 z3 => Sort -> z3 String Source
Convert a sort to a string.
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String Source
Convert a FuncDecl to a string.