52 for(patht::iterator it=loop.begin();
56 body.push_back(*(it->loc));
60 std::map<exprt, polynomialt> polynomials;
67 std::cout <<
"Polynomial accelerating program:\n";
69 for(goto_programt::instructionst::iterator it=body.begin();
73 program.output_instruction(
ns,
"scratch", std::cout, *it);
76 std::cout <<
"Modified:\n";
78 for(expr_sett::iterator it=targets.begin();
82 std::cout <<
expr2c(*it,
ns) <<
'\n';
86 for(goto_programt::instructionst::iterator it=body.begin();
90 if(it->is_assign() || it->is_decl())
92 assigns.push_back(*it);
103 for(expr_sett::iterator it=targets.begin();
120 if(influence.find(target)==influence.end())
123 std::cout <<
"Found nonrecursive expression: "
131 if(target.
id()==ID_index ||
132 target.
id()==ID_dereference)
141 std::map<exprt, polynomialt> this_poly;
142 this_poly[target]=poly;
146 polynomials.insert(std::make_pair(target, poly));
152 std::cout <<
"Failed to fit a polynomial for "
160 if(polynomials.empty())
177 bool path_is_monotone;
184 catch(
const std::string &s)
187 std::cout <<
"Assumptions error: " << s <<
'\n';
193 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
194 it!=polynomials.end();
197 replace_expr(it->first, it->second.to_expr(), guard_last);
246 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
247 it!=polynomials.end();
250 program.assign(it->first, it->second.to_expr());
260 std::cout <<
"Failed to accelerate a nonrecursive expression\n";
285 std::vector<expr_listt> parameters;
286 std::set<std::pair<expr_listt, exprt> > coefficients;
294 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
295 <<
", which depends on:\n";
297 for(expr_sett::iterator it=influence.begin();
301 std::cout <<
expr2c(*it,
ns) <<
'\n';
305 for(expr_sett::iterator it=influence.begin();
309 if(it->id()==ID_index ||
310 it->id()==ID_dereference)
318 exprs.push_back(*it);
319 parameters.push_back(exprs);
322 parameters.push_back(exprs);
328 parameters.push_back(exprs);
336 parameters.push_back(exprs);
347 for(std::vector<expr_listt>::iterator it=parameters.begin();
348 it!=parameters.end();
353 coefficients.insert(std::make_pair(*it, coeff.
symbol_expr()));
365 std::map<exprt, int> values;
367 for(expr_sett::iterator it=influence.begin();
375 std::cout <<
"Fitting polynomial over " << values.size()
379 for(
int n=0; n<=2; n++)
381 for(expr_sett::iterator it=influence.begin();
395 for(expr_sett::iterator it=influence.begin();
405 std::cout <<
"Fitting polynomial with program:\n";
422 catch(
const std::string &s)
424 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
428 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
469 std::cout <<
"Fitting constant, eval'd to: "
479 mon.
terms.push_back(term);
480 mon.
coeff=mp.to_long();
487 catch(
const std::string &s)
489 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
493 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
502 std::map<exprt, int> &values,
503 std::set<std::pair<expr_listt, exprt> > &coefficients,
512 for(std::map<exprt, int>::iterator it=values.begin();
516 typet this_type=it->first.type();
517 if(this_type.
id()==ID_pointer)
520 std::cout <<
"Overriding pointer type\n";
525 if(!expr_type.has_value())
531 expr_type =
join_types(*expr_type, this_type);
537 "joined types must be non-empty bitvector types");
540 for(std::map<exprt, int>::iterator it=values.begin();
548 for(
int i=0; i < num_unwindings; i++)
550 program.
append(loop_body);
556 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
557 it!=coefficients.end();
560 int concrete_value=1;
562 for(expr_listt::const_iterator e_it=it->first.begin();
563 e_it!=it->first.end();
570 concrete_value *= num_unwindings;
574 std::map<exprt, int>::iterator v_it=values.find(e);
576 if(v_it!=values.end())
578 concrete_value *= v_it->second;
622 for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
623 r_it!=orig_body.rend();
626 if(r_it->is_assign())
637 for(expr_sett::iterator s_it=lhs_syms.begin();
638 s_it!=lhs_syms.end();
641 if(cone.find(*s_it)!=cone.end())
645 body.push_front(*r_it);
646 cone.erase(assignment.
lhs());
656 std::map<exprt, polynomialt> polynomials,
671 std::vector<exprt> polynomials_hold;
676 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
677 it!=polynomials.end();
680 const equal_exprt holds(it->first, it->second.to_expr());
683 polynomials_hold.push_back(holds);
686 program.append(body);
693 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
694 it!=polynomials_hold.end();
701 std::cout <<
"Checking following program for inductiveness:\n";
711 std::cout <<
"Not inductive!\n";
720 catch(
const std::string &s)
722 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
727 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
734 std::map<exprt, polynomialt> &polynomials,
742 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
743 it!=polynomials.end();
746 it->second.substitute(substitution);
758 vars.erase(loop_counter_name);
781 for(patht::reverse_iterator r_it=path.rbegin();
794 if(lhs.
id()==ID_symbol)
798 else if(lhs.
id()==ID_index ||
799 lhs.
id()==ID_dereference)
808 else if(t->is_assume() || t->is_assert())
817 if(!r_it->guard.is_true() && !r_it->guard.is_nil())