-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Bindings for the Z3 Theorem Prover
--   
@package z3
@version 0.3.0


-- | Low-level bindings to Z3 API.
module Z3.Base

-- | A Z3 <i>configuration object</i>.
data Config

-- | A Z3 <i>logical context</i>.
data Context

-- | A Z3 <i>Lisp-link symbol</i>.
data Symbol

-- | A Z3 <i>AST node</i>.
data AST

-- | Kind of Z3 AST representing <i>types</i>.
data Sort

-- | Kind of AST used to represent function symbols.
data FuncDecl

-- | A kind of Z3 AST used to represent constant and function declarations.
data App

-- | A kind of AST used to represent pattern and multi-patterns used to
--   guide quantifier instantiation.
data Pattern

-- | A model for the constraints asserted into the logical context.
data Model

-- | 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
data Solver

-- | Result of a satisfiability check.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result

-- | Create a configuration.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f</a>
mkConfig :: IO Config

-- | Delete a configuration.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774</a>
delConfig :: Config -> IO ()

-- | Run a computation using a temporally created configuration.
withConfig :: (Config -> IO a) -> IO a

-- | Set a configuration parameter.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3</a>
--   
--   See:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html</a>
setParamValue :: Config -> String -> String -> IO ()

-- | Create a context using the given configuration.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46</a>
mkContext :: Config -> IO Context

-- | Delete the given logical context.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200</a>
delContext :: Context -> IO ()

-- | Run a computation using a temporally created context.
withContext :: Config -> (Context -> IO a) -> IO a

-- | Create a Z3 symbol using a string.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae</a>
mkStringSymbol :: Context -> String -> IO Symbol

-- | Create the <i>Boolean</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342</a>
mkBoolSort :: Context -> IO Sort

-- | Create an <i>integer</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015</a>
mkIntSort :: Context -> IO Sort

-- | Create a <i>real</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0</a>
mkRealSort :: Context -> IO Sort

-- | Create a bit-vector type of the given size.
--   
--   This type can also be seen as a machine integer.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688</a>
mkBvSort :: Context -> Int -> IO Sort

-- | Create an array type
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445</a>
mkArraySort :: Context -> Sort -> Sort -> IO Sort

-- | A Z3 function
mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl

-- | Create a constant or function application.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe</a>
mkApp :: Context -> FuncDecl -> [AST] -> IO AST

-- | Declare and create a constant.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef</a>
mkConst :: Context -> Symbol -> Sort -> IO AST

-- | Create an AST node representing <i>true</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7</a>
mkTrue :: Context -> IO AST

-- | Create an AST node representing <i>false</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d</a>
mkFalse :: Context -> IO AST

-- | Create an AST node representing <i>l = r</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c</a>
mkEq :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing <i>not(a)</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072</a>
mkNot :: Context -> AST -> IO AST

-- | Create an AST node representing an if-then-else: <i>ite(t1, t2,
--   t3)</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547</a>
mkIte :: Context -> AST -> AST -> AST -> IO AST

-- | Create an AST node representing <i>t1 iff t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042</a>
mkIff :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing <i>t1 implies t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517</a>
mkImplies :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing <i>t1 xor t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec</a>
mkXor :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing args[0] and ... and args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61</a>
mkAnd :: Context -> [AST] -> IO AST

-- | Create an AST node representing args[0] or ... or args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9</a>
mkOr :: Context -> [AST] -> IO AST

-- | The distinct construct is used for declaring the arguments pairwise
--   distinct.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7</a>
mkDistinct :: Context -> [AST] -> IO AST

-- | Create an AST node representing args[0] + ... + args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5</a>
mkAdd :: Context -> [AST] -> IO AST

-- | Create an AST node representing args[0] * ... * args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890</a>
mkMul :: Context -> [AST] -> IO AST

