25 <<
"Program constraints:"
28 for(
const auto &step : equation.
SSA_steps)
30 std::cout <<
"// " << step.source.pc->location_number <<
" ";
31 std::cout << step.source.pc->source_location.as_string() <<
"\n";
32 const irep_idt &
function = step.source.function;
34 if(step.is_assignment())
36 std::string string_value =
from_expr(ns,
function, step.cond_expr);
37 std::cout <<
"(" << count <<
") " << string_value <<
"\n";
39 if(!step.guard.is_true())
41 std::string string_value =
from_expr(ns,
function, step.guard);
43 std::cout <<
"guard: " << string_value <<
"\n";
48 else if(step.is_assert())
50 std::string string_value =
from_expr(ns,
function, step.cond_expr);
51 std::cout <<
"(" << count <<
") ASSERT(" << string_value <<
") "
54 if(!step.guard.is_true())
56 std::string string_value =
from_expr(ns,
function, step.guard);
58 std::cout <<
"guard: " << string_value <<
"\n";
63 else if(step.is_assume())
65 std::string string_value =
from_expr(ns,
function, step.cond_expr);
66 std::cout <<
"(" << count <<
") ASSUME(" << string_value <<
") "
69 if(!step.guard.is_true())
71 std::string string_value =
from_expr(ns,
function, step.guard);
73 std::cout <<
"guard: " << string_value <<
"\n";
78 else if(step.is_constraint())
80 std::string string_value =
from_expr(ns,
function, step.cond_expr);
81 std::cout <<
"(" << count <<
") CONSTRAINT(" << string_value <<
") "
86 else if(step.is_shared_read() || step.is_shared_write())
88 std::string string_value =
from_expr(ns,
function, step.ssa_lhs);
89 std::cout <<
"(" << count <<
") SHARED_"
90 << (step.is_shared_write() ?
"WRITE" :
"READ") <<
"("
91 << string_value <<
")\n";
93 if(!step.guard.is_true())
95 std::string string_value =
from_expr(ns,
function, step.guard);
97 std::cout <<
"guard: " << string_value <<
"\n";