#include <scratch_program.h>
Public Member Functions | |
| scratch_programt (symbol_tablet &_symbol_table) | |
| ~scratch_programt () | |
| void | append (goto_programt::instructionst &instructions) |
| void | append (goto_programt &program) |
| void | append_path (patht &path) |
| void | append_loop (goto_programt &program, goto_programt::targett loop_header) |
| targett | assign (const exprt &lhs, const exprt &rhs) |
| targett | assume (const exprt &guard) |
| bool | check_sat (bool do_slice) |
| bool | check_sat () |
| exprt | eval (const exprt &e) |
| void | fix_types () |
 Public Member Functions inherited from goto_programt | |
| std::ostream & | output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const |
| See below. More... | |
| std::ostream & | output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructiont &instruction) const |
| goto_programt () | |
| goto_programt (const goto_programt &)=delete | |
| goto_programt & | operator= (const goto_programt &)=delete |
| goto_programt (goto_programt &&other) | |
| goto_programt & | operator= (goto_programt &&other) |
| void | get_decl_identifiers (decl_identifierst &decl_identifiers) const |
| Public Member Functions inherited from goto_program_templatet< codet, exprt > | |
| goto_program_templatet (const goto_program_templatet &)=delete | |
| Copying is deleted as this class contains pointers that cannot be copied. More... | |
| goto_program_templatet (goto_program_templatet &&other) | |
| goto_program_templatet () | |
| Constructor. More... | |
| goto_program_templatet & | operator= (const goto_program_templatet &)=delete |
| goto_program_templatet & | operator= (goto_program_templatet &&other) |
| targett | const_cast_target (const_targett t) |
| Convert a const_targett to a targett - use with care and avoid whenever possible. More... | |
| const_targett | const_cast_target (const_targett t) const |
| Dummy for templates with possible const contexts. More... | |
| std::list< Target > | get_successors (Target target) const |
| void | compute_incoming_edges () |
| void | insert_before_swap (targett target) |
| Insertion that preserves jumps to "target". More... | |
| void | insert_before_swap (targett target, instructiont &instruction) |
| Insertion that preserves jumps to "target". More... | |
| void | insert_before_swap (targett target, goto_program_templatet< codet, exprt > &p) |
| Insertion that preserves jumps to "target". More... | |
| targett | insert_before (const_targett target) |
| Insertion before the given target. More... | |
| targett | insert_after (const_targett target) |
| Insertion after the given target. More... | |
| void | destructive_append (goto_program_templatet< codet, exprt > &p) |
| Appends the given program, which is destroyed. More... | |
| void | destructive_insert (const_targett target, goto_program_templatet< codet, exprt > &p) |
| Inserts the given program at the given location. More... | |
| targett | add_instruction () |
| Adds an instruction at the end. More... | |
| targett | add_instruction (goto_program_instruction_typet type) |
| Adds an instruction of given type at the end. More... | |
| std::ostream & | output (const namespacet &ns, const irep_idt &identifier, std::ostream &out) const |
| Output goto program to given stream. More... | |
| std::ostream & | output (std::ostream &out) const |
| Output goto-program to given stream. More... | |
| virtual std::ostream & | output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const=0 |
| Output a single instruction. More... | |
| void | compute_target_numbers () |
| Compute the target numbers. More... | |
| void | compute_location_numbers (unsigned &nr) |
| Compute location numbers. More... | |
| void | compute_location_numbers () |
| Compute location numbers. More... | |
| void | compute_loop_numbers () |
| Compute loop numbers. More... | |
| void | update () |
| Update all indices. More... | |
| bool | empty () const |
| Is the program empty? More... | |
| virtual | ~goto_program_templatet () |
| void | swap (goto_program_templatet< codet, exprt > &program) |
| Swap the goto program. More... | |
| void | clear () |
| Clear the goto program. More... | |
| targett | get_end_function () |
| void | copy_from (const goto_program_templatet< codet, exprt > &src) |
| Copy a full goto program, preserving targets. More... | |
| bool | has_assertion () const |
| Does the goto program have an assertion? More... | |
Public Attributes | |
| bool | constant_propagation |
| Public Attributes inherited from goto_program_templatet< codet, exprt > | |
| instructionst | instructions |
| The list of instructions in the goto program. More... | |
Protected Attributes | |
| goto_symex_statet | symex_state |
| goto_functionst | functions |
| symbol_tablet & | symbol_table |
| const namespacet | ns |
| symex_target_equationt | equation |
| goto_symext | symex |
| propt * | satcheck |
| bv_pointerst | satchecker |
| smt2_dect | z3 |
| prop_convt * | checker |
Additional Inherited Members | |
| Public Types inherited from goto_programt | |
| typedef std::set< irep_idt > | decl_identifierst |
| Public Types inherited from goto_program_templatet< codet, exprt > | |
| typedef std::list< instructiont > | instructionst |
| typedef instructionst::iterator | targett |
| typedef instructionst::const_iterator | const_targett |
| typedef std::list< targett > | targetst |
| typedef std::list< const_targett > | const_targetst |
| Static Public Member Functions inherited from goto_program_templatet< codet, exprt > | |
| static const irep_idt | get_function_id (const_targett l) |
| static const irep_idt | get_function_id (const goto_program_templatet< codet, exprt > &p) |
| static irep_idt | loop_id (const_targett target) |
| Human-readable loop name. More... | |
Detailed Description
Definition at line 32 of file scratch_program.h.
Constructor & Destructor Documentation
◆ scratch_programt()
|
inlineexplicit |
Definition at line 35 of file scratch_program.h.
◆ ~scratch_programt()
|
inline |
Definition at line 48 of file scratch_program.h.
References satcheck.
Member Function Documentation
◆ append() [1/2]
| void scratch_programt::append | ( | goto_programt::instructionst & | instructions | ) |
Definition at line 76 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::instructions.
Referenced by append_loop(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), polynomial_acceleratort::check_inductive(), disjunctive_polynomial_accelerationt::find_path(), polynomial_acceleratort::fit_const(), and sat_path_enumeratort::next().
◆ append() [2/2]
| void scratch_programt::append | ( | goto_programt & | program | ) |
Definition at line 175 of file scratch_program.cpp.
References goto_program_templatet< codeT, guardT >::copy_from(), and goto_program_templatet< codet, exprt >::destructive_append().
◆ append_loop()
| void scratch_programt::append_loop | ( | goto_programt & | program, |
| goto_programt::targett | loop_header | ||
| ) |
Definition at line 183 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), append(), assume(), goto_program_templatet< codet, exprt >::instructions, SKIP, and goto_program_templatet< codet, exprt >::update().
◆ append_path()
| void scratch_programt::append_path | ( | patht & | path | ) |
Definition at line 151 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), ASSUME, and goto_program_templatet< codet, exprt >::instructions.
Referenced by acceleration_utilst::check_inductive().
◆ assign()
| goto_programt::targett scratch_programt::assign | ( | const exprt & | lhs, |
| const exprt & | rhs | ||
| ) |
Definition at line 84 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), and ASSIGN.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), acceleration_utilst::assign_array(), acceleratet::build_state_machine(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), acceleration_utilst::do_nonrecursive(), acceleration_utilst::stash_variables(), and polynomial_acceleratort::stash_variables().
◆ assume()
| goto_programt::targett scratch_programt::assume | ( | const exprt & | guard | ) |
Definition at line 95 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), and ASSUME.
Referenced by append_loop(), acceleration_utilst::assign_array(), acceleratet::build_state_machine(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), disjunctive_polynomial_accelerationt::find_path(), disjunctive_polynomial_accelerationt::fit_polynomial(), and sat_path_enumeratort::next().
◆ check_sat() [1/2]
| bool scratch_programt::check_sat | ( | bool | do_slice | ) |
Definition at line 25 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::add_instruction(), checker, constant_propagation, goto_symext::constant_propagation, symex_target_equationt::convert(), symex_target_equationt::count_assertions(), decision_proceduret::D_SATISFIABLE, decision_proceduret::dec_solve(), END_FUNCTION, equation, fix_types(), functions, ns, goto_program_templatet< codet, exprt >::output(), remove_skip(), slice(), symex, symex_state, and goto_program_templatet< codet, exprt >::update().
Referenced by acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), acceleration_utilst::do_assumptions(), disjunctive_polynomial_accelerationt::find_path(), polynomial_acceleratort::fit_const(), disjunctive_polynomial_accelerationt::fit_polynomial(), polynomial_acceleratort::fit_polynomial_sliced(), and sat_path_enumeratort::next().
◆ check_sat() [2/2]
|
inline |
Definition at line 63 of file scratch_program.h.
◆ eval()
Definition at line 67 of file scratch_program.cpp.
References checker, decision_proceduret::get(), ns, goto_symex_statet::rename(), and symex_state.
Referenced by sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), acceleration_utilst::extract_polynomial(), polynomial_acceleratort::fit_const(), sat_path_enumeratort::record_path(), and disjunctive_polynomial_accelerationt::record_path().
◆ fix_types()
| void scratch_programt::fix_types | ( | ) |
Definition at line 128 of file scratch_program.cpp.
References goto_program_templatet< codet, exprt >::instructions, code_assignt::lhs(), code_assignt::rhs(), to_code_assign(), and exprt::type().
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), and check_sat().
Member Data Documentation
◆ checker
|
protected |
Definition at line 85 of file scratch_program.h.
Referenced by check_sat(), and eval().
◆ constant_propagation
| bool scratch_programt::constant_propagation |
Definition at line 72 of file scratch_program.h.
Referenced by check_sat().
◆ equation
|
protected |
Definition at line 79 of file scratch_program.h.
Referenced by check_sat().
◆ functions
|
protected |
Definition at line 76 of file scratch_program.h.
Referenced by check_sat().
◆ ns
|
protected |
Definition at line 78 of file scratch_program.h.
Referenced by check_sat(), and eval().
◆ satcheck
|
protected |
Definition at line 82 of file scratch_program.h.
Referenced by ~scratch_programt().
◆ satchecker
|
protected |
Definition at line 83 of file scratch_program.h.
◆ symbol_table
|
protected |
Definition at line 77 of file scratch_program.h.
◆ symex
|
protected |
Definition at line 80 of file scratch_program.h.
Referenced by check_sat().
◆ symex_state
|
protected |
Definition at line 75 of file scratch_program.h.
Referenced by check_sat(), and eval().
◆ z3
|
protected |
Definition at line 84 of file scratch_program.h.
The documentation for this class was generated from the following files:
- goto-instrument/accelerate/scratch_program.h
- goto-instrument/accelerate/scratch_program.cpp