-- | Create an AST node representing args[0] - ... - args[num_args - 1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9</a>
mkSub :: Context -> [AST] -> IO AST

-- | Create an AST node representing -arg.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea</a>
mkUnaryMinus :: Context -> AST -> IO AST

-- | Create an AST node representing arg1 div arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3</a>
mkDiv :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing arg1 mod arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713</a>
mkMod :: Context -> AST -> AST -> IO AST

-- | Create an AST node representing arg1 rem arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff</a>
mkRem :: Context -> AST -> AST -> IO AST

-- | Create less than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534</a>
mkLt :: Context -> AST -> AST -> IO AST

-- | Create less than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf</a>
mkLe :: Context -> AST -> AST -> IO AST

-- | Create greater than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3</a>
mkGt :: Context -> AST -> AST -> IO AST

-- | Create greater than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942</a>
mkGe :: Context -> AST -> AST -> IO AST

-- | Coerce an integer to a real.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21</a>
mkInt2Real :: Context -> AST -> IO AST

-- | Coerce a real to an integer.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d</a>
mkReal2Int :: Context -> AST -> IO AST

-- | Check if a real number is an integer.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3</a>
mkIsInt :: Context -> AST -> IO AST

-- | Bitwise negation.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080</a>
mkBvnot :: Context -> AST -> IO AST

-- | Take conjunction of bits in vector, return vector of length 1.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8</a>
mkBvredand :: Context -> AST -> IO AST

-- | Take disjunction of bits in vector, return vector of length 1.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2</a>
mkBvredor :: Context -> AST -> IO AST

-- | Bitwise and.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d</a>
mkBvand :: Context -> AST -> AST -> IO AST

-- | Bitwise or.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5</a>
mkBvor :: Context -> AST -> AST -> IO AST

-- | Bitwise exclusive-or.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8</a>
mkBvxor :: Context -> AST -> AST -> IO AST

-- | Bitwise nand.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61</a>
mkBvnand :: Context -> AST -> AST -> IO AST

-- | Bitwise nor.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb</a>
mkBvnor :: Context -> AST -> AST -> IO AST

-- | Bitwise xnor.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6</a>
mkBvxnor :: Context -> AST -> AST -> IO AST

-- | Standard two's complement unary minus.
--   
--   Reference:
--   &lt;<a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7</a>
mkBvneg :: Context -> AST -> IO AST

-- | Standard two's complement addition.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158</a>
mkBvadd :: Context -> AST -> AST -> IO AST

-- | Standard two's complement subtraction.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e</a>
mkBvsub :: Context -> AST -> AST -> IO AST

-- | Standard two's complement multiplication.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c</a>
mkBvmul :: Context -> AST -> AST -> IO AST

-- | Unsigned division.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544</a>
mkBvudiv :: Context -> AST -> AST -> IO AST

-- | Two's complement signed division.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0</a>
mkBvsdiv :: Context -> AST -> AST -> IO AST

-- | Unsigned remainder.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d</a>
mkBvurem :: Context -> AST -> AST -> IO AST

-- | Two's complement signed remainder (sign follows dividend).
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1</a>
mkBvsrem :: Context -> AST -> AST -> IO AST

-- | Two's complement signed remainder (sign follows divisor).
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879</a>
mkBvsmod :: Context -> AST -> AST -> IO AST

-- | Unsigned less than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4</a>
mkBvult :: Context -> AST -> AST -> IO AST

-- | Two's complement signed less than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a</a>
mkBvslt :: Context -> AST -> AST -> IO AST

-- | Unsigned less than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87</a>
mkBvule :: Context -> AST -> AST -> IO AST

-- | Two's complement signed less than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d</a>
mkBvsle :: Context -> AST -> AST -> IO AST

-- | Unsigned greater than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df</a>
mkBvuge :: Context -> AST -> AST -> IO AST

-- | Two's complement signed greater than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5</a>
mkBvsge :: Context -> AST -> AST -> IO AST

-- | Unsigned greater than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3</a>
mkBvugt :: Context -> AST -> AST -> IO AST

-- | Two's complement signed greater than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0</a>
mkBvsgt :: Context -> AST -> AST -> IO AST

-- | Concatenate the given bit-vectors.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa</a>
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 <i>n</i>, where <i>n = high - low + 1</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317</a>
mkExtract :: Context -> Int -> Int -> AST -> IO AST

-- | Sign-extend of the given bit-vector to the (signed) equivalent
--   bitvector of size <i>m+i</i>, where <i>m</i> is the size of the given
--   bit-vector.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e</a>
mkSignExt :: Context -> Int -> AST -> IO AST

-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
--   bitvector of size <i>m+i</i>, where <i>m</i> is the size of the given
--   bit-vector.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3</a>
mkZeroExt :: Context -> Int -> AST -> IO AST

-- | Repeat the given bit-vector up length <i>i</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d</a>
mkRepeat :: Context -> Int -> AST -> IO AST

-- | Shift left.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1</a>
mkBvshl :: Context -> AST -> AST -> IO AST

-- | Logical shift right.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512</a>
mkBvlshr :: Context -> AST -> AST -> IO AST

-- | Arithmetic shift right.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4</a>
mkBvashr :: Context -> AST -> AST -> IO AST

-- | Rotate bits of <i>t1</i> to the left <i>i</i> times.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda</a>
mkRotateLeft :: Context -> Int -> AST -> IO AST

-- | Rotate bits of <i>t1</i> to the right <i>i</i> times.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c</a>
mkRotateRight :: Context -> Int -> AST -> IO AST

-- | Rotate bits of <i>t1</i> to the left <i>t2</i> times.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7</a>
mkExtRotateLeft :: Context -> AST -> AST -> IO AST

-- | Rotate bits of <i>t1</i> to the right <i>t2</i> times.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f</a>
mkExtRotateRight :: Context -> AST -> AST -> IO AST

-- | Create an <i>n</i> bit bit-vector from the integer argument <i>t1</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5</a>
mkInt2bv :: Context -> Int -> AST -> IO AST

-- | Create an integer from the bit-vector argument <i>t1</i>. If
--   <i>is_signed</i> is false, then the bit-vector <i>t1</i> is treated as
--   unsigned. So the result is non-negative and in the range
--   [0..2^<i>N</i>-1], where <i>N</i> are the number of bits in <i>t1</i>.
--   If <i>is_signed</i> is true, <i>t1</i> is treated as a signed
--   bit-vector.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4</a>
mkBv2int :: Context -> AST -> Bool -> IO AST

-- | Check that bit-wise negation does not overflow when <i>t1</i> is
--   interpreted as a signed bit-vector.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7</a>
mkBvnegNoOverflow :: Context -> AST -> IO AST

-- | Create a predicate that checks that the bit-wise addition of <i>t1</i>
--   and <i>t2</i> does not overflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f</a>
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST

-- | Create a predicate that checks that the bit-wise signed addition of
--   <i>t1</i> and <i>t2</i> does not underflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947</a>
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST

-- | Create a predicate that checks that the bit-wise signed subtraction of
--   <i>t1</i> and <i>t2</i> does not overflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c</a>
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST

-- | Create a predicate that checks that the bit-wise subtraction of
--   <i>t1</i> and <i>t2</i> does not underflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4</a>
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST

-- | Create a predicate that checks that the bit-wise multiplication of
--   <i>t1</i> and <i>t2</i> does not overflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df</a>
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST

-- | Create a predicate that checks that the bit-wise signed multiplication
--   of <i>t1</i> and <i>t2</i> does not underflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda</a>
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST

-- | Create a predicate that checks that the bit-wise signed division of
--   <i>t1</i> and <i>t2</i> does not overflow.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e</a>
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.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67</a>
mkSelect :: Context -> AST -> AST -> IO AST

-- | Array update.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593</a>
mkStore :: Context -> AST -> AST -> AST -> IO AST

-- | Create the constant array.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d</a>
mkConstArray :: Context -> Sort -> AST -> IO AST

-- | map f on the the argument arrays.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d</a>
mkMap :: Context -> FuncDecl -> Int -> [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.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d</a>
mkArrayDefault :: Context -> AST -> IO AST

-- | Create a numeral of a given sort.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c</a>
mkNumeral :: Context -> String -> Sort -> IO AST

-- | Create a numeral of sort <i>int</i>.
mkInt :: Integral a => Context -> a -> IO AST

-- | Create a numeral of sort <i>real</i>.
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

-- | Return the size of the given bit-vector sort.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419</a>
getBvSortSize :: Context -> Sort -> IO Int

-- | Return the sort of an AST node.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933</a>
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.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4</a>
getBool :: Context -> AST -> IO (Maybe Bool)

-- | Return <tt>Z3Int</tt> value
getInt :: Context -> AST -> IO Integer

-- | Return <tt>Z3Real</tt> value
getReal :: Context -> AST -> IO Rational

-- | Evaluate an AST node in the given model.
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))

