Asks an SMT solver whether simplifier rewrites preserved meaning. More...

#include <simplification_equivalence.h>

Public Member Functions
	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)

Detailed Description

Asks an SMT solver whether simplifier rewrites preserved meaning.

Holds one solver per calling thread for its lifetime and pushes a frame per query. A solver per query would be simpler, but create_solver leaks its tuple flattener (solve.cpp) – ~14 KB, harmless at one call per run and fatal at one call per rewrite, which is what the installed checker does. Per thread rather than one flat: –parallel-solving simplifies on several threads at once, and an smt_convt is not safe to share between them.

Free symbols stay free, so equivalent means equivalence under every valuation, not merely on some model. Declines (returns skipped) rather than guessing for shapes whose equality is not a plain SMT question – pointers, side effects, code, and terms conversion cannot be asked to build – the last of which has to be screened up front, see sorts_agree() in the implementation (esbmc/esbmc#7220).

Constructor & Destructor Documentation

◆ simplification_equivalence_checkert()

simplification_equivalence_checkert::simplification_equivalence_checkert	(	const namespacet &	ns,
		const optionst &	options )

◆ ~simplification_equivalence_checkert()

simplification_equivalence_checkert::~simplification_equivalence_checkert ( )

default

Member Function Documentation

◆ check()

simplification_equivalencet simplification_equivalence_checkert::check	(	const expr2tc &	before,
		const expr2tc &	after,
		std::string *	witness = nullptr )

Parameters

witness when non-null and the verdict is differs, receives a valuation of the free symbols on which the two disagree.

The documentation for this class was generated from the following files:

src/solvers/smt/simplification_equivalence.h
src/solvers/smt/simplification_equivalence.cpp