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.
Synopsis
- data Btor
- new :: IO Btor
- 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_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_QUANT_SYNTH_ITE_COMPLETE
- | OPT_QUANT_FIXSYNTH
- | OPT_NUM_OPTS
- setOpt :: Btor -> Option -> CUInt -> IO ()
- getOpt :: Btor -> Option -> IO CUInt
- setSatSolver :: Btor -> String -> IO ()
- data Node
- sat :: Btor -> IO Status
- limitedSat :: Btor -> Int -> Int -> IO Status
- simplify :: Btor -> IO Status
- data Status
- assert :: Btor -> Node -> IO ()
- assume :: Btor -> Node -> IO ()
- failed :: Btor -> Node -> IO Bool
- fixateAssumptions :: Btor -> IO ()
- resetAssumptions :: Btor -> IO ()
- push :: Btor -> CUInt -> IO ()
- pop :: Btor -> CUInt -> IO ()
- var :: Btor -> Sort -> String -> 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
- array :: Btor -> Sort -> String -> IO Node
- fun :: Btor -> [Node] -> Node -> IO Node
- uf :: Btor -> Sort -> String -> IO Node
- param :: Btor -> Sort -> String -> IO Node
- forall :: Btor -> [Node] -> Node -> IO Node
- exists :: Btor -> [Node] -> Node -> IO Node
- implies :: Btor -> Node -> Node -> IO Node
- iff :: Btor -> Node -> Node -> IO Node
- cond :: Btor -> Node -> Node -> Node -> IO Node
- eq :: Btor -> Node -> Node -> IO Node
- ne :: Btor -> Node -> Node -> 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
- 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
- uaddo :: Btor -> Node -> Node -> IO Node
- saddo :: Btor -> Node -> Node -> IO Node
- inc :: Btor -> 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
- read :: Btor -> Node -> Node -> IO Node
- write :: Btor -> Node -> Node -> Node -> IO Node
- apply :: Btor -> [Node] -> Node -> IO Node
- getSort :: Btor -> Node -> IO Sort
- funGetDomainSort :: Btor -> Node -> IO Sort
- funGetCodomainSort :: Btor -> Node -> IO Sort
- getFunArity :: Btor -> Node -> IO CUInt
- getSymbol :: Btor -> Node -> IO (Maybe String)
- setSymbol :: Btor -> Node -> String -> IO ()
- getBits :: Btor -> Node -> IO String
- 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
- bvAssignment :: Btor -> Node -> IO String
- data Sort
- boolSort :: Btor -> IO Sort
- bitvecSort :: Btor -> CUInt -> IO Sort
- funSort :: Btor -> [Sort] -> Sort -> IO Sort
- 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
- funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int)
- dumpBtorNode :: Btor -> File -> Node -> IO ()
- dumpSmt2Node :: Btor -> File -> Node -> IO ()
- dumpBtor :: Btor -> File -> IO ()
- dumpSmt2 :: Btor -> File -> IO ()
- withDumpFile :: String -> (File -> IO ()) -> IO ()
- withTempDumpFile :: (File -> IO ()) -> IO String
- setTerm :: Btor -> (Ptr () -> IO Int) -> IO ()
Boolector state, options and configurations
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.
SAT/SMT queries
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.
Status.
Assert and assume
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.
Variables and constants
var :: Btor -> Sort -> String -> IO Node Source #
Create a bit vector variable of sort sort
.
The name must be unique.
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
.
Booleans
true :: Btor -> IO Node Source #
Create constant true. This is represented by the bit vector constant one with bit width one.
Bit-vectors
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).
Arrays
array :: Btor -> Sort -> String -> IO Node Source #
Create a one-dimensional bit vector array with sort sort
.
The name must be unique.
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
.
uf :: Btor -> Sort -> String -> IO Node Source #
Create an uninterpreted function with sort sort
.
The name must be unique.
Parameters
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.
Quantified terms
Operations
Implications and conditionals
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.
Equality checking
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.
Bit flipping, extraction, extension, and reduction
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
.
Bit-wise operations
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 left.
Given bit vector node n1
, the value it represents is the number of bits
by which node n0
is rotated to the left.
ror :: 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.
Arithmetic operations
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.
inc :: Btor -> Node -> IO Node Source #
Create bit vector expression that increments bit vector node
by one.
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.
Comparison operations
Array operations
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
.
Function operations
apply :: Btor -> [Node] -> Node -> IO Node Source #
Create a function application on function n_fun
with arguments
arg_nodes
.
Accessors
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.
Models
bvAssignment :: Btor -> Node -> IO String Source #
Generate an assignment string for bit vector expression if
sat
has returned Sat
and model generation has been enabled.
The expression can be an arbitrary bit vector expression which
occurs in an assertion or current assumption. The assignment string has to
be freed by free_bv_assignment
.
TODO: we should change this function to return a ModelString and use free_bv_assignment to actually free the assignments. We're very leaky right now.
Sorts
Accessors
isEqualSort :: Btor -> Node -> Node -> IO Bool Source #
Determine if n0
and n1
have the same sort or not.
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.
Debug dumping
dumpBtorNode :: Btor -> File -> Node -> IO () Source #
Recursively dump node
to file in BTOR_ format.
dumpSmt2Node :: Btor -> File -> Node -> IO () Source #
Recursively dump node
to file in SMT-LIB v2 format.