Commits

Iago Abal committed a3e4b4f

Add bit-vectors to Z3.Base

Comments (0)

Files changed (1)

     , mkBoolSort
     , mkIntSort
     , mkRealSort
+    , mkBvSort
 
     -- * Constants and Applications
     , mkFuncDecl
     , mkReal2Int
     , mkIsInt
 
+    -- * Bit-vectors
+    , mkBvnot
+    , mkBvredand
+    , mkBvredor
+    , mkBvand
+    , mkBvor
+    , mkBvxor
+    , mkBvnand
+    , mkBvnor
+    , mkBvxnor
+    , mkBvneg
+    , mkBvadd
+    , mkBvsub
+    , mkBvmul
+    , mkBvudiv
+    , mkBvsdiv
+    , mkBvurem
+    , mkBvsrem
+    , mkBvsmod
+    , mkBvult
+    , mkBvslt
+    , mkBvule
+    , mkBvsle
+    , mkBvuge
+    , mkBvsge
+    , mkBvugt
+    , mkBvsgt
+    , mkConcat
+    , mkExtract
+    , mkSignExt
+    , mkZeroExt
+    , mkRepeat
+    , mkBvshl
+    , mkBvlshr
+    , mkBvashr
+    , mkRotateLeft
+    , mkRotateRight
+    , mkExtRotateLeft
+    , mkExtRotateRight
+    , mkInt2bv
+    , mkBv2int
+    , mkBvnegNoOverflow
+    , mkBvaddNoOverflow
+    , mkBvaddNoUnderflow
+    , mkBvsubNoOverflow
+    , mkBvsubNoUnderflow
+    , mkBvmulNoOverflow
+    , mkBvmulNoUnderflow
+    , mkBvsdivNoOverflow
+
     -- * Numerals
     , mkNumeral
     , mkInt
     , mkExists
 
     -- * Accessors
+    , getBvSortSize
+    , getSort
     , getBool
     , getInt
     , getReal
 mkRealSort :: Context -> IO Sort
 mkRealSort c = Sort <$> z3_mk_real_sort (unContext c)
 
--- TODO Sorts: from Z3_mk_bv_sort on
+-- | Create a bit-vector type of the given size.
+--
+-- This type can also be seen as a machine integer.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>
+mkBvSort :: Context -> Int -> IO Sort
+mkBvSort c n = Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n)
+
+-- TODO Sorts: from Z3_mk_finite_domain_sort on
 
 ---------------------------------------------------------------------
 -- Constants and Applications
 mkIsInt :: Context -> AST -> IO AST
 mkIsInt c e = AST <$> z3_mk_is_int (unContext c) (unAST e)
 
