boolector-0.0.0.7: Haskell bindings for the Boolector SMT solver

Safe HaskellNone
LanguageHaskell2010

Boolector

Contents

Description

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

Boolector monadic computations

data Boolector a Source #

Bolector monad, keeping track of underlying solver state.

Instances
Monad Boolector Source # 
Instance details

Defined in Boolector

Methods

(>>=) :: Boolector a -> (a -> Boolector b) -> Boolector b #

(>>) :: Boolector a -> Boolector b -> Boolector b #

return :: a -> Boolector a #

fail :: String -> Boolector a #

Functor Boolector Source # 
Instance details

Defined in Boolector

Methods

fmap :: (a -> b) -> Boolector a -> Boolector b #

(<$) :: a -> Boolector b -> Boolector a #

Applicative Boolector Source # 
Instance details

Defined in Boolector

Methods

pure :: a -> Boolector a #

(<*>) :: Boolector (a -> b) -> Boolector a -> Boolector b #

liftA2 :: (a -> b -> c) -> Boolector a -> Boolector b -> Boolector c #

(*>) :: Boolector a -> Boolector b -> Boolector b #

(<*) :: Boolector a -> Boolector b -> Boolector a #

MonadIO Boolector Source # 
Instance details

Defined in Boolector

Methods

liftIO :: IO a -> Boolector a #

MonadBoolector Boolector Source # 
Instance details

Defined in Boolector

MonadState BoolectorState Boolector Source # 
Instance details

Defined in Boolector

class MonadIO m => MonadBoolector m where Source #

Type class for Monads that wish to perform symbolic computations.

Minimal complete definition

getBoolectorState, putBoolectorState

Methods

getBoolectorState :: m BoolectorState Source #

Get the Boolector state.

putBoolectorState :: BoolectorState -> m () Source #

Put the Boolector state.

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

newBoolectorState :: Maybe Int -> 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

data Option Source #

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 Source # 
Instance details

Defined in Boolector.Foreign

Eq Option Source # 
Instance details

Defined in Boolector.Foreign

Methods

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

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

Ord Option Source # 
Instance details

Defined in Boolector.Foreign

Show Option Source # 
Instance details

Defined in Boolector.Foreign

setOpt :: MonadBoolector m => Option -> Word32 -> m () Source #

Set option.

getOpt :: MonadBoolector m => Option -> m Word32 Source #

Get option.

data SatSolver Source #

Which sat solver to use.

Constructors

Lingeling 
PicoSAT 
MiniSAT 
Instances
Show SatSolver Source # 
Instance details

Defined in Boolector

setSatSolver :: MonadBoolector m => SatSolver -> m () Source #

Set the SAT solver to use. Returns True if sucessfull.

SAT/SMT queries

data Node Source #

Node data type wrapping the underlying Boolector node with a show string.

Instances
Eq Node Source # 
Instance details

Defined in Boolector

Methods

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

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

Ord Node Source # 
Instance details

Defined in Boolector

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 #

Show Node Source # 
Instance details

Defined in Boolector

Methods

showsPrec :: Int -> Node -> ShowS #

show :: Node -> String #

showList :: [Node] -> ShowS #

sat :: MonadBoolector m => m Status Source #

Solve an input formula.

limitedSat Source #

Arguments

:: 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.

data Status Source #

Status.

Constructors

Unknown 
Sat 
Unsat 
Instances
Enum Status Source # 
Instance details

Defined in Boolector.Foreign

Eq Status Source # 
Instance details

Defined in Boolector.Foreign

Methods

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

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

Ord Status Source # 
Instance details

Defined in Boolector.Foreign

Show Status Source # 
Instance details

Defined in Boolector.Foreign

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

bool :: MonadBoolector m => Bool -> m Node Source #

Like true and false

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

zero :: MonadBoolector m => Sort -> m Node Source #

Create bit vector constant zero of sort sort.

one :: MonadBoolector m => Sort -> m Node Source #

Create bit vector constant one of sort sort.

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

fun Source #

Arguments

:: MonadBoolector m 
=> [Node]

Parameters of function.

-> Node

Function body parameterized over param_nodes.

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

forall Source #

Arguments

:: MonadBoolector m 
=> [Node]

Quantified variables (create with param)

-> Node

Term where variables may occur. (Cannot contain functions.)

-> m Node 

Create a universally quantified term.

exists Source #

Arguments

:: MonadBoolector m 
=> [Node]

Quantified variables (create with param)

-> Node

Term where variables may occur. (Cannot contain functions.)

-> m Node 

Create an existentially quantifed term.

Operations

Implications and conditionals

implies :: MonadBoolector m => Node -> Node -> m Node Source #

Create boolean implication.

iff :: MonadBoolector m => Node -> Node -> m Node Source #

