smt_convt Class Reference

Slim, frontend-facing SMT interface. More...

#include <smt_conv.h>

Public Member Functions
	smt_convt (std::unique_ptr< smt_solver_baset > impl)
	~smt_convt ()
void	push_ctx ()
void	pop_ctx ()
smt_resultt	dec_solve ()
smt_resultt	dec_solve_assuming (const std::vector< expr2tc > &assumptions)
	Solve with each boolean expression in assumptions held true for this query only.
bool	supports_assumptions () const
void	pre_solve ()
const std::string	solver_text ()
void	convert_ast (const expr2tc &expr)
	Encode an expression into the solver context.
void	convert_assign (const expr2tc &expr)
void	define (const expr2tc &expr)
	Like convert_assign, but only binds the symbol to its value; nothing is asserted.
void	renumber_symbol_address (const expr2tc &guard, const expr2tc &addr_symbol, const expr2tc &new_size)
	Re-register the address-space entry for a renumbered dynamic object.
expr2tc	get (const expr2tc &expr)
	Fetch the model value of an expression.
expr2tc	get_by_type (const expr2tc &expr)
expr2tc	get_by_ast (const expr2tc &expr)
tvt	l_get (const expr2tc &expr)
	Boolean model value of an expression.
bool	has_model () const
	Whether a satisfiable result can be turned into a model.
void	assert_expr (const expr2tc &e)
	Assert a boolean expression into the solver context.
void	note_division_operands (const expr2tc &expr, std::unordered_set< const expr2t * > &seen)
	Record divisions in expr so the modulus conversion can lower a remainder compositionally exactly when its operands are also divided somewhere in the formula.
void	begin_step (const expr2tc &guard, const expr2tc &cond)
	Bracket the conversion of one SSA step by its guard and condition, and name the assignment it makes, if any.
void	note_assignment (const expr2tc &lhs, const expr2tc &rhs)
void	end_step ()
void	dump_expr (const expr2tc &expr)
	Convert and dump an expression in SMT format (–ssa-smt-trace).
std::string	dump_smt ()
void	print_model ()

Detailed Description

Slim, frontend-facing SMT interface.

smt_convt owns a full solver implementation (smt_solver_baset) and exposes only the expr2tc-level API that the rest of ESBMC needs: convert an SSA equation, solve, and read back model values. The solver-handle types (smt_astt, smt_sortt, ast_vec) and the AST/sort construction machinery stay inside smt_solver_baset and are not reachable through this header.

Callers that genuinely need the implementation (the equation conversion loop, runtime_encoded_equationt) reach it through solver(); this is a transitional escape hatch while the conversion loop still lives in goto-symex.

Constructor & Destructor Documentation

smt_convt()

smt_convt::smt_convt ( std::unique_ptr< smt_solver_baset > impl )

explicit

~smt_convt()

smt_convt::~smt_convt ( )

default

Member Function Documentation

assert_expr()

void smt_convt::assert_expr

(

const expr2tc &

e

)

Assert a boolean expression into the solver context.

begin_step()

void smt_convt::begin_step	(	const expr2tc &	guard,
		const expr2tc &	cond )

Bracket the conversion of one SSA step by its guard and condition, and name the assignment it makes, if any.

Every step must be bracketed; a bitcast converted outside one is read by no rebuild.

convert_assign()

void smt_convt::convert_assign

(

const expr2tc &

expr

)

convert_ast()

void smt_convt::convert_ast

(

const expr2tc &

expr

)

Encode an expression into the solver context.

The resulting solver AST is retained internally (the SSA equation only needs the side effect of conversion, never the handle), so neither these nor any other smt_convt method exposes a solver-handle type.

dec_solve()

smt_resultt smt_convt::dec_solve

(

)

dec_solve_assuming()

smt_resultt smt_convt::dec_solve_assuming

(

const std::vector< expr2tc > &

assumptions

)

Solve with each boolean expression in assumptions held true for this query only.

define()

void smt_convt::define

(

const expr2tc &

expr

)

Like convert_assign, but only binds the symbol to its value; nothing is asserted.

dump_expr()

void smt_convt::dump_expr

(

const expr2tc &

expr

)

Convert and dump an expression in SMT format (–ssa-smt-trace).

dump_smt()

std::string smt_convt::dump_smt

(

)

end_step()

void smt_convt::end_step

(

)

get()

expr2tc smt_convt::get

(

const expr2tc &

expr

)

Fetch the model value of an expression.

get_by_ast()

expr2tc smt_convt::get_by_ast

(

const expr2tc &

expr

)

get_by_type()

expr2tc smt_convt::get_by_type

(

const expr2tc &

expr

)

has_model()

bool smt_convt::has_model

(

)

const

Whether a satisfiable result can be turned into a model.

False for the subprocess SMT-LIB backends with no interactive model solver attached: they answer sat/unsat, but get() and l_get() have nothing to read.

l_get()

tvt smt_convt::l_get

(

const expr2tc &

expr

)

Boolean model value of an expression.

note_assignment()

void smt_convt::note_assignment	(	const expr2tc &	lhs,
		const expr2tc &	rhs )

note_division_operands()

void smt_convt::note_division_operands	(	const expr2tc &	expr,
		std::unordered_set< const expr2t * > &	seen )

Record divisions in expr so the modulus conversion can lower a remainder compositionally exactly when its operands are also divided somewhere in the formula.

Nodes in seen are skipped and visited ones added, so a set shared across calls walks each node once; the expressions must outlive seen.

pop_ctx()

void smt_convt::pop_ctx

(

)

pre_solve()

void smt_convt::pre_solve

(

)

print_model()

void smt_convt::print_model

(

)

push_ctx()

void smt_convt::push_ctx

(

)

renumber_symbol_address()

void smt_convt::renumber_symbol_address	(	const expr2tc &	guard,
		const expr2tc &	addr_symbol,
		const expr2tc &	new_size )

Re-register the address-space entry for a renumbered dynamic object.

solver_text()

const std::string smt_convt::solver_text

(

)

supports_assumptions()

bool smt_convt::supports_assumptions

(

)

const

---

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

• src/solvers/smt/smt_conv.h
• src/solvers/smt/smt_conv.cpp