simplification_equivalence.h File Reference

#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>

Include dependency graph for simplification_equivalence.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	simplification_equivalence_checkert
	Asks an SMT solver whether simplifier rewrites preserved meaning. More...
struct	simplification_check_scopet
	Reports the stats and uninstalls the checker when it goes out of scope. More...

Namespaces
namespace	simplification_check_stats
	How much check() actually decided, over every caller.

Enumerations
enum class	simplification_equivalencet { equivalent , differs , malformed , skipped }
	Verdict on one simplifier rewrite (esbmc/esbmc#4625). More...

Functions
simplification_equivalencet	check_simplification_equivalence (const expr2tc &before, const expr2tc &after, const namespacet &ns, const optionst &options)
	One-shot convenience over the above; builds and discards a solver.
void	install_simplification_equivalence_check (const namespacet &ns, const optionst &options)
	Install the above as simplify()'s checker for the rest of the run: every rewrite is proved, and a differs verdict logs both expressions and exits.
void	simplification_check_stats::report ()

Enumeration Type Documentation

simplification_equivalencet

enum class simplification_equivalencet

strong

Verdict on one simplifier rewrite (esbmc/esbmc#4625).

Enumerator
equivalent	The solver proved before == after for every valuation.
differs	The solver found a valuation where they differ: a simplifier bug.
malformed	after has operands whose sorts disagree: also a simplifier bug, and one that would abort any backend rather than yield a wrong answer.
skipped	Not decided – a shape the check declines, or a solver failure.

Function Documentation

check_simplification_equivalence()

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

One-shot convenience over the above; builds and discards a solver.

install_simplification_equivalence_check()

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

Install the above as simplify()'s checker for the rest of the run: every rewrite is proved, and a differs verdict logs both expressions and exits.

Does nothing unless the build enabled the check.