-- | Convert the given model into a string.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af</a>
showModel :: Context -> Model -> IO String

-- | Convert the given logical context into a string.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216</a>
showContext :: Context -> IO String

-- | Assert a constraing into the logical context.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a</a>
assertCnstr :: Context -> AST -> IO ()

-- | Check whether the given logical context is consistent or not.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03</a>
check :: Context -> IO Result

-- | Get model (logical context is consistent)
--   
--   Reference :
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a</a>
getModel :: Context -> IO (Result, Maybe Model)

-- | Delete a model object.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee</a>
delModel :: Context -> Model -> IO ()

-- | Create a backtracking point.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f</a>
push :: Context -> IO ()

-- | Backtrack <i>n</i> backtracking points.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61</a>
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

-- | Solvers available in Z3.
--   
--   These are described at <a>http://smtlib.cs.uiowa.edu/logics.html</a>
--   
--   <i>WARNING</i>: Support for solvers is fragile, you may experience
--   segmentation faults!

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
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 &lt; 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 &lt; 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

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
mkSolver :: Context -> IO Solver

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
mkSimpleSolver :: Context -> IO Solver

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
mkSolverForLogic :: Context -> Logic -> IO Solver

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverSetParams :: Context -> Solver -> Params -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverPush :: Context -> Solver -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverPop :: Context -> Solver -> Int -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverReset :: Context -> Solver -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverAssertCnstr :: Context -> Solver -> AST -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverCheck :: Context -> Solver -> IO Result

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
solverGetReasonUnknown :: Context -> Solver -> IO String

