Copyright	(c) Galois, Inc. 2010
License	BSD3
Maintainer	jhendrix@galois.com
Stability	experimental
Portability	not portable (c2hs, language extensions)
Safe Haskell	Safe
Language	Haskell98

Data.ABC.Internal.ABCGlobal

Contents

Counterexamples

Description

Incomplete. Binding of misc/util/abc_global.h which contains miscellaneous functions for ABC, including a counterexample datastructure and error handling mechanisms.

Synopsis

Counterexamples

data Abc_Cex_t_ Source #

Constructors

Abc_Cex_t_

Fields

iPo'Abc_Cex :: Int
the zero-based number of PO, for which verification failed
iFrame'Abc_Cex :: Int
the zero-based number of the time-frame, for which verificaiton failed
nRegs'Abc_Cex :: Int
the number of registers in the miter
nPis'Abc_Cex :: Int
the number of primary inputs in the miter
nBits'Abc_Cex :: Int
the number of words of bit data used (ezyang: where by words they actually mean bits)
pData'regs'Abc_Cex :: [Bool]
The cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) The format of the data is as such:
- First, the initial values for all registers
- Then, the iFrame+1 sets of inputs, which represent what we inputted into the network at each timestep. For a combinational network, this means there is only 1 set.
pData'inputs'Abc_Cex :: [[Bool]]
outer length: iFrame+1; inner length: nPis

Instances

Eq Abc_Cex_t_ Source #
Methods (==) :: Abc_Cex_t_ -> Abc_Cex_t_ -> Bool # (/=) :: Abc_Cex_t_ -> Abc_Cex_t_ -> Bool #
Read Abc_Cex_t_ Source #
Methods readsPrec :: Int -> ReadS Abc_Cex_t_ # readList :: ReadS [Abc_Cex_t_] # readPrec :: ReadPrec Abc_Cex_t_ # readListPrec :: ReadPrec [Abc_Cex_t_] #
Show Abc_Cex_t_ Source #
Methods showsPrec :: Int -> Abc_Cex_t_ -> ShowS # show :: Abc_Cex_t_ -> String # showList :: [Abc_Cex_t_] -> ShowS #

type Abc_Cex_t = Ptr Abc_Cex_t_ Source #

peekAbcCex :: Abc_Cex_t -> IO Abc_Cex_t_ Source #

Peek into the value of a Abc_Cex_t.