Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module exposes a DSL for writing symbolic computations atop the Boolector SMT solver. The monadic interface manages the interface to Boolector, caches already created sorts and variables, etc. A Boolector computation should not be shared between threads.
Consider, the simple example from the Z3 tutorial https://rise4fun.com/z3/tutorialcontent/guide#h23 written in SMT LIB format:
(declare-fun f (Int) Int) (declare-fun a () Int) ; a is a constant (declare-const b Int) ; syntax sugar for (declare-fun b () Int) (assert (> a 20)) (assert (> b a)) (assert (= (f 10) 1)) (check-sat) (get-model)
With this library you can write the same program in Haskell:
main :: IO () main = do bs <- B.newBoolectorState
Nothing B.evalBoolector
bs $ do -- Create sorts: u32 <- B.bitvecSort
32 fSort <- B.funSort
[u32] u32 -- Create variables f, a, and b: f <- B.uf
fSort "f" a <- B.var
u32 "a" b <- B.var
u32 "b" -- Create several constants: c20 <- B.unsignedInt
20 u32 c10 <- B.unsignedInt
10 u32 c1 <- B.one
u32 -- Make assertions: B.assert
=<< B.ugt
a c20 B.assert
=<< B.ugt
b a res <- B.apply
[c10] f B.assert
=<< B.eq
res c1 -- Check satisfiability: B.Sat
<- B.sat
-- Get model: ma <- B.unsignedBvAssignment
a mb <- B.unsignedBvAssignment
b -- Check model: assert (ma == 21) $ return () assert (mb == 22) $ return ()
The API is inspired by the Z3 Haskell API http://hackage.haskell.org/package/z3.
Synopsis
- data Boolector a
- class MonadIO m => MonadBoolector m where
- getBoolectorState :: m BoolectorState
- putBoolectorState :: BoolectorState -> m ()
- evalBoolector :: BoolectorState -> Boolector a -> IO a
- runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState)
- data BoolectorState
- newBoolectorState :: Maybe Integer -> IO BoolectorState
- createDefaultSorts :: Boolector ()
- 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
- setOpt :: MonadBoolector m => Option -> Word32 -> m ()
- getOpt :: MonadBoolector m => Option -> m Word32
- data SatSolver
- setSatSolver :: MonadBoolector m => SatSolver -> m ()
- data Node
- sat :: MonadBoolector m => m Status
- limitedSat :: MonadBoolector m => Int -> Int -> m Status
- simplify :: MonadBoolector m => m Status
- data Status
- assert :: MonadBoolector m => Node -> m ()
- assume :: MonadBoolector m => Node -> m ()
- failed :: MonadBoolector m => Node -> m Bool
- fixateAssumptions :: MonadBoolector m => m ()
- resetAssumptions :: MonadBoolector m => m ()
- push :: MonadBoolector m => Word32 -> m ()
- pop :: MonadBoolector m => Word32 -> m ()
- var :: MonadBoolector m => Sort -> String -> m Node
- const :: MonadBoolector m => String -> m Node
- constd :: MonadBoolector m => Sort -> String -> m Node
- consth :: MonadBoolector m => Sort -> String -> m Node
- bool :: MonadBoolector m => Bool -> m Node
- true :: MonadBoolector m => m Node
- false :: MonadBoolector m => m Node
- zero :: MonadBoolector m => Sort -> m Node
- one :: MonadBoolector m => Sort -> m Node
- ones :: MonadBoolector m => Sort -> m Node
- unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node
- signedInt :: MonadBoolector m => Integer -> Sort -> m Node
- array :: MonadBoolector m => Sort -> String -> m Node
- fun :: MonadBoolector m => [Node] -> Node -> m Node
- uf :: MonadBoolector m => Sort -> String -> m Node
- param :: MonadBoolector m => Sort -> String -> m Node
- forall :: MonadBoolector m => [Node] -> Node -> m Node
- exists :: MonadBoolector m => [Node] -> Node -> m Node
- implies :: MonadBoolector m => Node -> Node -> m Node
- iff :: MonadBoolector m => Node -> Node -> m Node
- cond :: MonadBoolector m => Node -> Node -> Node -> m Node
- eq :: MonadBoolector m => Node -> Node -> m Node
- ne :: MonadBoolector m => Node -> Node -> m Node
- not :: MonadBoolector m => Node -> m Node
- neg :: MonadBoolector m => Node -> m Node
- redor :: MonadBoolector m => Node -> m Node
- redxor :: MonadBoolector m => Node -> m Node
- redand :: MonadBoolector m => Node -> m Node
- slice :: MonadBoolector m => Node -> Word32 -> Word32 -> m Node
- uext :: MonadBoolector m => Node -> Word32 -> m Node
- sext :: MonadBoolector m => Node -> Word32 -> m Node
- concat :: MonadBoolector m => Node -> Node -> m Node
- repeat :: MonadBoolector m => Node -> Word32 -> m Node
- xor :: MonadBoolector m => Node -> Node -> m Node
- xnor :: MonadBoolector m => Node -> Node -> m Node
- and :: MonadBoolector m => Node -> Node -> m Node
- nand :: MonadBoolector m => Node -> Node -> m Node
- or :: MonadBoolector m => Node -> Node -> m Node
- nor :: MonadBoolector m => Node -> Node -> m Node
- sll :: MonadBoolector m => Node -> Node -> m Node
- srl :: MonadBoolector m => Node -> Node -> m Node
- sra :: MonadBoolector m => Node -> Node -> m Node
- rol :: MonadBoolector m => Node -> Node -> m Node
- ror :: MonadBoolector m => Node -> Node -> m Node
- add :: MonadBoolector m => Node -> Node -> m Node
- inc :: Node -> Boolector Node
- sub :: MonadBoolector m => Node -> Node -> m Node
- dec :: MonadBoolector m => Node -> m Node
- mul :: MonadBoolector m => Node -> Node -> m Node
- udiv :: MonadBoolector m => Node -> Node -> m Node
- sdiv :: MonadBoolector m => Node -> Node -> m Node
- urem :: MonadBoolector m => Node -> Node -> m Node
- srem :: MonadBoolector m => Node -> Node -> m Node
- smod :: MonadBoolector m => Node -> Node -> m Node
- uaddo :: MonadBoolector m => Node -> Node -> m Node
- saddo :: MonadBoolector m => Node -> Node -> m Node
- usubo :: MonadBoolector m => Node -> Node -> m Node
- ssubo :: MonadBoolector m => Node -> Node -> m Node
- umulo :: MonadBoolector m => Node -> Node -> m Node
- smulo :: MonadBoolector m => Node -> Node -> m Node
- sdivo :: MonadBoolector m => Node -> Node -> m Node
- ult :: MonadBoolector m => Node -> Node -> m Node
- slt :: MonadBoolector m => Node -> Node -> m Node
- ulte :: MonadBoolector m => Node -> Node -> m Node
- slte :: MonadBoolector m => Node -> Node -> m Node
- ugt :: MonadBoolector m => Node -> Node -> m Node
- sgt :: MonadBoolector m => Node -> Node -> m Node
- ugte :: MonadBoolector m => Node -> Node -> m Node
- sgte :: MonadBoolector m => Node -> Node -> m Node
- read :: MonadBoolector m => Node -> Node -> m Node
- write :: MonadBoolector m => Node -> Node -> Node -> m Node
- apply :: MonadBoolector m => [Node] -> Node -> m Node
- getSort :: MonadBoolector m => Node -> m Sort
- funGetDomainSort :: MonadBoolector m => Node -> m Sort
- funGetCodomainSort :: MonadBoolector m => Node -> m Sort
- funGetArity :: MonadBoolector m => Node -> m Word
- getSymbol :: MonadBoolector m => Node -> m (Maybe String)
- setSymbol :: MonadBoolector m => Node -> String -> m ()
- getWidth :: MonadBoolector m => Node -> m Word32
- getIndexWidth :: MonadBoolector m => Node -> m Word32
- isConst :: MonadBoolector m => Node -> m Bool
- isVar :: MonadBoolector m => Node -> m Bool
- isArray :: MonadBoolector m => Node -> m Bool
- isArrayVar :: MonadBoolector m => Node -> m Bool
- isParam :: MonadBoolector m => Node -> m Bool
- isBoundParam :: MonadBoolector m => Node -> m Bool
- isUf :: MonadBoolector m => Node -> m Bool
- isFun :: MonadBoolector m => Node -> m Bool
- bvAssignment :: MonadBoolector m => Node -> m String
- unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
- signedBvAssignment :: MonadBoolector m => Node -> m Integer
- boolAssignment :: MonadBoolector m => Node -> m Bool
- boolConst :: MonadBoolector m => Node -> m (Maybe Bool)
- signedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
- unsignedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
- data Sort
- data SortTy
- sortTy :: Sort -> SortTy
- boolSort :: Boolector Sort
- bitvecSort :: MonadBoolector m => Word -> m Sort
- funSort :: MonadBoolector m => [Sort] -> Sort -> m Sort
- arraySort :: MonadBoolector m => Sort -> Sort -> m Sort
- isEqualSort :: MonadBoolector m => Node -> Node -> m Bool
- isArraySort :: Sort -> Bool
- isBoolSort :: Sort -> Bool
- isBitvecSort :: Sort -> Bool
- isFunSort :: Sort -> Bool
- funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)
- dump :: MonadBoolector m => DumpFormat -> FilePath -> m ()
- dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m ()
- dumpToString :: MonadBoolector m => DumpFormat -> m String
- dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String
- data DumpFormat
Boolector monadic computations
Bolector monad, keeping track of underlying solver state.
Instances
Monad Boolector Source # | |
Functor Boolector Source # | |
MonadFail Boolector Source # | |
Applicative Boolector Source # | |
MonadIO Boolector Source # | |
MonadBoolector Boolector Source # | |
Defined in Boolector | |
MonadState BoolectorState Boolector Source # | |
Defined in Boolector get :: Boolector BoolectorState # put :: BoolectorState -> Boolector () # state :: (BoolectorState -> (a, BoolectorState)) -> Boolector a # |
class MonadIO m => MonadBoolector m where Source #
Type class for Monads that wish to perform symbolic computations.
getBoolectorState :: m BoolectorState Source #
Get the Boolector state.
putBoolectorState :: BoolectorState -> m () Source #
Put the Boolector state.
Instances
MonadBoolector Boolector Source # | |
Defined in Boolector |
evalBoolector :: BoolectorState -> Boolector a -> IO a Source #
Evaluate a Boolector action with a given configurations.
runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState) Source #
Like evalBoolector
, but take an explicit starting BoolectorState, and
return the final BoolectorState
Boolector state
data BoolectorState Source #
Solver state and cache
Instances
MonadState BoolectorState Boolector Source # | |
Defined in Boolector get :: Boolector BoolectorState # put :: BoolectorState -> Boolector () # state :: (BoolectorState -> (a, BoolectorState)) -> Boolector a # |
newBoolectorState :: Maybe Integer -> IO BoolectorState Source #
Create new Boolector state with optional timeout. By default, we enable support for model generation and incremental solving.
createDefaultSorts :: Boolector () Source #
Create some default, sane sorts.
Options and configurations
Solver option. See https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37
Which sat solver to use.
setSatSolver :: MonadBoolector m => SatSolver -> m () Source #
Set the SAT solver to use. Returns True
if sucessfull.
SAT/SMT queries
Node data type wrapping the underlying Boolector node with a show string.
sat :: MonadBoolector m => m Status Source #
Solve an input formula.
:: MonadBoolector m | |
=> Int | Limit for lemmas on demand (-1 unlimited). |
-> Int | Conflict limit for SAT solver (-1 unlimited). |
-> m Status |
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.
simplify :: MonadBoolector m => m Status Source #
Simplify current input formula.
Status.
Assert and assume
assert :: MonadBoolector m => Node -> m () Source #
Add a constraint.
assume :: MonadBoolector m => Node -> m () Source #
Add an assumption.
failed :: MonadBoolector m => Node -> m Bool Source #
Determine if assumption node is a failed assumption.
fixateAssumptions :: MonadBoolector m => m () Source #
Add all assumptions as assertions.
resetAssumptions :: MonadBoolector m => m () Source #
Resets all added assumptions.
push :: MonadBoolector m => Word32 -> m () Source #
Push new context levels.
pop :: MonadBoolector m => Word32 -> m () Source #
Pop context levels.
Variables and constants
var :: MonadBoolector m => Sort -> String -> m Node Source #
Create a bit vector variable of sort sort
.
const :: MonadBoolector m => String -> m Node Source #
Create bit vector constant representing the bit vector bits
.
constd :: MonadBoolector m => Sort -> String -> m Node Source #
Create bit vector constant representing the decimal number str
.
consth :: MonadBoolector m => Sort -> String -> m Node Source #
Create bit vector constant representing the hexadecimal number str
.
Booleans
true :: MonadBoolector m => m Node Source #
Create constant true. This is represented by the bit vector constant one with bit width one.
false :: MonadBoolector m => m Node Source #
Create bit vector constant zero with bit width one.
Bit-vectors
ones :: MonadBoolector m => Sort -> m Node Source #
Create bit vector constant of sort sort
, where each bit is set to one.
unsignedInt :: MonadBoolector m => Integer -> Sort -> m 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).
signedInt :: MonadBoolector m => Integer -> Sort -> m 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 :: MonadBoolector m => Sort -> String -> m Node Source #
Create a one-dimensional bit vector array with sort sort
.
The name must be unique.
Functions
:: MonadBoolector m | |
=> [Node] | Parameters of function. |
-> Node | Function body parameterized over |
-> m Node |
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 :: MonadBoolector m => Sort -> String -> m Node Source #
Create an uninterpreted function with sort sort
.
The name must be unique.
Parameters
param :: MonadBoolector m => Sort -> String -> m 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
:: MonadBoolector m | |
=> [Node] | Quantified variables (create with |
-> Node | Term where variables may occur. (Cannot contain functions.) |
-> m Node |
Create a universally quantified term.
:: MonadBoolector m | |
=> [Node] | Quantified variables (create with |
-> Node | Term where variables may occur. (Cannot contain functions.) |
-> m Node |
Create an existentially quantifed term.
Operations
Implications and conditionals
:: MonadBoolector m | |
=> Node | Condition |
-> Node | Then node |
-> Node | Else node |
-> m Node |
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 :: MonadBoolector m => Node -> Node -> m 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 :: MonadBoolector m => Node -> Node -> m 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 :: MonadBoolector m => Node -> m Node Source #
Create *or* reduction of node node
.
All bits of node node
are combined by a Boolean *or*.
redxor :: MonadBoolector m => Node -> m Node Source #
Create *xor* reduction of node node
.
All bits of node
are combined by a Boolean *xor*.
redand :: MonadBoolector m => Node -> m Node Source #
Create *and* reduction of node node
.
All bits of node
are combined by a Boolean *and*.
:: MonadBoolector m | |
=> Node | Bit vector node. |
-> Word32 | Upper index which must be greater than or equal to zero, and less than the bit width of |
-> Word32 | Lower index which must be greater than or equal to zero, and less than or equal to |
-> m Node |
Create a bit vector slice of node
from index upper
to index lower
.
uext :: MonadBoolector m => Node -> Word32 -> m Node Source #
Create unsigned extension.
The bit vector node
is padded with width
* zeroes.
sext :: MonadBoolector m => Node -> Word32 -> m 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
.
concat :: MonadBoolector m => Node -> Node -> m Node Source #
Create the concatenation of two bit vectors.
repeat :: MonadBoolector m => Node -> Word32 -> m Node Source #
Create n
concatenations of a given node node
.
Bit-wise operations
:: MonadBoolector m | |
=> Node | First bit vector operand where the bit width is a power of two and greater than 1. |
-> Node | Second bit vector operand with bit width log2 of the bit width of |
-> m Node |
Create a logical shift left.
Given node n1
, the value it represents is the number of zeroes shifted
into node n0
from the right.
:: MonadBoolector m | |
=> Node | First bit vector operand where the bit width is a power of two and greater than 1. |
-> Node | Second bit vector operand with bit width log2 of the bit width of |
-> m Node |
Create a logical shift right.
Given node n1
, the value it represents is the number of zeroes shifted
into node n0
from the left.
:: MonadBoolector m | |
=> Node | First bit vector operand where the bit width is a power of two and greater than 1. |
-> Node | Second bit vector operand with bit width log2 of the bit width of |
-> m Node |
Create an arithmetic shift right.
Analogously to srl
, but whether zeroes or ones are shifted in depends on
the most significant bit of n0
.
:: MonadBoolector m | |
=> Node | First bit vector operand where the bit width is a power of two and greater than 1. |
-> Node | Second bit vector operand with bit width log2 of the bit width of |
-> m Node |
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.
:: MonadBoolector m | |
=> Node | First bit vector operand where the bit width is a power of two and greater than 1. |
-> Node | Second bit vector operand with bit width log2 of the bit width of |
-> m Node |
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
inc :: Node -> Boolector Node Source #
Create bit vector expression that increments bit vector node
by one.
dec :: MonadBoolector m => Node -> m Node Source #
Create bit vector expression that decrements bit vector node
by one.
smod :: MonadBoolector m => Node -> Node -> m Node Source #
Create a, signed remainder where its sign matches the sign of the divisor.
Overflow detection
uaddo :: MonadBoolector m => Node -> Node -> m Node Source #
Create an unsigned bit vector addition overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
saddo :: MonadBoolector m => Node -> Node -> m Node Source #
Create a signed bit vector addition overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
usubo :: MonadBoolector m => Node -> Node -> m Node Source #
Create an unsigned bit vector subtraction overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
ssubo :: MonadBoolector m => Node -> Node -> m Node Source #
Create a signed bit vector subtraction overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
umulo :: MonadBoolector m => Node -> Node -> m Node Source #
Create an unsigned bit vector multiplication overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
smulo :: MonadBoolector m => Node -> Node -> m Node Source #
Create signed multiplication overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
sdivo :: MonadBoolector m => Node -> Node -> m Node Source #
Create a signed bit vector division overflow detection. Returns bit vector with bit-width one, which indicates if the operation overflows.
Comparison operations
ugte :: MonadBoolector m => Node -> Node -> m Node Source #
Create an unsigned greater than or equal.
Array operations
:: MonadBoolector m | |
=> Node | Array operand. |
-> Node | Bit vector index. The bit width of |
-> m Node |
Create a read on array n_array
at position n_index
.
:: MonadBoolector m | |
=> Node | Array operand. |
-> Node | Bit vector index. |
-> Node | Bit vector value. |
-> m Node |
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
:: MonadBoolector m | |
=> [Node] | Arguments to be applied. |
-> Node | Number of arguments to be applied. |
-> m Node |
Create a function application on function n_fun
with arguments
arg_nodes
.
Accessors
getSort :: MonadBoolector m => Node -> m Sort Source #
Get the sort of given node
. The result does not have to be released.
funGetDomainSort :: MonadBoolector m => Node -> m Sort Source #
Get the domain sort of given function node node
.
The result does not have to be released.
funGetCodomainSort :: MonadBoolector m => Node -> m Sort Source #
Get the codomain sort of given function node node
.
The result does not have to be released.
funGetArity :: MonadBoolector m => Node -> m Word Source #
Get the arity of function node.
getWidth :: MonadBoolector m => Node -> m Word32 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.
getIndexWidth :: MonadBoolector m => Node -> m Word32 Source #
Get the bit width of indices of n_array
.
isVar :: MonadBoolector m => Node -> m Bool Source #
Determine if given node is a bit vector variable.
isArrayVar :: MonadBoolector m => Node -> m Bool Source #
Determine if given node is an array node.
isBoundParam :: MonadBoolector m => Node -> m Bool Source #
Determine if given parameter node is bound by a function.
isUf :: MonadBoolector m => Node -> m Bool Source #
Determine if given node is an uninterpreted function node.
Models
bvAssignment :: MonadBoolector m => Node -> m String Source #
Generate an assignment string for bit vector expression if boolector_sat has returned BOOLECTOR_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 freeBvAssignment
.
unsignedBvAssignment :: MonadBoolector m => Node -> m Integer Source #
Get unsigned integer value from model.
signedBvAssignment :: MonadBoolector m => Node -> m Integer Source #
Get signed integer value from model.
boolAssignment :: MonadBoolector m => Node -> m Bool Source #
Get Boolean value from model.
Constant nodes
boolConst :: MonadBoolector m => Node -> m (Maybe Bool) Source #
Get the bool value of a constant node if it is constant.
signedBvConst :: MonadBoolector m => Node -> m (Maybe Integer) Source #
Get the signed integer value of a constant node if it is constant.
unsignedBvConst :: MonadBoolector m => Node -> m (Maybe Integer) Source #
Get the unsigned integer value of a constant node if it is constant.
Sorts
Sort wraps the udnerlying Boolector sort with a showable type.
Type of sorts, used to keep track of sorts without having to go back into C-land.
bitvecSort :: MonadBoolector m => Word -> m Sort Source #
Create bit vector sort of bit width width
.
Accessors
isEqualSort :: MonadBoolector m => Node -> Node -> m Bool Source #
Determine if n0
and n1
have the same sort or not.
isArraySort :: Sort -> Bool Source #
Determine if sort
is an array sort.
isBoolSort :: Sort -> Bool Source #
Determine if sort
is a bool sort.
isBitvecSort :: Sort -> Bool Source #
Determine if sort
is a bit-vector sort.
funSortCheck :: MonadBoolector m => [Node] -> Node -> m (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
dump :: MonadBoolector m => DumpFormat -> FilePath -> m () Source #
Dump formula to file in BTOR or SMT-LIB v2 format.
dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m () Source #
Recursively dump node
to file in BTOR or SMT-LIB v2 format.
dumpToString :: MonadBoolector m => DumpFormat -> m String Source #
Same as dump
, but returns string.
TODO: this is super slow, we should request feature from boolector.
dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String Source #
Same as dumpNode
, but returns string.
TODO: this is super slow, we should request feature from boolector.
data DumpFormat Source #
Output dump format.
Instances
Eq DumpFormat Source # | |
Defined in Boolector (==) :: DumpFormat -> DumpFormat -> Bool # (/=) :: DumpFormat -> DumpFormat -> Bool # | |
Show DumpFormat Source # | |
Defined in Boolector showsPrec :: Int -> DumpFormat -> ShowS # show :: DumpFormat -> String # showList :: [DumpFormat] -> ShowS # |