-- | Pretty-printing mode for converting ASTs to strings. The mode can be
--   one of the following:
--   
--   <ul>
--   <li>Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
--   format.</li>
--   <li>Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.</li>
--   <li>Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
--   format.</li>
--   <li>Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
--   compliant format.</li>
--   </ul>
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

-- | 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 Params
instance Eq Solver
instance Eq Result
instance Ord Result
instance Read Result
instance Show Result
instance Show Z3ErrorCode
instance Show Logic
instance Exception Z3Error
instance Show Z3Error


-- | High-level interface to configuration options.
module Z3.Opts

-- | Z3 configuration.
data Opts

-- | Set configuration.
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 <a>Base</a>.
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 <a>http://smtlib.cs.uiowa.edu/logics.html</a>
--   
--   <i>WARNING</i>: Support for solvers is fragile, you may experience
--   segmentation faults!

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
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 &lt; 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 &lt; 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

-- | A Z3 <i>Lisp-link symbol</i>.
data Symbol

-- | A Z3 <i>AST node</i>.
data AST

-- | Kind of Z3 AST representing <i>types</i>.
data Sort

-- | Kind of AST used to represent function symbols.
data FuncDecl

-- | A kind of Z3 AST used to represent constant and function declarations.
data App

-- | A kind of AST used to represent pattern and multi-patterns used to
--   guide quantifier instantiation.
data Pattern

