28 program.append(
fixed);
37 for(distinguish_valuest::iterator jt=it->begin();
41 exprt distinguisher=jt->first;
42 bool taken=jt->second;
47 distinguisher.
swap(negated);
50 or_exprt disjunct(new_path, distinguisher);
51 new_path.
swap(disjunct);
54 program.assume(new_path);
64 std::cout <<
"Found a path\n";
72 catch(
const std::string &s)
74 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
78 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
86 for(natural_loops_mutablet::natural_loopt::const_iterator it =
loop.begin();
96 for(
const auto &succ : succs)
134 bool found_branch=
false;
136 for(
const auto &succ : succs)
139 bool taken=scratch_program.
eval(distinguisher).
is_true();
144 (succ->location_number <
next->location_number))
153 INVARIANT(found_branch,
"no branch taken");
164 for(goto_programt::targetst::iterator it=t->targets.begin();
165 it!=t->targets.end();
170 cond = t->condition();
190 std::map<exprt, exprt> shadow_distinguishers;
194 for(
auto &instruction :
fixed.instructions)
196 if(instruction.is_assert())
197 instruction.turn_into_assume();
223 exprt &distinguisher=*it;
224 symbolt shadow_sym=
utils.fresh_symbol(
"polynomial::shadow_distinguisher",
227 shadow_distinguishers[distinguisher]=shadow;
243 if(!
loop.contains(t))
246 fixedt->turn_into_skip();
254 exprt &distinguisher=d->second;
255 exprt &shadow=shadow_distinguishers[distinguisher];
261 assign->swap(*fixedt);
277 for(
const auto &target : t->targets)
279 if(target->location_number > t->location_number)
282 if(!
loop.contains(target))
290 fixedt->targets.clear();
291 fixedt->targets.push_back(kill);
301 fixedt->targets.clear();
302 fixedt->targets.push_back(end);
307 fixedt->targets.clear();
308 fixedt->targets.push_back(kill);
321 const exprt &shadow=shadow_distinguishers[expr];
A goto_instruction_codet representing an assignment in the program.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
The Boolean constant false.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
guard_managert & guard_manager
acceleration_utilst utils
distinguish_mapt distinguishing_points
message_handlert & message_handler
goto_programt::targett loop_header
void build_path(scratch_programt &scratch_program, patht &path)
std::list< distinguish_valuest > accelerated_paths
symbol_table_baset & symbol_table
goto_programt & goto_program
void record_path(scratch_programt &scratch_program)
std::map< exprt, bool > distinguish_valuest
natural_loops_mutablet::natural_loopt & loop
std::list< exprt > distinguishers
void find_distinguishing_points()
void append(goto_programt::instructionst &instructions)
exprt eval(const exprt &e)
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
std::list< path_nodet > patht
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.