diff --git a/aig.cabal b/aig.cabal
--- a/aig.cabal
+++ b/aig.cabal
@@ -1,5 +1,5 @@
 Name:               aig
-Version:            0.1.0.0
+Version:            0.2
 License:            BSD3
 License-file:       LICENSE
 Author:             Galois Inc.
@@ -34,13 +34,16 @@
     Data.AIG
     Data.AIG.Interface
     Data.AIG.Operations
+    Data.AIG.Trace
 
   default-Language: Haskell2010
-  ghc-options:      -Wall
+  ghc-options:      -Wall -fno-ignore-asserts -O2
+  ghc-prof-options: -prof -auto-all -caf-all
   build-depends:
     base == 4.*,
     mtl,
-    vector
+    vector,
+    QuickCheck >= 2.7
 
 -- Ugh. Temporary fix to make Hackage happy.
 --  if flag(enable-hpc)
diff --git a/src/Data/AIG/Interface.hs b/src/Data/AIG/Interface.hs
--- a/src/Data/AIG/Interface.hs
+++ b/src/Data/AIG/Interface.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE DeriveFunctor #-}
 
 {- |
 Module      : Data.AIG.Interface
@@ -17,6 +18,7 @@
   ( -- * Main interface classes
     IsLit(..)
   , IsAIG(..)
+  , lazyMux
 
     -- * Helper datatypes
   , Proxy(..)
@@ -24,17 +26,51 @@
   , Network(..)
   , networkInputCount
 
+  -- * Literal representations
+  , LitView(..)
+  , LitTree(..)
+  , toLitTree
+  , fromLitTree
+  , toLitForest
+  , fromLitForest
+  , foldAIG
+  , foldAIGs
+  , unfoldAIG
+  , unfoldAIGs
+
     -- * Representations of prover results
   , SatResult(..)
   , VerifyResult(..)
   , toSatResult
   , toVerifyResult
+
+    -- * QuickCheck generators and testing
+  , genLitView
+  , genLitTree
+  , getMaxInput
+  , buildNetwork
+  , randomNetwork
   ) where
 
-import Control.Applicative ((<$>))
+import Control.Applicative
 import Control.Monad
 import Prelude hiding (not, and, or)
+import Test.QuickCheck (Gen, Arbitrary(..), generate, oneof, sized, choose)
 
+-- | Concrete datatype representing the ways
+--   an AIG can be constructed.
+data LitView a
+  = And !a !a
+  | NotAnd !a !a
+  | Input !Int
+  | NotInput !Int
+  | TrueLit
+  | FalseLit
+ deriving (Eq,Show,Ord,Functor)
+
+newtype LitTree = LitTree { unLitTree :: LitView LitTree }
+ deriving (Eq,Show,Ord)
+
 class IsLit l where
   -- | Negate a literal.
   not :: l s -> l s
@@ -163,6 +199,82 @@
     f <- evaluator g inputs
     return (f <$> outputs)
 
+  -- | Build an evaluation function over an AIG using the provided view function
+  abstractEvaluateAIG
+          :: g s
+          -> (LitView a -> IO a)
+          -> IO (l s -> IO a)
+
+-- | Evaluate the given literal using the provided view function
+foldAIG :: IsAIG l g
+        => g s
+        -> (LitView a -> IO a)
+        -> l s
+        -> IO a
+foldAIG n view l = do
+   eval <- abstractEvaluateAIG n view
+   eval l
+
+-- | Evaluate the given list of literals using the provided view function
+foldAIGs :: IsAIG l g
+        => g s
+        -> (LitView a -> IO a)
+        -> [l s]
+        -> IO [a]
+foldAIGs n view ls = do
+   eval <- abstractEvaluateAIG n view
+   mapM eval ls
+
+
+-- | Build an AIG literal by unfolding a constructor function
+unfoldAIG :: IsAIG l g
+          => g s
+          -> (a -> IO (LitView a))
+          -> a -> IO (l s)
+unfoldAIG n unfold = f
+ where f = unfold >=> g
+       g (And x y)    = and' (f x) (f y)
+       g (NotAnd x y) = fmap not $ and' (f x) (f y)
+       g (Input i)    = getInput n i
+       g (NotInput i) = fmap not $ getInput n i
+       g TrueLit      = return $ trueLit n
+       g FalseLit     = return $ falseLit n
+       and' mx my = do
+          x <- mx
+          y <- my
+          and n x y
+
+-- | Build a list of AIG literals by unfolding a constructor function
+unfoldAIGs :: IsAIG l g
+          => g s
+          -> (a -> IO (LitView a))
+          -> [a] -> IO [l s]
+unfoldAIGs n unfold = mapM (unfoldAIG n unfold)
+
+-- | Extract a tree representation of the given literal
+toLitTree :: IsAIG l g => g s -> l s -> IO LitTree
+toLitTree g = foldAIG g (return . LitTree)
+
+-- | Construct an AIG literal from a tree representation
+fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s)
+fromLitTree g = unfoldAIG g (return . unLitTree)
+
+-- | Extract a forest representation of the given list of literal s
+toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree]
+toLitForest g = foldAIGs g (return . LitTree)
+
+-- | Construct a list of AIG literals from a forest representation
+fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s]
+fromLitForest g = unfoldAIGs g (return . unLitTree)
+
+-- | Short-cutting mux operator that optimizes the case
+--   where the test bit is a concrete literal
+lazyMux :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s) -> IO (l s)
+lazyMux g c
+  | c === (trueLit g)  = \x _y -> x
+  | c === (falseLit g) = \_x y -> y
+  | otherwise = \x y -> join $ pure (mux g c) <*> x <*> y
+
 -- | A network is an and-inverstor graph paired with it's outputs,
 --   thus representing a complete combinational circuit.
 data Network l g where
