Data.AIG.Trace

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.

Documentation

class Traceable l where

Minimal complete definition

compareLit, showLit

Methods

compareLit :: l s -> l s -> Ordering

showLit :: l s -> String

newtype TraceLit l s

Constructors

TraceLit

Fields

• unTraceLit :: l s

Instances

TraceOutput l g (TraceLit l s)

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> TraceLit l s -> String

TraceOp l g b => TraceOp l g ([TraceLit l s] -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> ([TraceLit l s] -> b) -> [TraceLit l s] -> b

TraceOp l g b => TraceOp l g (TraceLit l s -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (TraceLit l s -> b) -> TraceLit l s -> b

IsLit l => IsLit (TraceLit l)

Methods

not :: TraceLit l s -> TraceLit l s

(===) :: TraceLit l s -> TraceLit l s -> Bool

(IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g)

Methods

withNewGraph :: Proxy (TraceLit l) (TraceGraph l g) -> (forall s. TraceGraph l g s -> IO a) -> IO a

newGraph :: Proxy (TraceLit l) (TraceGraph l g) -> IO (SomeGraph (TraceGraph l g))

aigerNetwork :: Proxy (TraceLit l) (TraceGraph l g) -> FilePath -> IO (Network (TraceLit l) (TraceGraph l g))

trueLit :: TraceGraph l g s -> TraceLit l s

falseLit :: TraceGraph l g s -> TraceLit l s

constant :: TraceGraph l g s -> Bool -> TraceLit l s

asConstant :: TraceGraph l g s -> TraceLit l s -> Maybe Bool

newInput :: TraceGraph l g s -> IO (TraceLit l s)

and :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

ands :: TraceGraph l g s -> [TraceLit l s] -> IO (TraceLit l s)

or :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

eq :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

implies :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

xor :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

mux :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

inputCount :: TraceGraph l g s -> IO Int

getInput :: TraceGraph l g s -> Int -> IO (TraceLit l s)

writeAiger :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> IO ()

writeAigerWithLatches :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> Int -> IO ()

writeCNF :: TraceGraph l g s -> TraceLit l s -> FilePath -> IO [Int]

checkSat :: TraceGraph l g s -> TraceLit l s -> IO SatResult

cec :: Network (TraceLit l) (TraceGraph l g) -> Network (TraceLit l) (TraceGraph l g) -> IO VerifyResult

evaluator :: TraceGraph l g s -> [Bool] -> IO (TraceLit l s -> Bool)

evaluate :: Network (TraceLit l) (TraceGraph l g) -> [Bool] -> IO [Bool]

litView :: TraceGraph l g s -> TraceLit l s -> IO (LitView (TraceLit l s))

abstractEvaluateAIG :: TraceGraph l g s -> (LitView a -> IO a) -> IO (TraceLit l s -> IO a)

Traceable l => Eq (TraceLit l s)

Methods

(==) :: TraceLit l s -> TraceLit l s -> Bool

(/=) :: TraceLit l s -> TraceLit l s -> Bool

Traceable l => Ord (TraceLit l s)

Methods

compare :: TraceLit l s -> TraceLit l s -> Ordering

(<) :: TraceLit l s -> TraceLit l s -> Bool

(<=) :: TraceLit l s -> TraceLit l s -> Bool

(>) :: TraceLit l s -> TraceLit l s -> Bool

(>=) :: TraceLit l s -> TraceLit l s -> Bool

max :: TraceLit l s -> TraceLit l s -> TraceLit l s

min :: TraceLit l s -> TraceLit l s -> TraceLit l s

data TraceGraph (l :: * -> *) g s

Constructors

TraceGraph

Fields

• tGraph :: g s
• tActive :: IORef (Maybe Handle)

Instances

(IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g)

Methods

withNewGraph :: Proxy (TraceLit l) (TraceGraph l g) -> (forall s. TraceGraph l g s -> IO a) -> IO a

newGraph :: Proxy (TraceLit l) (TraceGraph l g) -> IO (SomeGraph (TraceGraph l g))

aigerNetwork :: Proxy (TraceLit l) (TraceGraph l g) -> FilePath -> IO (Network (TraceLit l) (TraceGraph l g))

trueLit :: TraceGraph l g s -> TraceLit l s

falseLit :: TraceGraph l g s -> TraceLit l s

constant :: TraceGraph l g s -> Bool -> TraceLit l s

asConstant :: TraceGraph l g s -> TraceLit l s -> Maybe Bool

newInput :: TraceGraph l g s -> IO (TraceLit l s)

and :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

ands :: TraceGraph l g s -> [TraceLit l s] -> IO (TraceLit l s)

or :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

eq :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

implies :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

xor :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

mux :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s)

inputCount :: TraceGraph l g s -> IO Int

getInput :: TraceGraph l g s -> Int -> IO (TraceLit l s)

writeAiger :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> IO ()

writeAigerWithLatches :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> Int -> IO ()

writeCNF :: TraceGraph l g s -> TraceLit l s -> FilePath -> IO [Int]

checkSat :: TraceGraph l g s -> TraceLit l s -> IO SatResult

cec :: Network (TraceLit l) (TraceGraph l g) -> Network (TraceLit l) (TraceGraph l g) -> IO VerifyResult

evaluator :: TraceGraph l g s -> [Bool] -> IO (TraceLit l s -> Bool)

evaluate :: Network (TraceLit l) (TraceGraph l g) -> [Bool] -> IO [Bool]

litView :: TraceGraph l g s -> TraceLit l s -> IO (LitView (TraceLit l s))

abstractEvaluateAIG :: TraceGraph l g s -> (LitView a -> IO a) -> IO (TraceLit l s -> IO a)

proxy :: Traceable l => Proxy l g -> Proxy (TraceLit l) (TraceGraph l g)

activateTracing :: TraceGraph l g s -> FilePath -> IO ()

deactiveTracing :: TraceGraph l g s -> IO ()

withTracing :: TraceGraph l g s -> FilePath -> IO a -> IO a

class TraceOp l g a where

Minimal complete definition

traceOp

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> a -> a

Instances

TraceOutput l g x => TraceOp l g (IO x)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> IO x -> IO x

TraceOp l g b => TraceOp l g (FilePath -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (FilePath -> b) -> FilePath -> b

TraceOp l g b => TraceOp l g ([TraceLit l s] -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> ([TraceLit l s] -> b) -> [TraceLit l s] -> b

TraceOp l g b => TraceOp l g (TraceLit l s -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (TraceLit l s -> b) -> TraceLit l s -> b

TraceOp l g b => TraceOp l g (Int -> b)

Methods

traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (Int -> b) -> Int -> b

class TraceOutput l g x where

Minimal complete definition

traceOutput

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> x -> String

Instances

TraceOutput l g VerifyResult

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> VerifyResult -> String

TraceOutput l g SatResult

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> SatResult -> String

TraceOutput l g ()

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> () -> String

TraceOutput l g Int

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> Int -> String

TraceOutput l g x => TraceOutput l g (LitView x)

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> LitView x -> String

TraceOutput l g a => TraceOutput l g [a]

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> [a] -> String

TraceOutput l g (TraceLit l s)

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> TraceLit l s -> String

withNewGraphTracing :: (IsAIG l g, Traceable l) => Proxy l g -> FilePath -> (forall s. TraceGraph l g s -> IO a) -> IO a