{-# LINE 1 "src/Boolector/Foreign.chs" #-}
{-# LANGUAGE StandaloneDeriving #-}
module Boolector.Foreign (
Btor
, new
, Option(..)
, setOpt
, getOpt
, setSatSolver
, Node
, sat
, limitedSat
, simplify
, Status(..)
, assert
, assume
, failed
, fixateAssumptions
, resetAssumptions
, push
, pop
, var
, const
, constd
, consth
, true
, false
, zero
, one
, ones
, unsignedInt
, int
, array
, fun
, uf
, param
, forall
, exists
, implies
, iff
, cond
, eq
, ne
, not
, neg
, redor
, redxor
, redand
, slice
, uext
, sext
, concat
, repeat
, xor
, xnor
, and
, nand
, or
, nor
, sll
, srl
, sra
, rol
, ror
, add
, uaddo
, saddo
, inc
, sub
, usubo
, ssubo
, dec
, mul
, umulo
, smulo
, udiv
, sdiv
, sdivo
, urem
, srem
, smod
, ult
, slt
, ulte
, slte
, ugt
, sgt
, ugte
, sgte
, read
, write
, apply
, getSort
, funGetDomainSort
, funGetCodomainSort
, getFunArity
, getSymbol
, setSymbol
, getWidth
, getIndexWidth
, isConst
, isVar
, isArray
, isArrayVar
, isParam
, isBoundParam
, isUf
, isFun
, bvAssignment
, Sort
, boolSort
, bitvecSort
, funSort
, arraySort
, isEqualSort
, isArraySort
, isBitvecSort
, isFunSort
, funSortCheck
, dumpBtorNode
, dumpSmt2Node
, dumpBtor
, dumpSmt2
, fopen
, setTerm
) 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 Prelude hiding (read, not, and, or, const, concat, repeat)
import Foreign hiding (xor, new)
import Foreign.C
import Control.Monad
{-# LINE 166 "src/Boolector/Foreign.chs" #-}
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 180 "src/Boolector/Foreign.chs" #-}
newtype Btor = Btor (C2HSImp.ForeignPtr (Btor))
withBtor :: Btor -> (C2HSImp.Ptr Btor -> IO b) -> IO b
withBtor (Btor fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 183 "src/Boolector/Foreign.chs" #-}
deriving instance Eq Btor
deriving instance Ord Btor
newtype Node = Node (C2HSImp.ForeignPtr (Node))
withNode :: Node -> (C2HSImp.Ptr Node -> IO b) -> IO b
withNode (Node fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 188 "src/Boolector/Foreign.chs" #-}
deriving instance Eq Node
deriving instance Ord Node
newtype Sort = Sort (C2HSImp.ForeignPtr (Sort))
withSort :: Sort -> (C2HSImp.Ptr Sort -> IO b) -> IO b
withSort (Sort fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 193 "src/Boolector/Foreign.chs" #-}
deriving instance Eq Sort
deriving instance Ord Sort
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 291 "src/Boolector/Foreign.chs" #-}
new :: IO (Btor)
new = do
ptrBtor <- new'_
foreignPtrBtor <- newForeignPtr boolector_delete ptrBtor
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 :: (Btor) -> (CUInt) -> IO ()
push a1 a2 =
(withBtor) a1 $ \a1' ->
let {a2' = fromIntegral a2} in
push'_ a1' a2' >>
return ()
{-# LINE 318 "src/Boolector/Foreign.chs" #-}
pop :: (Btor) -> (CUInt) -> IO ()
pop a1 a2 =
(withBtor) a1 $ \a1' ->
let {a2' = fromIntegral a2} in
pop'_ a1' a2' >>
return ()
{-# LINE 321 "src/Boolector/Foreign.chs" #-}
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 ()
setSatSolver :: (Btor) -> (String) -> IO ()
setSatSolver a1 a2 =
(withBtor) a1 $ \a1' ->
C2HSImp.withCString a2 $ \a2' ->
setSatSolver'_ a1' a2' >>
return ()
{-# LINE 343 "src/Boolector/Foreign.chs" #-}
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 346 "src/Boolector/Foreign.chs" #-}
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 349 "src/Boolector/Foreign.chs" #-}
assert :: (Btor) -> (Node) -> IO ()
assert a1 a2 =
(withBtor) a1 $ \a1' ->
(withNode) a2 $ \a2' ->
assert'_ a1' a2' >>
return ()
{-# LINE 356 "src/Boolector/Foreign.chs" #-}
assume :: (Btor) -> (Node) -> IO ()
assume a1 a2 =
(withBtor) a1 $ \a1' ->
(withNode) a2 $ \a2' ->
assume'_ a1' a2' >>
return ()
{-# LINE 359 "src/Boolector/Foreign.chs" #-}
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 365 "src/Boolector/Foreign.chs" #-}
fixateAssumptions :: (Btor) -> IO ()
fixateAssumptions a1 =
(withBtor) a1 $ \a1' ->
fixateAssumptions'_ a1' >>
return ()
{-# LINE 368 "src/Boolector/Foreign.chs" #-}
resetAssumptions :: (Btor) -> IO ()
resetAssumptions a1 =
(withBtor) a1 $ \a1' ->
resetAssumptions'_ a1' >>
return ()
{-# LINE 371 "src/Boolector/Foreign.chs" #-}
sat :: (Btor) -> IO ((Status))
sat a1 =
(withBtor) a1 $ \a1' ->
sat'_ a1' >>= \res ->
let {res' = (toEnum . fromIntegral) res} in
return (res')
{-# LINE 378 "src/Boolector/Foreign.chs" #-}
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 391 "src/Boolector/Foreign.chs" #-}
simplify :: (Btor) -> IO ((Status))
simplify a1 =
(withBtor) a1 $ \a1' ->
simplify'_ a1' >>= \res ->
let {res' = (toEnum . fromIntegral) res} in
return (res')
{-# LINE 394 "src/Boolector/Foreign.chs" #-}
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 401 "src/Boolector/Foreign.chs" #-}
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 404 "src/Boolector/Foreign.chs" #-}
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 407 "src/Boolector/Foreign.chs" #-}
true :: (Btor) -> IO ((Node))
true a1 =
(withBtor) a1 $ \a1' ->
true'_ a1' >>= \res ->
(\x -> C2HSImp.newForeignPtr_ x >>= (return . Node)) res >>= \res' ->
return (res')
{-# LINE 411 "src/Boolector/Foreign.chs" #-}
false :: (Btor) -> IO ((Node))
false a1 =
(withBtor) a1 $ \a1' ->
false'_ a1' >>= \res ->
(\x -> C2HSImp.newForeignPtr_ x >>= (return . Node)) res >>= \res' ->
return (res')
{-# LINE 414 "src/Boolector/Foreign.chs" #-}
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 417 "src/Boolector/Foreign.chs" #-}
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 420 "src/Boolector/Foreign.chs" #-}
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 423 "src/Boolector/Foreign.chs" #-}
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 430 "src/Boolector/Foreign.chs" #-}
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 437 "src/Boolector/Foreign.chs" #-}
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 442 "src/Boolector/Foreign.chs" #-}
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 445 "src/Boolector/Foreign.chs" #-}
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 448 "src/Boolector/Foreign.chs" #-}
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 453 "src/Boolector/Foreign.chs" #-}
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 458 "src/Boolector/Foreign.chs" #-}
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 463 "src/Boolector/Foreign.chs" #-}
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 466 "src/Boolector/Foreign.chs" #-}
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 471 "src/Boolector/Foreign.chs" #-}
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 477 "src/Boolector/Foreign.chs" #-}
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 480 "src/Boolector/Foreign.chs" #-}
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 483 "src/Boolector/Foreign.chs" #-}
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 490 "src/Boolector/Foreign.chs" #-}
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 493 "src/Boolector/Foreign.chs" #-}
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 503 "src/Boolector/Foreign.chs" #-}
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 509 "src/Boolector/Foreign.chs" #-}
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 520 "src/Boolector/Foreign.chs" #-}
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 527 "src/Boolector/Foreign.chs" #-}
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 530 "src/Boolector/Foreign.chs" #-}
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 533 "src/Boolector/Foreign.chs" #-}
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 536 "src/Boolector/Foreign.chs" #-}
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 539 "src/Boolector/Foreign.chs" #-}
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 542 "src/Boolector/Foreign.chs" #-}
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 548 "src/Boolector/Foreign.chs" #-}
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 554 "src/Boolector/Foreign.chs" #-}
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 560 "src/Boolector/Foreign.chs" #-}
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 566 "src/Boolector/Foreign.chs" #-}
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 572 "src/Boolector/Foreign.chs" #-}
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 579 "src/Boolector/Foreign.chs" #-}
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 582 "src/Boolector/Foreign.chs" #-}
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 585 "src/Boolector/Foreign.chs" #-}
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 588 "src/Boolector/Foreign.chs" #-}
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 591 "src/Boolector/Foreign.chs" #-}
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 594 "src/Boolector/Foreign.chs" #-}
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 597 "src/Boolector/Foreign.chs" #-}
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 600 "src/Boolector/Foreign.chs" #-}
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 603 "src/Boolector/Foreign.chs" #-}
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 606 "src/Boolector/Foreign.chs" #-}
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 609 "src/Boolector/Foreign.chs" #-}
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 612 "src/Boolector/Foreign.chs" #-}
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 615 "src/Boolector/Foreign.chs" #-}
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 618 "src/Boolector/Foreign.chs" #-}
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 621 "src/Boolector/Foreign.chs" #-}
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 624 "src/Boolector/Foreign.chs" #-}
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 627 "src/Boolector/Foreign.chs" #-}
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 634 "src/Boolector/Foreign.chs" #-}
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 637 "src/Boolector/Foreign.chs" #-}
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 640 "src/Boolector/Foreign.chs" #-}
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 643 "src/Boolector/Foreign.chs" #-}
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 646 "src/Boolector/Foreign.chs" #-}
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 649 "src/Boolector/Foreign.chs" #-}
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 652 "src/Boolector/Foreign.chs" #-}
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 655 "src/Boolector/Foreign.chs" #-}
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 664 "src/Boolector/Foreign.chs" #-}
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 667 "src/Boolector/Foreign.chs" #-}
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 676 "src/Boolector/Foreign.chs" #-}
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 685 "src/Boolector/Foreign.chs" #-}
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 693 "src/Boolector/Foreign.chs" #-}
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)
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)
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)
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)
withNodes :: [Node] -> ([Ptr Node] -> IO a) -> IO a
withNodes [] f = f []
withNodes (hx:hxs) f = withNode hx $ \cx -> withNodes hxs $ \cxs -> f (cx:cxs)
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 761 "src/Boolector/Foreign.chs" #-}
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 764 "src/Boolector/Foreign.chs" #-}
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 767 "src/Boolector/Foreign.chs" #-}
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 770 "src/Boolector/Foreign.chs" #-}
foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_symbol"
getSymbol'_ :: Ptr Btor -> Ptr Node -> IO CString
getSymbol :: Btor -> Node -> IO (Maybe String)
getSymbol hbtor hnode = withBtor hbtor $ \cbtor ->
withNode hnode $ \cnode -> do
cstrPtr <- getSymbol'_ cbtor cnode
if cstrPtr == nullPtr
then return Nothing
else Just `liftM` peekCString cstrPtr
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 786 "src/Boolector/Foreign.chs" #-}
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 794 "src/Boolector/Foreign.chs" #-}
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 797 "src/Boolector/Foreign.chs" #-}
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 800 "src/Boolector/Foreign.chs" #-}
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 803 "src/Boolector/Foreign.chs" #-}
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 806 "src/Boolector/Foreign.chs" #-}
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 809 "src/Boolector/Foreign.chs" #-}
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 812 "src/Boolector/Foreign.chs" #-}
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 815 "src/Boolector/Foreign.chs" #-}
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 818 "src/Boolector/Foreign.chs" #-}
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 821 "src/Boolector/Foreign.chs" #-}
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
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 853 "src/Boolector/Foreign.chs" #-}
boolSort :: (Btor) -> IO ((Sort))
boolSort a1 =
(withBtor) a1 $ \a1' ->
boolSort'_ a1' >>= \res ->
(\x -> C2HSImp.newForeignPtr_ x >>= (return . Sort)) res >>= \res' ->
return (res')
{-# LINE 861 "src/Boolector/Foreign.chs" #-}
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 864 "src/Boolector/Foreign.chs" #-}
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)
withSorts :: [Sort] -> ([Ptr Sort] -> IO a) -> IO a
withSorts [] f = f []
withSorts (hx:hxs) f = withSort hx $ \cx -> withSorts hxs $ \cxs -> f (cx:cxs)
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 884 "src/Boolector/Foreign.chs" #-}
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 887 "src/Boolector/Foreign.chs" #-}
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 890 "src/Boolector/Foreign.chs" #-}
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 893 "src/Boolector/Foreign.chs" #-}
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 896 "src/Boolector/Foreign.chs" #-}
newtype File = File (C2HSImp.ForeignPtr (File))
withFile :: File -> (C2HSImp.Ptr File -> IO b) -> IO b
withFile (File fptr) = C2HSImp.withForeignPtr fptr
{-# LINE 903 "src/Boolector/Foreign.chs" #-}
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 906 "src/Boolector/Foreign.chs" #-}
dumpBtorNode :: (Btor) -> (File) -> (Node) -> IO ()
dumpBtorNode a1 a2 a3 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
(withNode) a3 $ \a3' ->
dumpBtorNode'_ a1' a2' a3' >>
return ()
{-# LINE 909 "src/Boolector/Foreign.chs" #-}
dumpBtor :: (Btor) -> (File) -> IO ()
dumpBtor a1 a2 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
dumpBtor'_ a1' a2' >>
return ()
{-# LINE 912 "src/Boolector/Foreign.chs" #-}
dumpSmt2Node :: (Btor) -> (File) -> (Node) -> IO ()
dumpSmt2Node a1 a2 a3 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
(withNode) a3 $ \a3' ->
dumpSmt2Node'_ a1' a2' a3' >>
return ()
{-# LINE 915 "src/Boolector/Foreign.chs" #-}
dumpSmt2 :: (Btor) -> (File) -> IO ()
dumpSmt2 a1 a2 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
dumpSmt2'_ a1' a2' >>
return ()
{-# LINE 918 "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 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)))
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_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_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)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_var"
isVar'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array"
isArray'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array_var"
isArrayVar'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_param"
isParam'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_bound_param"
isBoundParam'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_uf"
isUf'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_fun"
isFun'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO C2HSImp.CInt)))
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_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))))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_array_sort"
isArraySort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_bitvec_sort"
isBitvecSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Boolector/Foreign.chs.h __c2hs_wrapped__boolector_is_fun_sort"
isFunSort'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Sort)) -> (IO C2HSImp.CInt)))
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 ())))