claripy.backends.backend_smtlib.BackendSMTLibBase

class documentation

class BackendSMTLibBase(Backend): (source)

Known subclasses: claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

View In Hierarchy

Undocumented

Method __init__ Undocumented
Method BoolS Undocumented
Method BoolV Undocumented
Method BVS Undocumented
Method BVV Undocumented
Method StringS Undocumented
Method StringV Undocumented
Instance Variable daggify Undocumented
Instance Variable reuse_z3_solver Undocumented
Property is_smt_backend Undocumented
Method _check_satisfiability This function does a constraint check and returns the solvers state
Method _get_all_vars_and_constraints Undocumented
Method _get_full_model_smt_script Returns a SMT script that declare all the symbols and constraint and checks their satisfiability (check-sat)
Method _get_satisfiability_smt_script Returns a SMT script that declare all the symbols and constraint and checks their satisfiability (check-sat)
Method _op_raw_add Undocumented
Method _op_raw_and Undocumented
Method _op_raw_eq Undocumented
Method _op_raw_ge Undocumented
Method _op_raw_gt Undocumented
Method _op_raw_if Undocumented
Method _op_raw_inttostr Undocumented
Method _op_raw_isdigit Undocumented
Method _op_raw_le Undocumented
Method _op_raw_lt Undocumented
Method _op_raw_ne Undocumented
Method _op_raw_not Undocumented
Method _op_raw_or Undocumented
Method _op_raw_str_concat Undocumented
Method _op_raw_str_contains Undocumented
Method _op_raw_str_indexof Undocumented
Method _op_raw_str_prefixof Undocumented
Method _op_raw_str_replace Undocumented
Method _op_raw_str_strlen Undocumented
Method _op_raw_str_strtoint Undocumented
Method _op_raw_str_substr Undocumented
Method _op_raw_str_suffixof Undocumented
Method _op_raw_sub Undocumented
Method _satisfiable This function does a constraint check and returns a model for a solver.
Method _smtlib_exprs Undocumented

Inherited from Backend:

Method add This function adds constraints to the backend solver.
Method apply_annotation This should apply the annotation on the backend object, and return a new backend object.
Method batch_eval Evaluate one or multiple expressions.
Method call Calls operation `op` on args `args` with this backend.
Method cardinality This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation.
Method check_satisfiability This function does a constraint check and returns the solvers state
Method convert Resolves a claripy.ast.Base into something usable by the backend.
Method convert_list Undocumented
Method default_op Undocumented
Method downsize Clears all caches associated with this backend.
Method eval This function returns up to `n` possible solutions for expression `expr`.
Method handles Checks whether this backend can handle the expression.
Method has_false Should return False if `e` can possibly be False.
Method has_true Should return True if `e` can possible be True.
Method identical This should return whether `a` is identical to `b`. Of course, this isn't always clear. True should mean that it is definitely identical. False eans that, conservatively, it might not be.
Method is_false Should return True if e can be easily found to be False.
Method is_true Should return True if `e` can be easily found to be True.
Method max Return the maximum value of expr.
Method min Return the minimum value of `expr`.
Method multivalued Undocumented
Method name This should return the name of an expression.
Method satisfiable This function does a constraint check and checks if the solver is in a sat state.
Method simplify Undocumented
Method singlevalued Undocumented
Method solution Return True if `v` is a solution of `expr` with the extra constraints, False otherwise.
Method solver This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().
Method unsat_core This function returns the unsat core from the backend solver.
Class Variable __slots__ Undocumented
Method _abstract Abstracts the BackendObject e to an AST.
Method _add This function adds constraints to the backend solver.
Method _batch_eval Evaluate one or multiple expressions.
Method _call _call
Method _cardinality This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation.
Method _convert Converts `r` to something usable by this backend.
Method _eval This function returns up to `n` possible solutions for expression `expr`.
Method _has_false The native version of :func:`has_false`.
Method _has_true The native version of :func:`has_true`.
Method _identical This should return whether `a` is identical to `b`. This is the native version of ``identical()``.
Method _is_false The native version of is_false.
Method _is_true The native version of is_true.
Method _make_expr_ops Fill up `self._op_expr` dict.
Method _make_raw_ops Undocumented
Method _max Return the maximum value of expr.
Method _min Return the minimum value of expr.
Method _name This should return the name of an object.
Method _simplify Undocumented
Method _solution Return True if v is a solution of expr with the extra constraints, False otherwise.
Method _unsat_core This function returns the unsat core from the backend solver.
Instance Variable _cache_objects Undocumented
Instance Variable _false_cache Undocumented
Instance Variable _op_expr Undocumented
Instance Variable _op_raw Undocumented
Instance Variable _solver_required Undocumented
Instance Variable _tls Undocumented
Instance Variable _true_cache Undocumented
Property _object_cache Undocumented
def __init__(self, *args, **kwargs): (source)
overrides claripy.backends.Backend.__init__
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

