Generic base class for SMT Solvers
Synopsis
Declared in <llvm/Support/SMTAPI.h>
class SMTSolver;Description
This class is responsible for wrapping all sorts and expression generation, through the mk* methods. It also provides methods to create SMT expressions straight from clang's AST, through the from* methods.
Member Functions
Name |
Description |
|
Construct an empty SMT solver. |
|
Destroy this SMT solver. |
|
Given a constraint, adds it to the solver |
|
Check if the constraints are satisfiable |
Dump this solver to the debug stream. |
|
|
If a model is available, return the value of a given bitvector symbol. |
|
Return an appropriate bitvector sort for the given bitwidth. |
|
Return a boolean sort. |
|
If a model is available, return the value of a given boolean symbol. |
|
Return a floating‐point sort of width 128. |
|
Return a floating‐point sort of width 16. |
|
Return a floating‐point sort of width 32. |
|
Return a floating‐point sort of width 64. |
|
Return an appropriate floating‐point rounding mode. |
Return an appropriate floating‐point sort for the given bitwidth. |
|
|
|
|
Return an appropriate sort for the given expression. |
|
Return statistics collected by this solver. |
|
Checks if the solver supports floating‐points. |
|
Creates a boolean and operation |
|
Creates a bitvector addition operation |
|
Creates a predicate that checks for overflow in a bitvector addition operation |
|
Creates a predicate that checks for underflow in a signed bitvector addition operation |
|
Creates a bitvector and operation |
|
Creates a bitvector arithmetic shift right operation |
|
Creates a bitvector concat operation |
|
Creates a bitvector extract operation |
|
Creates a bitvector logical shift right operation |
|
Creates a bitvector multiplication operation |
|
Creates a predicate that checks for overflow in a bitvector multiplication operation |
|
Creates a predicate that checks for underflow in a signed bitvector multiplication operation |
|
Creates a bitvector negation operation |
|
Creates a predicate that checks for overflow in a bitvector negation operation |
|
Creates a bitvector not operation |
|
Creates a bitvector or operation |
|
Creates a bitvector signed division operation |
|
Creates a predicate that checks for overflow in a signed bitvector division/modulus operation |
|
Creates a bitvector signed modulus operation |
|
Creates a bitvector signed greater‐equal‐than operation |
|
Creates a bitvector signed greater‐than operation |
|
Creates a bitvector logical shift left operation |
|
Creates a bitvector sign extension operation |
|
Creates a bitvector signed less‐equal‐than operation |
|
Creates a bitvector signed less‐than operation |
|
Creates a bitvector subtraction operation |
|
Creates a predicate that checks for overflow in a signed bitvector subtraction operation |
|
Creates a predicate that checks for underflow in a bitvector subtraction operation |
|
Creates a bitvector unsigned division operation |
|
Creates a bitvector unsigned modulus operation |
|
Creates a bitvector unsigned greater‐equal‐than operation |
|
Creates a bitvector unsigned greater‐than operation |
|
Creates a bitvector unsigned less‐equal‐than operation |
|
Creates a bitvector unsigned less‐than operation |
|
Creates a bitvector xor operation |
|
Creates a bitvector zero extension operation |
|
Constructs an SMTExprRef from an APSInt and its bit width |
|
Constructs an SMTExprRef from a boolean. |
|
Creates a boolean equality operation |
|
Creates a floating‐point addition operation |
|
Creates a floating‐point division operation |
|
Creates a floating‐point equality operation |
|
Creates a floating‐point greater‐than‐or‐equal operation |
|
Creates a floating‐point greater‐than operation |
|
Creates a floating‐point isInfinite operation |
|
Creates a floating‐point isNaN operation |
|
Creates a floating‐point isNormal operation |
|
Creates a floating‐point isZero operation |
|
Creates a floating‐point less‐than‐or‐equal operation |
|
Creates a floating‐point less‐than operation |
|
Creates a floating‐point multiplication operation |
|
Creates a floating‐point negation operation |
|
Creates a floating‐point remainder operation |
|
Creates a floating‐point subtraction operation |
|
Creates a floating‐point conversion from floatint‐point to floating‐point operation |
|
Creates a floating‐point conversion from floatint‐point to signed bitvector operation |
|
Creates a floating‐point conversion from floatint‐point to unsigned bitvector operation |
|
Constructs an SMTExprRef from a finite APFloat. |
|
Creates a boolean ite operation |
|
Creates a boolean not operation |
|
Creates a boolean or operation |
|
Creates a floating‐point conversion from signed bitvector to floatint‐point operation |
|
Creates a new symbol, given a name and a sort |
|
Creates a floating‐point conversion from unsigned bitvector to floatint‐point operation |
|
Pop the previous solver state |
|
Print this solver to an output stream. |
|
Push the current solver state |
|
Reset the solver and remove all constraints. |
|
Sets the requested option. |
|
Set an unsigned solver option. |
Created with MrDocs