Commits

Cláudio Lourenço committed 0827f90

Lifted Bit-vectors to Z3.Monad
#changelog

Comments (0)

Files changed (1)

   , mkBoolSort
   , mkIntSort
   , mkRealSort
+  , mkBvSort
   , mkArraySort
 
   -- * Constants and Applications
   , 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
+
   -- * Arrays
   , mkSelect
   , mkStore
   , mkExists
 
   -- * Accessors
+  , getBvSortSize
   , getBool
   , getInt
   , getReal
 mkRealSort :: MonadZ3 z3 => z3 Sort
 mkRealSort = liftScalar Base.mkRealSort
 
+-- | Create a bit-vector type of the given size.
+--
+-- This type can also be seen as a machine integer.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>
+mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
+mkBvSort = liftFun1 Base.mkBvSort
+
 -- | Create an array type
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>
 mkIsInt = liftFun1 Base.mkIsInt
 
 ---------------------------------------------------------------------
+-- Bit-vectors
+
+-- | Bitwise negation.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>
+mkBvnot :: MonadZ3 z3 => AST -> z3 AST
+mkBvnot = liftFun1 Base.mkBvnot
+
+-- | Take conjunction of bits in vector, return vector of length 1.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>
+mkBvredand :: MonadZ3 z3 => AST -> z3 AST
+mkBvredand = liftFun1 Base.mkBvredand
+
+-- | Take disjunction of bits in vector, return vector of length 1.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>
+mkBvredor :: MonadZ3 z3 => AST -> z3 AST
+mkBvredor = liftFun1 Base.mkBvredor
+
+-- | Bitwise and.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>
+mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvand  = liftFun2 Base.mkBvand
+
+-- | Bitwise or.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>
+mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvor = liftFun2 Base.mkBvor
+
+-- | Bitwise exclusive-or.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>
+mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvxor = liftFun2 Base.mkBvxor
+
+-- | Bitwise nand.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>
+mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvnand = liftFun2 Base.mkBvnand 
+
+-- | Bitwise nor.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>
+mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvnor = liftFun2 Base.mkBvnor 
+
+-- | Bitwise xnor.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>
+mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvxnor = liftFun2 Base.mkBvxnor 
+
+-- | Standard two's complement unary minus.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
+mkBvneg :: MonadZ3 z3 => AST -> z3 AST
+mkBvneg = liftFun1 Base.mkBvneg
+
+-- | Standard two's complement addition.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>
+mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvadd = liftFun2 Base.mkBvadd
+
+-- | Standard two's complement subtraction.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>
+mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsub = liftFun2 Base.mkBvsub
+
+-- | Standard two's complement multiplication.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>
+mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvmul = liftFun2 Base.mkBvmul 
+
+-- | Unsigned division.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>
+mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvudiv = liftFun2 Base.mkBvudiv
+
+-- | Two's complement signed division.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>
+mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsdiv = liftFun2 Base.mkBvsdiv 
+
+-- | Unsigned remainder.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>
+mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvurem = liftFun2 Base.mkBvurem
+
+-- | Two's complement signed remainder (sign follows dividend).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>
+mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsrem = liftFun2 Base.mkBvsrem 
+
+-- | Two's complement signed remainder (sign follows divisor).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>
+mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsmod = liftFun2 Base.mkBvsmod
+
+-- | Unsigned less than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>
+mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvult = liftFun2 Base.mkBvult 
+
+-- | Two's complement signed less than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>
+mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvslt = liftFun2 Base.mkBvslt
+
+-- | Unsigned less than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>
+mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvule = liftFun2 Base.mkBvule 
+
+-- | Two's complement signed less than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>
+mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsle = liftFun2 Base.mkBvsle 
+
+-- | Unsigned greater than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>
+mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvuge = liftFun2 Base.mkBvuge
+
+-- | Two's complement signed greater than or equal to.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>
+mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsge = liftFun2 Base.mkBvsge 
+
+-- | Unsigned greater than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>
+mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvugt = liftFun2 Base.mkBvugt
+
+-- | Two's complement signed greater than.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>
+mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsgt = liftFun2 Base.mkBvsgt 
+
+-- | Concatenate the given bit-vectors.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>
+mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkConcat = liftFun2 Base.mkConcat
+
+-- | Extract the bits high down to low from a bitvector of size m to yield a new
+-- bitvector of size /n/, where /n = high - low + 1/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>
+mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
+mkExtract = liftFun3 Base.mkExtract
+
+-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector
+-- of size /m+i/, where /m/ is the size of the given bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>
+mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkSignExt = liftFun2 Base.mkSignExt
+
+-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
+-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>
+mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkZeroExt = liftFun2 Base.mkZeroExt
+
+-- | Repeat the given bit-vector up length /i/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>
+mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkRepeat = liftFun2 Base.mkRepeat
+
+-- | Shift left.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>
+mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvshl = liftFun2 Base.mkBvshl
+
+-- | Logical shift right.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>
+mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvlshr = liftFun2 Base.mkBvlshr
+
+-- | Arithmetic shift right.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>
+mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvashr = liftFun2 Base.mkBvashr
+
+-- | Rotate bits of /t1/ to the left /i/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>
+mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkRotateLeft = liftFun2 Base.mkRotateLeft
+
+-- | Rotate bits of /t1/ to the right /i/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>
+mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkRotateRight = liftFun2 Base.mkRotateRight
+
+-- | Rotate bits of /t1/ to the left /t2/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>
+mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkExtRotateLeft = liftFun2 Base.mkExtRotateLeft
+
+-- | Rotate bits of /t1/ to the right /t2/ times.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>
+mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkExtRotateRight = liftFun2 Base.mkExtRotateRight
+
+-- | Create an /n/ bit bit-vector from the integer argument /t1/.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>
+mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
+mkInt2bv = liftFun2 Base.mkInt2bv
+
+-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false,
+-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative
+-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/.
+-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>
+mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
+mkBv2int = liftFun2 Base.mkBv2int
+
+-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/
+-- does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>
+mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
+mkBvaddNoOverflow = liftFun3 Base.mkBvaddNoOverflow
+
+-- | Create a predicate that checks that the bit-wise signed addition of /t1/
+-- and /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>
+mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvaddNoUnderflow = liftFun2 Base.mkBvaddNoUnderflow
+
+-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/
+-- and /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>
+mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsubNoOverflow = liftFun2 Base.mkBvsubNoOverflow
+
+-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and
+-- /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>
+mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsubNoUnderflow = liftFun2 Base.mkBvsubNoUnderflow
+
+-- | Create a predicate that checks that the bit-wise signed division of /t1/
+-- and /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>
+mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvsdivNoOverflow = liftFun2 Base.mkBvsdivNoOverflow
+
+-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as
+-- a signed bit-vector.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>
+mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
+mkBvnegNoOverflow = liftFun1 Base.mkBvnegNoOverflow
+
+-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and
+-- /t2/ does not overflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>
+mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
+mkBvmulNoOverflow = liftFun3 Base.mkBvmulNoOverflow
+
+-- | Create a predicate that checks that the bit-wise signed multiplication of
+-- /t1/ and /t2/ does not underflow.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>
+mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
+mkBvmulNoUnderflow = liftFun2 Base.mkBvmulNoUnderflow
+
+---------------------------------------------------------------------
 -- Arrays
 
 -- | Array read. The argument a is the array and i is the index of the array
 ---------------------------------------------------------------------
 -- 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 :: MonadZ3 z3 => Sort -> z3 Int
+getBvSortSize = liftFun1 Base.getBvSortSize
+
 -- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>