@@ -185,20 +297,83 @@
 data SatResult
    = Unsat
    | Sat !([Bool])
+   | SatUnknown
   deriving (Eq,Show)
 
 -- | Result of a verification check.
 data VerifyResult
    = Valid
    | Invalid [Bool]
+   | VerifyUnknown
   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
+toVerifyResult SatUnknown = VerifyUnknown
 
 -- | Convert a verify result to a sat result by negating it.
 toSatResult :: VerifyResult -> SatResult
 toSatResult Valid = Unsat
 toSatResult (Invalid l) = Sat l
+toSatResult VerifyUnknown = SatUnknown
+
+-- | Generate an arbitrary `LitView` given a generator for `a`
+genLitView :: Gen a -> Gen (LitView a)
+genLitView gen = oneof
+     [ return TrueLit
+     , return FalseLit
+     , sized $ \n -> choose (0,n-1) >>= \i -> return (Input i)
+     , sized $ \n -> choose (0,n-1) >>= \i -> return (NotInput i)
+     , do x <- gen
+          y <- gen
+          return (And x y)
+     , do x <- gen
+          y <- gen
+          return (NotAnd x y)
+     ]
+
+-- | Generate an arbitrary `LitTree`
+genLitTree :: Gen LitTree
+genLitTree = fmap LitTree $ genLitView genLitTree
+
+-- | Given a LitTree, calculate the maximum input number in the tree.
+--   Returns 0 if no inputs are referenced.
+getMaxInput :: LitTree -> Int
+getMaxInput (LitTree x) =
+  case x of
+     TrueLit -> 0
+     FalseLit -> 0
+     Input i -> i
+     NotInput i -> i
+     And a b -> max (getMaxInput a) (getMaxInput b)
+     NotAnd a b -> max (getMaxInput a) (getMaxInput b)
+
+instance Arbitrary LitTree where
+  arbitrary = genLitTree
+  shrink (LitTree TrueLit)      = []
+  shrink (LitTree FalseLit)     = []
+  shrink (LitTree (Input _))    = [LitTree TrueLit, LitTree FalseLit]
+  shrink (LitTree (NotInput _)) = [LitTree TrueLit, LitTree FalseLit]
+  shrink (LitTree (And x y)) =
+      [ LitTree TrueLit, LitTree FalseLit, x, y ] ++
+      [ LitTree (And x' y') | (x',y') <- shrink (x,y) ]
+  shrink (LitTree (NotAnd x y)) =
+      [ LitTree TrueLit, LitTree FalseLit, x, y ] ++
+      [ LitTree (NotAnd x' y') | (x',y') <- shrink (x,y) ]
+
+
+-- | Given a list of LitTree, construct a corresponding AIG network
+buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g)
+buildNetwork proxy litForrest = do
+   let maxInput = foldr max 0 $ map getMaxInput litForrest
+   (SomeGraph g) <- newGraph proxy
+   forM_ [0..maxInput] (\_ -> newInput g)
+   ls <- fromLitForest g litForrest
+   return (Network g ls)
+
+-- | Generate a random network by building a random `LitTree`
+--   and using that to construct a network.
+randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)
+randomNetwork proxy = generate arbitrary >>= buildNetwork proxy
diff --git a/src/Data/AIG/Operations.hs b/src/Data/AIG/Operations.hs
--- a/src/Data/AIG/Operations.hs
+++ b/src/Data/AIG/Operations.hs
@@ -8,13 +8,14 @@
 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.
