Boolector.Foreign

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.

Boolector state, options and configurations

data Btor

Boolector instances.

Instances

Eq Btor

Methods

(==) :: Btor -> Btor -> Bool

(/=) :: Btor -> Btor -> Bool

Ord Btor

Methods

compare :: Btor -> Btor -> Ordering

(<) :: Btor -> Btor -> Bool

(<=) :: Btor -> Btor -> Bool

(>) :: Btor -> Btor -> Bool

(>=) :: Btor -> Btor -> Bool

max :: Btor -> Btor -> Btor

min :: Btor -> Btor -> Btor

new :: IO Btor

Create a new instance of Boolector.

data Option

Solver option. See https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37

Constructors

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

Instances

Enum Option

Methods

succ :: Option -> Option

pred :: Option -> Option

toEnum :: Int -> Option

fromEnum :: Option -> Int

enumFrom :: Option -> [Option]

enumFromThen :: Option -> Option -> [Option]

enumFromTo :: Option -> Option -> [Option]

enumFromThenTo :: Option -> Option -> Option -> [Option]

Eq Option

Methods

(==) :: Option -> Option -> Bool

(/=) :: Option -> Option -> Bool

Ord Option

Methods

compare :: Option -> Option -> Ordering

(<) :: Option -> Option -> Bool

(<=) :: Option -> Option -> Bool

(>) :: Option -> Option -> Bool

(>=) :: Option -> Option -> Bool

max :: Option -> Option -> Option

min :: Option -> Option -> Option

Show Option

Methods

showsPrec :: Int -> Option -> ShowS

show :: Option -> String

showList :: [Option] -> ShowS

setOpt :: Btor -> Option -> CUInt -> IO ()

Set option. See btortypes.h

getOpt :: Btor -> Option -> IO CUInt

Get the current value of an option.

setSatSolver :: Btor -> String -> IO ()

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

data Node

AST node.

Instances

Eq Node

Methods

(==) :: Node -> Node -> Bool

(/=) :: Node -> Node -> Bool

Ord Node

Methods

compare :: Node -> Node -> Ordering

(<) :: Node -> Node -> Bool

(<=) :: Node -> Node -> Bool

(>) :: Node -> Node -> Bool

(>=) :: Node -> Node -> Bool

max :: Node -> Node -> Node

min :: Node -> Node -> Node

sat :: Btor -> IO Status

Solve an input formula.

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.

limitedSat :: Btor -> Int -> Int -> IO 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.

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.

simplify :: Btor -> IO Status

Simplify current input formula.

data Status

Status.

Constructors

Unknown

Sat

Unsat

Instances

Enum Status

Methods

succ :: Status -> Status

pred :: Status -> Status

toEnum :: Int -> Status

fromEnum :: Status -> Int

enumFrom :: Status -> [Status]

enumFromThen :: Status -> Status -> [Status]

enumFromTo :: Status -> Status -> [Status]

enumFromThenTo :: Status -> Status -> Status -> [Status]

Eq Status

Methods

(==) :: Status -> Status -> Bool

(/=) :: Status -> Status -> Bool

Ord Status

Methods

compare :: Status -> Status -> Ordering

(<) :: Status -> Status -> Bool

(<=) :: Status -> Status -> Bool

(>) :: Status -> Status -> Bool

(>=) :: Status -> Status -> Bool

max :: Status -> Status -> Status

min :: Status -> Status -> Status

Show Status

Methods

showsPrec :: Int -> Status -> ShowS

show :: Status -> String

showList :: [Status] -> ShowS

Assert and assume

assert :: Btor -> Node -> IO ()

Add a constraint.

assume :: Btor -> Node -> IO ()

Add an assumption.

failed :: Btor -> Node -> IO Bool

Determine if assumption node is a failed assumption.

Failed assumptions are those assumptions, that force an input formula to become unsatisfiable.

fixateAssumptions :: Btor -> IO ()

Add all assumptions as assertions.

resetAssumptions :: Btor -> IO ()

Resets all added assumptions.

push :: Btor -> CUInt -> IO ()

Push new context levels.

pop :: Btor -> CUInt -> IO ()

Pop context levels.

Variables and constants

var :: Btor -> Sort -> String -> IO Node

Create a bit vector variable of sort sort.

The name must be unique.

const :: Btor -> String -> IO Node

Create bit vector constant representing the bit vector bits.

constd :: Btor -> Sort -> String -> IO Node

Create bit vector constant representing the decimal number str.

consth :: Btor -> Sort -> String -> IO Node

Create bit vector constant representing the hexadecimal number str.

Booleans

true :: Btor -> IO Node

