Undocumented
Method | __init__ |
Undocumented |
Method | abstract |
Undocumented |
Method | call |
Calls operation `op` on args `args` with this backend. |
Method | resolve |
Undocumented |
Method | simplify |
Undocumented |
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(). |
Static Method | _translate |
Undocumented |
Method | _add |
This function adds constraints to the backend solver. |
Method | _background |
Undocumented |
Method | _batch |
Evaluate one or multiple expressions. |
Method | _check |
Undocumented |
Method | _convert |
Converts `r` to something usable by this backend. |
Method | _eval |
This function returns up to `n` possible solutions for expression `expr`. |
Method | _max |
Return the maximum value of expr. |
Method | _min |
Return the minimum value of expr. |
Method | _results |
Undocumented |
Method | _simplify |
Undocumented |
Method | _synchronize |
Undocumented |
Instance Variable | _cache |
Undocumented |
Instance Variable | _child |
Undocumented |
Instance Variable | _lock |
Undocumented |
Inherited from BackendZ3
:
Method | add |
This function adds constraints to the backend solver. |
Method |
|
Undocumented |
Method |
|
Undocumented |
Method | BVS |
Undocumented |
Method | BVV |
Undocumented |
Method | clone |
Undocumented |
Method | downsize |
Clears all caches associated with this backend. |
Method | FPS |
Undocumented |
Method | FPV |
Undocumented |
Method |
|
Undocumented |
Method |
|
Undocumented |
Instance Variable | reuse |
Undocumented |
Property | extra |
Undocumented |
Static Method | _abstract |
Undocumented |
Static Method | _abstract |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op_raw_ |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _op |
Undocumented |
Static Method | _z3 |
This is a better hashing function for z3 Ast objects. Z3_get_ast_hash() creates too many hash collisions. |
Method | _abstract |
Abstracts the BackendObject e to an AST. |
Method | _abstract |
Undocumented |
Method | _abstract |
Undocumented |
Method | _abstract |
Undocumented |
Method | _extrema |
_max if is_max else _min |
Method | _generic |
Converts a Z3 model to a name->primitive dict. |
Method | _identical |
This should return whether `a` is identical to `b`. This is the native version of ``identical()``. |
Method | _is |
The native version of is_false. |
Method | _is |
The native version of is_true. |
Method | _name |
This should return the name of an object. |
Method | _op_raw_ |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_fp |
Undocumented |
Method | _op_raw_ |
Undocumented |
Method | _op_raw_ |
Undocumented |
Method | _op_raw_ |
Undocumented |
Method | _op_raw_ |
Undocumented |
Method | _pop |
Undocumented |
Method | _primitive |
Undocumented |
Method | _satisfiable |
This function does a constraint check and returns a model for a solver. |
Method | _solution |
Return True if v is a solution of expr with the extra constraints, False otherwise. |
Method | _unsat |
This function returns the unsat core from the backend solver. |
Class Variable | _split |
Undocumented |
Instance Variable | _ast |
Undocumented |
Property | _ast |
Undocumented |
Property | _boolref |
Undocumented |
Property | _c |
Undocumented |
Property | _context |
Undocumented |
Property | _sym |
Undocumented |
Property | _var |
Undocumented |
Inherited from Backend
(via BackendZ3
):
Method | apply |
This should apply the annotation on the backend object, and return a new backend object. |
Method | batch |
Evaluate one or multiple expressions. |
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 |
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 |
Undocumented |
Method | default |
Undocumented |
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 |
Should return False if `e` can possibly be False. |
Method | has |
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 |
Should return True if e can be easily found to be False. |
Method | is |
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 | singlevalued |
Undocumented |
Method | solution |
Return True if `v` is a solution of `expr` with the extra constraints, False otherwise. |
Method | unsat |
This function returns the unsat core from the backend solver. |
Class Variable | __slots__ |
Undocumented |
Property | is |
Undocumented |
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 | _check |
This function does a constraint check and returns the solvers state |
Method | _has |
The native version of :func:`has_false`. |
Method | _has |
The native version of :func:`has_true`. |
Method | _make |
Fill up `self._op_expr` dict. |
Method | _make |
Undocumented |
Instance Variable | _false |
Undocumented |
Instance Variable | _op |
Undocumented |
Instance Variable | _op |
Undocumented |
Instance Variable | _solver |
Undocumented |
Instance Variable | _tls |
Undocumented |
Instance Variable | _true |
Undocumented |
Property | _object |
Undocumented |
Calls operation `op` on args `args` with this backend. :return: A backend object representing the result.
This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().
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().
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.
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).
Return the maximum value of expr. :param expr: expression (backend object) to evaluate :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 signed: Whether to solve for the maximum signed integer instead of the unsigned max :param model_callback: a function that will be executed with recovered models (if any) :return: the maximum possible value of expr (backend object)
Return the minimum value of expr. :param expr: expression (backend object) to evaluate :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 signed: Whether to solve for the minimum signed integer instead of the unsigned min :param model_callback: a function that will be executed with recovered models (if any) :return: the minimum possible value of expr (backend object)