ai_domain.h

Go to the documentation of this file.

 
#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
#define CPROVER_ANALYSES_AI_DOMAIN_H
 
#include <goto-programs/goto_program.h>
#include <irep2/irep2_utils.h>
 
// forward reference the abstract interpreter interface
class ai_baset;

class ai_domain_baset
{
protected:
  ai_domain_baset()
  {
  }
 
public:
  virtual ~ai_domain_baset()
  {
  }

 
  virtual void transform(
    goto_programt::const_targett from,
    goto_programt::const_targett to,
    ai_baset &ai,
    const namespacet &ns) = 0;
 
  virtual void output(std::ostream &out) const = 0;

  virtual void make_bottom() = 0;

  virtual void make_top() = 0;

  virtual void make_entry() = 0;
 
  virtual bool is_bottom() const = 0;
 
  virtual bool is_top() const = 0;



  virtual bool ai_simplify(expr2tc &condition, const namespacet &ns) const = 0;

  virtual bool ai_simplify_lhs(expr2tc &condition, const namespacet &ns) const;

  virtual expr2tc to_predicate(void) const
  {
    if (is_bottom())
      return gen_false_expr();
    return gen_true_expr();
  }
};
 
#endif