-- GENERATED by C->Haskell Compiler, version 0.20.1 The shapeless maps, 31 Oct 2014 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Data/ABC/Internal/FRAIG.chs" #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}

{- |
Module      : Data.ABC.Internal.FRAIG
Copyright   : Galois, Inc. 2010-2014
License     : BSD3
Maintainer  : jhendrix@galois.com
Stability   : experimental
Portability : non-portable (c2hs, language extensions)

*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.
-}

module Data.ABC.Internal.FRAIG
    ( Prove_Params_t_(..)
    , proveParamsDefault
    ) where

import Control.Applicative
import Control.Monad
import Foreign
import Foreign.C
import qualified System.IO.Unsafe as Unsafe





type Prove_Params_t = Ptr (Prove_Params_t_)
{-# LINE 33 "src/Data/ABC/Internal/FRAIG.chs" #-}


data Prove_Params_t_ = Prove_Params_t_
    {
    -- general parameters
      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

    -- iterations
    , nItersMax'Prove_Params :: Int              -- ^ the number of iterations

    -- mitering
    , nMiteringLimitStart'Prove_Params :: Int    -- ^ starting mitering limit
    , nMiteringLimitMulti'Prove_Params :: Float  -- ^ multiplicative coefficient to increase the limit in each iteration

    -- rewriting
    , nRewritingLimitStart'Prove_Params :: Int   -- ^ the number of rewriting iterations
    , nRewritingLimitMulti'Prove_Params :: Float -- ^ multiplicative coefficient to increase the limit in each iteration

    -- fraiging
    , nFraigingLimitStart'Prove_Params :: Int    -- ^ starting backtrack(conflict) limit
    , nFraigingLimitMulti'Prove_Params :: Float  -- ^ multiplicative coefficient to increase the limit in each iteration

    -- last-gasp BDD construction
    , nBddSizeLimit'Prove_Params :: Int          -- ^ the number of BDD nodes when construction is aborted
    , fBddReorder'Prove_Params :: Bool           -- ^ enables dynamic BDD variable reordering

    -- last-gasp mitering
    , nMiteringLimitLast'Prove_Params :: Int     -- ^ final mitering limit

    -- global SAT solver limits
    , nTotalBacktrackLimit'Prove_Params :: Int64 -- ^ global limit on the number of backtracks
    , nTotalInspectLimit'Prove_Params :: Int64   -- ^ global limit on the number of clause inspects

    -- global resources applied
    , nTotalBacktracksMade'Prove_Params :: Int64 -- ^ the total number of backtracks made
    , nTotalInspectsMade'Prove_Params :: Int64   -- ^ the total number of inspects made
    } deriving (Read, Show, Eq)

instance Storable Prove_Params_t_ where
    sizeOf _ = 88
{-# LINE 75 "src/Data/ABC/Internal/FRAIG.chs" #-}

    alignment _ = 4 -- {#alignment Prove_Params_t #}
    peek p = Prove_Params_t_
        <$> liftM toBool ((\ptr -> do {peekByteOff ptr 0 ::IO CInt}) p)
        <*> liftM toBool ((\ptr -> do {peekByteOff ptr 4 ::IO CInt}) p)
        <*> liftM toBool ((\ptr -> do {peekByteOff ptr 8 ::IO CInt}) p)
        <*> liftM toBool ((\ptr -> do {peekByteOff ptr 12 ::IO CInt}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 16 ::IO CInt}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 20 ::IO CInt}) p)
        <*> liftM realToFrac ((\ptr -> do {peekByteOff ptr 24 ::IO CFloat}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 28 ::IO CInt}) p)
        <*> liftM realToFrac ((\ptr -> do {peekByteOff ptr 32 ::IO CFloat}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 36 ::IO CInt}) p)
        <*> liftM realToFrac ((\ptr -> do {peekByteOff ptr 40 ::IO CFloat}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 44 ::IO CInt}) p)
        <*> liftM toBool ((\ptr -> do {peekByteOff ptr 48 ::IO CInt}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 52 ::IO CInt}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 56 ::IO CLong}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 64 ::IO CLong}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 72 ::IO CLong}) p)
        <*> liftM fromIntegral ((\ptr -> do {peekByteOff ptr 80 ::IO CLong}) p)
    poke p x = do
        (\ptr val -> do {pokeByteOff ptr 0 (val::CInt)})  p (fromBool $ fUseFraiging'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 4 (val::CInt)})  p (fromBool $ fUseRewriting'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 8 (val::CInt)})  p (fromBool $ fUseBdds'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 12 (val::CInt)})  p (fromBool $ fVerbose'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 16 (val::CInt)})  p (fromIntegral $ nItersMax'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 20 (val::CInt)})  p (fromIntegral $ nMiteringLimitStart'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 24 (val::CFloat)})  p (realToFrac $ nMiteringLimitMulti'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 28 (val::CInt)})  p (fromIntegral $ nRewritingLimitStart'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 32 (val::CFloat)})  p (realToFrac $ nRewritingLimitMulti'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 36 (val::CInt)})  p (fromIntegral $ nFraigingLimitStart'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 40 (val::CFloat)})  p (realToFrac $ nFraigingLimitMulti'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 44 (val::CInt)})  p (fromIntegral $ nBddSizeLimit'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 48 (val::CInt)})  p (fromBool $ fBddReorder'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 52 (val::CInt)})  p (fromIntegral $ nMiteringLimitLast'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 56 (val::CLong)})  p (fromIntegral $ nTotalBacktrackLimit'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 64 (val::CLong)})  p (fromIntegral $ nTotalInspectLimit'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 72 (val::CLong)})  p (fromIntegral $ nTotalBacktracksMade'Prove_Params x)
        (\ptr val -> do {pokeByteOff ptr 80 (val::CLong)})  p (fromIntegral $ nTotalInspectsMade'Prove_Params x)

-- fraigMan.c

proveParamsSetDefault :: IO ((Prove_Params_t_))
proveParamsSetDefault =
  alloca $ \a1' -> 
  proveParamsSetDefault'_ a1' >>
  peek  a1'>>= \a1'' -> 
  return (a1'')

{-# LINE 120 "src/Data/ABC/Internal/FRAIG.chs" #-}



-- a more appropriate name in a convenient form
proveParamsDefault :: Prove_Params_t_
proveParamsDefault = Unsafe.unsafePerformIO proveParamsSetDefault

foreign import ccall safe "Data/ABC/Internal/FRAIG.chs.h Prove_ParamsSetDefault"
  proveParamsSetDefault'_ :: ((Prove_Params_t) -> (IO ()))