+A collection of higher-level operations (mostly 2's complement arithmetic operations)
+that can be built from the primitive And-Inverter Graph interface.
 -}
 
 module Data.AIG.Operations
   ( -- * Bitvectors
     BV
+  , empty
   , length
   , at
   , (!)
@@ -23,9 +24,14 @@
   , take
   , drop
   , slice
+  , sliceRev
+  , mapM
+  , zipWith
   , zipWithM
   , msb
   , lsb
+  , bvSame
+  , bvShow
 
     -- ** Building bitvectors
   , generateM_msb0
@@ -33,9 +39,28 @@
   , generateM_lsb0
   , generate_lsb0
   , replicate
+  , replicateM
   , bvFromInteger
+  , bvFromList
   , muxInteger
+  , singleton
 
+    -- ** Lazy operators
+  , lAnd
+  , lAnd'
+  , lOr
+  , lOr'
+  , lXor
+  , lXor'
+  , lEq
+  , lEq'
+  , lNot
+  , lNot'
+
+    -- ** Conditionals
+  , ite
+  , iteM
+
     -- ** Deconstructing bitvectors
   , asUnsigned
   , asSigned
@@ -48,9 +73,13 @@
   , addC
   , sub
   , subC
+  , addConst
+  , subConst
 
     -- ** Multiplication and division
   , mul
+  , mulFull
+  , smulFull
   , squot
   , srem
   , uquot
@@ -65,55 +94,52 @@
 
     -- ** Numeric comparisons
   , bvEq
+  , isZero
+  , nonZero
   , sle
   , slt
   , ule
   , ult
+  , sabs
 
     -- ** Extensions
   , sext
   , zext
+  , trunc
+  , zeroIntCoerce
+  , signIntCoerce
 
     -- * Polynomial multiplication and modulus
   , pmul
   , pmod
   ) where
 
-import Control.Applicative
+import Control.Applicative hiding (empty)
 import Control.Exception
 import qualified Control.Monad
-import Control.Monad.State hiding (zipWithM)
+import Control.Monad.State hiding (zipWithM, replicateM, mapM)
 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 Data.Vector.Generic.Mutable as MV
+
+import Prelude hiding (and, concat, length, not, or, replicate, splitAt, tail, (++), take, drop, zipWith, mapM)
 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 }
+  deriving (Eq, Ord, Show)
 
 instance Functor BV where
   fmap f (BV v) = BV (f <$> v)
 
+-- | Empty bitvector
+empty :: BV l
+empty = BV V.empty
+
 -- | Number of bits in a bit vector
 length :: BV l -> Int
 length (BV v) = V.length v
@@ -123,23 +149,47 @@
 
 -- | 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.
