simplification_check.h

Go to the documentation of this file.

#ifndef ESBMC_IREP2_SIMPLIFICATION_CHECK_H
#define ESBMC_IREP2_SIMPLIFICATION_CHECK_H
 
#include <functional>
#include <irep2/irep2_expr.h>

namespace simplification_check
{
using checkert =
  std::function<void(const expr2tc &before, const expr2tc &after)>;
 
void install(checkert checker);

void clear();
 
namespace detail
{
void run(const expr2tc &before, const expr2tc &after);
}

inline void verify_rewrite(const expr2tc &before, const expr2tc &after)
{
#ifdef ENABLE_SIMPLIFIER_EQUIVALENCE_CHECK
  detail::run(before, after);
#else
  (void)before;
  (void)after;
#endif
}

inline void verify_node_rewrite(const expr2t &before, const expr2tc &after)
{
#ifdef ENABLE_SIMPLIFIER_EQUIVALENCE_CHECK
  detail::run(before.clone(), after);
#else
  (void)before;
  (void)after;
#endif
}

inline void verify_rewrite_or_node(
  const expr2tc &before,
  const expr2t &node,
  const expr2tc &after)
{
#ifdef ENABLE_SIMPLIFIER_EQUIVALENCE_CHECK
  detail::run(is_nil_expr(before) ? node.clone() : before, after);
#else
  (void)before;
  (void)node;
  (void)after;
#endif
}
} // namespace simplification_check
 
#endif