63 for(distinguish_valuest::iterator jt=it->begin();
67 exprt distinguisher=jt->first;
68 bool taken=jt->second;
73 distinguisher.
swap(negated);
76 or_exprt disjunct(new_path, distinguisher);
77 new_path.
swap(disjunct);
90 std::cout <<
"Found a path\n";
100 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
104 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
112 for(natural_loops_mutablet::natural_loopt::iterator it=
loop.begin();
122 for(
const auto &succ : succs)
148 assert(succs.size() > 0);
160 bool found_branch=
false;
162 for(
const auto &succ : succs)
165 bool taken=scratch_program.
eval(distinguisher).
is_true();
170 (succ->location_number <
next->location_number))
179 assert(found_branch);
190 for(goto_programt::targetst::iterator it=t->targets.begin();
191 it!=t->targets.end();
217 std::map<exprt, exprt> shadow_distinguishers;
250 exprt &distinguisher=*it;
254 shadow_distinguishers[distinguisher]=shadow;
257 assign->make_assignment();
281 exprt &distinguisher=d->second;
282 exprt &shadow=shadow_distinguishers[distinguisher];
285 assign->make_assignment();
288 assign->swap(*fixedt);
294 assert(fixedt->is_goto());
304 for(
const auto &target : t->targets)
306 if(target->location_number > t->location_number)
317 fixedt->targets.clear();
318 fixedt->targets.push_back(kill);
328 fixedt->targets.clear();
329 fixedt->targets.push_back(end);
334 fixedt->targets.clear();
335 fixedt->targets.push_back(kill);
348 const exprt &shadow=shadow_distinguishers[expr];
void update()
Update all indices.
targett add_instruction()
Adds an instruction at the end.
Generate Equation using Symbolic Execution.
instructionst instructions
The list of instructions in the goto program.
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...
std::list< distinguish_valuest > accelerated_paths
natural_loops_mutablet::natural_loopt & loop
std::list< Target > get_successors(Target target) const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
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)
API to expression classes.
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
targett insert_after(const_targett target)
Insertion after the given target.
bool check_sat(bool do_slice)
The boolean constant false.
targett insert_before(const_targett target)
Insertion before the given target.
symbol_tablet & symbol_table
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
std::map< exprt, bool > distinguish_valuest
Base class for all expressions.
void find_distinguishing_points()
#define Forall_goto_program_instructions(it, program)
goto_programt::targett loop_header
Expression to hold a symbol (variable)
instructionst::iterator targett
goto_programt & goto_program