simplification_equivalence.cpp File Reference

#include <solvers/smt/simplification_equivalence.h>
#include <cstddef>
#include <cstdlib>
#include <memory>
#include <set>
#include <string>
#include <irep2/irep2_utils.h>
#include <irep2/simplification_check.h>
#include <solvers/smt/smt_conv.h>
#include <solvers/smt/smt_result.h>
#include <solvers/solve.h>
#include <util/arith/ieee_float.h>
#include <util/message/format.h>
#include <util/message/message.h>

Include dependency graph for simplification_equivalence.cpp:

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

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 ()

Variables
std::atomic< unsigned long >	simplification_check_stats::proved {0}
std::atomic< unsigned long >	simplification_check_stats::declined {0}
std::atomic< unsigned long >	simplification_check_stats::ill_sorted {0}
	Of the declines, those whose before was already ill-sorted – a defect elsewhere in ESBMC rather than a limit of the check, so a nonzero count is something to go and look at.
std::atomic< unsigned long >	simplification_check_stats::violations {0}
	Rewrites the check rejected.

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.