+{-# INLINE generate_lsb0 #-}
 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_lsb0 c f = BV (V.reverse (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 LSB-first order, i.e., @f 0@ is the least significant bit.
+{-# INLINE generateM_lsb0 #-}
 generateM_lsb0
-   :: Monad m
+   :: MonadIO 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))
+generateM_lsb0 c f = do
+   mv <- liftIO (MV.new c)
+   let buildVec i | i >= c = liftIO (V.unsafeFreeze mv) >>= return . BV
+                  | otherwise = (f i >>= liftIO . MV.unsafeWrite mv (c-i-1)) >> (buildVec $! (i+1))
+   buildVec 0
+--generateM_lsb0 c f = return . BV . V.reverse =<< V.generateM c f
 
+{-# INLINE generateM_scan_lsb0 #-}
+generateM_scan_lsb0
+   :: MonadIO m
+   => Int            -- ^ @n@, length of the generated bitvector
+   -> (Int -> a -> m (l,a))   -- ^ @f@, computation to generate a bit literal
+   -> a
+   -> m (BV l, a)
+generateM_scan_lsb0 c f a0 = do
+   mv <- liftIO (MV.new c)
+   let buildVec i a | i >= c = liftIO (V.unsafeFreeze mv) >>= \v -> return (BV v, a)
+                    | otherwise = do (x,a') <- f i a
+                                     liftIO (MV.unsafeWrite mv (c-i-1) x)
+                                     (buildVec $! (i+1)) a'
+   buildVec 0 a0
+
+
 -- | 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.
+{-# INLINE generate_msb0 #-}
 generate_msb0
    :: Int            -- ^ @n@, length of the generated bitvector
    -> (Int -> l)     -- ^ @f@, function to calculate bit literals
@@ -148,6 +198,7 @@
 
 -- | 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.
+{-# INLINE generateM_msb0 #-}
 generateM_msb0
    :: Monad m
    => Int            -- ^ @n@, length of the generated bitvector
@@ -162,6 +213,18 @@
    -> BV l
 replicate c e = BV (V.replicate c e)
 
+-- | Generate a bit vector of length @n@ where every bit value is generated in turn by @m@.
+replicateM
+   :: Monad m
+   => Int     -- ^ @n@, length of the bitvector
+   -> m l     -- ^ @m@, the computation to produce a literal
+   -> m (BV l)
+replicateM c e = return . BV =<< V.replicateM c e
+
+-- | Generate a one-element bitvector containing the given literal
+singleton :: l -> BV l
+singleton = BV . V.singleton
+
 -- | 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.
@@ -193,10 +256,29 @@
       -> 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)
 
+
+-- | Extract @n@ bits starting at index @i@, counting from
+--   the end of the vector instead of the beginning.
+--   The vector must contain at least @i+n@ elements.
+sliceRev
+      :: BV l
+      -> Int   -- ^ @i@, 0-based start index from the end of the vector
+      -> Int   -- ^ @n@, bits to take
+      -> BV l
+sliceRev (BV v) i n = BV (V.slice i' n v)
+  where i' = V.length v - i - n
+
+-- | Apply a monadic operation to each element of a bitvector in sequence
+mapM :: Monad m => (a -> m b) -> BV a -> m (BV b)
+mapM f (BV x) = V.mapM f x >>= return . BV
+
+-- | Combine two bitvectors with a bitwise function
+zipWith :: (l -> l -> l) -> BV l -> BV l -> BV l
+zipWith f (BV x) (BV y) = assert (V.length x == V.length y) $ BV $ V.zipWith f x y
+
 -- | 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
+zipWithM :: Monad m => (l -> l -> m l) -> BV l -> BV l -> m (BV l)
+zipWithM f (BV x) (BV y) = assert (V.length x == V.length y) $ V.zipWithM f x y >>= return . BV
 
 -- | Convert a bitvector to a list, most significant bit first.
 bvToList :: BV l -> [l]
@@ -212,6 +294,14 @@
 (!) :: BV l -> Int -> l
 (!) v i = v `at` (length v - 1 - i)
 
+-- | Display a bitvector as a string of bits with most significant bits first.
+--   Concrete literals are displayed as '0' or '1', whereas symbolic literals are displayed as 'x'.
+bvShow :: IsAIG l g => g s -> BV (l s) -> String
+bvShow g v = map f $ bvToList v
+ where f x | x === trueLit g  = '1'
+           | x === falseLit g = '0'
+           | otherwise = 'x'
+
 -- | Generate a bitvector from an integer value, using 2's complement representation.
 bvFromInteger
    :: IsAIG l g
@@ -219,7 +309,8 @@
    -> 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)
+bvFromInteger g n v = generate_msb0 n $ \i -> constant g (v `testBit` (n-i-1))
+   --generate_lsb0 n $ \i -> constant g (v `testBit` i)
 
 -- | Interpret a bitvector as an unsigned integer.  Return @Nothing@ if
 --   the bitvector is not concrete.
@@ -229,25 +320,19 @@
         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
+          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
+asSigned g v = assert (n > 0) $ (signfix =<< asUnsigned g (drop 1 v))
   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
+        signfix x
+            | msb v === trueLit g  = Just (x - 2^(n-1))
+            | msb v === falseLit g = Just x
+            | otherwise = Nothing
 
 -- | Retrieve the most significant bit of a bitvector.
 msb :: BV l -> l
@@ -282,46 +367,179 @@
   | c === falseLit g = y
   | otherwise = join $ zipWithM (mux g c) <$> x <*> y
 
+{-# INLINE lNot #-}
+-- | Lazy negation of a circuit.
+lNot :: IsAIG l g => g s -> IO (l s) -> IO (l s)
+lNot g = fmap (lNot' g)
+
+{-# INLINE lNot' #-}
+lNot' :: IsAIG l g => g s -> l s -> l s
+lNot' g x | x === trueLit g = falseLit g
+          | x === falseLit g = trueLit g
+          | otherwise = not x
+
+{-# INLINE lOr #-}
+-- | Build a short-cut OR circuit.  If the left argument
+--   evaluates to the constant true, the right argument
+--   will not be evaluated.
+lOr :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
+lOr g x y = lNot g (lAnd g (lNot g x) (lNot g y))
+
+{-# INLINE lOr' #-}
+lOr' :: IsAIG l g => g s -> l s -> l s -> IO (l s)
+lOr' g x y = lNot g (lAnd' g (lNot' g x) (lNot' g y))
+
+{-# INLINE lEq #-}
+-- | Construct a lazy equality test.  If both arguments are constants,
+--   the output will also be a constant.
+lEq :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
+lEq g x y = lNot g (lXor g x y)
+
+{-# INLINE lEq' #-}
+lEq' :: IsAIG l g => g s -> l s -> l s -> IO (l s)
+lEq' g x y = lNot g (lXor' g x y)
+
+-- | Build a short-cut AND circuit.  If the left argument
+--   evaluates to the constant false, the right argument
+--   will not be evaluated.
+lAnd :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
+lAnd g x y = do
+  x' <- x
+  if      x' === trueLit g  then y
+  else if x' === falseLit g then return (falseLit g)
+  else do
+      y' <- y
+      if      y' === trueLit g  then return x'
+      else if y' === falseLit g then return (falseLit g)
+      else and g x' y'
+
+lAnd'' :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s)
+lAnd'' g x y =
+  if      x === trueLit g  then y
+  else if x === falseLit g then return (falseLit g)
+  else do
+      y' <- y
+      if      y' === trueLit g  then return x
+      else if y' === falseLit g then return (falseLit g)
+      else and g x y'
+
+lAnd' :: IsAIG l g => g s -> l s -> l s -> IO (l s)
+lAnd' g x y =
+  if      x === trueLit g  then return y
+  else if x === falseLit g then return (falseLit g)
+  else if y === trueLit g  then return x
+  else if y === falseLit g then return (falseLit g)
+  else and g x y
+
+lXor' :: IsAIG l g => g s -> l s -> l s -> IO (l s)
+lXor' g x y =
+  if      x === trueLit g  then return (not y)
+  else if x === falseLit g then return y
+  else if y === trueLit g  then return (not x)
+  else if y === falseLit g then return x
+  else xor g x y
+
+-- | Construct a lazy xor.  If both arguments are constants,
+--   the output will also be a constant.
+lXor :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
+lXor g x y = do
+  x' <- x
+  y' <- y
+  if      x' === trueLit g  then return (not y')
+  else if x' === falseLit g then return y'
+  else if y' === trueLit g  then return (not x')
+  else if y' === falseLit g then return x'
+  else xor g x' y'
+
+
+-- | A half adder which takes two inputs and returns output and carry.
+{-# INLINE halfAdder #-}
+halfAdder :: IsAIG l g => g s -> l s -> l s -> IO (l s, l s)
+halfAdder g b c = do
+  c_out <- lAnd' g b c
+  s <- lAnd'' g (not c_out) (lOr' g b c)
+  return (s, c_out)
+
+
+-- | A full adder which takes three inputs and returns output and carry.
+{-# INLINE fullAdder #-}
+fullAdder :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s)
+fullAdder g a b c_in = do
+   s <- lXor' g c_in =<< lXor' g a b
+   c_out <- lOr g (lAnd' g a b) (lAnd'' g c_in (lXor' g a b))
+   return (s, c_out)
+
 -- | 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
+ripple_add g x _ | length x == 0 = return (x, falseLit g)
+ripple_add g x y = do
+   let unfold i = fullAdder g (x!i) (y!i)
+   generateM_scan_lsb0 (length x) unfold (falseLit g)
 
+-- ripple_add g x y = do
+--     r <- newIORef (falseLit g)
+--     let unfold i = do (s,c) <- fullAdder g (x!i) (y!i) =<< readIORef r
+--                       writeIORef r c
+--                       return s
+--     sum <- generateM_lsb0 (length x) unfold
+--     c_out <- readIORef r
+--     return (sum,c_out)
+
+
 -- | A subtraction circuit which takes three inputs and returns output and carry.
+{-# INLINE fullSub #-}
 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
+  s <- lEq' g x =<< (lEq' g y b_in)
+  b_out <- lOr g (lAnd' g y b_in) (lAnd'' g (not x) (lOr' g y b_in))
   return (s, b_out)
 
+
 -- | Subtract two bit vectors, returning result and borrow bit.
-full_sub :: IsAIG l g
+ripple_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)
+ripple_sub g x _ | length x == 0 = return (x,falseLit g)
+ripple_sub g x y = do
+  let unfold i = fullSub g (x ! i) (y ! i)
+  generateM_scan_lsb0 (length x) unfold (falseLit g)
 
+-- ripple_sub g x y = do
+--     r <- newIORef (falseLit g)
+--     let unfold i = do (s,b) <- fullSub g (x!i) (y!i) =<< readIORef r
+--                       writeIORef r b
+--                       return s
+--     diff <- generateM_lsb0 (length x) unfold
+--     b_out <- readIORef r
+--     return (diff,b_out)
+
+
+-- | Compute just the borrow bit of a subtraction.
+{-# INLINE ripple_sub_borrow #-}
+ripple_sub_borrow :: IsAIG l g
+         => g s
+         -> BV (l s)
+         -> BV (l s)
+         -> IO (l s)
+ripple_sub_borrow g x y = go 0 (falseLit g)
+   where n = length x
+         go i b | i >= n = return b
+                | otherwise = (go $! (i+1)) =<<
+                                  (lOr g (lAnd' g b (y!i))
+                                         (lAnd'' g (lNot' g (x!i)) (lOr' g (y!i) b))
+                                  )
+
 -- | 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
+  where unfold i = StateT $ halfAdder g (lNot' g (x ! i))
 
 -- | 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))
@@ -329,7 +547,7 @@
 
 -- | 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)
+addC g x y = assert (length x == length y) $ ripple_add g x y
 
 -- | 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))
@@ -337,22 +555,70 @@
 
 -- | 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)
+subC g x y = assert (length x == length y) $ ripple_sub g x y
 
+-- | Add a constant value to a bitvector
+addConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))
+addConst g x y = do
+  let n = length x
+  m <- MV.new n
+  let adderStepM c i
+        | i == n = return ()
+        | otherwise = do
+          let a = x ! i
+          let b = y `testBit` i
+          ac <- lAnd' g a c
+          negAnegC <- lAnd' g (lNot' g a) (lNot' g c)
+          aEqC <- lOr' g ac negAnegC
+          if b
+            then do
+              MV.write m (n-i-1) aEqC
+              adderStepM (lNot' g negAnegC) (i+1)
+            else do
+              MV.write m (n-i-1) (lNot' g aEqC)
+              adderStepM ac (i+1)
+  adderStepM (falseLit g) 0
+  fmap BV $ V.freeze m
 
--- | Multiply two bitvectors with the same size.
+--addConst g x c = add g x (bvFromInteger g (length x) c)
+
+-- | Add a constant value to a bitvector
+subConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))
+subConst g x c = addConst g x (-c)
+
+
+-- | Multiply two bitvectors with the same size, with result
+--   of the same size as the arguments.
+--   Overflow is silently discarded.
 mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
-mul g x y = do
+mul g x y = assert (length x == length 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
+        z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)
         updateBits (i+1) z'
   updateBits 0 $ replicate (length x) (falseLit g)
 
+-- | Unsigned multiply two bitvectors with size @m@ and size @n@,
+--   resulting in a vector of size @m+n@.
+mulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
+mulFull g x y =
+    let len = length x + length y
+        x' = zext g x len
+        y' = zext g y len
+     in mul g x' y'
+
+-- | Signed multiply two bitvectors with size @m@ and size @n@,
+--   resulting in a vector of size @m+n@.
+smulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
+smulFull g x y = do
+    let len = length x + length y
+        x' = sext g x len
+        y' = sext g y len
+     in mul g x' y'
+
 -- | 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
@@ -365,19 +631,19 @@
 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)
