claripy.backends.backend_smtlib

module documentation
(source)

Undocumented

Class BackendSMTLibBase No class docstring; 0/1 property, 0/2 instance variable, 2/36 methods documented
Variable l Undocumented
Function _expr_to_smtlib Dump the symbol in its smt-format depending on its type
Function _exprs_to_smtlib Dump all the variables and all the constraints in an smt-lib format
Function _normalize_arguments Since we decided to emulate integer with bitvector, this method transform their concrete value (if any) in the corresponding integer
l = (source)

Undocumented

def _expr_to_smtlib(e, daggify=True): (source)

Dump the symbol in its smt-format depending on its type :param e: symbol to dump :param daggify: The daggify parameter can be used to switch from a linear-size representation that uses ‘let’ operators to represent the formula as a dag or a simpler (but possibly exponential) representation that expands the formula as a tree :return string: smt-lib representation of the symbol

def _exprs_to_smtlib(*exprs, **kwargs): (source)

Dump all the variables and all the constraints in an smt-lib format :param exprs : List of variable declaration and constraints that have to be dumped in an smt-lib format :return string: smt-lib representation of the list of expressions

def _normalize_arguments(expr_left, expr_right): (source)

Since we decided to emulate integer with bitvector, this method transform their concrete value (if any) in the corresponding integer