Copyright	(c) Galois Inc. 2014
License	BSD3
Maintainer	jhendrix@galois.com
Stability	experimental
Portability	portable
Safe Haskell	None
Language	Haskell2010

Data.AIG.Trace

Description

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 Source #

Minimal complete definition

compareLit, showLit

Methods

compareLit :: l s -> l s -> Ordering Source #

showLit :: l s -> String Source #

newtype TraceLit l s Source #

Constructors

TraceLit
Fields unTraceLit :: l s

Instances

TraceOutput l g (TraceLit l s) Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> TraceLit l s -> String Source #
TraceOp l g b => TraceOp l g ([TraceLit l s] -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> ([TraceLit l s] -> b) -> [TraceLit l s] -> b Source #
TraceOp l g b => TraceOp l g (TraceLit l s -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (TraceLit l s -> b) -> TraceLit l s -> b Source #
IsLit l => IsLit (TraceLit l) Source #
Methods not :: TraceLit l s -> TraceLit l s Source # (===) :: TraceLit l s -> TraceLit l s -> Bool Source #
(IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g) Source #
Methods withNewGraph :: Proxy (TraceLit l) (TraceGraph l g) -> (forall s. TraceGraph l g s -> IO a) -> IO a Source # newGraph :: Proxy (TraceLit l) (TraceGraph l g) -> IO (SomeGraph (TraceGraph l g)) Source # aigerNetwork :: Proxy (TraceLit l) (TraceGraph l g) -> FilePath -> IO (Network (TraceLit l) (TraceGraph l g)) Source # trueLit :: TraceGraph l g s -> TraceLit l s Source # falseLit :: TraceGraph l g s -> TraceLit l s Source # constant :: TraceGraph l g s -> Bool -> TraceLit l s Source # asConstant :: TraceGraph l g s -> TraceLit l s -> Maybe Bool Source # newInput :: TraceGraph l g s -> IO (TraceLit l s) Source # and :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # ands :: TraceGraph l g s -> [TraceLit l s] -> IO (TraceLit l s) Source # or :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # eq :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # implies :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # xor :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # mux :: TraceGraph l g s -> TraceLit l s -> TraceLit l s -> TraceLit l s -> IO (TraceLit l s) Source # inputCount :: TraceGraph l g s -> IO Int Source # getInput :: TraceGraph l g s -> Int -> IO (TraceLit l s) Source # writeAiger :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> IO () Source # writeCNF :: TraceGraph l g s -> TraceLit l s -> FilePath -> IO [Int] Source # checkSat :: TraceGraph l g s -> TraceLit l s -> IO SatResult Source # cec :: Network (TraceLit l) (TraceGraph l g) -> Network (TraceLit l) (TraceGraph l g) -> IO VerifyResult Source # evaluator :: TraceGraph l g s -> [Bool] -> IO (TraceLit l s -> Bool) Source # evaluate :: Network (TraceLit l) (TraceGraph l g) -> [Bool] -> IO [Bool] Source # litView :: TraceGraph l g s -> TraceLit l s -> IO (LitView (TraceLit l s)) Source # abstractEvaluateAIG :: TraceGraph l g s -> (LitView a -> IO a) -> IO (TraceLit l s -> IO a) Source #
Traceable l => Eq (TraceLit l s) Source #
Methods (==) :: TraceLit l s -> TraceLit l s -> Bool # (/=) :: TraceLit l s -> TraceLit l s -> Bool #
Traceable l => Ord (TraceLit l s) Source #
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 Source #

Constructors

TraceGraph
Fields tGraph :: g s tActive :: IORef (Maybe Handle)

Instances

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

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

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

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

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

class TraceOp l g a where Source #

Minimal complete definition

traceOp

Methods

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

Instances

TraceOutput l g x => TraceOp l g (IO x) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> IO x -> IO x Source #
TraceOp l g b => TraceOp l g (FilePath -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (FilePath -> b) -> FilePath -> b Source #
TraceOp l g b => TraceOp l g ([TraceLit l s] -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> ([TraceLit l s] -> b) -> [TraceLit l s] -> b Source #
TraceOp l g b => TraceOp l g (TraceLit l s -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (TraceLit l s -> b) -> TraceLit l s -> b Source #
TraceOp l g b => TraceOp l g (Int -> b) Source #
Methods traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> (Int -> b) -> Int -> b Source #

class TraceOutput l g x where Source #

Minimal complete definition

traceOutput

Methods

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

Instances

TraceOutput l g VerifyResult Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> VerifyResult -> String Source #
TraceOutput l g SatResult Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> SatResult -> String Source #
TraceOutput l g () Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> () -> String Source #
TraceOutput l g Int Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> Int -> String Source #
TraceOutput l g x => TraceOutput l g (LitView x) Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> LitView x -> String Source #
TraceOutput l g a => TraceOutput l g [a] Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> [a] -> String Source #
TraceOutput l g (TraceLit l s) Source #
Methods traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> TraceLit l s -> String Source #

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