-- | A model for the constraints asserted into the logical context.
data Model

-- | Result of a satisfiability check.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result

-- | Create a Z3 symbol using a string.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae</a>
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol

-- | Create the <i>boolean</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342</a>
mkBoolSort :: MonadZ3 z3 => z3 Sort

-- | Create the <i>integer</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015</a>
mkIntSort :: MonadZ3 z3 => z3 Sort

-- | Create the <i>real</i> type.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0</a>
mkRealSort :: MonadZ3 z3 => z3 Sort

-- | A Z3 function
mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl

-- | Create a constant or function application.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe</a>
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST

-- | Declare and create a constant.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef</a>
mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST

-- | Create an AST node representing <i>true</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7</a>
mkTrue :: MonadZ3 z3 => z3 AST

-- | Create an AST node representing <i>false</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d</a>
mkFalse :: MonadZ3 z3 => z3 AST

-- | Create an AST node representing <i>l = r</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c</a>
mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing <i>not(a)</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072</a>
mkNot :: MonadZ3 z3 => AST -> z3 AST

-- | Create an AST node representing an if-then-else: <i>ite(t1, t2,
--   t3)</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547</a>
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST

-- | Create an AST node representing <i>t1 iff t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042</a>
mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing <i>t1 implies t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517</a>
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing <i>t1 xor t2</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec</a>
mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing args[0] and ... and args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61</a>
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST

-- | Create an AST node representing args[0] or ... or args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9</a>
mkOr :: MonadZ3 z3 => [AST] -> z3 AST

-- | The distinct construct is used for declaring the arguments pairwise
--   distinct.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7</a>
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST

-- | Create an AST node representing args[0] + ... + args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5</a>
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST

-- | Create an AST node representing args[0] * ... * args[num_args-1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890</a>
mkMul :: MonadZ3 z3 => [AST] -> z3 AST

-- | Create an AST node representing args[0] - ... - args[num_args - 1].
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9</a>
mkSub :: MonadZ3 z3 => [AST] -> z3 AST

-- | Create an AST node representing -arg.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea</a>
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST

-- | Create an AST node representing arg1 div arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3</a>
mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing arg1 mod arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713</a>
mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create an AST node representing arg1 rem arg2.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff</a>
mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create less than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534</a>
mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create less than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf</a>
mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create greater than.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3</a>
mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Create greater than or equal to.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942</a>
mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST

-- | Coerce an integer to a real.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21</a>
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST

-- | Coerce a real to an integer.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d</a>
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST

-- | Check if a real number is an integer.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3</a>
mkIsInt :: MonadZ3 z3 => AST -> z3 AST

-- | Create a numeral of a given sort.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c</a>
mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST

-- | Create a numeral of sort <i>int</i>.
mkInt :: (MonadZ3 z3, Integral a) => a -> z3 AST

-- | Create a numeral of sort <i>real</i>.
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

-- | Returns <tt>Just True</tt>, <tt>Just False</tt>, or <tt>Nothing</tt>
--   for <i>undefined</i>.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4</a>
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

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

-- | Convert the given model into a string.
showModel :: MonadZ3 z3 => Model -> z3 String

-- | Convert Z3's logical context into a string.
showContext :: MonadZ3 z3 => z3 String

-- | Assert a constraing into the logical context.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a</a>
assertCnstr :: MonadZ3 z3 => AST -> z3 ()

-- | Check whether the given logical context is consistent or not.
check :: MonadZ3 z3 => z3 Result

-- | Get model.
--   
--   Reference :
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a</a>
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)

