aig (empty) → 0.1.0.0

raw patch · 6 files changed

+919/−0 lines, 6 filesdep +basedep +mtldep +vectorsetup-changed

Dependencies added: base, mtl, vector

Files

LICENSE +30/−0
Setup.hs +2/−0
aig.cabal +47/−0
src/Data/AIG.hs +16/−0
src/Data/AIG/Interface.hs +204/−0
src/Data/AIG/Operations.hs +620/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Galois, Inc.++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the names of the authors nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ aig.cabal view

@@ -0,0 +1,47 @@+Name:               aig+Version:            0.1.0.0+License:            BSD3+License-file:       LICENSE+Author:             Galois Inc.+Maintainer:         jhendrix@galois.com+Copyright:          (c) 2014 Galois Inc.+Category:           Data+build-type:         Simple+cabal-Version:      >= 1.10+Synopsis:           And-inverter graphs in Haskell.+Description:+  This package provides a generic interfaces for working+  with And-Inverter graphs (AIGs) in Haskell.  And-Inverter graphs+  are a useful format for representing combinatorial and+  sequential boolean circuits in a way that is amenable to+  simulation and analysis.++  These interfaces allow clients to write code that can create+  and use AIGs without depending on a particular AIG package.++-- Ugh. Temporary fix to make Hackage happy.+--flag enable-hpc+--  Description: Collect HPC coverage information.+--  Default: False++source-repository head+  type: git+  location: https://github.com/GaloisInc/aig.git++library+  hs-source-dirs:   src+  exposed-modules:+    Data.AIG+    Data.AIG.Interface+    Data.AIG.Operations++  default-Language: Haskell2010+  ghc-options:      -Wall+  build-depends:+    base == 4.*,+    mtl,+    vector++-- Ugh. Temporary fix to make Hackage happy.+--  if flag(enable-hpc)+--    ghc-options: -fhpc -hpcdir .hpc

+ src/Data/AIG.hs view

@@ -0,0 +1,16 @@+{- |+Module      : Data.AIG+Copyright   : (c) Galois, Inc. 2014+License     : BSD3+Maintainer  : jhendrix@galois.com+Stability   : experimental+Portability : portable+-}++module Data.AIG +  ( module Data.AIG.Interface+  , module Data.AIG.Operations+  ) where++import Data.AIG.Interface+import Data.AIG.Operations

+ src/Data/AIG/Interface.hs view