Create constant true. This is represented by the bit vector constant one with bit width one.

false :: Btor -> IO Node

Create bit vector constant zero with bit width one.

Bit-vectors

zero :: Btor -> Sort -> IO Node

Create bit vector constant zero of sort sort.

one :: Btor -> Sort -> IO Node

Create bit vector constant one of sort sort.

ones :: Btor -> Sort -> IO Node

Create bit vector constant of sort sort, where each bit is set to one.

unsignedInt :: Btor -> CUInt -> Sort -> IO Node

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

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

Create a one-dimensional bit vector array with sort sort.

The name must be unique.

Functions

fun :: Btor -> [Node] -> Node -> IO 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 :: Btor -> Sort -> String -> IO Node

Create an uninterpreted function with sort sort.

The name must be unique.

Parameters

param :: Btor -> Sort -> String -> IO Node

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

forall :: Btor -> [Node] -> Node -> IO Node

Create a universally quantified term.

exists :: Btor -> [Node] -> Node -> IO Node

Create an existentially quantifed term.

Operations

Implications and conditionals

implies :: Btor -> Node -> Node -> IO Node

Create boolean implication.

iff :: Btor -> Node -> Node -> IO Node

Create Boolean equivalence.

cond :: Btor -> Node -> Node -> Node -> IO 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 :: Btor -> Node -> Node -> IO Node

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

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

not :: Btor -> Node -> IO Node

Create the one's complement of bit vector node.

neg :: Btor -> Node -> IO Node

Create the two's complement of bit vector node.

redor :: Btor -> Node -> IO Node

Create *or* reduction of node node.

All bits of node node are combined by a Boolean *or*.

redxor :: Btor -> Node -> IO Node

Create *xor* reduction of node node.

All bits of node are combined by a Boolean *xor*.

redand :: Btor -> Node -> IO Node

Create *and* reduction of node node.

All bits of node are combined by a Boolean *and*.

slice :: Btor -> Node -> CUInt -> CUInt -> IO Node

Create a bit vector slice of node from index upper to index lower.

uext :: Btor -> Node -> CUInt -> IO Node

Create unsigned extension.

The bit vector node is padded with width * zeroes.

sext :: Btor -> Node -> CUInt -> IO Node

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 :: Btor -> Node -> Node -> IO Node

Create the concatenation of two bit vectors.

repeat :: Btor -> Node -> CUInt -> IO Node

Create n concatenations of a given node node.

Bit-wise operations

xor :: Btor -> Node -> Node -> IO Node

Create a bit vector *xor*.

xnor :: Btor -> Node -> Node -> IO Node

Create a bit vector *xnor*.

and :: Btor -> Node -> Node -> IO Node

Create a bit vector *and*.

nand :: Btor -> Node -> Node -> IO Node

Create a bit vector *nand*.

or :: Btor -> Node -> Node -> IO Node

Create a bit vector *or*.

nor :: Btor -> Node -> Node -> IO Node

Create a bit vector *nor*.

sll :: Btor -> Node -> Node -> IO 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.

srl :: Btor -> Node -> Node -> IO 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.

sra :: Btor -> Node -> Node -> IO 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.

rol :: Btor -> Node -> Node -> IO 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.

ror :: Btor -> Node -> Node -> IO 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

add :: Btor -> Node -> Node -> IO Node

Create bit vector addition.

uaddo :: Btor -> Node -> Node -> IO Node

Create an unsigned bit vector addition overflow detection.

saddo :: Btor -> Node -> Node -> IO Node

Create a signed bit vector addition overflow detection.

inc :: Btor -> Node -> IO Node

Create bit vector expression that increments bit vector node by one.

sub :: Btor -> Node -> Node -> IO Node

Create a bit vector subtraction.

usubo :: Btor -> Node -> Node -> IO Node

Create an unsigned bit vector subtraction overflow detection.

ssubo :: Btor -> Node -> Node -> IO Node

Create a signed bit vector subtraction overflow detection.

dec :: Btor -> Node -> IO Node

Create bit vector expression that decrements bit vector node by one.

mul :: Btor -> Node -> Node -> IO Node

Create a bitvector multiplication.

umulo :: Btor -> Node -> Node -> IO Node

Create an unsigned bit vector multiplication overflow detection.

smulo :: Btor -> Node -> Node -> IO Node

Create signed multiplication overflow detection.

udiv :: Btor -> Node -> Node -> IO Node

Create unsigned division.

sdiv :: Btor -> Node -> Node -> IO Node

Create signed division.

sdivo :: Btor -> Node -> Node -> IO Node

Create a signed bit vector division overflow detection.

