aig-0.2.3: And-inverter graphs in Haskell.

Copyright(c) Galois, Inc. 2014
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.AIG.Interface

Contents

Description

Interfaces for building, simulating and analysing And-Inverter Graphs (AIG).

Synopsis

Main interface classes

class IsLit l where Source

Methods

not :: l s -> l s Source

Negate a literal.

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

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.

Instances

IsLit l => IsLit (TraceLit l) 

class IsLit l => IsAIG l g | g -> l where Source

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.

Methods

withNewGraph Source

Arguments

:: 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 

Create a temporary graph, and use it to compute a result value.

newGraph :: Proxy l g -> IO (SomeGraph g) Source

Build a new graph instance, and packge it into the SomeGraph type that remembers the IsAIG implementation.

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

Read an AIG from a file, assumed to be in Aiger format

trueLit :: g s -> l s Source

Get unique literal in graph representing constant true.

falseLit :: g s -> l s Source

Get unique literal in graph representing constant false.

constant :: g s -> Bool -> l s Source

Generate a constant literal value

asConstant :: g s -> l s -> Maybe Bool Source

Return if the literal is a fixed constant. If the literal is symbolic, return Nothing.

newInput :: g s -> IO (l s) Source

Generate a fresh input literal

and :: g s -> l s -> l s -> IO (l s) Source

Compute the logical and of two literals

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

Build the conjunction of a list of literals

or :: g s -> l s -> l s -> IO (l s) Source

Compute the logical or of two literals

eq :: g s -> l s -> l s -> IO (l s) Source

Compute the logical equality of two literals

implies :: g s -> l s -> l s -> IO (l s) Source

Compute the logical implication of two literals

xor :: g s -> l s -> l s -> IO (l s) Source

Compute the exclusive or of two literals

mux :: g s -> l s -> l s -> l s -> IO (l s) Source

Perform a mux (if-then-else on the bits).

inputCount :: g s -> IO Int Source

Return number of inputs in the graph.

getInput :: g s -> Int -> IO (l s) Source

Get input at given index in the graph.

writeAiger :: FilePath -> Network l g -> IO () Source

Write network out to AIGER file.

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

Write network out to DIMACS CNF file. Returns vector mapping combinational inputs to CNF Variable numbers.

checkSat :: g s -> l s -> IO SatResult Source

Check if literal is satisfiable in network.

cec :: Network l g -> Network l g -> IO VerifyResult Source

Perform combinational equivalence checking.

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

Evaluate the network on a set of concrete inputs.

evaluate :: Network l g -> [Bool] -> IO [Bool] Source

Evaluate the network on a set of concrete inputs.

litView :: g s -> l s -> IO (LitView (l s)) Source

Examine the outermost structure of a literal to see how it was constructed

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

Build an evaluation function over an AIG using the provided view function

Instances

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

lazyMux :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s) -> IO (l s) Source

Short-cutting mux operator that optimizes the case where the test bit is a concrete literal

Helper datatypes

data Proxy l g where Source

A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.

Constructors

Proxy :: IsAIG l g => (forall a. a -> a) -> Proxy l g 

data SomeGraph g where Source

Some graph quantifies over the state phantom variable for a graph.

Constructors

SomeGraph :: g s -> SomeGraph g 

data Network l g where Source

A network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit.

Constructors

Network :: IsAIG l g => g s -> [l s] -> Network l g 

networkInputCount :: Network l g -> IO Int Source

Get number of inputs associated with current network.

networkOutputCount :: Network l g -> Int Source

Number of outputs associated with a network.

Literal representations

data LitView a Source

Concrete datatype representing the ways an AIG can be constructed.

Constructors

And !a !a 
NotAnd !a !a 
Input !Int 
NotInput !Int 
TrueLit 
FalseLit 

Instances

toLitTree :: IsAIG l g => g s -> l s -> IO LitTree Source

Extract a tree representation of the given literal

fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s) Source

Construct an AIG literal from a tree representation

toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree] Source

Extract a forest representation of the given list of literal s

fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s] Source

Construct a list of AIG literals from a forest representation

foldAIG :: IsAIG l g => g s -> (LitView a -> IO a) -> l s -> IO a Source

Evaluate the given literal using the provided view function

foldAIGs :: IsAIG l g => g s -> (LitView a -> IO a) -> [l s] -> IO [a] Source

Evaluate the given list of literals using the provided view function

unfoldAIG :: IsAIG l g => g s -> (a -> IO (LitView a)) -> a -> IO (l s) Source

Build an AIG literal by unfolding a constructor function

unfoldAIGs :: IsAIG l g => g s -> (a -> IO (LitView a)) -> [a] -> IO [l s] Source

Build a list of AIG literals by unfolding a constructor function

Representations of prover results

data SatResult Source

Satisfiability check result.

Constructors

Unsat 
Sat ![Bool] 
SatUnknown 

data VerifyResult Source

Result of a verification check.

Constructors

Valid 
Invalid [Bool] 
VerifyUnknown 

toSatResult :: VerifyResult -> SatResult Source

Convert a verify result to a sat result by negating it.

toVerifyResult :: SatResult -> VerifyResult Source

Convert a sat result to a verify result by negating it.

QuickCheck generators and testing

genLitView :: Gen a -> Gen (LitView a) Source

Generate an arbitrary LitView given a generator for a

genLitTree :: Gen LitTree Source

Generate an arbitrary LitTree

getMaxInput :: LitTree -> Int Source

Given a LitTree, calculate the maximum input number in the tree. Returns 0 if no inputs are referenced.

buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g) Source

Given a list of LitTree, construct a corresponding AIG network

randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g) Source

Generate a random network by building a random LitTree and using that to construct a network.