abcBridge-0.14: Bindings for ABC, A System for Sequential Synthesis and Verification

CopyrightGalois, Inc. 2010-2014
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilitynon-portable (c2hs, language extensions)
Safe HaskellNone
LanguageHaskell98

Data.ABC.Internal.FRAIG

Description

  • Incomplete.* Binding of sat/fraig/fraig.h for configuring the process of generating functionally reduced AIGs. Fraiging is the special sauce that makes ABC outperform many vanilla SAT solvers.

Documentation

data Prove_Params_t_ Source

Constructors

Prove_Params_t_ 

Fields

fUseFraiging'Prove_Params :: Bool

enables fraiging

fUseRewriting'Prove_Params :: Bool

enables rewriting

fUseBdds'Prove_Params :: Bool

enables BDD construction when other methods fail

fVerbose'Prove_Params :: Bool

prints verbose stats

nItersMax'Prove_Params :: Int

the number of iterations

nMiteringLimitStart'Prove_Params :: Int

starting mitering limit

nMiteringLimitMulti'Prove_Params :: Float

multiplicative coefficient to increase the limit in each iteration

nRewritingLimitStart'Prove_Params :: Int

the number of rewriting iterations

nRewritingLimitMulti'Prove_Params :: Float

multiplicative coefficient to increase the limit in each iteration

nFraigingLimitStart'Prove_Params :: Int

starting backtrack(conflict) limit

nFraigingLimitMulti'Prove_Params :: Float

multiplicative coefficient to increase the limit in each iteration

nBddSizeLimit'Prove_Params :: Int

the number of BDD nodes when construction is aborted

fBddReorder'Prove_Params :: Bool

enables dynamic BDD variable reordering

nMiteringLimitLast'Prove_Params :: Int

final mitering limit

nTotalBacktrackLimit'Prove_Params :: Int64

global limit on the number of backtracks

nTotalInspectLimit'Prove_Params :: Int64

global limit on the number of clause inspects

nTotalBacktracksMade'Prove_Params :: Int64

the total number of backtracks made

nTotalInspectsMade'Prove_Params :: Int64

the total number of inspects made