urem :: Btor -> Node -> Node -> IO Node

Create an unsigned remainder.

srem :: Btor -> Node -> Node -> IO Node

Create a signed remainder.

smod :: Btor -> Node -> Node -> IO Node

Create a, signed remainder where its sign matches the sign of the divisor.

Comparison operations

ult :: Btor -> Node -> Node -> IO Node

Create an unsigned less than.

slt :: Btor -> Node -> Node -> IO Node

Create a signed less than.

ulte :: Btor -> Node -> Node -> IO Node

Create an unsigned less than or equal.

slte :: Btor -> Node -> Node -> IO Node

Create a signed less than or equal.

ugt :: Btor -> Node -> Node -> IO Node

Create an unsigned greater than.

sgt :: Btor -> Node -> Node -> IO Node

Create a signed greater than.

ugte :: Btor -> Node -> Node -> IO Node

Create an unsigned greater than or equal.

sgte :: Btor -> Node -> Node -> IO Node

Create a signed greater than or equal.

Array operations

read :: Btor -> Node -> Node -> IO Node

Create a read on array n_array at position n_index.

write :: Btor -> Node -> Node -> Node -> IO 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

apply :: Btor -> [Node] -> Node -> IO Node

Create a function application on function n_fun with arguments arg_nodes.

Accessors

getSort :: Btor -> Node -> IO Sort

Get the sort of given node.

funGetDomainSort :: Btor -> Node -> IO Sort

Get the domain sort of given function node node.

funGetCodomainSort :: Btor -> Node -> IO Sort

Get the codomain sort of given function node node.

getFunArity :: Btor -> Node -> IO CUInt

Get the arity of function node.

getSymbol :: Btor -> Node -> IO (Maybe String)

Get the symbol of an expression.

setSymbol :: Btor -> Node -> String -> IO ()

Set the symbol of an expression.

getWidth :: Btor -> Node -> IO CUInt

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 :: Btor -> Node -> IO CUInt

Get the bit width of indices of n_array.

isConst :: Btor -> Node -> IO Bool

Determine if given node is a constant node.

isVar :: Btor -> Node -> IO Bool

Determine if given node is a bit vector variable.

isArray :: Btor -> Node -> IO Bool

Determine if given node is an array node.

isArrayVar :: Btor -> Node -> IO Bool

Determine if given node is an array node.

isParam :: Btor -> Node -> IO Bool

Determine if given node is a parameter node.

isBoundParam :: Btor -> Node -> IO Bool

Determine if given parameter node is bound by a function.

isUf :: Btor -> Node -> IO Bool

Determine if given node is an uninterpreted function node.

isFun :: Btor -> Node -> IO Bool

Determine if given node is a function node.

Models

bvAssignment :: Btor -> Node -> IO String

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

data Sort

Sort.

Instances

Eq Sort

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Ord Sort

Methods

compare :: Sort -> Sort -> Ordering

(<) :: Sort -> Sort -> Bool

(<=) :: Sort -> Sort -> Bool

(>) :: Sort -> Sort -> Bool

(>=) :: Sort -> Sort -> Bool

max :: Sort -> Sort -> Sort

min :: Sort -> Sort -> Sort

boolSort :: Btor -> IO Sort

Create Boolean sort.

bitvecSort :: Btor -> CUInt -> IO Sort

Create bit vector sort of bit width width.

funSort :: Btor -> [Sort] -> Sort -> IO Sort

Create function sort.

arraySort :: Btor -> Sort -> Sort -> IO Sort

Create array sort.

Accessors

isEqualSort :: Btor -> Node -> Node -> IO Bool

Determine if n0 and n1 have the same sort or not.

isArraySort :: Btor -> Sort -> IO Bool

Determine if sort is an array sort.

isBitvecSort :: Btor -> Sort -> IO Bool

Determine if sort is a bit-vector sort.

isFunSort :: Btor -> Sort -> IO Bool

Determine if sort is a function sort.

funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int)

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 ()

Recursively dump node to file in BTOR_ format.

dumpSmt2Node :: Btor -> File -> Node -> IO ()

Recursively dump node to file in SMT-LIB v2 format.

dumpBtor :: Btor -> File -> IO ()

Dump formula to file in BTOR_ format.

dumpSmt2 :: Btor -> File -> IO ()

Dumps formula to file in SMT-LIB v2 format.

Helpers

withDumpFile :: String -> (File -> IO ()) -> IO ()

Helper for writing to dump file.

withTempDumpFile :: (File -> IO ()) -> IO String

Helper for writing to dump file.

setTerm :: Btor -> (Ptr () -> IO Int) -> IO ()

Set a termination callback.