module greed.state_plugins.solver
class SimStateSolver
A plugin that allows for constraints to be added to the state and unified access to the solver backend.
method __init__
property constraints
property frame
property memory_constraints
property path_constraints
property timed_out
method add_memory_constraint
Add a memory constraint to the state (at the current frame level).
Args:
constraint: The constraint to add.
method add_path_constraint
Add a path constraint to the state (at the current frame level).
Args:
constraint: The constraint to add.
method are_formulas_sat
Check if a list of formulas is satisfiable given the current state of the solver.
Args:
terms: The list of formulas to check.
method constraints_at
Returns the constraints at a specific frame or all the constraints if frame is None.
Args:
frame: The frame level in the solver to check.
method copy
Deep copy this state plugin.
method dispose_context
Dispose the solver context.
method eval
Evaluate a term.
Args:
term: The term to evaluate.raw: If True, return the raw value of the term.
Returns: The evaluated term.
method eval_memory
Evaluate a memory region in the memory.
Args:
memory: The memory region to evaluate.length: The length of the memory region to evaluate.raw: If True, return the raw value of the memory region.
Returns: The evaluated memory region.
Raises:
AssertionError: If the length is not concrete.
method eval_memory_at
Evaluate a portion of a memory region starting at a given offset.
Args:
array: The memory region to evaluate.offset: The offset to start evaluating from.length: The length of the memory region to evaluate.raw: If True, return the raw value of the memory region.
Returns: The evaluated memory region.
Raises:
AssertionError: If the offset or the length is not concrete.
method is_concrete
Check if a term is concrete.
method is_formula_false
Check if a formula is false given the current state of the solver.
Args:
formula: The formula to check.
method is_formula_sat
Check if a formula is satisfiable given the current state of the solver.
Args:
formula: The formula to check.
method is_formula_true
Check if a formula is true given the current state of the solver.
Args:
formula: The formula to check.
method is_formula_unsat
Check if a formula is unsatisfiable given the current state of the solver.
Args:
formula: The formula to check.
method is_sat
Check if the solver is in a satisfiable state.
method is_unsat
Check if the solver is in an unsatisfiable state.
method memory_constraints_at
Returns the memory constraints at a specific frame. If frame is None, returns ALL the currently active memory constraints.
Args:
frame: The frame level in the solver to check.
method path_constraints_at
Returns the path constraints at a specific frame. If frame is None, returns ALL the currently active path constraints.
Args:
frame: The frame level in the solver to check.
method pop
Pop a frame from the solver stack.
method pop_all
Pop all the frames from the solver stack.
method push
Push a new frame on the solver stack.
method simplify
Simplify registers by replacing them with their concrete values if possible.
This file was automatically generated via lazydocs.