27 for(
auto &entry :
solver.get_cache())
29 const auto &expr = entry.first;
32 auto value =
solver.l_get(entry.second);
34 std::cout <<
"|| " <<
format(expr) <<
" --> " << value <<
"\n";
40 for(
auto &entry :
solver.get_map().get_mapping())
42 const auto &identifier = entry.first;
43 auto symbol =
symbol_exprt(identifier, entry.second.type);
44 auto value =
solver.get(symbol);
45 std::cout <<
"|| " <<
format(symbol) <<
" --> " <<
format(value) <<
"\n";
50 for(
auto &entry :
solver.get_symbols())
52 const auto &identifier = entry.first;
53 auto value =
solver.l_get(entry.second);
54 std::cout <<
"|| " << identifier <<
" --> " << value <<
"\n";
60 const std::unordered_map<exprt, exprt, irep_hash> &memory,
77 if(
m_it == memory.end())
97 const std::unordered_map<exprt, exprt, irep_hash> &memory,
107 const std::vector<framet> &
frames,
113 propertyt::tracet trace;
116 std::unordered_map<exprt, exprt, irep_hash> memory;
148 state.
updates.emplace_back(address, value);
149 memory[address] = value;
159 if(value.is_not_nil() && value != evaluate_expr)
161 state.
updates.emplace_back(address, value);
162 memory[address] = value;
167 trace.push_back(std::move(state));
174 const std::vector<framet> &
frames,
176 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
207 throw "error reported by solver";
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
exprt translate(exprt) const
An interface for a decision procedure for satisfiability problems.
Base class for all expressions.
const irep_idt & id() const
void set_verbosity(unsigned _verbosity)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Operator to return the address of an object.
Expression to hold a symbol (variable)
static exprt evaluator_rec(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
static exprt evaluator(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
std::optional< propertyt::tracet > counterexample_found(const std::vector< framet > &frames, const workt &work, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)
void show_assignment(const bv_pointers_widet &solver)
propertyt::tracet counterexample(const std::vector< framet > &frames, const workt &work, const bv_pointers_widet &solver, const axiomst &axioms, const namespacet &ns)
static exprt implication(exprt lhs, exprt rhs)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_expr(exprt src, const namespacet &ns)
Simplify State Expression.
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
std::vector< trace_updatet > updates