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

Data.AIG.Interface

Contents

Main interface classes
Helper datatypes
Literal representations
Representations of prover results
QuickCheck generators and testing

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.

Minimal complete definition

aigerNetwork, trueLit, falseLit, newInput, and, inputCount, getInput, writeAiger, writeCNF, checkSat, cec, evaluator, litView, abstractEvaluateAIG

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

Functor LitView
Foldable LitView
Traversable LitView
TraceOutput l g x => TraceOutput l g (LitView x)
Eq a => Eq (LitView a)
Ord a => Ord (LitView a)
Show a => Show (LitView a)

newtype LitTree Source

Constructors

LitTree
Fields unLitTree :: LitView LitTree

Instances

Eq LitTree
Ord LitTree
Show LitTree
Arbitrary LitTree

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

Instances

Eq SatResult
Show SatResult
TraceOutput l g SatResult

data VerifyResult Source

Result of a verification check.

Constructors

Valid
Invalid [Bool]
VerifyUnknown

Instances

Eq VerifyResult
Show VerifyResult
TraceOutput l g VerifyResult

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.