36 std::map<exprt, polynomialt> polynomials;
42 std::cout <<
"Polynomial accelerating program:\n";
44 for(goto_programt::instructionst::iterator
55 std::cout <<
"Modified:\n";
57 for(expr_sett::iterator it=
modified.begin();
61 std::cout <<
expr2c(*it,
ns) <<
'\n';
82 for(expr_sett::iterator it=
modified.begin();
89 if(it->type().id()==ID_bool)
95 if(target.
id()==ID_index ||
96 target.
id()==ID_dereference)
104 std::map<exprt, polynomialt> this_poly;
105 this_poly[target]=poly;
110 std::cout <<
"Fitted a polynomial for " <<
expr2c(target,
ns)
113 polynomials[target]=poly;
120 if(polynomials.empty())
133 for(patht::iterator it=accelerator.
path.begin();
134 it!=accelerator.
path.end();
137 if(it->loc->is_assign() || it->loc->is_decl())
139 assigns.push_back(*(it->loc));
143 for(expr_sett::iterator it=dirty.begin();
148 std::cout <<
"Trying to accelerate " <<
expr2c(*it,
ns) <<
'\n';
151 if(it->type().id()==ID_bool)
156 std::cout <<
"Ignoring boolean\n";
161 if(it->id()==ID_index ||
162 it->id()==ID_dereference)
165 std::cout <<
"Ignoring array reference\n";
174 std::cout <<
"We've accelerated it already\n";
185 std::cout <<
"Ignoring because it depends on an array\n";
196 std::map<exprt, polynomialt> this_poly;
197 this_poly[target]=poly;
201 polynomials[target]=poly;
208 std::cout <<
"Failed to accelerate " <<
expr2c(*it,
ns) <<
'\n';
228 bool path_is_monotone;
235 catch(
const std::string &s)
238 std::cout <<
"Assumptions error: " << s <<
'\n';
242 exprt pre_guard(guard);
244 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
245 it!=polynomials.end();
294 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
295 it!=polynomials.end();
298 program.assign(it->first, it->second.to_expr());
327 program.append(
fixed);
328 program.append(
fixed);
337 for(distinguish_valuest::iterator jt=it->begin();
341 exprt distinguisher=jt->first;
342 bool taken=jt->second;
347 distinguisher.
swap(negated);
350 or_exprt disjunct(new_path, distinguisher);
351 new_path.
swap(disjunct);
354 program.assume(new_path);
364 std::cout <<
"Found a path\n";
372 catch(
const std::string &s)
374 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
378 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
390 std::vector<expr_listt> parameters;
391 std::set<std::pair<expr_listt, exprt> > coefficients;
399 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
400 <<
", which depends on:\n";
402 for(expr_sett::iterator it=influence.begin();
406 std::cout <<
expr2c(*it,
ns) <<
'\n';
410 for(expr_sett::iterator it=influence.begin();
414 if(it->id()==ID_index ||
415 it->id()==ID_dereference)
424 exprs.push_back(*it);
425 parameters.push_back(exprs);
428 parameters.push_back(exprs);
434 parameters.push_back(exprs);
438 parameters.push_back(exprs);
442 parameters.push_back(exprs);
444 for(std::vector<expr_listt>::iterator it=parameters.begin();
445 it!=parameters.end();
449 coefficients.insert(make_pair(*it, coeff.
symbol_expr()));
470 std::map<exprt, exprt> ivals1;
471 std::map<exprt, exprt> ivals2;
472 std::map<exprt, exprt> ivals3;
474 for(expr_sett::iterator it=influence.begin();
523 std::map<exprt, exprt> values;
525 for(expr_sett::iterator it=influence.begin();
529 values[*it]=ivals1[*it];
534 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
544 for(
int n=0; n <= 1; n++)
546 for(expr_sett::iterator it=influence.begin();
550 values[*it]=ivals2[*it];
553 values[*it]=ivals3[*it];
556 values[*it]=ivals1[*it];
560 for(expr_sett::iterator it=influence.begin();
564 values[*it]=ivals3[*it];
578 for(distinguish_valuest::iterator jt=it->begin();
582 exprt distinguisher=jt->first;
583 bool taken=jt->second;
588 distinguisher.
swap(negated);
591 or_exprt disjunct(new_path, distinguisher);
592 new_path.
swap(disjunct);
595 program.assume(new_path);
610 std::cout <<
"Found a polynomial\n";
620 catch(
const std::string &s)
622 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
626 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
634 std::map<exprt, exprt> &values,
635 std::set<std::pair<expr_listt, exprt> > &coefficients,
643 for(std::map<exprt, exprt>::iterator it=values.begin();
647 if(!expr_type.has_value())
649 expr_type=it->first.type();
653 expr_type =
join_types(*expr_type, it->first.type());
658 for(std::map<exprt, exprt>::iterator it=values.begin();
662 program.
assign(it->first, it->second);
666 for(
int i=0; i<num_unwindings; i++)
668 program.
append(loop_body);
674 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
675 it!=coefficients.end();
680 for(expr_listt::const_iterator e_it=it->first.begin();
681 e_it!=it->first.end();
689 from_integer(num_unwindings, *expr_type), concrete_value);
690 mult.
swap(concrete_value);
694 std::map<exprt, exprt>::iterator v_it=values.find(e);
698 mult_exprt mult(concrete_value, v_it->second);
699 mult.
swap(concrete_value);
739 for(
const auto &loop_instruction :
loop)
747 for(
const auto &jt : succs)
772 "we should have a looping path, so we should never hit a location "
773 "with no successors.");
785 bool found_branch=
false;
787 for(
const auto &succ : succs)
790 bool taken=scratch_program.
eval(distinguisher).
is_true();
795 (succ->location_number < next->location_number))
815 for(goto_programt::targetst::iterator it=t->targets.begin();
816 it!=t->targets.end();
821 cond = t->get_condition();
841 std::map<exprt, exprt> shadow_distinguishers;
847 if(instruction.is_assert())
849 instruction.type =
ASSUME;
872 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
876 exprt &distinguisher=*it;
880 shadow_distinguishers[distinguisher]=shadow;
899 fixedt->turn_into_skip();
907 exprt &distinguisher=d->second;
908 exprt &shadow=shadow_distinguishers[distinguisher];
914 assign->swap(*fixedt);
930 for(
const auto &target : t->targets)
932 if(target->location_number > t->location_number)
943 fixedt->targets.clear();
944 fixedt->targets.push_back(kill);
954 fixedt->targets.clear();
955 fixedt->targets.push_back(end);
960 fixedt->targets.clear();
961 fixedt->targets.push_back(kill);
974 const exprt &shadow=shadow_distinguishers[expr];
991 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
1009 for(expr_sett::iterator it=influence.begin();
1010 it!=influence.end();
1013 if(it->id()==ID_index ||
1014 it->id()==ID_dereference)