rajdeep87
commented
7 years ago Inferring reason using SAT solver.
get_reason(statement, initial_value, final_value, reason);
Choose a subset of initial_value say v using some heuristic.
We do the following to check if v is the reason:
*solver << implies_exprt(and_expr(statement, conjunction(v)), conjunction(final_value));
result = (*solver)();
if(result == SAT) then v is the reason
Following scenario shows invalid result produced by the abductive generalisation transformer: Input:: Initial value::
$guard#25 && !(x#phi25 >= 1) && !(-((signed __CPROVER_bitvector[33])x#phi25) >= 1) && $cond#23 && $guard#0 && !$cond#21 && !$guard#24 && $guard#22 && !(-((signed __CPROVER_bitvector[33])x#16) >= 1)Antecedent clause (statement)::
x#phi25 == ($guard#24 ? x#24 : x#22)Final value::
!(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)Variable set::
$cond#21 $cond#23 $guard#0 $guard#22 $guard#24 $guard#25 x#16 x#22 x#24 x#phi25Output: Generalization of Initial value::
!(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)We want a generalisation of the initial value. But the adductive transformer simply returns the same final value that is passed to the following abductive transformer.
ssa_analyzer(*solver, SSA, implies_exprt(conjunction(final_value), statement), template_generator);