{-# LANGUAGE OverloadedStrings, Safe #-}
module SMTLib1.QF_BV (module X, module SMTLib1.QF_BV) where

import SMTLib1 as X
import Data.String(IsString(..))


tBitVec :: Integer -> Sort
tBitVec :: Integer -> Sort
tBitVec n :: Integer
n = Name -> [Integer] -> Sort
I "BitVec" [Integer
n]

isBitVec :: Sort -> Maybe Integer
isBitVec :: Sort -> Maybe Integer
isBitVec (I "BitVec" [n :: Integer
n]) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
isBitVec _                = Maybe Integer
forall a. Maybe a
Nothing

-- | BitVec[1]
bit0 :: Term
bit0 :: Term
bit0 = Sort -> [Term] -> Term
App "bit0" []

-- | BitVec[1]
bit1 :: Term
bit1 :: Term
bit1 = Sort -> [Term] -> Term
App "bit1" []

-- | [m] -> [n] -> [m+n]
concat :: Term -> Term -> Term
concat :: Term -> Term -> Term
concat x :: Term
x y :: Term
y = Sort -> [Term] -> Term
App "concat" [Term
x,Term
y]

extract :: Integer -> Integer -> Term -> Term
extract :: Integer -> Integer -> Term -> Term
extract i :: Integer
i j :: Integer
j t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "extract" [Integer
i,Integer
j]) [Term
t]

bvnot :: Term -> Term
bvnot :: Term -> Term
bvnot t :: Term
t = Sort -> [Term] -> Term
App "bvnot" [Term
t]

bvand :: Term -> Term -> Term
bvand :: Term -> Term -> Term
bvand s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvand" [Term
s,Term
t]

bvor :: Term -> Term -> Term
bvor :: Term -> Term -> Term
bvor s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvor" [Term
s,Term
t]

bvneg :: Term -> Term
bvneg :: Term -> Term
bvneg t :: Term
t  = Sort -> [Term] -> Term
App "bvneg" [Term
t]

bvadd :: Term -> Term -> Term
bvadd :: Term -> Term -> Term
bvadd s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvadd" [Term
s,Term
t]

bvmul :: Term -> Term -> Term
bvmul :: Term -> Term -> Term
bvmul s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvmul" [Term
s,Term
t]

bvudiv :: Term -> Term -> Term
bvudiv :: Term -> Term -> Term
bvudiv s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvudiv" [Term
s,Term
t]

bvurem :: Term -> Term -> Term
bvurem :: Term -> Term -> Term
bvurem s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvurem" [Term
s,Term
t]

bvshl :: Term -> Term -> Term
bvshl :: Term -> Term -> Term
bvshl s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvshl" [Term
s,Term
t]

bvlshr :: Term -> Term -> Term
bvlshr :: Term -> Term -> Term
bvlshr s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvlshr" [Term
s,Term
t]


bv :: Integer -> Integer -> Term
bv :: Integer -> Integer -> Term
bv x :: Integer
x m :: Integer
m = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 then Integer -> Term
forall a. Show a => a -> Term
lit Integer
x else Term -> Term
bvneg (Integer -> Term
forall a. Show a => a -> Term
lit (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x))
  where lit :: a -> Term
lit y :: a
y = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I (String -> Name
forall a. IsString a => String -> a
fromString ("bv" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y)) [Integer
m]) []

bvnand :: Term -> Term -> Term
bvnand :: Term -> Term -> Term
bvnand s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvnand" [Term
s,Term
t]

bvnor :: Term -> Term -> Term
bvnor :: Term -> Term -> Term
bvnor s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvnor" [Term
s,Term
t]

bvxor :: Term -> Term -> Term
bvxor :: Term -> Term -> Term
bvxor s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvxor" [Term
s,Term
t]

bvxnor :: Term -> Term -> Term
bvxnor :: Term -> Term -> Term
bvxnor s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvxnor" [Term
s,Term
t]

bvcomp :: Term -> Term -> Term
bvcomp :: Term -> Term -> Term
bvcomp s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvcomp" [Term
s,Term
t]

bvsub :: Term -> Term -> Term
bvsub :: Term -> Term -> Term
bvsub s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvsub" [Term
s,Term
t]

bvsdiv :: Term -> Term -> Term
bvsdiv :: Term -> Term -> Term
bvsdiv s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvsdiv" [Term
s,Term
t]

bvsrem :: Term -> Term -> Term
bvsrem :: Term -> Term -> Term
bvsrem s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvsrem" [Term
s,Term
t]

bvsmod :: Term -> Term -> Term
bvsmod :: Term -> Term -> Term
bvsmod s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvsmod" [Term
s,Term
t]

bvashr :: Term -> Term -> Term
bvashr :: Term -> Term -> Term
bvashr s :: Term
s t :: Term
t = Sort -> [Term] -> Term
App "bvashr" [Term
s,Term
t]

repeat :: Integer -> Term -> Term
repeat :: Integer -> Term -> Term
repeat i :: Integer
i t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "repeat" [Integer
i]) [Term
t]

zero_extend :: Integer -> Term -> Term
zero_extend :: Integer -> Term -> Term
zero_extend i :: Integer
i t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "zero_extend" [Integer
i]) [Term
t]

sign_extend :: Integer -> Term -> Term
sign_extend :: Integer -> Term -> Term
sign_extend i :: Integer
i t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "sign_extend" [Integer
i]) [Term
t]

rotate_left :: Integer -> Term -> Term
rotate_left :: Integer -> Term -> Term
rotate_left i :: Integer
i t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "rotate_left" [Integer
i]) [Term
t]

rotate_right :: Integer -> Term -> Term
rotate_right :: Integer -> Term -> Term
rotate_right i :: Integer
i t :: Term
t = Sort -> [Term] -> Term
App (Name -> [Integer] -> Sort
I "rotate_right" [Integer
i]) [Term
t]

bvule :: Term -> Term -> Formula
bvule :: Term -> Term -> Formula
bvule s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvule" [Term
s,Term
t]

bvugt :: Term -> Term -> Formula
bvugt :: Term -> Term -> Formula
bvugt s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvugt" [Term
s,Term
t]

bvuge :: Term -> Term -> Formula
bvuge :: Term -> Term -> Formula
bvuge s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvuge" [Term
s,Term
t]

bvslt :: Term -> Term -> Formula
bvslt :: Term -> Term -> Formula
bvslt s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvslt" [Term
s,Term
t]

bvsle :: Term -> Term -> Formula
bvsle :: Term -> Term -> Formula
bvsle s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvsle" [Term
s,Term
t]

bvsgt :: Term -> Term -> Formula
bvsgt :: Term -> Term -> Formula
bvsgt s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvsgt" [Term
s,Term
t]

bvsge :: Term -> Term -> Formula
bvsge :: Term -> Term -> Formula
bvsge s :: Term
s t :: Term
t = Sort -> [Term] -> Formula
FPred "bvsge" [Term
s,Term
t]