-- GENERATED by C->Haskell Compiler, version 0.28.3 Switcheroo, 25 November 2017 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Boolector/Foreign.chs" #-}
{- |

   This module exports a subset of the low-level C Boolector API to Haskell
   code.  In general, you don't want to use this module and should use the
   'Boolector' module instead.

-}
{-# LANGUAGE StandaloneDeriving #-}
module Boolector.Foreign where
import qualified Foreign.C.String as C2HSImp
import qualified Foreign.C.Types as C2HSImp
import qualified Foreign.ForeignPtr as C2HSImp
import qualified Foreign.Marshal.Utils as C2HSImp
import qualified Foreign.Ptr as C2HSImp



import Foreign
import Foreign.C

import Control.Monad


{-# LINE 16 "src/Boolector/Foreign.chs" #-}





--
-- Types
--

-- | Status.
data Status = Unknown
            | Sat
            | Unsat
  deriving (Eq,Ord,Show)
instance Enum Status where
  succ Unknown = Sat
  succ Sat = Unsat
  succ Unsat = error "Status.succ: Unsat has no successor"

  pred Sat = Unknown
  pred Unsat = Sat
  pred Unknown = error "Status.pred: Unknown has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from Unsat

  fromEnum Unknown = 0
  fromEnum Sat = 10
  fromEnum Unsat = 20

  toEnum 0 = Unknown
  toEnum 10 = Sat
  toEnum 20 = Unsat
  toEnum unmatched = error ("Status.toEnum: Cannot match " ++ show unmatched)

{-# LINE 30 "src/Boolector/Foreign.chs" #-}


-- | Boolector instances.
newtype Btor = Btor (C2HSImp.ForeignPtr (Btor))
withBtor :: Btor -> (C2HSImp.Ptr Btor -> IO b) -> IO b
withBtor (Btor fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 33 "src/Boolector/Foreign.chs" #-}

deriving instance Eq Btor
deriving instance Ord Btor

-- | AST node.
newtype Node = Node (C2HSImp.ForeignPtr (Node))
withNode :: Node -> (C2HSImp.Ptr Node -> IO b) -> IO b
withNode (Node fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 38 "src/Boolector/Foreign.chs" #-}

deriving instance Eq Node
deriving instance Ord Node

-- | Sort.
newtype Sort = Sort (C2HSImp.ForeignPtr (Sort))
withSort :: Sort -> (C2HSImp.Ptr Sort -> IO b) -> IO b
withSort (Sort fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 43 "src/Boolector/Foreign.chs" #-}

deriving instance Eq Sort
deriving instance Ord Sort

-- | Solver option.
-- See <https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37>
data Option = OPT_MODEL_GEN
            | OPT_INCREMENTAL
            | OPT_INCREMENTAL_SMT1
            | OPT_INPUT_FORMAT
            | OPT_OUTPUT_NUMBER_FORMAT
            | OPT_OUTPUT_FORMAT
            | OPT_ENGINE
            | OPT_SAT_ENGINE
            | OPT_AUTO_CLEANUP
            | OPT_PRETTY_PRINT
            | OPT_EXIT_CODES
            | OPT_SEED
            | OPT_VERBOSITY
            | OPT_LOGLEVEL
            | OPT_REWRITE_LEVEL
            | OPT_SKELETON_PREPROC
            | OPT_ACKERMANN
            | OPT_BETA_REDUCE_ALL
            | OPT_ELIMINATE_SLICES
            | OPT_VAR_SUBST
            | OPT_UCOPT
            | OPT_MERGE_LAMBDAS
            | OPT_EXTRACT_LAMBDAS
            | OPT_NORMALIZE
            | OPT_NORMALIZE_ADD
            | OPT_FUN_PREPROP
            | OPT_FUN_PRESLS
            | OPT_FUN_DUAL_PROP
            | OPT_FUN_DUAL_PROP_QSORT
            | OPT_FUN_JUST
            | OPT_FUN_JUST_HEURISTIC
            | OPT_FUN_LAZY_SYNTHESIZE
            | OPT_FUN_EAGER_LEMMAS
            | OPT_FUN_STORE_LAMBDAS
            | OPT_SLS_NFLIPS
            | OPT_SLS_STRATEGY
            | OPT_SLS_JUST
            | OPT_SLS_MOVE_GW
            | OPT_SLS_MOVE_RANGE
            | OPT_SLS_MOVE_SEGMENT
            | OPT_SLS_MOVE_RAND_WALK
            | OPT_SLS_PROB_MOVE_RAND_WALK
            | OPT_SLS_MOVE_RAND_ALL
            | OPT_SLS_MOVE_RAND_RANGE
            | OPT_SLS_MOVE_PROP
            | OPT_SLS_MOVE_PROP_N_PROP
            | OPT_SLS_MOVE_PROP_N_SLS
            | OPT_SLS_MOVE_PROP_FORCE_RW
            | OPT_SLS_MOVE_INC_MOVE_TEST
            | OPT_SLS_USE_RESTARTS
            | OPT_SLS_USE_BANDIT
            | OPT_PROP_NPROPS
            | OPT_PROP_USE_RESTARTS
            | OPT_PROP_USE_BANDIT
            | OPT_PROP_PATH_SEL
            | OPT_PROP_PROB_USE_INV_VALUE
            | OPT_PROP_PROB_FLIP_COND
            | OPT_PROP_PROB_FLIP_COND_CONST
            | OPT_PROP_FLIP_COND_CONST_DELTA
            | OPT_PROP_FLIP_COND_CONST_NPATHSEL
            | OPT_PROP_PROB_SLICE_KEEP_DC
            | OPT_PROP_PROB_CONC_FLIP
            | OPT_PROP_PROB_SLICE_FLIP
            | OPT_PROP_PROB_EQ_FLIP
            | OPT_PROP_PROB_AND_FLIP
            | OPT_PROP_NO_MOVE_ON_CONFLICT
            | OPT_AIGPROP_USE_RESTARTS
            | OPT_AIGPROP_USE_BANDIT
            | OPT_QUANT_SYNTH
            | OPT_QUANT_DUAL_SOLVER
            | OPT_QUANT_SYNTH_LIMIT
            | OPT_QUANT_SYNTH_ITE_COMPLETE
            | OPT_QUANT_FIXSYNTH
            | OPT_QUANT_SYNTH_QI
            | OPT_QUANT_DER
            | OPT_QUANT_CER
            | OPT_QUANT_MINISCOPE
            | OPT_DEFAULT_TO_CADICAL
            | OPT_SORT_EXP
            | OPT_SORT_AIG
            | OPT_SORT_AIGVEC
            | OPT_AUTO_CLEANUP_INTERNAL
            | OPT_SIMPLIFY_CONSTRAINTS
            | OPT_CHK_FAILED_ASSUMPTIONS
            | OPT_CHK_MODEL
            | OPT_CHK_UNCONSTRAINED
            | OPT_PARSE_INTERACTIVE
            | OPT_SAT_ENGINE_LGL_FORK
            | OPT_INCREMENTAL_RW
            | OPT_DECLSORT_BV_WIDTH
            | OPT_NUM_OPTS
  deriving (Eq,Ord,Show)
instance Enum Option where
  succ OPT_MODEL_GEN = OPT_INCREMENTAL
  succ OPT_INCREMENTAL = OPT_INCREMENTAL_SMT1
  succ OPT_INCREMENTAL_SMT1 = OPT_INPUT_FORMAT
  succ OPT_INPUT_FORMAT = OPT_OUTPUT_NUMBER_FORMAT
  succ OPT_OUTPUT_NUMBER_FORMAT = OPT_OUTPUT_FORMAT
  succ OPT_OUTPUT_FORMAT = OPT_ENGINE
  succ OPT_ENGINE = OPT_SAT_ENGINE
  succ OPT_SAT_ENGINE = OPT_AUTO_CLEANUP
  succ OPT_AUTO_CLEANUP = OPT_PRETTY_PRINT
  succ OPT_PRETTY_PRINT = OPT_EXIT_CODES
  succ OPT_EXIT_CODES = OPT_SEED
  succ OPT_SEED = OPT_VERBOSITY
  succ OPT_VERBOSITY = OPT_LOGLEVEL
  succ OPT_LOGLEVEL = OPT_REWRITE_LEVEL
  succ OPT_REWRITE_LEVEL = OPT_SKELETON_PREPROC
  succ OPT_SKELETON_PREPROC = OPT_ACKERMANN
  succ OPT_ACKERMANN = OPT_BETA_REDUCE_ALL
  succ OPT_BETA_REDUCE_ALL = OPT_ELIMINATE_SLICES
  succ OPT_ELIMINATE_SLICES = OPT_VAR_SUBST
  succ OPT_VAR_SUBST = OPT_UCOPT
  succ OPT_UCOPT = OPT_MERGE_LAMBDAS
  succ OPT_MERGE_LAMBDAS = OPT_EXTRACT_LAMBDAS
  succ OPT_EXTRACT_LAMBDAS = OPT_NORMALIZE
  succ OPT_NORMALIZE = OPT_NORMALIZE_ADD
  succ OPT_NORMALIZE_ADD = OPT_FUN_PREPROP
  succ OPT_FUN_PREPROP = OPT_FUN_PRESLS
  succ OPT_FUN_PRESLS = OPT_FUN_DUAL_PROP
  succ OPT_FUN_DUAL_PROP = OPT_FUN_DUAL_PROP_QSORT
  succ OPT_FUN_DUAL_PROP_QSORT = OPT_FUN_JUST
  succ OPT_FUN_JUST = OPT_FUN_JUST_HEURISTIC
  succ OPT_FUN_JUST_HEURISTIC = OPT_FUN_LAZY_SYNTHESIZE
  succ OPT_FUN_LAZY_SYNTHESIZE = OPT_FUN_EAGER_LEMMAS
  succ OPT_FUN_EAGER_LEMMAS = OPT_FUN_STORE_LAMBDAS
  succ OPT_FUN_STORE_LAMBDAS = OPT_SLS_NFLIPS
  succ OPT_SLS_NFLIPS = OPT_SLS_STRATEGY
  succ OPT_SLS_STRATEGY = OPT_SLS_JUST
  succ OPT_SLS_JUST = OPT_SLS_MOVE_GW
  succ OPT_SLS_MOVE_GW = OPT_SLS_MOVE_RANGE
  succ OPT_SLS_MOVE_RANGE = OPT_SLS_MOVE_SEGMENT
  succ OPT_SLS_MOVE_SEGMENT = OPT_SLS_MOVE_RAND_WALK
  succ OPT_SLS_MOVE_RAND_WALK = OPT_SLS_PROB_MOVE_RAND_WALK
  succ OPT_SLS_PROB_MOVE_RAND_WALK = OPT_SLS_MOVE_RAND_ALL
  succ OPT_SLS_MOVE_RAND_ALL = OPT_SLS_MOVE_RAND_RANGE
  succ OPT_SLS_MOVE_RAND_RANGE = OPT_SLS_MOVE_PROP
  succ OPT_SLS_MOVE_PROP = OPT_SLS_MOVE_PROP_N_PROP
  succ OPT_SLS_MOVE_PROP_N_PROP = OPT_SLS_MOVE_PROP_N_SLS
  succ OPT_SLS_MOVE_PROP_N_SLS = OPT_SLS_MOVE_PROP_FORCE_RW
  succ OPT_SLS_MOVE_PROP_FORCE_RW = OPT_SLS_MOVE_INC_MOVE_TEST
  succ OPT_SLS_MOVE_INC_MOVE_TEST = OPT_SLS_USE_RESTARTS
  succ OPT_SLS_USE_RESTARTS = OPT_SLS_USE_BANDIT
  succ OPT_SLS_USE_BANDIT = OPT_PROP_NPROPS
  succ OPT_PROP_NPROPS = OPT_PROP_USE_RESTARTS
  succ OPT_PROP_USE_RESTARTS = OPT_PROP_USE_BANDIT
  succ OPT_PROP_USE_BANDIT = OPT_PROP_PATH_SEL
  succ OPT_PROP_PATH_SEL = OPT_PROP_PROB_USE_INV_VALUE
  succ OPT_PROP_PROB_USE_INV_VALUE = OPT_PROP_PROB_FLIP_COND
  succ OPT_PROP_PROB_FLIP_COND = OPT_PROP_PROB_FLIP_COND_CONST
  succ OPT_PROP_PROB_FLIP_COND_CONST = OPT_PROP_FLIP_COND_CONST_DELTA
  succ OPT_PROP_FLIP_COND_CONST_DELTA = OPT_PROP_FLIP_COND_CONST_NPATHSEL
  succ OPT_PROP_FLIP_COND_CONST_NPATHSEL = OPT_PROP_PROB_SLICE_KEEP_DC
  succ OPT_PROP_PROB_SLICE_KEEP_DC = OPT_PROP_PROB_CONC_FLIP
  succ OPT_PROP_PROB_CONC_FLIP = OPT_PROP_PROB_SLICE_FLIP
  succ OPT_PROP_PROB_SLICE_FLIP = OPT_PROP_PROB_EQ_FLIP
  succ OPT_PROP_PROB_EQ_FLIP = OPT_PROP_PROB_AND_FLIP
  succ OPT_PROP_PROB_AND_FLIP = OPT_PROP_NO_MOVE_ON_CONFLICT
  succ OPT_PROP_NO_MOVE_ON_CONFLICT = OPT_AIGPROP_USE_RESTARTS
  succ OPT_AIGPROP_USE_RESTARTS = OPT_AIGPROP_USE_BANDIT
  succ OPT_AIGPROP_USE_BANDIT = OPT_QUANT_SYNTH
  succ OPT_QUANT_SYNTH = OPT_QUANT_DUAL_SOLVER
  succ OPT_QUANT_DUAL_SOLVER = OPT_QUANT_SYNTH_LIMIT
  succ OPT_QUANT_SYNTH_LIMIT = OPT_QUANT_SYNTH_ITE_COMPLETE
  succ OPT_QUANT_SYNTH_ITE_COMPLETE = OPT_QUANT_FIXSYNTH
  succ OPT_QUANT_FIXSYNTH = OPT_QUANT_SYNTH_QI
  succ OPT_QUANT_SYNTH_QI = OPT_QUANT_DER
  succ OPT_QUANT_DER = OPT_QUANT_CER
  succ OPT_QUANT_CER = OPT_QUANT_MINISCOPE
  succ OPT_QUANT_MINISCOPE = OPT_DEFAULT_TO_CADICAL
  succ OPT_DEFAULT_TO_CADICAL = OPT_SORT_EXP
  succ OPT_SORT_EXP = OPT_SORT_AIG
  succ OPT_SORT_AIG = OPT_SORT_AIGVEC
  succ OPT_SORT_AIGVEC = OPT_AUTO_CLEANUP_INTERNAL
  succ OPT_AUTO_CLEANUP_INTERNAL = OPT_SIMPLIFY_CONSTRAINTS
  succ OPT_SIMPLIFY_CONSTRAINTS = OPT_CHK_FAILED_ASSUMPTIONS
  succ OPT_CHK_FAILED_ASSUMPTIONS = OPT_CHK_MODEL
  succ OPT_CHK_MODEL = OPT_CHK_UNCONSTRAINED
  succ OPT_CHK_UNCONSTRAINED = OPT_PARSE_INTERACTIVE
  succ OPT_PARSE_INTERACTIVE = OPT_SAT_ENGINE_LGL_FORK
  succ OPT_SAT_ENGINE_LGL_FORK = OPT_INCREMENTAL_RW
  succ OPT_INCREMENTAL_RW = OPT_DECLSORT_BV_WIDTH
  succ OPT_DECLSORT_BV_WIDTH = OPT_NUM_OPTS
  succ OPT_NUM_OPTS = error "Option.succ: OPT_NUM_OPTS has no successor"

  pred OPT_INCREMENTAL = OPT_MODEL_GEN
  pred OPT_INCREMENTAL_SMT1 = OPT_INCREMENTAL
  pred OPT_INPUT_FORMAT = OPT_INCREMENTAL_SMT1
  pred OPT_OUTPUT_NUMBER_FORMAT = OPT_INPUT_FORMAT
  pred OPT_OUTPUT_FORMAT = OPT_OUTPUT_NUMBER_FORMAT
  pred OPT_ENGINE = OPT_OUTPUT_FORMAT
  pred OPT_SAT_ENGINE = OPT_ENGINE
  pred OPT_AUTO_CLEANUP = OPT_SAT_ENGINE
  pred OPT_PRETTY_PRINT = OPT_AUTO_CLEANUP
  pred OPT_EXIT_CODES = OPT_PRETTY_PRINT
  pred OPT_SEED = OPT_EXIT_CODES
  pred OPT_VERBOSITY = OPT_SEED
  pred OPT_LOGLEVEL = OPT_VERBOSITY
  pred OPT_REWRITE_LEVEL = OPT_LOGLEVEL
  pred OPT_SKELETON_PREPROC = OPT_REWRITE_LEVEL
  pred OPT_ACKERMANN = OPT_SKELETON_PREPROC
  pred OPT_BETA_REDUCE_ALL = OPT_ACKERMANN
  pred OPT_ELIMINATE_SLICES = OPT_BETA_REDUCE_ALL
  pred OPT_VAR_SUBST = OPT_ELIMINATE_SLICES
  pred OPT_UCOPT = OPT_VAR_SUBST
  pred OPT_MERGE_LAMBDAS = OPT_UCOPT
  pred OPT_EXTRACT_LAMBDAS = OPT_MERGE_LAMBDAS
  pred OPT_NORMALIZE = OPT_EXTRACT_LAMBDAS
  pred OPT_NORMALIZE_ADD = OPT_NORMALIZE
  pred OPT_FUN_PREPROP = OPT_NORMALIZE_ADD
  pred OPT_FUN_PRESLS = OPT_FUN_PREPROP
  pred OPT_FUN_DUAL_PROP = OPT_FUN_PRESLS
  pred OPT_FUN_DUAL_PROP_QSORT = OPT_FUN_DUAL_PROP
  pred OPT_FUN_JUST = OPT_FUN_DUAL_PROP_QSORT
  pred OPT_FUN_JUST_HEURISTIC = OPT_FUN_JUST
  pred OPT_FUN_LAZY_SYNTHESIZE = OPT_FUN_JUST_HEURISTIC
  pred OPT_FUN_EAGER_LEMMAS = OPT_FUN_LAZY_SYNTHESIZE
  pred OPT_FUN_STORE_LAMBDAS = OPT_FUN_EAGER_LEMMAS
  pred OPT_SLS_NFLIPS = OPT_FUN_STORE_LAMBDAS
  pred OPT_SLS_STRATEGY = OPT_SLS_NFLIPS
  pred OPT_SLS_JUST = OPT_SLS_STRATEGY
  pred OPT_SLS_MOVE_GW = OPT_SLS_JUST
  pred OPT_SLS_MOVE_RANGE = OPT_SLS_MOVE_GW
  pred OPT_SLS_MOVE_SEGMENT = OPT_SLS_MOVE_RANGE
  pred OPT_SLS_MOVE_RAND_WALK = OPT_SLS_MOVE_SEGMENT
  pred OPT_SLS_PROB_MOVE_RAND_WALK = OPT_SLS_MOVE_RAND_WALK
  pred OPT_SLS_MOVE_RAND_ALL = OPT_SLS_PROB_MOVE_RAND_WALK
  pred OPT_SLS_MOVE_RAND_RANGE = OPT_SLS_MOVE_RAND_ALL
  pred OPT_SLS_MOVE_PROP = OPT_SLS_MOVE_RAND_RANGE
  pred OPT_SLS_MOVE_PROP_N_PROP = OPT_SLS_MOVE_PROP
  pred OPT_SLS_MOVE_PROP_N_SLS = OPT_SLS_MOVE_PROP_N_PROP
  pred OPT_SLS_MOVE_PROP_FORCE_RW = OPT_SLS_MOVE_PROP_N_SLS
  pred OPT_SLS_MOVE_INC_MOVE_TEST = OPT_SLS_MOVE_PROP_FORCE_RW
  pred OPT_SLS_USE_RESTARTS = OPT_SLS_MOVE_INC_MOVE_TEST
  pred OPT_SLS_USE_BANDIT = OPT_SLS_USE_RESTARTS
  pred OPT_PROP_NPROPS = OPT_SLS_USE_BANDIT
  pred OPT_PROP_USE_RESTARTS = OPT_PROP_NPROPS
  pred OPT_PROP_USE_BANDIT = OPT_PROP_USE_RESTARTS
  pred OPT_PROP_PATH_SEL = OPT_PROP_USE_BANDIT
  pred OPT_PROP_PROB_USE_INV_VALUE = OPT_PROP_PATH_SEL
  pred OPT_PROP_PROB_FLIP_COND = OPT_PROP_PROB_USE_INV_VALUE
  pred OPT_PROP_PROB_FLIP_COND_CONST = OPT_PROP_PROB_FLIP_COND
  pred OPT_PROP_FLIP_COND_CONST_DELTA = OPT_PROP_PROB_FLIP_COND_CONST
  pred OPT_PROP_FLIP_COND_CONST_NPATHSEL = OPT_PROP_FLIP_COND_CONST_DELTA
  pred OPT_PROP_PROB_SLICE_KEEP_DC = OPT_PROP_FLIP_COND_CONST_NPATHSEL
  pred OPT_PROP_PROB_CONC_FLIP = OPT_PROP_PROB_SLICE_KEEP_DC
  pred OPT_PROP_PROB_SLICE_FLIP = OPT_PROP_PROB_CONC_FLIP
  pred OPT_PROP_PROB_EQ_FLIP = OPT_PROP_PROB_SLICE_FLIP
  pred OPT_PROP_PROB_AND_FLIP = OPT_PROP_PROB_EQ_FLIP
  pred OPT_PROP_NO_MOVE_ON_CONFLICT = OPT_PROP_PROB_AND_FLIP
  pred OPT_AIGPROP_USE_RESTARTS = OPT_PROP_NO_MOVE_ON_CONFLICT
  pred OPT_AIGPROP_USE_BANDIT = OPT_AIGPROP_USE_RESTARTS
  pred OPT_QUANT_SYNTH = OPT_AIGPROP_USE_BANDIT
  pred OPT_QUANT_DUAL_SOLVER = OPT_QUANT_SYNTH
  pred OPT_QUANT_SYNTH_LIMIT = OPT_QUANT_DUAL_SOLVER
  pred OPT_QUANT_SYNTH_ITE_COMPLETE = OPT_QUANT_SYNTH_LIMIT
  pred OPT_QUANT_FIXSYNTH = OPT_QUANT_SYNTH_ITE_COMPLETE
  pred OPT_QUANT_SYNTH_QI = OPT_QUANT_FIXSYNTH
  pred OPT_QUANT_DER = OPT_QUANT_SYNTH_QI
  pred OPT_QUANT_CER = OPT_QUANT_DER
  pred OPT_QUANT_MINISCOPE = OPT_QUANT_CER
  pred OPT_DEFAULT_TO_CADICAL = OPT_QUANT_MINISCOPE
  pred OPT_SORT_EXP = OPT_DEFAULT_TO_CADICAL
  pred OPT_SORT_AIG = OPT_SORT_EXP
  pred OPT_SORT_AIGVEC = OPT_SORT_AIG
  pred OPT_AUTO_CLEANUP_INTERNAL = OPT_SORT_AIGVEC
  pred OPT_SIMPLIFY_CONSTRAINTS = OPT_AUTO_CLEANUP_INTERNAL
  pred OPT_CHK_FAILED_ASSUMPTIONS = OPT_SIMPLIFY_CONSTRAINTS
  pred OPT_CHK_MODEL = OPT_CHK_FAILED_ASSUMPTIONS
  pred OPT_CHK_UNCONSTRAINED = OPT_CHK_MODEL
  pred OPT_PARSE_INTERACTIVE = OPT_CHK_UNCONSTRAINED
  pred OPT_SAT_ENGINE_LGL_FORK = OPT_PARSE_INTERACTIVE
  pred OPT_INCREMENTAL_RW = OPT_SAT_ENGINE_LGL_FORK
  pred OPT_DECLSORT_BV_WIDTH = OPT_INCREMENTAL_RW
  pred OPT_NUM_OPTS = OPT_DECLSORT_BV_WIDTH
  pred OPT_MODEL_GEN = error "Option.pred: OPT_MODEL_GEN has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from OPT_NUM_OPTS

  fromEnum OPT_MODEL_GEN = 0
  fromEnum OPT_INCREMENTAL = 1
  fromEnum OPT_INCREMENTAL_SMT1 = 2
  fromEnum OPT_INPUT_FORMAT = 3
  fromEnum OPT_OUTPUT_NUMBER_FORMAT = 4
  fromEnum OPT_OUTPUT_FORMAT = 5
  fromEnum OPT_ENGINE = 6
  fromEnum OPT_SAT_ENGINE = 7
  fromEnum OPT_AUTO_CLEANUP = 8
  fromEnum OPT_PRETTY_PRINT = 9
  fromEnum OPT_EXIT_CODES = 10
  fromEnum OPT_SEED = 11
  fromEnum OPT_VERBOSITY = 12
  fromEnum OPT_LOGLEVEL = 13
  fromEnum OPT_REWRITE_LEVEL = 14
  fromEnum OPT_SKELETON_PREPROC = 15
  fromEnum OPT_ACKERMANN = 16
  fromEnum OPT_BETA_REDUCE_ALL = 17
  fromEnum OPT_ELIMINATE_SLICES = 18
  fromEnum OPT_VAR_SUBST = 19
  fromEnum OPT_UCOPT = 20
  fromEnum OPT_MERGE_LAMBDAS = 21
  fromEnum OPT_EXTRACT_LAMBDAS = 22
  fromEnum OPT_NORMALIZE = 23
  fromEnum OPT_NORMALIZE_ADD = 24
  fromEnum OPT_FUN_PREPROP = 25
  fromEnum OPT_FUN_PRESLS = 26
  fromEnum OPT_FUN_DUAL_PROP = 27
  fromEnum OPT_FUN_DUAL_PROP_QSORT = 28
  fromEnum OPT_FUN_JUST = 29
  fromEnum OPT_FUN_JUST_HEURISTIC = 30
  fromEnum OPT_FUN_LAZY_SYNTHESIZE = 31
  fromEnum OPT_FUN_EAGER_LEMMAS = 32
  fromEnum OPT_FUN_STORE_LAMBDAS = 33
  fromEnum OPT_SLS_NFLIPS = 34
  fromEnum OPT_SLS_STRATEGY = 35
  fromEnum OPT_SLS_JUST = 36
  fromEnum OPT_SLS_MOVE_GW = 37
  fromEnum OPT_SLS_MOVE_RANGE = 38
  fromEnum OPT_SLS_MOVE_SEGMENT = 39
  fromEnum OPT_SLS_MOVE_RAND_WALK = 40
  fromEnum OPT_SLS_PROB_MOVE_RAND_WALK = 41
  fromEnum OPT_SLS_MOVE_RAND_ALL = 42
  fromEnum OPT_SLS_MOVE_RAND_RANGE = 43
  fromEnum OPT_SLS_MOVE_PROP = 44
  fromEnum OPT_SLS_MOVE_PROP_N_PROP = 45
  fromEnum OPT_SLS_MOVE_PROP_N_SLS = 46
  fromEnum OPT_SLS_MOVE_PROP_FORCE_RW = 47
  fromEnum OPT_SLS_MOVE_INC_MOVE_TEST = 48
  fromEnum OPT_SLS_USE_RESTARTS = 49
  fromEnum OPT_SLS_USE_BANDIT = 50
  fromEnum OPT_PROP_NPROPS = 51
  fromEnum OPT_PROP_USE_RESTARTS = 52
  fromEnum OPT_PROP_USE_BANDIT = 53
  fromEnum OPT_PROP_PATH_SEL = 54
  fromEnum OPT_PROP_PROB_USE_INV_VALUE = 55
  fromEnum OPT_PROP_PROB_FLIP_COND = 56
  fromEnum OPT_PROP_PROB_FLIP_COND_CONST = 57
  fromEnum OPT_PROP_FLIP_COND_CONST_DELTA = 58
  fromEnum OPT_PROP_FLIP_COND_CONST_NPATHSEL = 59
  fromEnum OPT_PROP_PROB_SLICE_KEEP_DC = 60
  fromEnum OPT_PROP_PROB_CONC_FLIP = 61
  fromEnum OPT_PROP_PROB_SLICE_FLIP = 62
  fromEnum OPT_PROP_PROB_EQ_FLIP = 63
  fromEnum OPT_PROP_PROB_AND_FLIP = 64
  fromEnum OPT_PROP_NO_MOVE_ON_CONFLICT = 65
  fromEnum OPT_AIGPROP_USE_RESTARTS = 66
  fromEnum OPT_AIGPROP_USE_BANDIT = 67
  fromEnum OPT_QUANT_SYNTH = 68
  fromEnum OPT_QUANT_DUAL_SOLVER = 69
  fromEnum OPT_QUANT_SYNTH_LIMIT = 70
  fromEnum OPT_QUANT_SYNTH_ITE_COMPLETE = 71
  fromEnum OPT_QUANT_FIXSYNTH = 72
  fromEnum OPT_QUANT_SYNTH_QI = 73
  fromEnum OPT_QUANT_DER = 74
  fromEnum OPT_QUANT_CER = 75
  fromEnum OPT_QUANT_MINISCOPE = 76
  fromEnum OPT_DEFAULT_TO_CADICAL = 77
  fromEnum OPT_SORT_EXP = 78
  fromEnum OPT_SORT_AIG = 79
  fromEnum OPT_SORT_AIGVEC = 80
  fromEnum OPT_AUTO_CLEANUP_INTERNAL = 81
  fromEnum OPT_SIMPLIFY_CONSTRAINTS = 82
  fromEnum OPT_CHK_FAILED_ASSUMPTIONS = 83
  fromEnum OPT_CHK_MODEL = 84
  fromEnum OPT_CHK_UNCONSTRAINED = 85
  fromEnum OPT_PARSE_INTERACTIVE = 86
  fromEnum OPT_SAT_ENGINE_LGL_FORK = 87
  fromEnum OPT_INCREMENTAL_RW = 88
  fromEnum OPT_DECLSORT_BV_WIDTH = 89
  fromEnum OPT_NUM_OPTS = 90

  toEnum 0 = OPT_MODEL_GEN
  toEnum 1 = OPT_INCREMENTAL
  toEnum 2 = OPT_INCREMENTAL_SMT1
  toEnum 3 = OPT_INPUT_FORMAT
  toEnum 4 = OPT_OUTPUT_NUMBER_FORMAT
  toEnum 5 = OPT_OUTPUT_FORMAT
  toEnum 6 = OPT_ENGINE
  toEnum 7 = OPT_SAT_ENGINE
  toEnum 8 = OPT_AUTO_CLEANUP
  toEnum 9 = OPT_PRETTY_PRINT
  toEnum 10 = OPT_EXIT_CODES
  toEnum 11 = OPT_SEED
  toEnum 12 = OPT_VERBOSITY
  toEnum 13 = OPT_LOGLEVEL
  toEnum 14 = OPT_REWRITE_LEVEL
  toEnum 15 = OPT_SKELETON_PREPROC
  toEnum 16 = OPT_ACKERMANN
  toEnum 17 = OPT_BETA_REDUCE_ALL
  toEnum 18 = OPT_ELIMINATE_SLICES
  toEnum 19 = OPT_VAR_SUBST
  toEnum 20 = OPT_UCOPT
  toEnum 21 = OPT_MERGE_LAMBDAS
  toEnum 22 = OPT_EXTRACT_LAMBDAS
  toEnum 23 = OPT_NORMALIZE
  toEnum 24 = OPT_NORMALIZE_ADD
  toEnum 25 = OPT_FUN_PREPROP
  toEnum 26 = OPT_FUN_PRESLS
  toEnum 27 = OPT_FUN_DUAL_PROP
  toEnum 28 = OPT_FUN_DUAL_PROP_QSORT
  toEnum 29 = OPT_FUN_JUST
  toEnum 30 = OPT_FUN_JUST_HEURISTIC
  toEnum 31 = OPT_FUN_LAZY_SYNTHESIZE
  toEnum 32 = OPT_FUN_EAGER_LEMMAS
  toEnum 33 = OPT_FUN_STORE_LAMBDAS
  toEnum 34 = OPT_SLS_NFLIPS
  toEnum 35 = OPT_SLS_STRATEGY
  toEnum 36 = OPT_SLS_JUST
  toEnum 37 = OPT_SLS_MOVE_GW
  toEnum 38 = OPT_SLS_MOVE_RANGE
  toEnum 39 = OPT_SLS_MOVE_SEGMENT
  toEnum 40 = OPT_SLS_MOVE_RAND_WALK
  toEnum 41 = OPT_SLS_PROB_MOVE_RAND_WALK
  toEnum 42 = OPT_SLS_MOVE_RAND_ALL
  toEnum 43 = OPT_SLS_MOVE_RAND_RANGE
  toEnum 44 = OPT_SLS_MOVE_PROP
  toEnum 45 = OPT_SLS_MOVE_PROP_N_PROP
  toEnum 46 = OPT_SLS_MOVE_PROP_N_SLS
  toEnum 47 = OPT_SLS_MOVE_PROP_FORCE_RW
  toEnum 48 = OPT_SLS_MOVE_INC_MOVE_TEST
  toEnum 49 = OPT_SLS_USE_RESTARTS
  toEnum 50 = OPT_SLS_USE_BANDIT
  toEnum 51 = OPT_PROP_NPROPS
  toEnum 52 = OPT_PROP_USE_RESTARTS
  toEnum 53 = OPT_PROP_USE_BANDIT
  toEnum 54 = OPT_PROP_PATH_SEL
  toEnum 55 = OPT_PROP_PROB_USE_INV_VALUE
  toEnum 56 = OPT_PROP_PROB_FLIP_COND
  toEnum 57 = OPT_PROP_PROB_FLIP_COND_CONST
  toEnum 58 = OPT_PROP_FLIP_COND_CONST_DELTA
  toEnum 59 = OPT_PROP_FLIP_COND_CONST_NPATHSEL
  toEnum 60 = OPT_PROP_PROB_SLICE_KEEP_DC
  toEnum 61 = OPT_PROP_PROB_CONC_FLIP
  toEnum 62 = OPT_PROP_PROB_SLICE_FLIP
  toEnum 63 = OPT_PROP_PROB_EQ_FLIP
  toEnum 64 = OPT_PROP_PROB_AND_FLIP
  toEnum 65 = OPT_PROP_NO_MOVE_ON_CONFLICT
  toEnum 66 = OPT_AIGPROP_USE_RESTARTS
  toEnum 67 = OPT_AIGPROP_USE_BANDIT
  toEnum 68 = OPT_QUANT_SYNTH
  toEnum 69 = OPT_QUANT_DUAL_SOLVER
  toEnum 70 = OPT_QUANT_SYNTH_LIMIT
  toEnum 71 = OPT_QUANT_SYNTH_ITE_COMPLETE
  toEnum 72 = OPT_QUANT_FIXSYNTH
  toEnum 73 = OPT_QUANT_SYNTH_QI
  toEnum 74 = OPT_QUANT_DER
  toEnum 75 = OPT_QUANT_CER
  toEnum 76 = OPT_QUANT_MINISCOPE
  toEnum 77 = OPT_DEFAULT_TO_CADICAL
  toEnum 78 = OPT_SORT_EXP
  toEnum 79 = OPT_SORT_AIG
  toEnum 80 = OPT_SORT_AIGVEC
  toEnum 81 = OPT_AUTO_CLEANUP_INTERNAL
  toEnum 82 = OPT_SIMPLIFY_CONSTRAINTS
  toEnum 83 = OPT_CHK_FAILED_ASSUMPTIONS
  toEnum 84 = OPT_CHK_MODEL
  toEnum 85 = OPT_CHK_UNCONSTRAINED
  toEnum 86 = OPT_PARSE_INTERACTIVE
  toEnum 87 = OPT_SAT_ENGINE_LGL_FORK
  toEnum 88 = OPT_INCREMENTAL_RW
  toEnum 89 = OPT_DECLSORT_BV_WIDTH
  toEnum 90 = OPT_NUM_OPTS
  toEnum unmatched = error ("Option.toEnum: Cannot match " ++ show unmatched)

{-# LINE 141 "src/Boolector/Foreign.chs" #-}



--
--  Solver-level interface
--

-- | Create a new instance of Boolector.
new :: IO (Btor)
new = do
 ptrBtor <- new'_ 
 -- run delete on the btor at the end
 foreignPtrBtor <- newForeignPtr boolector_delete ptrBtor
 -- run release_all before delete
 addForeignPtrFinalizer boolector_release_all foreignPtrBtor 
 return $ Btor foreignPtrBtor

foreign import ccall "boolector_new"
  new'_ :: IO (Ptr Btor)

foreign import ccall "&boolector_delete"
  boolector_delete :: FinalizerPtr Btor

foreign import ccall "&boolector_release_all"
  boolector_release_all :: FinalizerPtr Btor

-- | Push new context levels.
push :: (Btor) -> (CUInt) -> IO ()
push a1 a2 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  push'_ a1' a2' >>
  return ()

{-# LINE 168 "src/Boolector/Foreign.chs" #-}


-- | Pop context levels.
pop :: (Btor) -> (CUInt) -> IO ()
pop a1 a2 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  pop'_ a1' a2' >>
  return ()

{-# LINE 171 "src/Boolector/Foreign.chs" #-}


-- | Set a termination callback.
setTerm :: Btor -> (Ptr () -> IO Int) -> IO ()
setTerm b callback = do
  cb <- makeWrapper callback
  withBtor b $ \ b' -> setTerm'_ b' cb nullPtr

foreign import ccall "wrapper"
  makeWrapper :: (Ptr () -> IO Int) -> IO (FunPtr (Ptr () -> IO Int))

foreign import ccall "boolector_set_term"
  setTerm'_ :: Ptr Btor -> (FunPtr (Ptr () -> IO Int)) -> Ptr () -> IO ()

--
-- Options
--

-- | Set the SAT solver to use.
--
-- Currently supported: @Lingeling@, @PicoSAT@, and @MiniSAT@.
-- Returns non-zero value if setting the SAT solver was successful.
setSatSolver :: (Btor) -> (String) -> IO ()
setSatSolver a1 a2 =
  (withBtor) a1 $ \a1' -> 
  C2HSImp.withCString a2 $ \a2' -> 
  setSatSolver'_ a1' a2' >>
  return ()

{-# LINE 193 "src/Boolector/Foreign.chs" #-}


-- | Set option. See btortypes.h
setOpt :: (Btor) -> (Option) -> (CUInt) -> IO ()
setOpt a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = (fromIntegral . fromEnum) a2} in 
  let {a3' = fromIntegral a3} in 
  setOpt'_ a1' a2' a3' >>
  return ()

{-# LINE 196 "src/Boolector/Foreign.chs" #-}


-- | Get the current value of an option.
getOpt :: (Btor) -> (Option) -> IO ((CUInt))
getOpt a1 a2 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = (fromIntegral . fromEnum) a2} in 
  getOpt'_ a1' a2' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

{-# LINE 199 "src/Boolector/Foreign.chs" #-}


-- | Check if Boolector has a given option.
hasOpt :: (Btor) -> (Option) -> IO ((Bool))
hasOpt a1 a2 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = (fromIntegral . fromEnum) a2} in 
  hasOpt'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 202 "src/Boolector/Foreign.chs" #-}


--
-- Solving
--

-- | Add a constraint.
assert :: (Btor) -> (Node) -> IO ()
assert a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  assert'_ a1' a2' >>
  return ()

{-# LINE 209 "src/Boolector/Foreign.chs" #-}


-- | Add an assumption.
assume :: (Btor) -> (Node) -> IO ()
assume a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  assume'_ a1' a2' >>
  return ()

{-# LINE 212 "src/Boolector/Foreign.chs" #-}


-- | Determine if assumption @node@ is a failed assumption.
--
-- Failed assumptions are those assumptions, that force an input formula
-- to become unsatisfiable.
failed :: (Btor) -> (Node) -> IO ((Bool))
failed a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  failed'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 218 "src/Boolector/Foreign.chs" #-}


-- | Add all assumptions as assertions.
fixateAssumptions :: (Btor) -> IO ()
fixateAssumptions a1 =
  (withBtor) a1 $ \a1' -> 
  fixateAssumptions'_ a1' >>
  return ()

{-# LINE 221 "src/Boolector/Foreign.chs" #-}


-- | Resets all added assumptions.
resetAssumptions :: (Btor) -> IO ()
resetAssumptions a1 =
  (withBtor) a1 $ \a1' -> 
  resetAssumptions'_ a1' >>
  return ()

{-# LINE 224 "src/Boolector/Foreign.chs" #-}


-- | Solve an input formula.
--
-- An input formula is defined by constraints added via 'assert'.
-- You can guide the search for a solution to an input formula by making
-- assumptions via 'assume'.
sat :: (Btor) -> IO ((Status))
sat a1 =
  (withBtor) a1 $ \a1' -> 
  sat'_ a1' >>= \res ->
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

{-# LINE 231 "src/Boolector/Foreign.chs" #-}


-- | Solve an input formula and limit the search by the number of lemmas
-- generated and the number of conflicts encountered by the underlying
-- SAT solver.
--
-- An input formula is defined by constraints added via 'assert'.
-- You can guide the search for a solution to an input formula by making
-- assumptions via 'assume'.
--
-- Returns 'Sat' if the input formula is satisfiable (under possibly given
-- assumptions), 'Usat' if the instance is unsatisfiable, and 'Unknown' if the
-- instance could not be solved within given limits.
limitedSat :: (Btor) -> (Int) -> (Int) -> IO ((Status))
limitedSat a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  let {a3' = fromIntegral a3} in 
  limitedSat'_ a1' a2' a3' >>= \res ->
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

{-# LINE 244 "src/Boolector/Foreign.chs" #-}


-- | Simplify current input formula.
simplify :: (Btor) -> IO ((Status))
simplify a1 =
  (withBtor) a1 $ \a1' -> 
  simplify'_ a1' >>= \res ->
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

{-# LINE 247 "src/Boolector/Foreign.chs" #-}


--
-- Expressions
--

-- | Copy expression (increments reference counter).
copy :: (Btor) -> (Node) -> IO ((Node))
copy a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  copy'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 254 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant representing the bit vector @bits@.
const :: (Btor) -> (String) -> IO ((Node))
const a1 a2 =
  (withBtor) a1 $ \a1' -> 
  C2HSImp.withCString a2 $ \a2' -> 
  const'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 257 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant representing the decimal number @str@.
constd :: (Btor) -> (Sort) -> (String) -> IO ((Node))
constd a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  constd'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 260 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant representing the hexadecimal number @str@.
consth :: (Btor) -> (Sort) -> (String) -> IO ((Node))
consth a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  consth'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 263 "src/Boolector/Foreign.chs" #-}


-- | Create constant true. This is represented by the bit vector constant one
-- with bit width one.
true :: (Btor) -> IO ((Node))
true a1 =
  (withBtor) a1 $ \a1' -> 
  true'_ a1' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 267 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant zero with bit width one.
false :: (Btor) -> IO ((Node))
false a1 =
  (withBtor) a1 $ \a1' -> 
  false'_ a1' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 270 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant zero of sort @sort@.
zero :: (Btor) -> (Sort) -> IO ((Node))
zero a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  zero'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 273 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant one of sort @sort@.
one :: (Btor) -> (Sort) -> IO ((Node))
one a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  one'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 276 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant of sort @sort@, where each bit is set to one.
ones :: (Btor) -> (Sort) -> IO ((Node))
ones a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  ones'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 279 "src/Boolector/Foreign.chs" #-}


-- |  Create bit vector constant representing the unsigned integer @u@ of
-- sort @sort@.
--
-- The constant is obtained by either truncating bits or by
-- unsigned extension (padding with zeroes).
unsignedInt :: (Btor) -> (CUInt) -> (Sort) -> IO ((Node))
unsignedInt a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  (withSort) a3 $ \a3' -> 
  unsignedInt'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 286 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector constant representing the signed integer @i@ of sort
-- @sort@.
--
-- The constant is obtained by either truncating bits or by
-- signed extension (padding with ones).
int :: (Btor) -> (CInt) -> (Sort) -> IO ((Node))
int a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  (withSort) a3 $ \a3' -> 
  int'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 293 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector variable of sort @sort@.
--
-- The name must be unique.
var :: (Btor) -> (Sort) -> (String) -> IO ((Node))
var a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  var'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 298 "src/Boolector/Foreign.chs" #-}


-- | Create the one's complement of bit vector @node@.
not :: (Btor) -> (Node) -> IO ((Node))
not a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  not'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 301 "src/Boolector/Foreign.chs" #-}


-- | Create the two's complement of bit vector @node@.
neg :: (Btor) -> (Node) -> IO ((Node))
neg a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  neg'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 304 "src/Boolector/Foreign.chs" #-}


-- | Create *or* reduction of node @node@.
--
-- All bits of node @node@ are combined by a Boolean *or*.
redor :: (Btor) -> (Node) -> IO ((Node))
redor a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  redor'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 309 "src/Boolector/Foreign.chs" #-}


-- | Create *xor* reduction of node @node@.
--
-- All bits of @node@ are combined by a Boolean *xor*.
redxor :: (Btor) -> (Node) -> IO ((Node))
redxor a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  redxor'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 314 "src/Boolector/Foreign.chs" #-}


-- | Create *and* reduction of node @node@.
--
-- All bits of @node@ are combined by a Boolean *and*.
redand :: (Btor) -> (Node) -> IO ((Node))
redand a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  redand'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 319 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector slice of @node@ from index @upper@ to index @lower@.
slice :: (Btor) -> (Node) -> (CUInt) -> (CUInt) -> IO ((Node))
slice a1 a2 a3 a4 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  let {a4' = fromIntegral a4} in 
  slice'_ a1' a2' a3' a4' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 322 "src/Boolector/Foreign.chs" #-}


-- | Create unsigned extension.
--
-- The bit vector @node@ is padded with @width@ * zeroes.
uext :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))
uext a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  uext'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 327 "src/Boolector/Foreign.chs" #-}


-- | Create signed extension.
--
-- The bit vector @node@ is padded with @width@ bits where the value
-- depends on the value of the most significant bit of node @n@.
sext :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))
sext a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  sext'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 333 "src/Boolector/Foreign.chs" #-}


-- | Create the concatenation of two bit vectors.
concat :: (Btor) -> (Node) -> (Node) -> IO ((Node))
concat a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  concat'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 336 "src/Boolector/Foreign.chs" #-}


-- | Create @n@ concatenations of a given node @node@.
repeat :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))
repeat a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  repeat'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 339 "src/Boolector/Foreign.chs" #-}


--
-- Implications.
--

-- | Create boolean implication.
implies :: (Btor) -> (Node) -> (Node) -> IO ((Node))
implies a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  implies'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 346 "src/Boolector/Foreign.chs" #-}


-- | Create Boolean equivalence.
iff :: (Btor) -> (Node) -> (Node) -> IO ((Node))
iff a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  iff'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 349 "src/Boolector/Foreign.chs" #-}


--
-- Equality.
--

-- | Create bit vector or array equality.
--
-- Both operands are either bit vectors with the same bit width or arrays
-- of the same type.
eq :: (Btor) -> (Node) -> (Node) -> IO ((Node))
eq a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  eq'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 359 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector or array inequality.
--
-- Both operands are either bit vectors with the same bit width or arrays
-- of the same type.
ne :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ne a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ne'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 365 "src/Boolector/Foreign.chs" #-}


--
-- Conditionals.
--

-- | Create an if-then-else.
--
-- If condition @n_cond@ is true, then @n_then@ is returned, else @n_else@
-- is returned.
-- Nodes @n_then@ and @n_else@ must be either both arrays or both bit vectors.
cond :: (Btor) -> (Node) -> (Node) -> (Node) -> IO ((Node))
cond a1 a2 a3 a4 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  (withNode) a4 $ \a4' -> 
  cond'_ a1' a2' a3' a4' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 376 "src/Boolector/Foreign.chs" #-}


--
-- Bit-wise operations.
--

-- | Create a bit vector *xor*.
xor :: (Btor) -> (Node) -> (Node) -> IO ((Node))
xor a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  xor'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 383 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector *xnor*.
xnor :: (Btor) -> (Node) -> (Node) -> IO ((Node))
xnor a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  xnor'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 386 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector *and*.
and :: (Btor) -> (Node) -> (Node) -> IO ((Node))
and a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  and'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 389 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector *nand*.
nand :: (Btor) -> (Node) -> (Node) -> IO ((Node))
nand a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  nand'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 392 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector *or*.
or :: (Btor) -> (Node) -> (Node) -> IO ((Node))
or a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  or'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 395 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector *nor*.
nor :: (Btor) -> (Node) -> (Node) -> IO ((Node))
nor a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  nor'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 398 "src/Boolector/Foreign.chs" #-}


-- | Create a logical shift left.
--
-- Given node @n1@, the value it represents is the number of zeroes shifted
-- into node @n0@ from the right.
sll :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sll a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sll'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 404 "src/Boolector/Foreign.chs" #-}


-- | Create a logical shift right.
--
-- Given node @n1@, the value it represents is the number of zeroes shifted
-- into node @n0@ from the left.
srl :: (Btor) -> (Node) -> (Node) -> IO ((Node))
srl a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  srl'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 410 "src/Boolector/Foreign.chs" #-}


-- | Create an arithmetic shift right.
--
-- Analogously to 'srl', but whether zeroes or ones are shifted in depends on
-- the most significant bit of @n0@.
sra :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sra a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sra'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 416 "src/Boolector/Foreign.chs" #-}


-- | Create a rotate left.
--
-- Given bit vector node @n1@, the value it represents is the number of bits
-- by which node @n0@ is rotated to the left.
rol :: (Btor) -> (Node) -> (Node) -> IO ((Node))
rol a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  rol'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 422 "src/Boolector/Foreign.chs" #-}

-- | Create a rotate right.
--
-- Given bit vector node @n1@, the value it represents is the number of bits by
-- which node @n0@ is rotated to the right.
ror :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ror a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ror'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 427 "src/Boolector/Foreign.chs" #-}


--
-- Arithmetic operations.
--

-- | Create bit vector addition.
add :: (Btor) -> (Node) -> (Node) -> IO ((Node))
add a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  add'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 434 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector expression that increments bit vector @node@ by one.
inc :: (Btor) -> (Node) -> IO ((Node))
inc a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  inc'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 437 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned bit vector addition overflow detection.
uaddo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
uaddo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  uaddo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 440 "src/Boolector/Foreign.chs" #-}


-- | Create a signed bit vector addition overflow detection.
saddo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
saddo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  saddo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 443 "src/Boolector/Foreign.chs" #-}


-- | Create a bit vector subtraction.
sub :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sub a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sub'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 446 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned bit vector subtraction overflow detection.
usubo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
usubo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  usubo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 449 "src/Boolector/Foreign.chs" #-}


-- | Create a signed bit vector subtraction overflow detection.
ssubo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ssubo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ssubo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 452 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector expression that decrements bit vector @node@ by one.
dec :: (Btor) -> (Node) -> IO ((Node))
dec a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  dec'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 455 "src/Boolector/Foreign.chs" #-}


-- | Create a bitvector multiplication.
mul :: (Btor) -> (Node) -> (Node) -> IO ((Node))
mul a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  mul'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 458 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned bit vector multiplication overflow detection.
umulo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
umulo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  umulo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 461 "src/Boolector/Foreign.chs" #-}


-- | Create signed multiplication overflow detection.
smulo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
smulo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  smulo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 464 "src/Boolector/Foreign.chs" #-}


-- | Create unsigned division.
udiv :: (Btor) -> (Node) -> (Node) -> IO ((Node))
udiv a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  udiv'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 467 "src/Boolector/Foreign.chs" #-}


-- | Create signed division.
sdiv :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sdiv a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sdiv'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 470 "src/Boolector/Foreign.chs" #-}


-- | Create a signed bit vector division overflow detection.
sdivo :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sdivo a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sdivo'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 473 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned remainder.
urem :: (Btor) -> (Node) -> (Node) -> IO ((Node))
urem a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  urem'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 476 "src/Boolector/Foreign.chs" #-}


-- | Create a signed remainder.
srem :: (Btor) -> (Node) -> (Node) -> IO ((Node))
srem a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  srem'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 479 "src/Boolector/Foreign.chs" #-}


-- | Create a, signed remainder where its sign matches the sign of the divisor.
smod :: (Btor) -> (Node) -> (Node) -> IO ((Node))
smod a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  smod'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 482 "src/Boolector/Foreign.chs" #-}


--
-- Comparison operations.
--

-- | Create an unsigned less than.
ult :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ult a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ult'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 489 "src/Boolector/Foreign.chs" #-}


-- | Create a signed less than.
slt :: (Btor) -> (Node) -> (Node) -> IO ((Node))
slt a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  slt'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 492 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned less than or equal.
ulte :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ulte a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ulte'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 495 "src/Boolector/Foreign.chs" #-}


-- | Create a signed less than or equal.
slte :: (Btor) -> (Node) -> (Node) -> IO ((Node))
slte a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  slte'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 498 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned greater than.
ugt :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ugt a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ugt'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 501 "src/Boolector/Foreign.chs" #-}


-- | Create a signed greater than.
sgt :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sgt a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sgt'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 504 "src/Boolector/Foreign.chs" #-}


-- | Create an unsigned greater than or equal.
ugte :: (Btor) -> (Node) -> (Node) -> IO ((Node))
ugte a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  ugte'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 507 "src/Boolector/Foreign.chs" #-}


-- | Create a signed greater than or equal.
sgte :: (Btor) -> (Node) -> (Node) -> IO ((Node))
sgte a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  sgte'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 510 "src/Boolector/Foreign.chs" #-}


--
-- Array operations
--

-- | Create a one-dimensional bit vector array with sort @sort@.
--
-- The name must be unique.
array :: (Btor) -> (Sort) -> (String) -> IO ((Node))
array a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  array'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 519 "src/Boolector/Foreign.chs" #-}


-- | Create a read on array @n_array@ at position @n_index@.
read :: (Btor) -> (Node) -> (Node) -> IO ((Node))
read a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  read'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 522 "src/Boolector/Foreign.chs" #-}


-- | Create a write on array @n_array@ at position @n_index@ with value
-- @n_value@.
--
-- The array is updated at exactly one position, all other elements remain
-- unchanged. The bit width of @n_index@ must be the same as the bit width of
-- the indices of @n_array@. The bit width of @n_value@ must be the same as
-- the bit width of the elements of @n_array@.
write :: (Btor) -> (Node) -> (Node) -> (Node) -> IO ((Node))
write a1 a2 a3 a4 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  (withNode) a4 $ \a4' -> 
  write'_ a1' a2' a3' a4' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 531 "src/Boolector/Foreign.chs" #-}


--
-- Functions
--

-- | Create an uninterpreted function with sort @sort@.
--
-- The name must be unique.
uf :: (Btor) -> (Sort) -> (String) -> IO ((Node))
uf a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  uf'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 540 "src/Boolector/Foreign.chs" #-}



-- | Create function parameter of sort @sort@.
--
-- This kind of node is used to create parameterized expressions, which are
-- used to create functions. Once a parameter is bound to a function, it
-- cannot be re-used in other functions.
param :: (Btor) -> (Sort) -> (String) -> IO ((Node))
param a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  param'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Node)) res >>= \res' ->
  return (res')

{-# LINE 548 "src/Boolector/Foreign.chs" #-}


-- | Create a function with body @node@ parameterized over parameters
-- @param_nodes@.
--
-- This kind of node is similar to macros in the SMT-LIB standard 2.0.
-- Note that as soon as a parameter is bound to a function, it can not be
-- reused in other functions.
-- Call a function via 'apply'.
fun :: Btor -> [Node] -> Node -> IO Node
fun hbtor hargs hret = withBtor hbtor $ \cbotr ->
  withNodes hargs $ \cargs ->
    withArrayLen cargs $ \len cargsPtr ->
      withNode hret $ \cret -> do
        cptr <- fun'_ cbotr cargsPtr (fromIntegral len) cret
        Node `liftM` newForeignPtr_ cptr

foreign import ccall "boolector_fun"
  fun'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)

-- | Create a function application on function @n_fun@ with arguments
-- @arg_nodes@.
apply :: Btor -> [Node] -> Node -> IO Node
apply hbtor hargs hfun = withBtor hbtor $ \cbotr ->
  withNodes hargs $ \cargs ->
    withArrayLen cargs $ \len cargsPtr ->
      withNode hfun $ \cfun -> do
        cptr <- apply'_ cbotr cargsPtr (fromIntegral len) cfun
        Node `liftM` newForeignPtr_ cptr

foreign import ccall "boolector_apply"
  apply'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)

-- | Create a universally quantified term.
forall :: Btor -> [Node] -> Node -> IO Node
forall hbtor hparams hbody = withBtor hbtor $ \cbotr ->
  withNodes hparams $ \cparams ->
    withArrayLen cparams $ \len cparamsPtr ->
      withNode hbody $ \cbody -> do
        cptr <- forall'_ cbotr cparamsPtr (fromIntegral len) cbody
        Node `liftM` newForeignPtr_ cptr

foreign import ccall "boolector_forall"
  forall'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)

-- | Create an existentially quantifed term.
exists :: Btor -> [Node] -> Node -> IO Node
exists hbtor hparams hbody = withBtor hbtor $ \cbotr ->
  withNodes hparams $ \cparams ->
    withArrayLen cparams $ \len cparamsPtr ->
      withNode hbody $ \cbody -> do
        cptr <- exists'_ cbotr cparamsPtr (fromIntegral len) cbody
        Node `liftM` newForeignPtr_ cptr

foreign import ccall "boolector_exists"
  exists'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)

-- | Helper function for executing list of Nodes.
withNodes :: [Node] -> ([Ptr Node] -> IO a) -> IO a
withNodes [] f = f []
withNodes (hx:hxs) f = withNode hx $ \cx -> withNodes hxs $ \cxs -> f (cx:cxs)


--
-- Accessors
--

-- | Get the sort of given node.
getSort :: (Btor) -> (Node) -> IO ((Sort))
getSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  getSort'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 616 "src/Boolector/Foreign.chs" #-}


-- | Get the domain sort of given function node node.
funGetDomainSort :: (Btor) -> (Node) -> IO ((Sort))
funGetDomainSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  funGetDomainSort'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 619 "src/Boolector/Foreign.chs" #-}


-- | Get the codomain sort of given function node node.
funGetCodomainSort :: (Btor) -> (Node) -> IO ((Sort))
funGetCodomainSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  funGetCodomainSort'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 622 "src/Boolector/Foreign.chs" #-}


-- | Get the arity of function node.
getFunArity :: (Btor) -> (Node) -> IO ((CUInt))
getFunArity a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  getFunArity'_ a1' a2' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

{-# LINE 625 "src/Boolector/Foreign.chs" #-}


-- | Get the symbol of an expression.
getSymbol :: (Btor) -> (Node) -> IO ((String))
getSymbol a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  getSymbol'_ a1' a2' >>= \res ->
  C2HSImp.peekCString res >>= \res' ->
  return (res')

{-# LINE 628 "src/Boolector/Foreign.chs" #-}


-- | Set the symbol of an expression.
setSymbol :: (Btor) -> (Node) -> (String) -> IO ()
setSymbol a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  setSymbol'_ a1' a2' a3' >>
  return ()

{-# LINE 631 "src/Boolector/Foreign.chs" #-}


-- | Get the bit width of an expression.
--
-- If the expression is an array, it returns the bit width of the array
-- elements.
-- If the expression is a function, it returns the bit width of the function's
-- return value.
getWidth :: (Btor) -> (Node) -> IO ((CUInt))
getWidth a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  getWidth'_ a1' a2' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

{-# LINE 639 "src/Boolector/Foreign.chs" #-}


-- | Get the bit width of indices of @n_array@.
getIndexWidth :: (Btor) -> (Node) -> IO ((CUInt))
getIndexWidth a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  getIndexWidth'_ a1' a2' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

{-# LINE 642 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is a constant node.
isConst :: (Btor) -> (Node) -> IO ((Bool))
isConst a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isConst'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 645 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is a bit vector variable.
isVar :: (Btor) -> (Node) -> IO ((Bool))
isVar a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isVar'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 648 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is an array node.
isArray :: (Btor) -> (Node) -> IO ((Bool))
isArray a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isArray'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 651 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is an array node.
isArrayVar :: (Btor) -> (Node) -> IO ((Bool))
isArrayVar a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isArrayVar'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 654 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is a parameter node.
isParam :: (Btor) -> (Node) -> IO ((Bool))
isParam a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isParam'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 657 "src/Boolector/Foreign.chs" #-}


-- | Determine if given parameter node is bound by a function.
isBoundParam :: (Btor) -> (Node) -> IO ((Bool))
isBoundParam a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isBoundParam'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 660 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is an uninterpreted function node.
isUf :: (Btor) -> (Node) -> IO ((Bool))
isUf a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isUf'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 663 "src/Boolector/Foreign.chs" #-}


-- | Determine if given node is a function node.
isFun :: (Btor) -> (Node) -> IO ((Bool))
isFun a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  isFun'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 666 "src/Boolector/Foreign.chs" #-}


-- | Check if sorts of given arguments matches the function signature.
-- Returns 'Nothing' if all sorts are correct; otherwise it returns the
-- position of the incorrect argument.
funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int)
funSortCheck hbtor hparams hfun = withBtor hbtor $ \cbotr ->
  withNodes hparams $ \cparams ->
    withArrayLen cparams $ \len cparamsPtr ->
      withNode hfun $ \cfun -> do
       rt <- funSortCheck'_ cbotr cparamsPtr (fromIntegral len) cfun
       return $ if rt == -1
                  then Nothing
                  else Just $ fromIntegral rt

foreign import ccall "boolector_fun_sort_check"
  funSortCheck'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO CInt

--
-- Models.
--

-- | Generate an assignment string for bit vector expression if
-- 'sat' has returned 'Sat' and model generation has been enabled.
--
-- The expression can be an arbitrary bit vector expression which
-- occurs in an assertion or current assumption. The assignment string has to
-- be freed by 'free_bv_assignment'.
bvAssignment :: (Btor) -> (Node) -> IO ((String))
bvAssignment a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  bvAssignment'_ a1' a2' >>= \res ->
  C2HSImp.peekCString res >>= \res' ->
  return (res')

{-# LINE 694 "src/Boolector/Foreign.chs" #-}


-- | Free an assignment string for bit vectors.  TODO: we should change
-- bv_assignment to return a ModelString and  use free to actually free the
-- assignments. We're very leaky right now.
freeBvAssignment :: (Btor) -> (String) -> IO ()
freeBvAssignment a1 a2 =
  (withBtor) a1 $ \a1' -> 
  C2HSImp.withCString a2 $ \a2' -> 
  freeBvAssignment'_ a1' a2' >>
  return ()

{-# LINE 699 "src/Boolector/Foreign.chs" #-}


--
-- Sorts.
--

-- | Create Boolean sort.
boolSort :: (Btor) -> IO ((Sort))
boolSort a1 =
  (withBtor) a1 $ \a1' -> 
  boolSort'_ a1' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 706 "src/Boolector/Foreign.chs" #-}


-- | Create bit vector sort of bit width @width@.
bitvecSort :: (Btor) -> (CUInt) -> IO ((Sort))
bitvecSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  bitvecSort'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 709 "src/Boolector/Foreign.chs" #-}


-- | Create function sort.
funSort :: Btor -> [Sort] -> Sort -> IO Sort
funSort hbtor hargs hret = withBtor hbtor $ \cbotr ->
  withSorts hargs $ \cargs ->
    withArrayLen cargs $ \len cargsPtr ->
      withSort hret $ \cret -> do
        cptr <- funSort'_ cbotr cargsPtr (fromIntegral len) cret
        Sort `liftM` newForeignPtr_ cptr

foreign import ccall "boolector_fun_sort"
  funSort'_ :: Ptr Btor -> Ptr (Ptr Sort) -> CUInt -> Ptr Sort -> IO (Ptr Sort)

-- | Helper function for executing list of Sorts.
withSorts :: [Sort] -> ([Ptr Sort] -> IO a) -> IO a
withSorts [] f = f []
withSorts (hx:hxs) f = withSort hx $ \cx -> withSorts hxs $ \cxs -> f (cx:cxs)

-- | Create array sort.
arraySort :: (Btor) -> (Sort) -> (Sort) -> IO ((Sort))
arraySort a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  (withSort) a3 $ \a3' -> 
  arraySort'_ a1' a2' a3' >>= \res ->
  (\x -> C2HSImp.newForeignPtr_ x >>=  (return . Sort)) res >>= \res' ->
  return (res')

{-# LINE 729 "src/Boolector/Foreign.chs" #-}


-- | Determine if @n0@ and @n1@ have the same sort or not.
isEqualSort :: (Btor) -> (Node) -> (Node) -> IO ((Bool))
isEqualSort a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withNode) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  isEqualSort'_ a1' a2' a3' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 732 "src/Boolector/Foreign.chs" #-}


-- | Determine if @sort@ is an array sort.
isArraySort :: (Btor) -> (Sort) -> IO ((Bool))
isArraySort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  isArraySort'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 735 "src/Boolector/Foreign.chs" #-}


-- | Determine if @sort@ is a bit-vector sort.
isBitvecSort :: (Btor) -> (Sort) -> IO ((Bool))
isBitvecSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  isBitvecSort'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 738 "src/Boolector/Foreign.chs" #-}


-- | Determine if @sort@ is a function sort.
isFunSort :: (Btor) -> (Sort) -> IO ((Bool))
isFunSort a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withSort) a2 $ \a2' -> 
  isFunSort'_ a1' a2' >>= \res ->
  let {res' = C2HSImp.toBool res} in
  return (res')

{-# LINE 741 "src/Boolector/Foreign.chs" #-}


--
-- Dumping
--

newtype File = File (C2HSImp.ForeignPtr (File))
withFile :: File -> (C2HSImp.Ptr File -> IO b) -> IO b
withFile (File fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 747 "src/Boolector/Foreign.chs" #-}


-- | libc's fopen
fopen :: (String) -> (String) -> IO ((File))
fopen a1 a2 =
  C2HSImp.withCString a1 $ \a1' -> 
  C2HSImp.withCString a2 $ \a2' -> 
  fopen'_ a1' a2' >>= \res ->
  (\x -> C2HSImp.newForeignPtr fclose x >>= (return . File)) res >>= \res' ->
  return (res')

{-# LINE 750 "src/Boolector/Foreign.chs" #-}


-- | Recursively dump @node@ to file in BTOR_ format.
dumpBtorNode :: (Btor) -> (File) -> (Node) -> IO ()
dumpBtorNode a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withFile) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  dumpBtorNode'_ a1' a2' a3' >>
  return ()

{-# LINE 753 "src/Boolector/Foreign.chs" #-}


-- | Dump formula to file in BTOR_ format.
dumpBtor :: (Btor) -> (File) -> IO ()
dumpBtor a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withFile) a2 $ \a2' -> 
  dumpBtor'_ a1' a2' >>
  return ()

{-# LINE 756 "src/Boolector/Foreign.chs" #-}


-- | Recursively dump @node@ to file in SMT-LIB v2 format.
dumpSmt2Node :: (Btor) -> (File) -> (Node) -> IO ()
dumpSmt2Node a1 a2 a3 =
  (withBtor) a1 $ \a1' -> 
  (withFile) a2 $ \a2' -> 
  (withNode) a3 $ \a3' -> 
  dumpSmt2Node'_ a1' a2' a3' >>
  return ()

{-# LINE 759 "src/Boolector/Foreign.chs" #-}


-- | Dumps formula to file in SMT-LIB v2 format.
dumpSmt2 :: (Btor) -> (File) -> IO ()
dumpSmt2 a1 a2 =
  (withBtor) a1 $ \a1' -> 
  (withFile) a2 $ \a2' -> 
  dumpSmt2'_ a1' a2' >>
  return ()

{-# LINE 762 "src/Boolector/Foreign.chs" #-}


foreign import ccall safe "Boolector/Foreign.chs.h boolector_push"
  push'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CUInt -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_pop"
  pop'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CUInt -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_set_sat_solver"
  setSatSolver'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_set_opt"
  setOpt'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CInt -> (C2HSImp.CUInt -> (IO ()))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_opt"
  getOpt'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CInt -> (IO C2HSImp.CUInt)))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_has_opt"
  hasOpt'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CInt -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_assert"
  assert'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_assume"
  assume'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_failed"
  failed'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_fixate_assumptions"
  fixateAssumptions'_ :: ((C2HSImp.Ptr (Btor)) -> (IO ()))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_reset_assumptions"
  resetAssumptions'_ :: ((C2HSImp.Ptr (Btor)) -> (IO ()))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sat"
  sat'_ :: ((C2HSImp.Ptr (Btor)) -> (IO C2HSImp.CInt))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_limited_sat"
  limitedSat'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO C2HSImp.CInt))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_simplify"
  simplify'_ :: ((C2HSImp.Ptr (Btor)) -> (IO C2HSImp.CInt))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_copy"
  copy'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_const"
  const'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_constd"
  constd'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_consth"
  consth'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_true"
  true'_ :: ((C2HSImp.Ptr (Btor)) -> (IO (C2HSImp.Ptr (Node))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_false"
  false'_ :: ((C2HSImp.Ptr (Btor)) -> (IO (C2HSImp.Ptr (Node))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_zero"
  zero'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_one"
  one'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ones"
  ones'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_unsigned_int"
  unsignedInt'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CUInt -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_int"
  int'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CInt -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_var"
  var'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_not"
  not'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_neg"
  neg'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_redor"
  redor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_redxor"
  redxor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_redand"
  redand'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_slice"
  slice'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (C2HSImp.CUInt -> (C2HSImp.CUInt -> (IO (C2HSImp.Ptr (Node)))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_uext"
  uext'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (C2HSImp.CUInt -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sext"
  sext'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (C2HSImp.CUInt -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_concat"
  concat'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_repeat"
  repeat'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (C2HSImp.CUInt -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_implies"
  implies'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_iff"
  iff'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_eq"
  eq'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ne"
  ne'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_cond"
  cond'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_xor"
  xor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_xnor"
  xnor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_and"
  and'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_nand"
  nand'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_or"
  or'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_nor"
  nor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sll"
  sll'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_srl"
  srl'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sra"
  sra'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_rol"
  rol'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ror"
  ror'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_add"
  add'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_inc"
  inc'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_uaddo"
  uaddo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_saddo"
  saddo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sub"
  sub'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_usubo"
  usubo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ssubo"
  ssubo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_dec"
  dec'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_mul"
  mul'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_umulo"
  umulo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_smulo"
  smulo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_udiv"
  udiv'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sdiv"
  sdiv'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sdivo"
  sdivo'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_urem"
  urem'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_srem"
  srem'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_smod"
  smod'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ult"
  ult'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_slt"
  slt'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ulte"
  ulte'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_slte"
  slte'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ugt"
  ugt'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sgt"
  sgt'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_ugte"
  ugte'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_sgte"
  sgte'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_array"
  array'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_read"
  read'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_write"
  write'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Node)))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_uf"
  uf'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_param"
  param'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (Node))))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_sort"
  getSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Sort)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_fun_get_domain_sort"
  funGetDomainSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Sort)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_fun_get_codomain_sort"
  funGetCodomainSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr (Sort)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_fun_arity"
  getFunArity'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CUInt)))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_symbol"
  getSymbol'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr C2HSImp.CChar))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_set_symbol"
  setSymbol'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO ()))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_width"
  getWidth'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CUInt)))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_index_width"
  getIndexWidth'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CUInt)))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_const"
  isConst'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_var"
  isVar'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array"
  isArray'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array_var"
  isArrayVar'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_param"
  isParam'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_bound_param"
  isBoundParam'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_uf"
  isUf'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_fun"
  isFun'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_bv_assignment"
  bvAssignment'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr C2HSImp.CChar))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_free_bv_assignment"
  freeBvAssignment'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_bool_sort"
  boolSort'_ :: ((C2HSImp.Ptr (Btor)) -> (IO (C2HSImp.Ptr (Sort))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_bitvec_sort"
  bitvecSort'_ :: ((C2HSImp.Ptr (Btor)) -> (C2HSImp.CUInt -> (IO (C2HSImp.Ptr (Sort)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_array_sort"
  arraySort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> ((C2HSImp.Ptr (Sort)) -> (IO (C2HSImp.Ptr (Sort))))))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_equal_sort"
  isEqualSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt{-bool-}))))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array_sort"
  isArraySort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_bitvec_sort"
  isBitvecSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_fun_sort"
  isFunSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt{-bool-})))

foreign import ccall "Boolector/Foreign.chs.h &fclose"
  fclose :: C2HSImp.FinalizerPtr File

foreign import ccall safe "Boolector/Foreign.chs.h fopen"
  fopen'_ :: ((C2HSImp.Ptr C2HSImp.CChar) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (IO (C2HSImp.Ptr (File)))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_dump_btor_node"
  dumpBtorNode'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (File)) -> ((C2HSImp.Ptr (Node)) -> (IO ()))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_dump_btor"
  dumpBtor'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (File)) -> (IO ())))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_dump_smt2_node"
  dumpSmt2Node'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (File)) -> ((C2HSImp.Ptr (Node)) -> (IO ()))))

foreign import ccall safe "Boolector/Foreign.chs.h boolector_dump_smt2"
  dumpSmt2'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (File)) -> (IO ())))