--- TODO Bit-vector, Arrays, Sets
+---------------------------------------------------------------------
+-- Bit-vectors
+
+-- | Bitwise negation.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>
+mkBvnot :: Context -> AST -> IO AST
+mkBvnot c e = AST <$> z3_mk_bvnot (unContext c) (unAST e)
+
+-- | Take conjunction of bits in vector, return vector of length 1.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>
+mkBvredand :: Context -> AST -> IO AST
+mkBvredand c e = AST <$> z3_mk_bvredand (unContext c) (unAST e)
+
+-- | Take disjunction of bits in vector, return vector of length 1.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>
+mkBvredor :: Context -> AST -> IO AST
+mkBvredor c e = AST <$> z3_mk_bvredor (unContext c) (unAST e)
+
+-- | Bitwise and.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>
+mkBvand :: Context -> AST -> AST -> IO AST
+mkBvand c e1 e2 = AST <$> z3_mk_bvand (unContext c) (unAST e1) (unAST e2)
+
+-- | Bitwise or.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>
+mkBvor :: Context -> AST -> AST -> IO AST
+mkBvor c e1 e2 = AST <$> z3_mk_bvor (unContext c) (unAST e1) (unAST e2)
+
+-- | Bitwise exclusive-or.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>
+mkBvxor :: Context -> AST -> AST -> IO AST
+mkBvxor c e1 e2 = AST <$> z3_mk_bvxor (unContext c) (unAST e1) (unAST e2)
+
+-- | Bitwise nand.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>
+mkBvnand :: Context -> AST -> AST -> IO AST
+mkBvnand c e1 e2 = AST <$> z3_mk_bvnand (unContext c) (unAST e1) (unAST e2)
+
+-- | Bitwise nor.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>
+mkBvnor :: Context -> AST -> AST -> IO AST
+mkBvnor c e1 e2 = AST <$> z3_mk_bvnor (unContext c) (unAST e1) (unAST e2)
+
+-- | Bitwise xnor.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>
+mkBvxnor :: Context -> AST -> AST -> IO AST
+mkBvxnor c e1 e2 = AST <$> z3_mk_bvxnor (unContext c) (unAST e1) (unAST e2)
+
+-- | Standard two's complement unary minus.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
+mkBvneg :: Context -> AST -> IO AST
+mkBvneg c e = AST <$> z3_mk_bvneg (unContext c) (unAST e)
+
+-- | Standard two's complement addition.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>
+mkBvadd :: Context -> AST -> AST -> IO AST
+mkBvadd c e1 e2 = AST <$> z3_mk_bvadd (unContext c) (unAST e1) (unAST e2)
+
+-- | Standard two's complement subtraction.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>
+mkBvsub :: Context -> AST -> AST -> IO AST
+mkBvsub c e1 e2 = AST <$> z3_mk_bvsub (unContext c) (unAST e1) (unAST e2)
+
+-- | Standard two's complement multiplication.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>
+mkBvmul :: Context -> AST -> AST -> IO AST
+mkBvmul c e1 e2 = AST <$> z3_mk_bvmul (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned division.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>
+mkBvudiv :: Context -> AST -> AST -> IO AST
+mkBvudiv c e1 e2 = AST <$> z3_mk_bvudiv (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed division.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>
+mkBvsdiv :: Context -> AST -> AST -> IO AST
+mkBvsdiv c e1 e2 = AST <$> z3_mk_bvsdiv (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned remainder.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>
+mkBvurem :: Context -> AST -> AST -> IO AST
+mkBvurem c e1 e2 = AST <$> z3_mk_bvurem (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed remainder (sign follows dividend).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>
+mkBvsrem :: Context -> AST -> AST -> IO AST
+mkBvsrem c e1 e2 = AST <$> z3_mk_bvsrem (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed remainder (sign follows divisor).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>
+mkBvsmod :: Context -> AST -> AST -> IO AST
+mkBvsmod c e1 e2 = AST <$> z3_mk_bvsmod (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned less than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>
+mkBvult :: Context -> AST -> AST -> IO AST
+mkBvult c e1 e2 = AST <$> z3_mk_bvult (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed less than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>
+mkBvslt :: Context -> AST -> AST -> IO AST
+mkBvslt c e1 e2 = AST <$> z3_mk_bvslt (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned less than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>
+mkBvule :: Context -> AST -> AST -> IO AST
+mkBvule c e1 e2 = AST <$> z3_mk_bvule (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed less than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>
+mkBvsle :: Context -> AST -> AST -> IO AST
+mkBvsle c e1 e2 = AST <$> z3_mk_bvsle (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned greater than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>
+mkBvuge :: Context -> AST -> AST -> IO AST
+mkBvuge c e1 e2 = AST <$> z3_mk_bvuge (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed greater than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>
+mkBvsge :: Context -> AST -> AST -> IO AST
+mkBvsge c e1 e2 = AST <$> z3_mk_bvsge (unContext c) (unAST e1) (unAST e2)
+
+-- | Unsigned greater than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>
+mkBvugt :: Context -> AST -> AST -> IO AST
+mkBvugt c e1 e2 = AST <$> z3_mk_bvugt (unContext c) (unAST e1) (unAST e2)
+
+-- | Two's complement signed greater than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>
+mkBvsgt :: Context -> AST -> AST -> IO AST
+mkBvsgt c e1 e2 = AST <$> z3_mk_bvsgt (unContext c) (unAST e1) (unAST e2)
+
+-- | Concatenate the given bit-vectors.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>
+mkConcat :: Context -> AST -> AST -> IO AST
+mkConcat c e1 e2 = AST <$> z3_mk_concat (unContext c) (unAST e1) (unAST e2)
+
+-- | Extract the bits high down to low from a bitvector of size m to yield a new
+-- bitvector of size /n/, where /n = high - low + 1/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>
+mkExtract :: Context -> Int -> Int -> AST -> IO AST
+mkExtract c j i e
+  = AST <$> z3_mk_extract (unContext c) (fromIntegral j) (fromIntegral i) (unAST e)
+
+-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector
+-- of size /m+i/, where /m/ is the size of the given bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>
+mkSignExt :: Context -> Int -> AST -> IO AST
+mkSignExt c i e
+  = AST <$> z3_mk_sign_ext (unContext c) (fromIntegral i) (unAST e)
+
+-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
+-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>
+mkZeroExt :: Context -> Int -> AST -> IO AST
+mkZeroExt c i e
+  = AST <$> z3_mk_zero_ext (unContext c) (fromIntegral i) (unAST e)
+
+-- | Repeat the given bit-vector up length /i/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>
+mkRepeat :: Context -> Int -> AST -> IO AST
+mkRepeat c i e
+  = AST <$> z3_mk_repeat (unContext c) (fromIntegral i) (unAST e)
+
+-- | Shift left.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>
+mkBvshl :: Context -> AST -> AST -> IO AST
+mkBvshl c e1 e2 = AST <$> z3_mk_bvshl (unContext c) (unAST e1) (unAST e2)
+
+-- | Logical shift right.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>
+mkBvlshr :: Context -> AST -> AST -> IO AST
+mkBvlshr c e1 e2 = AST <$> z3_mk_bvlshr (unContext c) (unAST e1) (unAST e2)
+
+-- | Arithmetic shift right.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>
+mkBvashr :: Context -> AST -> AST -> IO AST
+mkBvashr c e1 e2 = AST <$> z3_mk_bvashr (unContext c) (unAST e1) (unAST e2)
+
+-- | Rotate bits of /t1/ to the left /i/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>
+mkRotateLeft :: Context -> Int -> AST -> IO AST
+mkRotateLeft c i e
+  = AST <$> z3_mk_rotate_left (unContext c) (fromIntegral i) (unAST e)
+
+-- | Rotate bits of /t1/ to the right /i/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>
+mkRotateRight :: Context -> Int -> AST -> IO AST
+mkRotateRight c i e
+  = AST <$> z3_mk_rotate_right (unContext c) (fromIntegral i) (unAST e)
+
+-- | Rotate bits of /t1/ to the left /t2/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>
+mkExtRotateLeft :: Context -> AST -> AST -> IO AST
+mkExtRotateLeft c e1 e2
+  = AST <$> z3_mk_ext_rotate_left (unContext c) (unAST e1) (unAST e2)
+
+-- | Rotate bits of /t1/ to the right /t2/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>
+mkExtRotateRight :: Context -> AST -> AST -> IO AST
+mkExtRotateRight c e1 e2
+  = AST <$> z3_mk_ext_rotate_right (unContext c) (unAST e1) (unAST e2)
+
+-- | Create an /n/ bit bit-vector from the integer argument /t1/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>
+mkInt2bv :: Context -> Int -> AST -> IO AST
+mkInt2bv c i e
+  = AST <$> z3_mk_int2bv (unContext c) (fromIntegral i) (unAST e)
+
+-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false,
+-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative
+-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/.
+-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>
+mkBv2int :: Context -> AST -> Bool -> IO AST
+mkBv2int c e is_signed
+  = AST <$> z3_mk_bv2int (unContext c) (unAST e) (unBool is_signed)
+
+-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/
+-- does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>
+mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
+mkBvaddNoOverflow c e1 e2 is_signed =
+  AST <$> z3_mk_bvadd_no_overflow (unContext c) (unAST e1) (unAST e2)
+                                  (unBool is_signed)
+
+-- | Create a predicate that checks that the bit-wise signed addition of /t1/
+-- and /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>
+mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
+mkBvaddNoUnderflow c e1 e2 =
+  AST <$> z3_mk_bvadd_no_underflow (unContext c) (unAST e1) (unAST e2)
+
+-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/
+-- and /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>
+mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
+mkBvsubNoOverflow c e1 e2 =
+  AST <$> z3_mk_bvsub_no_overflow (unContext c) (unAST e1) (unAST e2)
+
+-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and
+-- /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>
+mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
+mkBvsubNoUnderflow c e1 e2 =
+  AST <$> z3_mk_bvsub_no_underflow (unContext c) (unAST e1) (unAST e2)
+
+-- | Create a predicate that checks that the bit-wise signed division of /t1/
+-- and /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>
+mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
+mkBvsdivNoOverflow c e1 e2 =
+  AST <$> z3_mk_bvsdiv_no_overflow (unContext c) (unAST e1) (unAST e2)
+
+-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as
+-- a signed bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>
+mkBvnegNoOverflow :: Context -> AST -> IO AST
+mkBvnegNoOverflow c e =
+  AST <$> z3_mk_bvneg_no_overflow (unContext c) (unAST e)
+
+-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and
+-- /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>
+mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
+mkBvmulNoOverflow c e1 e2 is_signed =
+  AST <$> z3_mk_bvmul_no_overflow (unContext c) (unAST e1) (unAST e2)
+                                  (unBool is_signed)
+
+-- | Create a predicate that checks that the bit-wise signed multiplication of
+-- /t1/ and /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>
+mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
+mkBvmulNoUnderflow c e1 e2 =
+  AST <$> z3_mk_bvmul_no_underflow (unContext c) (unAST e1) (unAST e2)
+
+-- TODO Arrays, Sets
 
 ---------------------------------------------------------------------
 -- Numerals
 ---------------------------------------------------------------------
 -- Accessors
 
+-- | Return the size of the given bit-vector sort.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>
+getBvSortSize :: Context -> Sort -> IO Int
+getBvSortSize c s =
+  fromIntegral <$> z3_get_bv_sort_size (unContext c) (unSort s)
+
+-- | Return the sort of an AST node.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933>
+getSort :: Context -> AST -> IO Sort
+getSort c e = Sort <$> z3_get_sort (unContext c) (unAST e)
+
 -- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@.
 castLBool :: Z3_lbool -> Maybe Bool
 castLBool lb