+-- -- | 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)
 
+-- 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
+
 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)
@@ -400,8 +666,8 @@
           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)
+          (s,b) <- ripple_sub g r divisor
+          divStep (i+1) (lNot' g b) =<< ite g b rs (s ++ q)
     divStep 0 (falseLit g) initial
 
 -- Perform quotRem on the absolute value of the operands.  Then, negate the
@@ -412,26 +678,39 @@
          -> 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')
+squotRem g dividend divisor =
+    assert (length dividend > 0 && length dividend == length divisor) $ do
+    let sign1 = msb dividend
+    let sign2 = msb divisor
+    signXor <- xor g sign1 sign2
+    dividend' <- negWhen g dividend sign1
+    divisor'  <- negWhen g divisor sign2
+    (q,r) <- uquotRem g dividend' divisor'
+    q' <- negWhen g q signXor
+    r' <- negWhen g r sign1
+    return (q',r')
 
+-- This code seems to have a bug...
+-- 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
@@ -440,41 +719,53 @@
 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 syntactic equalify of two bitvectors using the `===` operation
+bvSame :: IsLit l => BV (l s) -> BV (l s) -> Bool
+bvSame (BV x) (BV y) = assert (V.length x == V.length y) $ V.foldr (&&) True $ V.zipWith (===) 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)
+bvEq g x y = assert (n == length 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)
 
