{-# 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
, getBits
, 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
, withDumpFile, withTempDumpFile
, 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
import Control.Exception (bracket, finally, onException)
import System.IO.Temp
import System.Directory (removeFile)
{-# LINE 170 "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 184 "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 187 "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 192 "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 197 "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
| 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_QI
| OPT_QUANT_DER
| OPT_QUANT_CER
| OPT_QUANT_MINISCOPE
| 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_SAT_ENGINE_CADICAL_FREEZE
| OPT_SAT_ENGINE_N_THREADS
| OPT_SIMP_NORMAMLIZE_ADDERS
| OPT_DECLSORT_BV_WIDTH
| OPT_QUANT_SYNTH_ITE_COMPLETE
| OPT_QUANT_FIXSYNTH
| OPT_RW_ZERO_LOWER_SLICE
| OPT_NONDESTR_SUBST
| 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
succ OPT_BETA_REDUCE = 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_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_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_SAT_ENGINE_CADICAL_FREEZE
succ OPT_SAT_ENGINE_CADICAL_FREEZE = OPT_SAT_ENGINE_N_THREADS
succ OPT_SAT_ENGINE_N_THREADS = OPT_SIMP_NORMAMLIZE_ADDERS
succ OPT_SIMP_NORMAMLIZE_ADDERS = OPT_DECLSORT_BV_WIDTH
succ OPT_DECLSORT_BV_WIDTH = OPT_QUANT_SYNTH_ITE_COMPLETE
succ OPT_QUANT_SYNTH_ITE_COMPLETE = OPT_QUANT_FIXSYNTH
succ OPT_QUANT_FIXSYNTH = OPT_RW_ZERO_LOWER_SLICE
succ OPT_RW_ZERO_LOWER_SLICE = OPT_NONDESTR_SUBST
succ OPT_NONDESTR_SUBST = 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 = OPT_ACKERMANN
pred OPT_ELIMINATE_SLICES = OPT_BETA_REDUCE
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_QI = OPT_QUANT_SYNTH_LIMIT
pred OPT_QUANT_DER = OPT_QUANT_SYNTH_QI
pred OPT_QUANT_CER = OPT_QUANT_DER
pred OPT_QUANT_MINISCOPE = OPT_QUANT_CER
pred OPT_SORT_EXP = OPT_QUANT_MINISCOPE
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_SAT_ENGINE_CADICAL_FREEZE = OPT_SAT_ENGINE_LGL_FORK
pred OPT_SAT_ENGINE_N_THREADS = OPT_SAT_ENGINE_CADICAL_FREEZE
pred OPT_SIMP_NORMAMLIZE_ADDERS = OPT_SAT_ENGINE_N_THREADS
pred OPT_DECLSORT_BV_WIDTH = OPT_SIMP_NORMAMLIZE_ADDERS
pred OPT_QUANT_SYNTH_ITE_COMPLETE = OPT_DECLSORT_BV_WIDTH
pred OPT_QUANT_FIXSYNTH = OPT_QUANT_SYNTH_ITE_COMPLETE
pred OPT_RW_ZERO_LOWER_SLICE = OPT_QUANT_FIXSYNTH
pred OPT_NONDESTR_SUBST = OPT_RW_ZERO_LOWER_SLICE
pred OPT_NUM_OPTS = OPT_NONDESTR_SUBST
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 = 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_QI = 71
fromEnum OPT_QUANT_DER = 72
fromEnum OPT_QUANT_CER = 73
fromEnum OPT_QUANT_MINISCOPE = 74
fromEnum OPT_SORT_EXP = 75
fromEnum OPT_SORT_AIG = 76
fromEnum OPT_SORT_AIGVEC = 77
fromEnum OPT_AUTO_CLEANUP_INTERNAL = 78
fromEnum OPT_SIMPLIFY_CONSTRAINTS = 79
fromEnum OPT_CHK_FAILED_ASSUMPTIONS = 80
fromEnum OPT_CHK_MODEL = 81
fromEnum OPT_CHK_UNCONSTRAINED = 82
fromEnum OPT_PARSE_INTERACTIVE = 83
fromEnum OPT_SAT_ENGINE_LGL_FORK = 84
fromEnum OPT_SAT_ENGINE_CADICAL_FREEZE = 85
fromEnum OPT_SAT_ENGINE_N_THREADS = 86
fromEnum OPT_SIMP_NORMAMLIZE_ADDERS = 87
fromEnum OPT_DECLSORT_BV_WIDTH = 88
fromEnum OPT_QUANT_SYNTH_ITE_COMPLETE = 89
fromEnum OPT_QUANT_FIXSYNTH = 90
fromEnum OPT_RW_ZERO_LOWER_SLICE = 91
fromEnum OPT_NONDESTR_SUBST = 92
fromEnum OPT_NUM_OPTS = 93
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
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_QI
toEnum 72 = OPT_QUANT_DER
toEnum 73 = OPT_QUANT_CER
toEnum 74 = OPT_QUANT_MINISCOPE
toEnum 75 = OPT_SORT_EXP
toEnum 76 = OPT_SORT_AIG
toEnum 77 = OPT_SORT_AIGVEC
toEnum 78 = OPT_AUTO_CLEANUP_INTERNAL
toEnum 79 = OPT_SIMPLIFY_CONSTRAINTS
toEnum 80 = OPT_CHK_FAILED_ASSUMPTIONS
toEnum 81 = OPT_CHK_MODEL
toEnum 82 = OPT_CHK_UNCONSTRAINED
toEnum 83 = OPT_PARSE_INTERACTIVE
toEnum 84 = OPT_SAT_ENGINE_LGL_FORK
toEnum 85 = OPT_SAT_ENGINE_CADICAL_FREEZE
toEnum 86 = OPT_SAT_ENGINE_N_THREADS
toEnum 87 = OPT_SIMP_NORMAMLIZE_ADDERS
toEnum 88 = OPT_DECLSORT_BV_WIDTH
toEnum 89 = OPT_QUANT_SYNTH_ITE_COMPLETE
toEnum 90 = OPT_QUANT_FIXSYNTH
toEnum 91 = OPT_RW_ZERO_LOWER_SLICE
toEnum 92 = OPT_NONDESTR_SUBST
toEnum 93 = OPT_NUM_OPTS
toEnum unmatched = error ("Option.toEnum: Cannot match " ++ show unmatched)
{-# LINE 298 "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 325 "src/Boolector/Foreign.chs" #-}
pop :: (Btor) -> (CUInt) -> IO ()
pop a1 a2 =
(withBtor) a1 $ \a1' ->
let {a2' = fromIntegral a2} in
pop'_ a1' a2' >>
return ()
{-# LINE 328 "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 350 "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 353 "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 356 "src/Boolector/Foreign.chs" #-}
assert :: (Btor) -> (Node) -> IO ()
assert a1 a2 =
(withBtor) a1 $ \a1' ->
(withNode) a2 $ \a2' ->
assert'_ a1' a2' >>
return ()
{-# LINE 363 "src/Boolector/Foreign.chs" #-}
assume :: (Btor) -> (Node) -> IO ()
assume a1 a2 =
(withBtor) a1 $ \a1' ->
(withNode) a2 $ \a2' ->
assume'_ a1' a2' >>
return ()
{-# LINE 366 "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 372 "src/Boolector/Foreign.chs" #-}
fixateAssumptions :: (Btor) -> IO ()
fixateAssumptions a1 =
(withBtor) a1 $ \a1' ->
fixateAssumptions'_ a1' >>
return ()
{-# LINE 375 "src/Boolector/Foreign.chs" #-}
resetAssumptions :: (Btor) -> IO ()
resetAssumptions a1 =
(withBtor) a1 $ \a1' ->
resetAssumptions'_ a1' >>
return ()
{-# LINE 378 "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 385 "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 398 "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 401 "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 408 "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 411 "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 414 "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 418 "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 421 "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 424 "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 427 "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 430 "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 437 "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 444 "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 449 "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 452 "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 455 "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 460 "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 465 "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 470 "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 473 "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 478 "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 484 "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 487 "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 490 "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 497 "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 500 "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 510 "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 516 "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 527 "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 534 "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 537 "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 540 "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 543 "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 546 "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 549 "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 555 "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 561 "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 567 "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 573 "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 579 "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 586 "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 589 "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 592 "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 595 "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 598 "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 601 "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 604 "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 607 "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 610 "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 613 "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 616 "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 619 "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 622 "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 625 "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 628 "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 631 "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 634 "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 641 "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 644 "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 647 "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 650 "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 653 "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 656 "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 659 "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 662 "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 671 "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 674 "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 683 "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 692 "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 700 "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 768 "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 771 "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 774 "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 777 "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 793 "src/Boolector/Foreign.chs" #-}
getBits :: (Btor) -> (Node) -> IO ((String))
getBits a1 a2 =
(withBtor) a1 $ \a1' ->
(withNode) a2 $ \a2' ->
getBits'_ a1' a2' >>= \res ->
C2HSImp.peekCString res >>= \res' ->
return (res')
{-# LINE 796 "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 805 "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 808 "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 811 "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 814 "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 817 "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 820 "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 823 "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 826 "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 829 "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 832 "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 864 "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 872 "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 875 "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 895 "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 898 "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 901 "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 904 "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 907 "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 914 "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_ x >>= (return . File)) res >>= \res' ->
return (res')
{-# LINE 917 "src/Boolector/Foreign.chs" #-}
fclose :: (File) -> IO ()
fclose a1 =
(withFile) a1 $ \a1' ->
fclose'_ a1' >>
return ()
{-# LINE 920 "src/Boolector/Foreign.chs" #-}
fflush :: (File) -> IO ()
fflush a1 =
(withFile) a1 $ \a1' ->
fflush'_ a1' >>
return ()
{-# LINE 923 "src/Boolector/Foreign.chs" #-}
withDumpFile :: String
-> (File -> IO ())
-> IO ()
withDumpFile path act = bracket
(fopen path "w") fclose
(\fileHandle -> act fileHandle >> fflush fileHandle)
withTempDumpFile :: (File -> IO ()) -> IO String
withTempDumpFile act = do
path <- emptySystemTempFile "haskell-boolector"
withDumpFile path act `onException` removeFile path
readFile path `finally` removeFile path
dumpBtorNode :: (Btor) -> (File) -> (Node) -> IO ()
dumpBtorNode a1 a2 a3 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
(withNode) a3 $ \a3' ->
dumpBtorNode'_ a1' a2' a3' >>
return ()
{-# LINE 941 "src/Boolector/Foreign.chs" #-}
dumpBtor :: (Btor) -> (File) -> IO ()
dumpBtor a1 a2 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
dumpBtor'_ a1' a2' >>
return ()
{-# LINE 944 "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 947 "src/Boolector/Foreign.chs" #-}
dumpSmt2 :: (Btor) -> (File) -> IO ()
dumpSmt2 a1 a2 =
(withBtor) a1 $ \a1' ->
(withFile) a2 $ \a2' ->
dumpSmt2'_ a1' a2' >>
return ()
{-# LINE 950 "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_bits"
getBits'_ :: ((C2HSImp.Ptr (Btor)) -> ((C2HSImp.Ptr (Node)) -> (IO (C2HSImp.Ptr C2HSImp.CChar))))
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 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 fclose"
fclose'_ :: ((C2HSImp.Ptr (File)) -> (IO C2HSImp.CInt))
foreign import ccall safe "Boolector/Foreign.chs.h fflush"
fflush'_ :: ((C2HSImp.Ptr (File)) -> (IO C2HSImp.CInt))
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 ())))