claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

class documentation

class SMTLibSolverBackend(BackendSMTLibBase): (source)

Known subclasses: claripy.backends.backend_smtlib_solvers.abc_popen.SolverBackendABC, claripy.backends.backend_smtlib_solvers.cvc4_popen.SolverBackendCVC4, claripy.backends.backend_smtlib_solvers.z3_popen.SolverBackendZ3, claripy.backends.backend_smtlib_solvers.z3str_popen.SolverBackendZ3Str

View In Hierarchy

Undocumented

Method __init__ Undocumented
Method eval This function returns up to `n` possible solutions for expression `expr`.
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().
Instance Variable smt_script_log_dir Undocumented
Method _add This function adds constraints to the backend solver.
Method _batch_eval Evaluate one or multiple expressions.
Method _check_satisfiability This function does a constraint check and returns the solvers state
Method _check_satness Undocumented
Method _eval This function returns up to `n` possible solutions for expression `expr`.
Method _get_model Undocumented
Method _get_primitive_for_expr Undocumented
Method _is_false The native version of is_false.
Method _is_true The native version of is_true.
Method _satisfiable This function does a constraint check and returns a model for a solver.
Method _simplify Undocumented

Inherited from BackendSMTLibBase:

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 _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 _smtlib_exprs Undocumented

Inherited from Backend (via BackendSMTLibBase):

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 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 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 _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 _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 _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 _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_smtlib.BackendSMTLibBase.__init__

Undocumented

def eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend.eval

This function returns up to `n` possible solutions for expression `expr`. :param expr: expression (an AST) to evaluate :param n: number of results to return :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: A sequence of up to n results (backend objects)

def solver(self, timeout=None, max_memory=None): (source)
overrides claripy.backends.Backend.solver
overridden in claripy.backends.backend_smtlib_solvers.abc_popen.SolverBackendABC, claripy.backends.backend_smtlib_solvers.cvc4_popen.SolverBackendCVC4, claripy.backends.backend_smtlib_solvers.z3_popen.SolverBackendZ3, claripy.backends.backend_smtlib_solvers.z3str_popen.SolverBackendZ3Str

This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().

smt_script_log_dir = (source)

Undocumented

def _add(self, s, c, track=False): (source)
overrides claripy.backends.Backend._add

This function adds constraints to the backend solver. :param c: sequence of converted backend objects :param s: backend solver object :param bool track: True to enable constraint tracking, which is used in unsat_core().

def _batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._batch_eval

Evaluate one or multiple expressions. :param exprs: A list of expressions to evaluate. :param n: Number of different solutions to return. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver object, native to the backend, to assist in the evaluation. :param model_callback: a function that will be executed with recovered models (if any) :return: A list of up to n tuples, where each tuple is a solution for all expressions.

def _check_satisfiability(self, extra_constraints=(), solver=None, model_callback=None, extra_variables=()): (source)
overrides claripy.backends.backend_smtlib.BackendSMTLibBase._check_satisfiability

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 _check_satness(self, solver=None, extra_constraints=(), model_callback=None, extra_variables=()): (source)

Undocumented

def _eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._eval

This function returns up to `n` possible solutions for expression `expr`. :param expr: An expression (backend object) to evaluate. :param n: A number of results to return. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver). :param model_callback: a function that will be executed with recovered models (if any) :return: A sequence of up to n results (backend objects).

def _get_model(self, solver=None, extra_constraints=(), extra_variables=()): (source)

Undocumented

def _get_primitive_for_expr(self, model, e): (source)

Undocumented

def _is_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._is_false

The native version of is_false. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _is_true(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._is_true

The native version of is_true. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _satisfiable(self, solver=None, extra_constraints=(), model_callback=None, extra_variables=()): (source)
overrides claripy.backends.backend_smtlib.BackendSMTLibBase._satisfiable

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 _simplify(self, e): (source)
overrides claripy.backends.Backend._simplify

Undocumented