62 for(distinguish_valuest::iterator jt=it->begin();
66 exprt distinguisher=jt->first;
67 bool taken=jt->second;
72 distinguisher.
swap(negated);
75 or_exprt disjunct(new_path, distinguisher);
76 new_path.
swap(disjunct);
89 std::cout <<
"Found a path\n";
97 catch(
const std::string &s)
99 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
103 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
111 for(natural_loops_mutablet::natural_loopt::iterator it=
loop.begin();
121 for(
const auto &succ : succs)
147 assert(succs.size() > 0);
159 bool found_branch=
false;
161 for(
const auto &succ : succs)
164 bool taken=scratch_program.
eval(distinguisher).
is_true();
169 (succ->location_number <
next->location_number))
178 assert(found_branch);
189 for(goto_programt::targetst::iterator it=t->targets.begin();
190 it!=t->targets.end();
216 std::map<exprt, exprt> shadow_distinguishers;
249 exprt &distinguisher=*it;
253 shadow_distinguishers[distinguisher]=shadow;
256 assign->make_assignment();
280 exprt &distinguisher=d->second;
281 exprt &shadow=shadow_distinguishers[distinguisher];
284 assign->make_assignment();
287 assign->swap(*fixedt);
293 assert(fixedt->is_goto());
303 for(
const auto &target : t->targets)
305 if(target->location_number > t->location_number)
316 fixedt->targets.clear();
317 fixedt->targets.push_back(kill);
327 fixedt->targets.clear();
328 fixedt->targets.push_back(end);
333 fixedt->targets.clear();
334 fixedt->targets.push_back(kill);
347 const exprt &shadow=shadow_distinguishers[expr];
void update()
Update all indices.
message_handlert & message_handler
Generate Equation using Symbolic Execution.
targett insert_before(const_targett target)
Insertion before the given target.
acceleration_utilst utils
std::list< exprt > distinguishers
Goto Programs with Functions.
distinguish_mapt distinguishing_points
void build_path(scratch_programt &scratch_program, patht &path)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::list< distinguish_valuest > accelerated_paths
natural_loops_mutablet::natural_loopt & loop
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
instructionst::iterator targett
targett assume(const exprt &guard)
symbolt fresh_symbol(std::string base, typet type)
exprt eval(const exprt &e)
void record_path(scratch_programt &scratch_program)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
std::list< Target > get_successors(Target target) const
targett insert_after(const_targett target)
Insertion after the given target.
bool check_sat(bool do_slice)
The boolean constant false.
symbol_tablet & symbol_table
std::map< exprt, bool > distinguish_valuest
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void find_distinguishing_points()
#define Forall_goto_program_instructions(it, program)
goto_programt::targett loop_header
Expression to hold a symbol (variable)
goto_programt & goto_program