klara.klara_z3.inference_extension

module documentation
(source)

Integrate z3 solver to the inference system

Function disable Disable z3 solver for inference
Function enable Enable z3 solver support for inference system All inference result will check by solver for satisfiability, and unsat result are filtered :return: None
Function evaluate_paths Undocumented
Function expand_condition fully yield all possible paths of the condition "expr".
Function infer_check_sat wrap `infer` to filter unsat inference result
Function infer_expand Undocumented
Function result_check_sat Undocumented
Function result_expand Undocumented
Constant MANAGER Undocumented
def disable(): (source)

Disable z3 solver for inference

def enable(): (source)

Enable z3 solver support for inference system All inference result will check by solver for satisfiability, and unsat result are filtered :return: None

def evaluate_paths(conditions, z3_assumptions, context, inverted_conds=None): (source)

Undocumented

def expand_condition(expr, context): (source)

fully yield all possible paths of the condition "expr".

def infer_check_sat(func): (source)

wrap `infer` to filter unsat inference result

def infer_expand(node, context): (source)

Undocumented

def result_check_sat(self, context): (source)

Undocumented

def result_expand(self, context, z3_result): (source)

Undocumented

MANAGER = (source)

Undocumented

Value
CovManager()