enumerative_loop_contracts_synthesizer.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Enumerative Loop Contracts Synthesizer
 
Author: Qinheping Hu
 
\*******************************************************************/
 
 
// NOLINTNEXTLINE(whitespace/line_length)
#ifndef CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
// NOLINTNEXTLINE(whitespace/line_length)
#define CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
 
#include <util/options.h>
 
#include "cegis_verifier.h"
#include "loop_contracts_synthesizer_base.h"
 
class messaget;
class goto_modelt;
 
class enumerative_loop_contracts_synthesizert
  : public loop_contracts_synthesizer_baset
{
public:
  enumerative_loop_contracts_synthesizert(
    goto_modelt &goto_model,
    const optionst &options,
    messaget &log)
    : loop_contracts_synthesizer_baset(goto_model, log),
      options(options),
      ns(goto_model.symbol_table),
      original_symbol_table(goto_model.symbol_table)
  {
  }
 
  invariant_mapt synthesize_all() override;
  exprt synthesize(loop_idt loop_id) override;
 
  std::map<loop_idt, std::set<exprt>> get_assigns_map() const
  {
    return assigns_map;
  }
 
  const optionst &options;
  namespacet ns;
 
private:
  void init_candidates();
 
  void build_tmp_post_map();
 
  std::set<symbol_exprt> compute_dependent_symbols(
    const loop_idt &cause_loop_id,
    const exprt &new_clause,
    const std::set<exprt> &live_vars);
 
  exprt synthesize_range_predicate(const exprt &violated_predicate);
 
  exprt synthesize_same_object_predicate(const exprt &checked_pointer);
 
  exprt synthesize_strengthening_clause(
    const std::vector<exprt> terminal_symbols,
    const loop_idt &cause_loop_id,
    const irep_idt &violation_id,
    const std::vector<cext> &cexs);
 
  void synthesize_assigns(
    const exprt &checked_pointer,
    const std::list<loop_idt> cause_loop_ids);
 
  invariant_mapt in_invariant_clause_map;
  invariant_mapt pos_invariant_clause_map;
  invariant_mapt neg_guards;
 
  std::map<loop_idt, std::set<exprt>> assigns_map;
 
  std::unordered_map<exprt, exprt, irep_hash> tmp_post_map;
 
  const symbol_tablet original_symbol_table;
};
 
// NOLINTNEXTLINE(whitespace/line_length)
#endif // CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H