Create Boolean equivalence.

cond Source #

Arguments

:: 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

not :: MonadBoolector m => Node -> m Node Source #

Create the one's complement of bit vector node.

neg :: MonadBoolector m => Node -> m Node Source #

Create the two's complement of bit vector node.

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*.

slice Source #

Arguments

:: 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 node.

-> Word32

Lower index which must be greater than or equal to zero, and less than or equal to upper.

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

xor :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *xor*.

xnor :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *xnor*.

and :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *and*.

nand :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *nand*.

or :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *or*.

nor :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector *nor*.

sll Source #

Arguments

:: 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 n0.

-> 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.

srl Source #

Arguments

:: 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 n0.

-> 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.

sra Source #

Arguments

:: 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 n0.

-> 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.

rol Source #

Arguments

:: 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 n0.

-> 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.

ror Source #

Arguments

:: 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 n0.

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

add :: MonadBoolector m => Node -> Node -> m Node Source #

Create bit vector addition.

inc :: Node -> Boolector Node Source #

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

sub :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bit vector subtraction.

dec :: MonadBoolector m => Node -> m Node Source #

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

mul :: MonadBoolector m => Node -> Node -> m Node Source #

Create a bitvector multiplication.

udiv :: MonadBoolector m => Node -> Node -> m Node Source #

Create unsigned division.

sdiv :: MonadBoolector m => Node -> Node -> m Node Source #

Create signed division.

urem :: MonadBoolector m => Node -> Node -> m Node Source #

Create an unsigned remainder.

srem :: MonadBoolector m => Node -> Node -> m Node Source #

Create a signed remainder.

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

ult :: MonadBoolector m => Node -> Node -> m Node Source #

Create an unsigned less than.

slt :: MonadBoolector m => Node -> Node -> m Node Source #

Create a signed less than.

ulte :: MonadBoolector m => Node -> Node -> m Node Source #

Create an unsigned less than or equal.

slte :: MonadBoolector m => Node -> Node -> m Node Source #

Create a signed less than or equal.

ugt :: MonadBoolector m => Node -> Node -> m Node Source #

Create an unsigned greater than.

sgt :: MonadBoolector m => Node -> Node -> m Node Source #

Create a signed greater than.

ugte :: MonadBoolector m => Node -> Node -> m Node Source #

Create an unsigned greater than or equal.

sgte :: MonadBoolector m => Node -> Node -> m Node Source #

Create a signed greater than or equal.

Array operations

read Source #

Arguments

:: MonadBoolector m 
=> Node

Array operand.

-> Node

Bit vector index. The bit width of n_index must have the same bit width as the indices of n_array.

-> m Node 

Create a read on array n_array at position n_index.

write Source #

Arguments

:: 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

apply Source #

Arguments

:: 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.

getSymbol :: MonadBoolector m => Node -> m (Maybe String) Source #

Get the symbol of an expression.

setSymbol :: MonadBoolector m => Node -> String -> m () Source #

Set the symbol of an expression.

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.

isConst :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is a constant node.

isVar :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is a bit vector variable.

isArray :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is an array node.

isArrayVar :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is an array node.

isParam :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is a parameter 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.

isFun :: MonadBoolector m => Node -> m Bool Source #

Determine if given node is a 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.

Sorts

data Sort Source #

Sort wraps the udnerlying Boolector sort with a showable type.

Instances
Eq Sort Source # 
Instance details

Defined in Boolector

Methods

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

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

Ord Sort Source # 
Instance details

Defined in Boolector

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 #

Show Sort Source # 
Instance details

Defined in Boolector

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

data SortTy Source #

Type of sorts, used to keep track of sorts without having to go back into C-land.

Instances
Eq SortTy Source # 
Instance details

Defined in Boolector

Methods

(==) :: SortTy -> SortTy -> Bool #

(/=) :: SortTy -> SortTy -> Bool #

Ord SortTy Source # 
Instance details

Defined in Boolector

Show SortTy Source # 
Instance details

Defined in Boolector

sortTy :: Sort -> SortTy Source #

Get sort type

boolSort :: Boolector Sort Source #

Create Boolean sort.

bitvecSort :: MonadBoolector m => Word -> m Sort Source #

Create bit vector sort of bit width width.

funSort :: MonadBoolector m => [Sort] -> Sort -> m Sort Source #

Create function sort.

arraySort :: MonadBoolector m => Sort -> Sort -> m Sort Source #

Create array sort.

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.

isFunSort :: Sort -> Bool Source #

Determine if sort is a function 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.

Constructors

DumpBtor 
DumpSMT2 
Instances
Eq DumpFormat Source # 
Instance details

Defined in Boolector

Show DumpFormat Source # 
Instance details

Defined in Boolector