goto_invariant_synthesis.h

Go to the documentation of this file.

#ifndef GOTO_PROGRAMS_GOTO_INVARIANT_SYNTHESIS_H_
#define GOTO_PROGRAMS_GOTO_INVARIANT_SYNTHESIS_H_
 
#include <goto-programs/goto_functions.h>
#include <irep2/irep2_expr.h>

struct overflow_checkst
{
  bool signed_arith = false;
  bool unsigned_arith = false;
};

namespace invariant_synthesis
{
bool split_bound(
  const expr2tc &cond,
  expr2tc &counter,
  expr2tc &bound,
  bool &inclusive);

bool is_self_increment(
  const expr2tc &target,
  const expr2tc &source,
  expr2tc &addend);

bool entry_admits_two_disjunct_bound(const expr2tc &entry, bool inclusive);
} // namespace invariant_synthesis

void goto_synthesise_loop_invariants(
  goto_functionst &goto_functions,
  const overflow_checkst &overflow,
  bool k_induction_ran);
 
#endif /* GOTO_PROGRAMS_GOTO_INVARIANT_SYNTHESIS_H_ */