52 std::map<exprt, polynomialt> polynomials;
58 std::cout <<
"Polynomial accelerating program:\n";
60 for(goto_programt::instructionst::iterator
71 std::cout <<
"Modified:\n";
73 for(expr_sett::iterator it=
modified.begin();
77 std::cout <<
expr2c(*it,
ns) <<
'\n';
98 for(expr_sett::iterator it=
modified.begin();
105 if(it->type().id()==ID_bool)
111 if(target.
id()==ID_index ||
112 target.
id()==ID_dereference)
120 std::map<exprt, polynomialt> this_poly;
121 this_poly[target]=poly;
126 std::cout <<
"Fitted a polynomial for " <<
expr2c(target,
ns)
129 polynomials[target]=poly;
136 if(polynomials.empty())
149 for(patht::iterator it=accelerator.
path.begin();
150 it!=accelerator.
path.end();
153 if(it->loc->is_assign() || it->loc->is_decl())
155 assigns.push_back(*(it->loc));
159 for(expr_sett::iterator it=dirty.begin();
164 std::cout <<
"Trying to accelerate " <<
expr2c(*it,
ns) <<
'\n';
167 if(it->type().id()==ID_bool)
172 std::cout <<
"Ignoring boolean\n";
177 if(it->id()==ID_index ||
178 it->id()==ID_dereference)
181 std::cout <<
"Ignoring array reference\n";
190 std::cout <<
"We've accelerated it already\n";
201 std::cout <<
"Ignoring because it depends on an array\n";
212 std::map<exprt, polynomialt> this_poly;
213 this_poly[target]=poly;
217 polynomials[target]=poly;
224 std::cout <<
"Failed to accelerate " <<
expr2c(*it,
ns) <<
'\n';
244 bool path_is_monotone;
251 catch(
const std::string &s)
254 std::cout <<
"Assumptions error: " << s <<
'\n';
258 exprt pre_guard(guard);
260 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
261 it!=polynomials.end();
310 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
311 it!=polynomials.end();
314 program.assign(it->first, it->second.to_expr());
343 program.append(
fixed);
344 program.append(
fixed);
353 for(distinguish_valuest::iterator jt=it->begin();
357 exprt distinguisher=jt->first;
358 bool taken=jt->second;
363 distinguisher.
swap(negated);
366 or_exprt disjunct(new_path, distinguisher);
367 new_path.
swap(disjunct);
370 program.assume(new_path);
380 std::cout <<
"Found a path\n";
388 catch(
const std::string &s)
390 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
394 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
406 std::vector<expr_listt> parameters;
407 std::set<std::pair<expr_listt, exprt> > coefficients;
415 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
416 <<
", which depends on:\n";
418 for(expr_sett::iterator it=influence.begin();
422 std::cout <<
expr2c(*it,
ns) <<
'\n';
426 for(expr_sett::iterator it=influence.begin();
430 if(it->id()==ID_index ||
431 it->id()==ID_dereference)
440 exprs.push_back(*it);
441 parameters.push_back(exprs);
444 parameters.push_back(exprs);
450 parameters.push_back(exprs);
454 parameters.push_back(exprs);
458 parameters.push_back(exprs);
460 for(std::vector<expr_listt>::iterator it=parameters.begin();
461 it!=parameters.end();
465 coefficients.insert(make_pair(*it, coeff.
symbol_expr()));
486 std::map<exprt, exprt> ivals1;
487 std::map<exprt, exprt> ivals2;
488 std::map<exprt, exprt> ivals3;
490 for(expr_sett::iterator it=influence.begin();
539 std::map<exprt, exprt> values;
541 for(expr_sett::iterator it=influence.begin();
545 values[*it]=ivals1[*it];
550 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
560 for(
int n=0; n <= 1; n++)
562 for(expr_sett::iterator it=influence.begin();
566 values[*it]=ivals2[*it];
569 values[*it]=ivals3[*it];
572 values[*it]=ivals1[*it];
576 for(expr_sett::iterator it=influence.begin();
580 values[*it]=ivals3[*it];
594 for(distinguish_valuest::iterator jt=it->begin();
598 exprt distinguisher=jt->first;
599 bool taken=jt->second;
604 distinguisher.
swap(negated);
607 or_exprt disjunct(new_path, distinguisher);
608 new_path.
swap(disjunct);
611 program.assume(new_path);
626 std::cout <<
"Found a polynomial\n";
636 catch(
const std::string &s)
638 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
642 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
650 std::map<exprt, exprt> &values,
651 std::set<std::pair<expr_listt, exprt> > &coefficients,
659 for(std::map<exprt, exprt>::iterator it=values.begin();
663 if(!expr_type.has_value())
665 expr_type=it->first.type();
669 expr_type =
join_types(*expr_type, it->first.type());
674 for(std::map<exprt, exprt>::iterator it=values.begin();
678 program.
assign(it->first, it->second);
682 for(
int i=0; i<num_unwindings; i++)
684 program.
append(loop_body);
690 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
691 it!=coefficients.end();
696 for(expr_listt::const_iterator e_it=it->first.begin();
697 e_it!=it->first.end();
705 from_integer(num_unwindings, *expr_type), concrete_value);
706 mult.
swap(concrete_value);
710 std::map<exprt, exprt>::iterator v_it=values.find(e);
714 mult_exprt mult(concrete_value, v_it->second);
715 mult.
swap(concrete_value);
755 for(
const auto &loop_instruction :
loop)
763 for(
const auto &jt : succs)
788 "we should have a looping path, so we should never hit a location "
789 "with no successors.");
801 bool found_branch=
false;
803 for(
const auto &succ : succs)
806 bool taken=scratch_program.
eval(distinguisher).
is_true();
811 (succ->location_number < next->location_number))
831 for(goto_programt::targetst::iterator it=t->targets.begin();
832 it!=t->targets.end();
837 cond = t->get_condition();
857 std::map<exprt, exprt> shadow_distinguishers;
888 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
892 exprt &distinguisher=*it;
896 shadow_distinguishers[distinguisher]=shadow;
915 fixedt->turn_into_skip();
923 exprt &distinguisher=d->second;
924 exprt &shadow=shadow_distinguishers[distinguisher];
930 assign->swap(*fixedt);
946 for(
const auto &target : t->targets)
948 if(target->location_number > t->location_number)
959 fixedt->targets.clear();
960 fixedt->targets.push_back(kill);
970 fixedt->targets.clear();
971 fixedt->targets.push_back(end);
976 fixedt->targets.clear();
977 fixedt->targets.push_back(kill);
990 const exprt &shadow=shadow_distinguishers[expr];
1007 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
1025 for(expr_sett::iterator it=influence.begin();
1026 it!=influence.end();
1029 if(it->id()==ID_index ||
1030 it->id()==ID_dereference)