-- | Delete a model object.
--   
--   Reference:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee</a>
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 <i>n</i> backtracking points.
pop :: MonadZ3 z3 => Int -> z3 ()

-- | Pretty-printing mode for converting ASTs to strings. The mode can be
--   one of the following:
--   
--   <ul>
--   <li>Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
--   format.</li>
--   <li>Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.</li>
--   <li>Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
--   format.</li>
--   <li>Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
--   compliant format.</li>
--   </ul>
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
instance Functor Z3
instance Applicative Z3
instance Monad Z3
instance MonadIO Z3
instance MonadZ3 Z3


module Z3.Lang.Prelude

-- | Z3 monad.
data Z3 a

-- | Result of a satisfiability check.
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 <a>http://smtlib.cs.uiowa.edu/logics.html</a>

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
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 <a>http://smtlib.cs.uiowa.edu/logics.html</a>
--   
--   <i>WARNING</i>: Support for solvers is fragile, you may experience
--   segmentation faults!

-- | <i>Warning: New Z3 API support is still incomplete and fragile: you
--   may experience segmentation faults!</i>
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 &lt; 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 &lt; 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 <i>let</i>.
let_ :: IsTy a => Expr a -> Z3 (Expr a)

-- | Check whether the given logical context is consistent or not.
check :: MonadZ3 z3 => z3 Result

-- | Convert Z3's logical context into a string.
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 <i>n</i> backtracking points.
pop :: MonadZ3 z3 => Int -> z3 ()

-- | 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 <a>Result</a> 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 <i>int</i> sort in Z3.
class (IsNum a, Integral a) => IsInt a

-- | Typeclass for Haskell Z3 numbers of <i>real</i> sort in Z3.
class (IsNum a, Fractional a, Real a) => IsReal a

-- | Convertible types.
class (IsTy a, IsTy b) => Castable a b

-- | <i>literal</i> 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 <i>and</i>.
and_ :: [Expr Bool] -> Expr Bool

-- | Boolean binary <i>and</i>.
(&&*) :: Expr Bool -> Expr Bool -> Expr Bool

-- | Boolean variadic <i>or</i>.
or_ :: [Expr Bool] -> Expr Bool

-- | Boolean binary <i>or</i>.
(||*) :: Expr Bool -> Expr Bool -> Expr Bool

-- | Boolean variadic <i>distinct</i>.
distinct :: IsTy a => [Expr a] -> Expr Bool

-- | Boolean binary <i>xor</i>.
xor :: Expr Bool -> Expr Bool -> Expr Bool

-- | Boolean implication
implies :: Expr Bool -> Expr Bool -> Expr Bool

-- | An alias for <a>implies</a>.
(==>) :: Expr Bool -> Expr Bool -> Expr Bool

-- | Boolean <i>if and only if</i>.
iff :: Expr Bool -> Expr Bool -> Expr Bool

-- | An alias for <a>iff</a>.
(<=>) :: 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

-- | <pre>
--   k <a>divides</a> n == n %* k ==* 0
--   </pre>
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

-- | <i>if-then-else</i>.
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)


module Z3.Lang.Lg2

-- | Ceiling logarithm base two. Axiomatization of the <i>lg2</i> function.
--   Most likely Z3 is going to diverge if you use <i>lg2</i> to specify a
--   satisfiable problem since it cannot construct a recursive definition
--   for <i>lg2</i>, but it should work fine for unsatisfiable instances.
declareLg2 :: IsInt a => Z3 (Expr a -> Expr a)


module Z3.Lang.Pow2

-- | Raise to the power of 2. Axiomatization of the <i>2^n</i> function.
--   Most likely Z3 is going to diverge if you use <i>2^n</i> to specify a
--   satisfiable problem, since it cannot construct a recursive definition
--   for <i>2^n</i>, but it should work fine for unsatisfiable instances.
declarePow2 :: IsInt a => Z3 (Expr a -> Expr a)


module Z3.Lang.Nat
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


module Z3.Lang