aig-0.2.6: And-inverter graphs in Haskell.

Copyright(c) Galois Inc. 2014
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

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

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 #

writeAigerWithLatches :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> Int -> 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

Instances

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

writeAigerWithLatches :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> Int -> 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 #

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 #