@@ -0,0 +1,204 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Rank2Types #-}++{- |+Module      : Data.AIG.Interface+Copyright   : (c) Galois, Inc. 2014+License     : BSD3+Maintainer  : jhendrix@galois.com+Stability   : experimental+Portability : portable++Interfaces for building, simulating and analysing And-Inverter Graphs (AIG).+-}++module Data.AIG.Interface+  ( -- * Main interface classes+    IsLit(..)+  , IsAIG(..)++    -- * Helper datatypes+  , Proxy(..)+  , SomeGraph(..)+  , Network(..)+  , networkInputCount++    -- * Representations of prover results+  , SatResult(..)+  , VerifyResult(..)+  , toSatResult+  , toVerifyResult+  ) where++import Control.Applicative ((<$>))+import Control.Monad+import Prelude hiding (not, and, or)++class IsLit l where+  -- | Negate a literal.+  not :: l s -> l s++  -- | Tests whether two lits are identical.+  -- This is only a syntactic check, and may return false+  -- even if the two literals represent the same predicate.+  (===) :: l s -> l s -> Bool++-- | A proxy is used to identify a specific AIG instance when+-- calling methods that create new AIGs.+data Proxy l g where+  Proxy :: IsAIG l g => (forall a . a -> a) -> Proxy l g++-- | An And-Inverter-Graph is a data structure storing bit-level+-- nodes.+--+-- Graphs are and-inverter graphs, which contain a number of input+-- literals and Boolean operations for creating new literals.+-- Every literal is part of a specific graph, and literals from+-- different networks may not be mixed.+--+-- Both the types for literals and graphs must take a single+-- phantom type for an arugment that is used to ensure that literals+-- from different networks cannot be used in the same operation.+class IsLit l => IsAIG l g | g -> l where+  -- | Create a temporary graph, and use it to compute a result value.+  withNewGraph :: Proxy l g -- ^ A 'Proxy' value, used for selecting the concrete+                            --   implementation typeclass+               -> (forall s . g s -> IO a)+                            -- ^ The AIG graph computation to run+               -> IO a+  withNewGraph p f = newGraph p >>= (`withSomeGraph` f)++  -- | Build a new graph instance, and packge it into the+  --   'SomeGraph' type that remembers the IsAIG implementation.+  newGraph :: Proxy l g+           -> IO (SomeGraph g)+  newGraph p = withNewGraph p (return . SomeGraph)++  -- | Read an AIG from a file, assumed to be in Aiger format+  aigerNetwork :: Proxy l g+               -> FilePath+               -> IO (Network l g)++  -- | Get unique literal in graph representing constant true.+  trueLit :: g s -> l s++  -- | Get unique literal in graph representing constant false.+  falseLit :: g s -> l s++  -- | Generate a constant literal value+  constant :: g s -> Bool -> l s+  constant g True  = trueLit  g+  constant g False = falseLit g++  -- | Return if the literal is a fixed constant.  If the literal+  --   is symbolic, return @Nothing@.+  asConstant :: g s -> l s -> Maybe Bool+  asConstant g l | l === trueLit g = Just True+                 | l === falseLit g = Just False+                 | otherwise = Nothing++  -- | Generate a fresh input literal+  newInput :: g s -> IO (l s)++  -- | Compute the logical and of two literals+  and :: g s -> l s -> l s -> IO (l s)++  -- | Build the conjunction of a list of literals+  ands :: g s -> [l s] -> IO (l s)+  ands g [] = return (trueLit g)+  ands g (x:r) = foldM (and g) x r++  -- | Compute the logical or of two literals+  or :: g s -> l s -> l s -> IO (l s)+  or g x y = not <$> and g (not x) (not y)++  -- | Compute the logical equality of two literals+  eq :: g s -> l s -> l s -> IO (l s)+  eq g x y = not <$> xor g x y++  -- | Compute the logical implication of two literals+  implies :: g s -> l s -> l s -> IO (l s)+  implies g x y = or g (not x) y++  -- | Compute the exclusive or of two literals+  xor :: g s -> l s -> l s -> IO (l s)+  xor g x y = do+    o <- or g x y+    a <- and g x y+    and g o (not a)++  -- | Perform a mux (if-then-else on the bits).+  mux :: g s -> l s -> l s -> l s -> IO (l s)+  mux g c x y = do+   x' <- and g c x+   y' <- and g (not c) y+   or g x' y'++  -- | Return number of inputs in the graph.+  inputCount :: g s -> IO Int++  -- | Get input at given index in the graph.+  getInput :: g s -> Int -> IO (l s)++  -- | Write network out to AIGER file.+  writeAiger :: FilePath -> Network l g -> IO ()++  -- | Check if literal is satisfiable in network.+  checkSat :: g s -> l s -> IO SatResult++  -- | Perform combinational equivalence checking.+  cec :: Network l g -> Network l g -> IO VerifyResult++  -- | Evaluate the network on a set of concrete inputs.+  evaluator :: g s+            -> [Bool]+            -> IO (l s -> Bool)++  -- | Evaluate the network on a set of concrete inputs.+  evaluate :: Network l g+           -> [Bool]+           -> IO [Bool]+  evaluate (Network g outputs) inputs = do+    f <- evaluator g inputs+    return (f <$> outputs)++-- | A network is an and-inverstor graph paired with it's outputs,+--   thus representing a complete combinational circuit.+data Network l g where+   Network :: IsAIG l g => g s -> [l s] -> Network l g++networkInputCount :: Network l g -> IO Int+networkInputCount (Network g _) = inputCount g++-- | Some graph quantifies over the state phantom variable for a graph.+data SomeGraph g where+  SomeGraph :: g s -> SomeGraph g++-- | Unpack @SomeGraph@ in a local scope so it can be used to compute a result+withSomeGraph :: SomeGraph g+              -> (forall s . g s -> IO a)+              -> IO a+withSomeGraph (SomeGraph g) f = f g++-- | Satisfiability check result.+data SatResult+   = Unsat+   | Sat !([Bool])+  deriving (Eq,Show)++-- | Result of a verification check.+data VerifyResult+   = Valid+   | Invalid [Bool]+  deriving (Eq, Show)++-- | Convert a sat result to a verify result by negating it.+toVerifyResult :: SatResult -> VerifyResult+toVerifyResult Unsat = Valid+toVerifyResult (Sat l) = Invalid l++-- | Convert a verify result to a sat result by negating it.+toSatResult :: VerifyResult -> SatResult+toSatResult Valid = Unsat+toSatResult (Invalid l) = Sat l