+-- | Test if a bitvector is equal to zero
+isZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)
+isZero g (BV v) = V.foldM (\x y -> and g (lNot' g x) y) (trueLit g) v
+
+-- | Test if a bitvector is distinct from zero
+nonZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)
+nonZero g bv = lNot g $ isZero g bv
+
 -- | 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
+ult g x y = assert (length x == length y) $ ripple_sub_borrow 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
+ule g x y = lNot g $ 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
+slt g x y = assert (length x == length 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)
+  c0 <- and g xs (lNot' g 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)
+  c1 <- and g (lNot' g xs) ys
+  c2 <- and g (lNot' g 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
+sle g x y = lNot g $ 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
+sext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)
+sext _g 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@.
@@ -483,6 +774,27 @@
 zext g v r = assert (r >= n) $ replicate (r - n) (falseLit g) ++ v
   where n = length v
 
+-- | Truncate the given bit vector to the specified length
+trunc :: Int -> BV (l s) -> BV (l s)
+trunc w vx = assert (length vx >= w) $ drop (length vx - w) vx
+
+-- | Truncate or zero-extend a bitvector to have the specified number of bits
+zeroIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s)
+zeroIntCoerce g r t
+    | r > l = zext g t r
+    | r < l = trunc r t
+    | otherwise = t
+  where l = length t
+
+-- | Truncate or sign-extend a bitvector to have the specified number of bits
+signIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s)
+signIntCoerce g r t
+    | r > l = sext g t r
+    | r < l = trunc r t
+    | otherwise = t
+  where l = length t
+
+
 -- | @muxInteger mergeFn maxValue lv valueFn@ returns a circuit
 -- whose result is @valueFn v@ when @lv@ has value @v@.
 muxInteger :: (Integral i, Monad m)
@@ -606,7 +918,7 @@
         next :: [l s] -> IO [l s]
         next [] = return []
         next (b : bs) = do
-          m' <- mapM (and g b) m
+          m' <- Prelude.mapM (and g b) m
           let bs' = bs Prelude.++ [falseLit g]
           Control.Monad.zipWithM (xor g) m' bs'
 
@@ -614,7 +926,7 @@
         go i p acc
           | i >= length x = return acc
           | otherwise = do
-              px <- mapM (and g (x ! i)) p
+              px <- Prelude.mapM (and g (x ! i)) p
               acc' <- Control.Monad.zipWithM (xor g) px acc
               p' <- next p
               go (i+1) p' acc'
diff --git a/src/Data/AIG/Trace.hs b/src/Data/AIG/Trace.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/AIG/Trace.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+
+
+{- |
+Module      : Data.AIG.Interface
+Copyright   : (c) Galois, Inc. 2014
+License     : BSD3
+Maintainer  : jhendrix@galois.com
+Stability   : experimental
+Portability : portable
+
+A tracing wrapper AIG interface.  Given an underlying AIG interface, this
+wrapper intercepts all interface calls and logs them to a file for debugging
+purposes.
+-}
+
+module Data.AIG.Trace where
+
+import Prelude hiding (not, and, or)
+import Data.IORef
+import System.IO
+import Control.Exception
+import System.IO.Unsafe
+
+import Data.AIG.Interface
+
+
+class Traceable l where
+  compareLit :: l s -> l s -> Ordering
+  showLit :: l s -> String
+
+newtype TraceLit l s = TraceLit { unTraceLit :: l s }
+
+data TraceGraph (l :: * -> * ) g s
+   = TraceGraph
+   { tGraph :: g s
+   , tActive :: IORef (Maybe Handle)
+   }
+
+proxy :: Traceable l => Proxy l g -> Proxy (TraceLit l) (TraceGraph l g)
+proxy (Proxy _) = Proxy (\x -> x)
+
+activateTracing :: TraceGraph l g s -> FilePath -> IO ()
+activateTracing g fp = do
+    maybe (return ()) hClose =<< readIORef (tActive g)
+    h <- openFile fp WriteMode
+    writeIORef (tActive g) (Just h)
+
+deactiveTracing :: TraceGraph l g s -> IO ()
+deactiveTracing g = do
+    maybe (return ()) hClose =<< readIORef (tActive g)
+    writeIORef (tActive g) Nothing
+
+withTracing :: TraceGraph l g s -> FilePath -> IO a -> IO a
+withTracing g fp m =
+   bracket (do old <- readIORef (tActive g)
+               h <- openFile fp WriteMode
+               writeIORef (tActive g) (Just h)
+               return (h,old))
+           (\(h,old) -> hClose h >> writeIORef (tActive g) old)
+           (\_ -> m)
+
+instance IsLit l => IsLit (TraceLit l) where
+  not (TraceLit l) = TraceLit (not l)
+  (TraceLit x) === (TraceLit y) = x === y
+
+instance Traceable l => Eq (TraceLit l s) where
+  (TraceLit x) == (TraceLit y) = compareLit x y == EQ
+
+instance Traceable l => Ord (TraceLit l s) where
+  compare (TraceLit x) (TraceLit y) = compareLit x y
+
+
+class TraceOp l g a where
+  traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> a -> a
+
+class TraceOutput l g x where
+  traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> x -> String
+
+instance TraceOp l g b => TraceOp l g (Int -> b) where
+  traceOp g msg f i = traceOp g (msg++" "++show i) (f i)
+
+instance TraceOp l g b => TraceOp l g (TraceLit l s -> b) where
+  traceOp g msg f i = traceOp g (msg++" "++showLit (unTraceLit i)) (f i)
+
+instance TraceOp l g b => TraceOp l g ([TraceLit l s] -> b) where
+  traceOp g msg f is = traceOp g (msg++" ["++unwords (map (showLit . unTraceLit) is)++"]") (f is)
+
+instance TraceOp l g b => TraceOp l g (FilePath -> b) where
+  traceOp g msg f i = traceOp g (msg++" "++i) (f i)
+
+instance TraceOutput l g x => TraceOp l g (IO x) where
+  traceOp g msg f = do
+      mh <- readIORef (tActive g)
+      case mh of
+        Nothing -> f
+        Just h -> do
+            hPutStr h msg
+            hFlush h
+            x <- f
+            hPutStrLn h $ " result "++traceOutput g x
+            hFlush h
+            return x
+
+instance TraceOutput l g (TraceLit l s) where
+  traceOutput _g (TraceLit l) = showLit l
+
+instance TraceOutput l g Int where
+  traceOutput _g i = show i
+
+instance TraceOutput l g () where
+  traceOutput _g () = "()"
+
+instance TraceOutput l g SatResult where
+  traceOutput _g r = show r
+
+instance TraceOutput l g VerifyResult where
+  traceOutput _g r = show r
+
+withNewGraphTracing :: (IsAIG l g, Traceable l)
+                    => Proxy l g
+                    -> FilePath
+                    -> (forall s. TraceGraph l g s -> IO a)
+                    -> IO a
+withNewGraphTracing _ fp f = withNewGraph undefined $ \g -> withTracing g fp (f g)
+
+instance (IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g) where
+  withNewGraph _ f = withNewGraph undefined $ \g -> do
+                         r <- newIORef Nothing
+                         f (TraceGraph g r)
+
+  aigerNetwork _ fp = do
+          (Network g outs) <- aigerNetwork undefined fp
+          r <- newIORef Nothing
+          return (Network (TraceGraph g r) (map TraceLit outs))
+
+  trueLit g = TraceLit $ trueLit (tGraph g)
+  falseLit g = TraceLit $ falseLit (tGraph g)
+
+  newInput g = traceOp g "NewInput" $ fmap TraceLit $ newInput (tGraph g)
+
+  and g = traceOp g "and" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ and (tGraph g) x y
+  or g = traceOp g "or" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ or (tGraph g) x y
+  implies g = traceOp g "implies" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ implies (tGraph g) x y
+  eq g = traceOp g "eq" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ eq (tGraph g) x y
+  xor g = traceOp g "xor" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $  xor (tGraph g) x y
+  mux g = traceOp g "mux" $ \(TraceLit x) (TraceLit y) (TraceLit z) -> fmap TraceLit $ mux (tGraph g) x y z
+
+  inputCount g = traceOp g "inputCount" $ inputCount (tGraph g)
+
+  getInput g = traceOp g "getInput" $ \i -> fmap TraceLit $ getInput (tGraph g) i
+
+  writeAiger fp0 (Network g outs0) =
+       (traceOp g "writeAiger" $ \fp outs -> writeAiger fp (Network (tGraph g) (map unTraceLit outs))) fp0 outs0
+
+  checkSat g = traceOp g "checkSat" $ \(TraceLit x) -> checkSat (tGraph g) x
+
+  cec (Network g1 outs1') (Network g2 outs2') =
+      (traceOp g1 "cec" $ \outs1 outs2 ->
+        cec (Network (tGraph g1) (map unTraceLit outs1))
+            (Network (tGraph g2) (map unTraceLit outs2)))
+            outs1' outs2'
+
+  evaluator g ins =
+        do mh <- readIORef (tActive g)
+           maybe (return ()) (\h -> (hPutStrLn h $ unwords ["building evaluator",show ins]) >> hFlush h) mh
+           let traceIO l x h = (hPutStrLn h $ unwords ["evaluator call",show ins,showLit l,show x]) >> hFlush h
+           let trace l x =
+                  case mh of
+                     Nothing -> x
+                     Just h  -> seq (unsafePerformIO (traceIO l x h)) x
+           ev <- evaluator (tGraph g) ins
+           return (\(TraceLit l) -> trace l $ ev l)
+
+  abstractEvaluateAIG g f =
+        do mh <- readIORef (tActive g)
+           maybe (return ()) (\h -> (hPutStrLn h $ unwords ["building abstract evaluator"]) >> hFlush h) mh
+           let traceIO l h = (hPutStrLn h $ unwords ["abstract evaluator call",showLit l]) >> hFlush h
+           let trace l x =
+                  case mh of
+                     Nothing -> return x
+                     Just h  -> traceIO l h >> return x
+           ev <- abstractEvaluateAIG (tGraph g) f
+           return (\(TraceLit l) -> trace l =<< ev l)