Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This module exports a subset of the low-level C Boolector API to Haskell
code. In general, you don't want to use this module and should use the
Boolector
module instead.
- data Status
- newtype Btor = Btor (ForeignPtr Btor)
- withBtor :: Btor -> (Ptr Btor -> IO b) -> IO b
- newtype Node = Node (ForeignPtr Node)
- withNode :: Node -> (Ptr Node -> IO b) -> IO b
- newtype Sort = Sort (ForeignPtr Sort)
- withSort :: Sort -> (Ptr Sort -> IO b) -> IO b
- 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
- new :: IO Btor
- new'_ :: IO (Ptr Btor)
- boolector_delete :: FinalizerPtr Btor
- boolector_release_all :: FinalizerPtr Btor
- push :: Btor -> CUInt -> IO ()
- pop :: Btor -> CUInt -> IO ()
- setTerm :: Btor -> (Ptr () -> IO Int) -> IO ()
- makeWrapper :: (Ptr () -> IO Int) -> IO (FunPtr (Ptr () -> IO Int))
- setTerm'_ :: Ptr Btor -> FunPtr (Ptr () -> IO Int) -> Ptr () -> IO ()
- setSatSolver :: Btor -> String -> IO ()
- setOpt :: Btor -> Option -> CUInt -> IO ()
- getOpt :: Btor -> Option -> IO CUInt
- hasOpt :: Btor -> Option -> IO Bool
- assert :: Btor -> Node -> IO ()
- assume :: Btor -> Node -> IO ()
- failed :: Btor -> Node -> IO Bool
- fixateAssumptions :: Btor -> IO ()
- resetAssumptions :: Btor -> IO ()
- sat :: Btor -> IO Status
- limitedSat :: Btor -> Int -> Int -> IO Status
- simplify :: Btor -> IO Status
- copy :: Btor -> Node -> IO Node
- const :: Btor -> String -> IO Node
- constd :: Btor -> Sort -> String -> IO Node
- consth :: Btor -> Sort -> String -> IO Node
- true :: Btor -> IO Node
- false :: Btor -> IO Node
- zero :: Btor -> Sort -> IO Node
- one :: Btor -> Sort -> IO Node
- ones :: Btor -> Sort -> IO Node
- unsignedInt :: Btor -> CUInt -> Sort -> IO Node
- int :: Btor -> CInt -> Sort -> IO Node
- var :: Btor -> Sort -> String -> IO Node
- not :: Btor -> Node -> IO Node
- neg :: Btor -> Node -> IO Node
- redor :: Btor -> Node -> IO Node
- redxor :: Btor -> Node -> IO Node
- redand :: Btor -> Node -> IO Node
- slice :: Btor -> Node -> CUInt -> CUInt -> IO Node
- uext :: Btor -> Node -> CUInt -> IO Node
- sext :: Btor -> Node -> CUInt -> IO Node
- concat :: Btor -> Node -> Node -> IO Node
- repeat :: Btor -> Node -> CUInt -> IO Node
- implies :: Btor -> Node -> Node -> IO Node
- iff :: Btor -> Node -> Node -> IO Node
- eq :: Btor -> Node -> Node -> IO Node
- ne :: Btor -> Node -> Node -> IO Node
- cond :: Btor -> Node -> Node -> Node -> IO Node
- xor :: Btor -> Node -> Node -> IO Node
- xnor :: Btor -> Node -> Node -> IO Node
- and :: Btor -> Node -> Node -> IO Node
- nand :: Btor -> Node -> Node -> IO Node
- or :: Btor -> Node -> Node -> IO Node
- nor :: Btor -> Node -> Node -> IO Node
- sll :: Btor -> Node -> Node -> IO Node
- srl :: Btor -> Node -> Node -> IO Node
- sra :: Btor -> Node -> Node -> IO Node
- rol :: Btor -> Node -> Node -> IO Node
- ror :: Btor -> Node -> Node -> IO Node
- add :: Btor -> Node -> Node -> IO Node
- inc :: Btor -> Node -> IO Node
- uaddo :: Btor -> Node -> Node -> IO Node
- saddo :: Btor -> Node -> Node -> IO Node
- sub :: Btor -> Node -> Node -> IO Node
- usubo :: Btor -> Node -> Node -> IO Node
- ssubo :: Btor -> Node -> Node -> IO Node
- dec :: Btor -> Node -> IO Node
- mul :: Btor -> Node -> Node -> IO Node
- umulo :: Btor -> Node -> Node -> IO Node
- smulo :: Btor -> Node -> Node -> IO Node
- udiv :: Btor -> Node -> Node -> IO Node
- sdiv :: Btor -> Node -> Node -> IO Node
- sdivo :: Btor -> Node -> Node -> IO Node
- urem :: Btor -> Node -> Node -> IO Node
- srem :: Btor -> Node -> Node -> IO Node
- smod :: Btor -> Node -> Node -> IO Node
- ult :: Btor -> Node -> Node -> IO Node
- slt :: Btor -> Node -> Node -> IO Node
- ulte :: Btor -> Node -> Node -> IO Node
- slte :: Btor -> Node -> Node -> IO Node
- ugt :: Btor -> Node -> Node -> IO Node
- sgt :: Btor -> Node -> Node -> IO Node
- ugte :: Btor -> Node -> Node -> IO Node
- sgte :: Btor -> Node -> Node -> IO Node
- array :: Btor -> Sort -> String -> IO Node
- read :: Btor -> Node -> Node -> IO Node
- write :: Btor -> Node -> Node -> Node -> IO Node
- uf :: Btor -> Sort -> String -> IO Node
- param :: Btor -> Sort -> String -> IO Node
- fun :: Btor -> [Node] -> Node -> IO Node
- fun'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)
- apply :: Btor -> [Node] -> Node -> IO Node
- apply'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)
- forall :: Btor -> [Node] -> Node -> IO Node
- forall'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)
- exists :: Btor -> [Node] -> Node -> IO Node
- exists'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)
- withNodes :: [Node] -> ([Ptr Node] -> IO a) -> IO a
- getSort :: Btor -> Node -> IO Sort
- funGetDomainSort :: Btor -> Node -> IO Sort
- funGetCodomainSort :: Btor -> Node -> IO Sort
- getFunArity :: Btor -> Node -> IO CUInt
- getSymbol :: Btor -> Node -> IO String
- setSymbol :: Btor -> Node -> String -> IO ()
- getWidth :: Btor -> Node -> IO CUInt
- getIndexWidth :: Btor -> Node -> IO CUInt
- isConst :: Btor -> Node -> IO Bool
- isVar :: Btor -> Node -> IO Bool
- isArray :: Btor -> Node -> IO Bool
- isArrayVar :: Btor -> Node -> IO Bool
- isParam :: Btor -> Node -> IO Bool
- isBoundParam :: Btor -> Node -> IO Bool
- isUf :: Btor -> Node -> IO Bool
- isFun :: Btor -> Node -> IO Bool
- funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int)
- funSortCheck'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO CInt
- bvAssignment :: Btor -> Node -> IO String
- freeBvAssignment :: Btor -> String -> IO ()
- boolSort :: Btor -> IO Sort
- bitvecSort :: Btor -> CUInt -> IO Sort
- funSort :: Btor -> [Sort] -> Sort -> IO Sort
- funSort'_ :: Ptr Btor -> Ptr (Ptr Sort) -> CUInt -> Ptr Sort -> IO (Ptr Sort)
- withSorts :: [Sort] -> ([Ptr Sort] -> IO a) -> IO a
- arraySort :: Btor -> Sort -> Sort -> IO Sort
- isEqualSort :: Btor -> Node -> Node -> IO Bool
- isArraySort :: Btor -> Sort -> IO Bool
- isBitvecSort :: Btor -> Sort -> IO Bool
- isFunSort :: Btor -> Sort -> IO Bool
- newtype File = File (ForeignPtr File)
- withFile :: File -> (Ptr File -> IO b) -> IO b
- fopen :: String -> String -> IO File
- dumpBtorNode :: Btor -> File -> Node -> IO ()
- dumpBtor :: Btor -> File -> IO ()
- dumpSmt2Node :: Btor -> File -> Node -> IO ()
- dumpSmt2 :: Btor -> File -> IO ()
- push'_ :: Ptr Btor -> CUInt -> IO ()
- pop'_ :: Ptr Btor -> CUInt -> IO ()
- setSatSolver'_ :: Ptr Btor -> Ptr CChar -> IO ()
- setOpt'_ :: Ptr Btor -> CInt -> CUInt -> IO ()
- getOpt'_ :: Ptr Btor -> CInt -> IO CUInt
- hasOpt'_ :: Ptr Btor -> CInt -> IO CInt
- assert'_ :: Ptr Btor -> Ptr Node -> IO ()
- assume'_ :: Ptr Btor -> Ptr Node -> IO ()
- failed'_ :: Ptr Btor -> Ptr Node -> IO CInt
- fixateAssumptions'_ :: Ptr Btor -> IO ()
- resetAssumptions'_ :: Ptr Btor -> IO ()
- sat'_ :: Ptr Btor -> IO CInt
- limitedSat'_ :: Ptr Btor -> CInt -> CInt -> IO CInt
- simplify'_ :: Ptr Btor -> IO CInt
- copy'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- const'_ :: Ptr Btor -> Ptr CChar -> IO (Ptr Node)
- constd'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- consth'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- true'_ :: Ptr Btor -> IO (Ptr Node)
- false'_ :: Ptr Btor -> IO (Ptr Node)
- zero'_ :: Ptr Btor -> Ptr Sort -> IO (Ptr Node)
- one'_ :: Ptr Btor -> Ptr Sort -> IO (Ptr Node)
- ones'_ :: Ptr Btor -> Ptr Sort -> IO (Ptr Node)
- unsignedInt'_ :: Ptr Btor -> CUInt -> Ptr Sort -> IO (Ptr Node)
- int'_ :: Ptr Btor -> CInt -> Ptr Sort -> IO (Ptr Node)
- var'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- not'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- neg'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- redor'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- redxor'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- redand'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- slice'_ :: Ptr Btor -> Ptr Node -> CUInt -> CUInt -> IO (Ptr Node)
- uext'_ :: Ptr Btor -> Ptr Node -> CUInt -> IO (Ptr Node)
- sext'_ :: Ptr Btor -> Ptr Node -> CUInt -> IO (Ptr Node)
- concat'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- repeat'_ :: Ptr Btor -> Ptr Node -> CUInt -> IO (Ptr Node)
- implies'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- iff'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- eq'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ne'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- cond'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- xor'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- xnor'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- and'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- nand'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- or'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- nor'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sll'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- srl'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sra'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- rol'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ror'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- add'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- inc'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- uaddo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- saddo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sub'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- usubo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ssubo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- dec'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Node)
- mul'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- umulo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- smulo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- udiv'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sdiv'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sdivo'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- urem'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- srem'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- smod'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ult'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- slt'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ulte'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- slte'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ugt'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sgt'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- ugte'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- sgte'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- array'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- read'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- write'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> Ptr Node -> IO (Ptr Node)
- uf'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- param'_ :: Ptr Btor -> Ptr Sort -> Ptr CChar -> IO (Ptr Node)
- getSort'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Sort)
- funGetDomainSort'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Sort)
- funGetCodomainSort'_ :: Ptr Btor -> Ptr Node -> IO (Ptr Sort)
- getFunArity'_ :: Ptr Btor -> Ptr Node -> IO CUInt
- getSymbol'_ :: Ptr Btor -> Ptr Node -> IO (Ptr CChar)
- setSymbol'_ :: Ptr Btor -> Ptr Node -> Ptr CChar -> IO ()
- getWidth'_ :: Ptr Btor -> Ptr Node -> IO CUInt
- getIndexWidth'_ :: Ptr Btor -> Ptr Node -> IO CUInt
- isConst'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isVar'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isArray'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isArrayVar'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isParam'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isBoundParam'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isUf'_ :: Ptr Btor -> Ptr Node -> IO CInt
- isFun'_ :: Ptr Btor -> Ptr Node -> IO CInt
- bvAssignment'_ :: Ptr Btor -> Ptr Node -> IO (Ptr CChar)
- freeBvAssignment'_ :: Ptr Btor -> Ptr CChar -> IO ()
- boolSort'_ :: Ptr Btor -> IO (Ptr Sort)
- bitvecSort'_ :: Ptr Btor -> CUInt -> IO (Ptr Sort)
- arraySort'_ :: Ptr Btor -> Ptr Sort -> Ptr Sort -> IO (Ptr Sort)
- isEqualSort'_ :: Ptr Btor -> Ptr Node -> Ptr Node -> IO CInt
- isArraySort'_ :: Ptr Btor -> Ptr Sort -> IO CInt
- isBitvecSort'_ :: Ptr Btor -> Ptr Sort -> IO CInt
- isFunSort'_ :: Ptr Btor -> Ptr Sort -> IO CInt
- fclose :: FinalizerPtr File
- fopen'_ :: Ptr CChar -> Ptr CChar -> IO (Ptr File)
- dumpBtorNode'_ :: Ptr Btor -> Ptr File -> Ptr Node -> IO ()
- dumpBtor'_ :: Ptr Btor -> Ptr File -> IO ()
- dumpSmt2Node'_ :: Ptr Btor -> Ptr File -> Ptr Node -> IO ()
- dumpSmt2'_ :: Ptr Btor -> Ptr File -> IO ()
Documentation
Status.
Solver option. See https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37
setSatSolver :: Btor -> String -> IO () Source #
Set the SAT solver to use.
Currently supported: Lingeling
, PicoSAT
, and MiniSAT
.
Returns non-zero value if setting the SAT solver was successful.
failed :: Btor -> Node -> IO Bool Source #
Determine if assumption node
is a failed assumption.
Failed assumptions are those assumptions, that force an input formula to become unsatisfiable.
fixateAssumptions :: Btor -> IO () Source #
Add all assumptions as assertions.
resetAssumptions :: Btor -> IO () Source #
Resets all added assumptions.
limitedSat :: Btor -> Int -> Int -> IO Status Source #
Solve an input formula and limit the search by the number of lemmas generated and the number of conflicts encountered by the underlying SAT solver.
An input formula is defined by constraints added via assert
.
You can guide the search for a solution to an input formula by making
assumptions via assume
.
Returns Sat
if the input formula is satisfiable (under possibly given
assumptions), Usat
if the instance is unsatisfiable, and Unknown
if the
instance could not be solved within given limits.
const :: Btor -> String -> IO Node Source #
Create bit vector constant representing the bit vector bits
.
constd :: Btor -> Sort -> String -> IO Node Source #
Create bit vector constant representing the decimal number str
.
consth :: Btor -> Sort -> String -> IO Node Source #
Create bit vector constant representing the hexadecimal number str
.
true :: Btor -> IO Node Source #
Create constant true. This is represented by the bit vector constant one with bit width one.
ones :: Btor -> Sort -> IO Node Source #
Create bit vector constant of sort sort
, where each bit is set to one.
unsignedInt :: Btor -> CUInt -> Sort -> IO Node Source #
Create bit vector constant representing the unsigned integer u
of
sort sort
.
The constant is obtained by either truncating bits or by unsigned extension (padding with zeroes).
int :: Btor -> CInt -> Sort -> IO Node Source #
Create bit vector constant representing the signed integer i
of sort
sort
.
The constant is obtained by either truncating bits or by signed extension (padding with ones).
var :: Btor -> Sort -> String -> IO Node Source #
Create a bit vector variable of sort sort
.
The name must be unique.
redor :: Btor -> Node -> IO Node Source #
Create *or* reduction of node node
.
All bits of node node
are combined by a Boolean *or*.
redxor :: Btor -> Node -> IO Node Source #
Create *xor* reduction of node node
.
All bits of node
are combined by a Boolean *xor*.
redand :: Btor -> Node -> IO Node Source #
Create *and* reduction of node node
.
All bits of node
are combined by a Boolean *and*.
slice :: Btor -> Node -> CUInt -> CUInt -> IO Node Source #
Create a bit vector slice of node
from index upper
to index lower
.
uext :: Btor -> Node -> CUInt -> IO Node Source #
Create unsigned extension.
The bit vector node
is padded with width
* zeroes.
sext :: Btor -> Node -> CUInt -> IO Node Source #
Create signed extension.
The bit vector node
is padded with width
bits where the value
depends on the value of the most significant bit of node n
.
eq :: Btor -> Node -> Node -> IO Node Source #
Create bit vector or array equality.
Both operands are either bit vectors with the same bit width or arrays of the same type.
ne :: Btor -> Node -> Node -> IO Node Source #
Create bit vector or array inequality.
Both operands are either bit vectors with the same bit width or arrays of the same type.
cond :: Btor -> Node -> Node -> Node -> IO Node Source #
Create an if-then-else.
If condition n_cond
is true, then n_then
is returned, else n_else
is returned.
Nodes n_then
and n_else
must be either both arrays or both bit vectors.
sll :: Btor -> Node -> Node -> IO Node Source #
Create a logical shift left.
Given node n1
, the value it represents is the number of zeroes shifted
into node n0
from the right.
srl :: Btor -> Node -> Node -> IO Node Source #
Create a logical shift right.
Given node n1
, the value it represents is the number of zeroes shifted
into node n0
from the left.
sra :: Btor -> Node -> Node -> IO Node Source #
Create an arithmetic shift right.
Analogously to srl
, but whether zeroes or ones are shifted in depends on
the most significant bit of n0
.
rol :: Btor -> Node -> Node -> IO Node Source #
Create a rotate right.
Given bit vector node n1
, the value it represents is the number of bits by
which node n0
is rotated to the right.
Create a rotate left.
Given bit vector node n1
, the value it represents is the number of bits
by which node n0
is rotated to the left.
inc :: Btor -> Node -> IO Node Source #
Create bit vector expression that increments bit vector node
by one.
uaddo :: Btor -> Node -> Node -> IO Node Source #
Create an unsigned bit vector addition overflow detection.
saddo :: Btor -> Node -> Node -> IO Node Source #
Create a signed bit vector addition overflow detection.
usubo :: Btor -> Node -> Node -> IO Node Source #
Create an unsigned bit vector subtraction overflow detection.
ssubo :: Btor -> Node -> Node -> IO Node Source #
Create a signed bit vector subtraction overflow detection.
dec :: Btor -> Node -> IO Node Source #
Create bit vector expression that decrements bit vector node
by one.
umulo :: Btor -> Node -> Node -> IO Node Source #
Create an unsigned bit vector multiplication overflow detection.
sdivo :: Btor -> Node -> Node -> IO Node Source #
Create a signed bit vector division overflow detection.
smod :: Btor -> Node -> Node -> IO Node Source #
Create a, signed remainder where its sign matches the sign of the divisor.
array :: Btor -> Sort -> String -> IO Node Source #
Create a one-dimensional bit vector array with sort sort
.
The name must be unique.
write :: Btor -> Node -> Node -> Node -> IO Node Source #
Create a write on array n_array
at position n_index
with value
n_value
.
The array is updated at exactly one position, all other elements remain
unchanged. The bit width of n_index
must be the same as the bit width of
the indices of n_array
. The bit width of n_value
must be the same as
the bit width of the elements of n_array
.
uf :: Btor -> Sort -> String -> IO Node Source #
Create an uninterpreted function with sort sort
.
The name must be unique.
param :: Btor -> Sort -> String -> IO Node Source #
Create function parameter of sort sort
.
This kind of node is used to create parameterized expressions, which are used to create functions. Once a parameter is bound to a function, it cannot be re-used in other functions.
fun :: Btor -> [Node] -> Node -> IO Node Source #
Create a function with body node
parameterized over parameters
param_nodes
.
This kind of node is similar to macros in the SMT-LIB standard 2.0.
Note that as soon as a parameter is bound to a function, it can not be
reused in other functions.
Call a function via apply
.
apply :: Btor -> [Node] -> Node -> IO Node Source #
Create a function application on function n_fun
with arguments
arg_nodes
.
withNodes :: [Node] -> ([Ptr Node] -> IO a) -> IO a Source #
Helper function for executing list of Nodes.
funGetDomainSort :: Btor -> Node -> IO Sort Source #
Get the domain sort of given function node node.
funGetCodomainSort :: Btor -> Node -> IO Sort Source #
Get the codomain sort of given function node node.
getWidth :: Btor -> Node -> IO CUInt Source #
Get the bit width of an expression.
If the expression is an array, it returns the bit width of the array elements. If the expression is a function, it returns the bit width of the function's return value.
isBoundParam :: Btor -> Node -> IO Bool Source #
Determine if given parameter node is bound by a function.
funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int) Source #
Check if sorts of given arguments matches the function signature.
Returns Nothing
if all sorts are correct; otherwise it returns the
position of the incorrect argument.
freeBvAssignment :: Btor -> String -> IO () Source #
Free an assignment string for bit vectors. TODO: we should change bv_assignment to return a ModelString and use free to actually free the assignments. We're very leaky right now.
withSorts :: [Sort] -> ([Ptr Sort] -> IO a) -> IO a Source #
Helper function for executing list of Sorts.
isEqualSort :: Btor -> Node -> Node -> IO Bool Source #
Determine if n0
and n1
have the same sort or not.
dumpBtorNode :: Btor -> File -> Node -> IO () Source #
Recursively dump node
to file in BTOR_ format.