Undocumented

def BoolS(self, ast): (source)

Undocumented

def BoolV(self, ast): (source)

Undocumented

def BVS(self, ast): (source)

Undocumented

def BVV(self, ast): (source)

Undocumented

def StringS(self, ast): (source)

Undocumented

def StringV(self, ast): (source)

Undocumented

daggify = (source)

Undocumented

reuse_z3_solver: bool = (source)

Undocumented

@property
is_smt_backend = (source)
overrides claripy.backends.Backend.is_smt_backend

Undocumented

def _check_satisfiability(self, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._check_satisfiability
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

This function does a constraint check and returns the solvers state :param solver: The backend solver object. :param extra_constraints: Extra constraints (as ASTs) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: 'SAT', 'UNSAT', or 'UNKNOWN'

def _get_all_vars_and_constraints(self, solver=None, e_c=(), e_v=()): (source)

Undocumented

def _get_full_model_smt_script(self, constraints=(), variables=()): (source)

Returns a SMT script that declare all the symbols and constraint and checks their satisfiability (check-sat) :param extra-constraints: list of extra constraints that we want to evaluate only in the scope of this call :return string: smt-lib representation of the script that checks the satisfiability

def _get_satisfiability_smt_script(self, constraints=(), variables=()): (source)

Returns a SMT script that declare all the symbols and constraint and checks their satisfiability (check-sat) :param extra-constraints: list of extra constraints that we want to evaluate only in the scope of this call :return string: smt-lib representation of the script that checks the satisfiability

def _op_raw_add(self, *args): (source)

Undocumented

def _op_raw_and(self, *args): (source)

Undocumented

def _op_raw_eq(self, *args): (source)

Undocumented

def _op_raw_ge(self, *args): (source)

Undocumented

def _op_raw_gt(self, *args): (source)

Undocumented

def _op_raw_if(self, *args): (source)

Undocumented

def _op_raw_inttostr(self, input_bv): (source)

Undocumented

def _op_raw_isdigit(self, input_string): (source)

Undocumented

def _op_raw_le(self, *args): (source)

Undocumented

def _op_raw_lt(self, *args): (source)

Undocumented

def _op_raw_ne(self, *args): (source)

Undocumented

def _op_raw_not(self, *args): (source)

Undocumented

def _op_raw_or(self, *args): (source)

Undocumented

def _op_raw_str_concat(self, *args): (source)

Undocumented

def _op_raw_str_contains(self, *args): (source)

Undocumented

def _op_raw_str_indexof(self, *args): (source)

Undocumented

def _op_raw_str_prefixof(self, *args): (source)

Undocumented

def _op_raw_str_replace(self, *args): (source)

Undocumented

def _op_raw_str_strlen(self, *args): (source)

Undocumented

def _op_raw_str_strtoint(self, *args): (source)

Undocumented

def _op_raw_str_substr(self, *args): (source)

Undocumented

def _op_raw_str_suffixof(self, *args): (source)

Undocumented

def _op_raw_sub(self, *args): (source)

Undocumented

def _satisfiable(self, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._satisfiable
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

This function does a constraint check and returns a model for a solver. :param solver: The backend solver object :param extra_constraints: Extra constraints (backend objects) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: True if sat, otherwise false

def _smtlib_exprs(self, exprs): (source)

Undocumented