Copyright	(c) Galois, Inc. 2010
License	BSD3
Maintainer	jhendrix@galois.com
Stability	experimental
Portability	not portable (c2hs, language extensions)
Safe Haskell	None
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_
Read Abc_Cex_t_
Show Abc_Cex_t_

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.