goto_symex_property_decider.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Property Decider for Goto-Symex
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
 
#include <goto-symex/symex_target_equation.h>
 
#include "properties.h"
#include "solver_factory.h"
 
class ui_message_handlert;
 
class goto_symex_property_decidert
{
public:
  goto_symex_property_decidert(
    const optionst &options,
    ui_message_handlert &ui_message_handler,
    symex_target_equationt &equation,
    const namespacet &ns);
 
  void
  update_properties_goals_from_symex_target_equation(propertiest &properties);
 
  void convert_goals();
 
  void add_constraint_from_goals(
    std::function<bool(const irep_idt &property_id)> select_property);
 
  decision_proceduret::resultt solve();
 
  stack_decision_proceduret &get_decision_procedure() const;
 
  boolbvt &get_boolbv_decision_procedure() const;
 
  symex_target_equationt &get_equation() const;
 
  void update_properties_status_from_goals(
    propertiest &properties,
    std::unordered_set<irep_idt> &updated_properties,
    decision_proceduret::resultt dec_result,
    bool set_pass = true) const;
protected:
  const optionst &options;
  ui_message_handlert &ui_message_handler;
  symex_target_equationt &equation;
  std::unique_ptr<solver_factoryt::solvert> solver;
 
  struct goalt
  {
    std::vector<symex_target_equationt::SSA_stepst::iterator> instances;
 
    exprt condition;
 
    exprt as_expr() const;
  };
 
  std::map<irep_idt, goalt> goal_map;
};
 
#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H