whitesymex.solver module¶
- class whitesymex.solver.Solver¶
Bases:
objectSMT solver to solve path constraints.
- constraints¶
A list of path constraints.
- store¶
A dict mapping symbolic variables to concrete values.
- add(constraints: Union[z3.BoolRef, list[z3.BoolRef]])¶
Adds constraints to the solver.
- Parameters
constraints – A single constraint or a list of constraints to add.
- clone()¶
Returns a copy of the solver.
Both constraints and store are shallow-copied.
- eval(expression: z3.z3.ExprRef) → Union[bool, int]¶
Evaluates an expression using the concrete values from the store.
- Parameters
expression – An expression to be evaluated.
- Returns
The evaluated value of the expression.
- Raises
SolverError – Failed to evaluate the expression as int or bool.
- is_satisfiable() → bool¶
Checks and returns if the constraints are satisfiable.
- simplify(expression: z3.z3.ExprRef) → z3.z3.ExprRef¶
Simplifies an expression by substituting concrete values.
Only the variables that exist in store are substituted.
- Parameters
expression – An expression to be simplified.
- Returns
The substituted and simplified expression.