claripy.backends.backend_smtlib_solvers.abc_popen.SolverBackendABC

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().

Inherited from SMTLibSolverBackend:

Method	__init__	Undocumented
Method	eval	This function returns up to `n` possible solutions for expression `expr`.
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 (via SMTLibSolverBackend):

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 SMTLibSolverBackend, 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