+ src/Data/AIG/Operations.hs view

@@ -0,0 +1,620 @@+{-# LANGUAGE ScopedTypeVariables #-}++{- |+Module      : Data.AIG.Operations+Copyright   : (c) Galois, Inc. 2014+License     : BSD3+Maintainer  : jhendrix@galois.com+Stability   : experimental+Portability : portable++A collection of higher-level operations (mostly various 2's complement arithmetic operations)+that can be build from the primitive And-Inverter Graph interface.+-}++module Data.AIG.Operations+  ( -- * Bitvectors+    BV+  , length+  , at+  , (!)+  , (++)+  , concat+  , take+  , drop+  , slice+  , zipWithM+  , msb+  , lsb++    -- ** Building bitvectors+  , generateM_msb0+  , generate_msb0+  , generateM_lsb0+  , generate_lsb0+  , replicate+  , bvFromInteger+  , muxInteger++    -- ** Deconstructing bitvectors+  , asUnsigned+  , asSigned+  , bvToList++    -- * Numeric operations on bitvectors+    -- ** Addition and subtraction+  , neg+  , add+  , addC+  , sub+  , subC++    -- ** Multiplication and division+  , mul+  , squot+  , srem+  , uquot+  , urem++    -- ** Shifts and rolls+  , shl+  , sshr+  , ushr+  , rol+  , ror++    -- ** Numeric comparisons+  , bvEq+  , sle+  , slt+  , ule+  , ult++    -- ** Extensions+  , sext+  , zext++    -- * Polynomial multiplication and modulus+  , pmul+  , pmod+  ) where++import Control.Applicative+import Control.Exception+import qualified Control.Monad+import Control.Monad.State hiding (zipWithM)+import Data.Bits ((.|.), setBit, shiftL, testBit)+import qualified Data.Vector as V+import Prelude hiding (and, concat, length, not, or, replicate, splitAt, tail, (++), take, drop)+import qualified Prelude++import Data.AIG.Interface++-- | A full adder which takes three inputs and returns output and carry.+halfAdder :: IsAIG l g => g s -> l s -> l s -> IO (l s, l s)+halfAdder g b c = do+  b_or_c <- or g b c+  c_out <- and g b c+  s <- and g b_or_c (not c_out)+  return (s, c_out)++-- | A full adder which takes three inputs and returns output and carry.+fullAdder :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s)+fullAdder g a b c_in = do+  a_xor_b <- xor g a b+  s <- xor g a_xor_b c_in+  a_and_b <- and g a b+  c_out <- or g a_and_b =<< and g a_xor_b c_in+  return (s, c_out)++-- | A BitVector consists of a sequence of symbolic bits and can be used+--   for symbolic machine-word arithmetic.+newtype BV l = BV { unBV :: V.Vector l }++instance Functor BV where+  fmap f (BV v) = BV (f <$> v)++-- | Number of bits in a bit vector+length :: BV l -> Int+length (BV v) = V.length v++tail :: BV l -> BV l+tail (BV v) = BV (V.tail v)++-- | Generate a bitvector of length @n@, using function @f@ to specify the bit literals.+--   The indexes to @f@ are given in LSB-first order, i.e., @f 0@ is the least significant bit.+generate_lsb0+   :: Int            -- ^ @n@, length of the generated bitvector+   -> (Int -> l)     -- ^ @f@, function to calculate bit literals+   -> BV l+generate_lsb0 c f = BV (V.generate c (\i -> f ((c-1)-i)))++-- | Generate a bitvector of length @n@, using monadic function @f@ to generate the bit literals.+--   The indexes to @f@ are given in LSB-first order, i.e., @f 0@ is the least significant bit.+generateM_lsb0+   :: Monad m+   => Int            -- ^ @n@, length of the generated bitvector+   -> (Int -> m l)   -- ^ @f@, computation to generate a bit literal+   -> m (BV l)+generateM_lsb0 c f = return . BV . V.reverse =<< V.generateM c (\i -> f ((c-1)-i))++-- | Generate a bitvector of length @n@, using function @f@ to specify the bit literals.+--   The indexes to @f@ are given in MSB-first order, i.e., @f 0@ is the most significant bit.+generate_msb0+   :: Int            -- ^ @n@, length of the generated bitvector+   -> (Int -> l)     -- ^ @f@, function to calculate bit literals+   -> BV l+generate_msb0 c f = BV (V.generate c f)++-- | Generate a bitvector of length @n@, using monadic function @f@ to generate the bit literals.+--   The indexes to @f@ are given in MSB-first order, i.e., @f 0@ is the most significant bit.+generateM_msb0+   :: Monad m+   => Int            -- ^ @n@, length of the generated bitvector+   -> (Int -> m l)   -- ^ @f@, computation to generate a bit literal+   -> m (BV l)+generateM_msb0 c f = return . BV =<< V.generateM c f++-- | Generate a bit vector of length @n@ where every bit value is literal @l@.+replicate+   :: Int   -- ^ @n@, length of the bitvector+   -> l     -- ^ @l@, the value to replicate+   -> BV l+replicate c e = BV (V.replicate c e)++-- | Project the individual bits of a BitVector.+--   @x `at` 0@ is the most significant bit.+--   It is an error to request an out-of-bounds bit.+at :: BV l -> Int -> l+at (BV v) i = v V.! i++-- | Append two bitvectors, with the most significant bitvector given first.+(++) :: BV l -> BV l -> BV l+BV x ++ BV y = BV (x V.++ y)++-- | Concatenate a list of bitvectors, with the most significant bitvector at the+--   head of the list.+concat :: [BV l] -> BV l+concat v = BV (V.concat (unBV <$> v))++-- | Project out the `n` most significant bits from a bitvector.+take :: Int -> BV l -> BV l+take i (BV v) = BV (V.take i v)++-- | Drop the @n@ most significant bits from a bitvector.+drop :: Int -> BV l -> BV l+drop i (BV v) = BV (V.drop i v)++-- | Extract @n@ bits starting at index @i@.+--   The vector must contain at least @i+n@ elements+slice :: BV l+      -> Int   -- ^ @i@, 0-based start index+      -> Int   -- ^ @n@, bits to take+      -> BV l  -- ^ a vector consisting of the bits from @i@ to @i+n-1@+slice (BV v) i n = BV (V.slice i n v)++-- | Combine two bitvectors with a bitwise monadic combiner action.+zipWithM :: (l -> l -> IO l) -> BV l -> BV l -> IO (BV l)+zipWithM f (BV x) (BV y) = assert (V.length x == V.length y) $+  BV <$> V.zipWithM f x y++-- | Convert a bitvector to a list, most significant bit first.+bvToList :: BV l -> [l]+bvToList (BV v) = V.toList v++-- | Convert a list to a bitvector, assuming big-endian bit order.+bvFromList :: [l] -> BV l+bvFromList xs = BV (V.fromList xs)++-- | Select bits from a bitvector, starting from the least significant bit.+--   @x ! 0@ is the least significant bit.+--   It is an error to request an out-of-bounds bit.+(!) :: BV l -> Int -> l+(!) v i = v `at` (length v - 1 - i)++-- | Generate a bitvector from an integer value, using 2's complement representation.+bvFromInteger+   :: IsAIG l g+   => g s+   -> Int       -- ^ number of bits in the resulting bitvector+   -> Integer   -- ^ integer value+   -> BV (l s)+bvFromInteger g n v = generate_lsb0 n $ \i -> constant g (v `testBit` i)++-- | Interpret a bitvector as an unsigned integer.  Return @Nothing@ if+--   the bitvector is not concrete.+asUnsigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer+asUnsigned g v = go 0 0+  where n = length v+        go x i | i >= n = return x+        go x i = do+          b <- asConstant g (v `at` i)+          let y  = if b then 1 else 0+          let z = x `shiftL` 1 .|. y+          seq z $ go z (i+1)++-- | Interpret a bitvector as a signed integer.  Return @Nothing@ if+--   the bitvector is not concrete.+asSigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer+asSigned g v = assert (n > 0) $ go 0 1+  where n = length v+        m = n-1+        go x i | i < m = do+          b <- asConstant g (v `at` i)+          let y  = if b then 1 else 0+          let z = x `shiftL` 1 .|. y+          seq z $ go z (i+1)+        go x i = do+          msbv <- asConstant g (v `at` i)+          return $ if msbv then x - 2^m+                           else x++-- | Retrieve the most significant bit of a bitvector.+msb :: BV l -> l+msb v = v `at` 0++-- | Retrieve the least significant bit of a bitvector.+lsb :: BV l -> l+lsb v = v ! 0++-- | If-then-else combinator for bitvectors.+ite+   :: IsAIG l g+   => g s+   -> l s          -- ^ test bit+   -> BV (l s)     -- ^ then bitvector+   -> BV (l s)     -- ^ else bitvector+   -> IO (BV (l s))+ite g c x y = zipWithM (mux g c) x y++-- | If-then-else combinator for bitvector computations with optimistic+--   shortcutting.  If the test bit is concrete, we can avoid generating+--   either the if or the else circuit.+iteM+   :: IsAIG l g+   => g s+   -> l s                -- ^ test bit+   -> IO (BV (l s))      -- ^ then circuit computation+   -> IO (BV (l s))      -- ^ else circuit computation+   -> IO (BV (l s))+iteM g c x y+  | c === trueLit g = x+  | c === falseLit g = y+  | otherwise = join $ zipWithM (mux g c) <$> x <*> y++-- | Implements a ripple carry adder.  Both addends are assumed to have+--   the same length.+ripple_add :: IsAIG l g+           => g s+           -> BV (l s)+           -> BV (l s)+           -> l s                -- ^ carry-in bit+           -> IO (BV (l s), l s) -- ^ sum and carry-out bit+ripple_add _ x _ c | length x == 0 = return (x, c)+ripple_add g x y c0 = do+  let unfold i = StateT $ \c -> do+        fullAdder g (x `at` i) (y `at` i) c+  runStateT (generateM_lsb0 (length x) unfold) c0++-- | A subtraction circuit which takes three inputs and returns output and carry.+fullSub :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s)+fullSub g x y b_in = do+  y_eq_b <- eq g y b_in+  s <- eq g x y_eq_b++  y_and_b <- and g y b_in+  c2 <- and g (not x) =<< or g y b_in+  b_out <- or g y_and_b c2+  return (s, b_out)++-- | Subtract two bit vectors, returning result and borrow bit.+full_sub :: IsAIG l g+         => g s+         -> BV (l s)+         -> BV (l s)+         -> IO (BV (l s), l s)+full_sub g x _ | length x == 0 = return (x,falseLit g)+full_sub g x y = do+  let unfold i = StateT $ \b -> fullSub g (x `at` i) (y `at` i) b+  runStateT (generateM_lsb0 (length x) unfold) (falseLit g)++-- | Compute the 2's complement negation of a bitvector+neg :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))+neg g x = evalStateT (generateM_lsb0 (length x) unfold) (trueLit g)+  where unfold i = StateT $ \c -> halfAdder g (not (x `at` i)) c++-- | Add two bitvectors with the same size.  Discard carry bit.+add :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+add g x y = fst <$> addC g x y++-- | Add two bitvectors with the same size with carry.+addC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s)+addC g x y = ripple_add g x y (falseLit g)++-- | Subtract one bitvector from another with the same size.  Discard carry bit.+sub :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+sub g x y = fst <$> subC g x y++-- | Subtract one bitvector from another with the same size with carry.+subC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s)+subC g x y = ripple_add g x (not <$> y) (trueLit g)+++-- | Multiply two bitvectors with the same size.+mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+mul g x y = do+  -- Create mutable array to store result.+  let n = length y+  -- Function to update bits.+  let updateBits i z | i == n = return z+      updateBits i z = do+        z_inc <- add g z (shlC g x i)+        z' <- ite g (y ! i) z_inc z+        updateBits (i+1) z'+  updateBits 0 $ replicate (length x) (falseLit g)++-- | Compute the signed quotient of two signed bitvectors with the same size.+squot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+squot g x y = fst <$> squotRem g x y++-- | Compute the signed division remainder of two signed bitvectors with the same size.+srem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+srem g x y = snd <$> squotRem g x y++-- | Cons value to head of a list and shift other elements to left.+shiftL1 :: BV l -> l -> BV l+shiftL1 (BV v) e = assert (V.length v > 0) $ BV (V.tail v `V.snoc` e)++-- | Cons value to start of list and shift other elements right.+shiftR1 :: l -> BV l -> BV l+shiftR1 e (BV v) = assert (V.length v > 0) $ BV (e `V.cons` V.init v)++splitAt :: Int -> BV l -> (BV l, BV l)+splitAt n (BV v) = (BV x, BV y)+  where (x,y) = V.splitAt n v++stepN :: Monad m => Int -> (a -> m a) -> a -> m a+stepN n f x+  | n > 0 = stepN (n-1) f =<< f x+  | otherwise = return x++-- | Return absolute value of signed bitvector.+sabs :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))+sabs g x = assert (length x > 0) $ negWhen g x (msb x)+++negWhen :: IsAIG l g => g s -> BV (l s) -> l s -> IO (BV (l s))+negWhen g x c = iteM g c (neg g x) (return x)++-- | Bitblast version of unsigned @quotRem@.+uquotRem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), BV (l s))+uquotRem g dividend divisor = do+  let n = length dividend+  assert (n == length divisor) $ do+    -- Given an n-bit dividend and divisor, 'initial' is the starting value of+    -- the 2n-bit "remainder register" that carries both the quotient and remainder;+    let initial = zext g dividend (2*n)+    let divStep i p rr | i == n = return (q `shiftL1` p, r)+          where (r,q) = splitAt n rr+        divStep i p rr = do+          let rs = rr `shiftL1` p+          let (r,q) = splitAt n rs+           -- Subtract the divisor from the left half of the "remainder register"+          (s,b) <- full_sub g r divisor+          divStep (i+1) (not b) =<< ite g b rs (s ++ q)+    divStep 0 (falseLit g) initial++-- Perform quotRem on the absolute value of the operands.  Then, negate the+-- quotient if the signs of the operands differ and make the sign of a nonzero+-- remainder to match that of the dividend.+squotRem :: IsAIG l g+         => g s+         -> BV (l s)+         -> BV (l s)+         -> IO (BV (l s), BV (l s))+squotRem g dividend' divisor' = do+  let n = length dividend'+  assert (n > 0 && n == length divisor') $ do+    let dsign = msb dividend'+    dividend <- sabs g dividend'+    divisor  <- sabs g divisor'+    -- Given an n-bit dividend and divisor, 'initial' is the starting value of+    -- the 2n-bit "remainder register" that carries both the quotient and remainder;+    let initial = zext g dividend (2*n)+    let divStep rrOrig = do+          let (r,q) = splitAt n rrOrig+          s <- sub g r divisor+          ite g (msb s)+                (rrOrig `shiftL1` falseLit g)     -- rem < 0, orig rr's quot lsl'd w/ 0+                ((s ++ q) `shiftL1` trueLit g) -- rem >= 0, new rr's quot lsl'd w/ 1+    (qr,rr) <- splitAt n <$> stepN n divStep (initial `shiftL1` falseLit g)+    q' <- negWhen g qr =<< xor g dsign (msb divisor')+    r' <- negWhen g (falseLit g `shiftR1` rr) dsign+    return (q', r')++-- | Compute the unsigned quotient of two unsigned bitvectors with the same size.+uquot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+uquot g x y = fst <$> uquotRem g x y++-- | Compute the unsigned division remainder of two unsigned bitvectors with the same size.+urem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+urem g x y = snd <$> uquotRem g x y++-- | Test equality of two bitvectors with the same size.+bvEq :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)+bvEq g x y = go 0 (trueLit g)+  where n = length x+        go i r | i == n = return r+        go i r = go (i+1) =<< and g r =<< eq g (x `at` i) (y `at` i)++-- | Unsigned less-than on bitvector with the same size.+ult :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)+ult g x y = snd <$> full_sub g x y++-- | Unsigned less-than-or-equal on bitvector with the same size.+ule :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)+ule g x y = not <$> ult g y x++-- | Signed less-than on bitvector with the same size.+slt :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)+slt g x y = do+  let xs = x `at` 0+  let ys = y `at` 0+  -- x is negative and y is positive.+  c0 <- and g xs (not ys)+  -- x is positive and y is negative.+  c1 <- and g (not xs) ys+  c2 <- and g (not c1) =<< ult g (tail x) (tail y)+  or g c0 c2++-- | Signed less-than-or-equal on bitvector with the same size.+sle :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)+sle g x y = not <$> slt g y x++-- | @sext v n@ sign extends @v@ to be a vector with length @n@.+-- This function requires that @n >= length v@ and @length v > 0@.+sext :: BV l -> Int -> BV l+sext v r = assert (r >= n && n > 0) $ replicate (r - n) (msb v) ++ v+  where n = length v++-- | @zext g v n@ zero extends @v@ to be a vector with length @n@.+-- This function requires that @n >= length v@.+zext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)+zext g v r = assert (r >= n) $ replicate (r - n) (falseLit g) ++ v+  where n = length v++-- | @muxInteger mergeFn maxValue lv valueFn@ returns a circuit+-- whose result is @valueFn v@ when @lv@ has value @v@.+muxInteger :: (Integral i, Monad m)+           => (l -> m a -> m a -> m a) -- Combining operation for muxing on individual bit values+           -> i -- ^ Maximum value input vector is allowed to take.+           -> BV l -- ^ Input vector+           -> (i -> m a)+           -> m a+muxInteger mergeFn maxValue vx valueFn = impl (length vx) 0+  where impl _ y | y >= toInteger maxValue = valueFn maxValue+        impl 0 y = valueFn (fromInteger y)+        impl i y = mergeFn (vx ! j) (impl j (y `setBit` j)) (impl j y)+          where j = i - 1++-- | Shift left.  The least significant bit becomes 0.+shl :: IsAIG l g+    => g s+    -> BV (l s)       -- ^ the value to shift+    -> BV (l s)       -- ^ how many places to shift+    -> IO (BV (l s))+shl g x y = muxInteger (iteM g) (length x) y (return . shlC g x)++-- | Shift left by a constant.+shlC :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)+shlC g x s0 = slice x j (n-j) ++ replicate j (falseLit g)+  where n = length x+        j = min n s0++-- | Shift right by a constant.+shrC :: l s -> BV (l s) -> Int -> BV (l s)+shrC c x s0 = replicate j c ++ slice x 0 (n-j)+  where n = length x+        j = min n s0++-- | Signed right shift.  The most significant bit is copied.+sshr :: IsAIG l g+     => g s+     -> BV (l s)     -- ^ the value to shift+     -> BV (l s)     -- ^ how many places to shift+     -> IO (BV (l s))+sshr g x y = muxInteger (iteM g) (length x) y (return . shrC (msb x) x)++-- | Unsigned right shift.  The most significant bit becomes 0.+ushr :: IsAIG l g+     => g s+     -> BV (l s)     -- ^ the value to shift+     -> BV (l s)     -- ^ how many places to shift+     -> IO (BV (l s))+ushr g x y = muxInteger (iteM g) (length x) y (return . shrC (falseLit g) x)++-- | Rotate left by a constant.+rolC :: BV l -> Int -> BV l+rolC (BV x) i+  | V.null x  = BV x+  | otherwise = BV (V.drop j x V.++ V.take j x)+  where j = i `mod` V.length x++-- | Rotate right by a constant.+rorC :: BV l -> Int -> BV l+rorC x i = rolC x (- i)++-- | Rotate left.+rol :: IsAIG l g+    => g s+    -> BV (l s)    -- ^ the value to rotate+    -> BV (l s)    -- ^ how many places to rotate+    -> IO (BV (l s))+rol g x y = do+  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))+  muxInteger (iteM g) (length x - 1) r (return . rolC x)++-- | Rotate right.+ror :: IsAIG l g+    => g s+    -> BV (l s)    -- ^ the value to rotate+    -> BV (l s)    -- ^ how many places to rotate+    -> IO (BV (l s))+ror g x y = do+  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))+  muxInteger (iteM g) (length x - 1) r (return . rorC x)++-- | Polynomial multiplication. Note that the algorithm works the same+--   no matter which endianness convention is used.  Result length is+--   @max 0 (m+n-1)@, where @m@ and @n@ are the lengths of the inputs.+pmul :: IsAIG l g+     => g s+     -> BV (l s)+     -> BV (l s)+     -> IO (BV (l s))+pmul g x y = generateM_msb0 (max 0 (m + n - 1)) coeff+  where+    m = length x+    n = length y+    coeff k = foldM (xor g) (falseLit g) =<<+      sequence [ and g (at x i) (at y j) | i <- [0 .. k], let j = k - i, i < m, j < n ]++-- | Polynomial mod with symbolic modulus. Return value has length one+-- less than the length of the modulus.+pmod :: forall l g s. IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+pmod g x y = findmsb (bvToList y)+  where+    findmsb :: [l s] -> IO (BV (l s))+    findmsb [] = return (replicate (length y - 1) (falseLit g)) -- division by zero+    findmsb (c : cs)+      | c === trueLit g = usemask cs+      | c === falseLit g = findmsb cs+      | otherwise = do+          t <- usemask cs+          f <- findmsb cs+          zipWithM (mux g c) t f++    usemask :: [l s] -> IO (BV (l s))+    usemask m = do+      rs <- go 0 p0 z0+      return (zext g (bvFromList rs) (length y - 1))+      where+        msize = Prelude.length m+        p0 = Prelude.replicate (msize - 1) (falseLit g) Prelude.++ [trueLit g]+        z0 = Prelude.replicate msize (falseLit g)++        next :: [l s] -> IO [l s]+        next [] = return []+        next (b : bs) = do+          m' <- mapM (and g b) m+          let bs' = bs Prelude.++ [falseLit g]+          Control.Monad.zipWithM (xor g) m' bs'++        go :: Int -> [l s] -> [l s] -> IO [l s]+        go i p acc+          | i >= length x = return acc+          | otherwise = do+              px <- mapM (and g (x ! i)) p+              acc' <- Control.Monad.zipWithM (xor g) px acc+              p' <- next p+              go (i+1) p' acc'