simplification_equivalence.h

Go to the documentation of this file.

#ifndef _ESBMC_PROP_SMT_SIMPLIFICATION_EQUIVALENCE_H_
#define _ESBMC_PROP_SMT_SIMPLIFICATION_EQUIVALENCE_H_
 
#include <atomic>
#include <map>
#include <memory>
#include <mutex>
#include <string>
#include <thread>
#include <irep2/irep2_expr.h>
#include <util/symtab/namespace.h>
#include <util/config/options.h>

enum class simplification_equivalencet
{
  equivalent,
  differs,
  malformed,
  skipped
};
 
class smt_convt;

class simplification_equivalence_checkert
{
public:
  simplification_equivalence_checkert(
    const namespacet &ns,
    const optionst &options);
  ~simplification_equivalence_checkert();

  simplification_equivalencet check(
    const expr2tc &before,
    const expr2tc &after,
    std::string *witness = nullptr);
 
private:
  void record_witness(
    const expr2tc &before,
    const expr2tc &after,
    smt_convt &ctx,
    std::string &witness);

  smt_convt &solver();
  void drop_solver();
 
  namespacet ns;
  optionst options;
  std::mutex solvers_mutex;
  std::map<std::thread::id, std::unique_ptr<smt_convt>> solvers;
};

simplification_equivalencet check_simplification_equivalence(
  const expr2tc &before,
  const expr2tc &after,
  const namespacet &ns,
  const optionst &options);

void install_simplification_equivalence_check(
  const namespacet &ns,
  const optionst &options);

struct simplification_check_scopet
{
  ~simplification_check_scopet();
};

namespace simplification_check_stats
{
extern std::atomic<unsigned long> proved;
extern std::atomic<unsigned long> declined;
extern std::atomic<unsigned long> ill_sorted;
extern std::atomic<unsigned long> violations;
 
void report();
} // namespace simplification_check_stats
 
#endif