Decision procedure interface for various SMT 2.x solvers. More...

#include <smt2_dec.h>

Inheritance diagram for smt2_dect:

Collaboration diagram for smt2_dect:

Public Member Functions
	smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)

virtual resultt	dec_solve ()

virtual std::string	decision_procedure_text () const

virtual bool	has_set_assumptions () const

Public Member Functions inherited from smt2_convt
	smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)

virtual	~smt2_convt ()

virtual literalt	convert (const exprt &expr)

virtual void	set_frozen (literalt)

virtual void	set_to (const exprt &expr, bool value)

virtual exprt	get (const exprt &expr) const

virtual void	print_assignment (std::ostream &out) const

virtual tvt	l_get (literalt l) const

virtual void	set_assumptions (const bvt &bv)

void	convert_expr (const exprt &)

void	convert_type (const typet &)

void	convert_literal (const literalt)

Public Member Functions inherited from prop_convt
	prop_convt (const namespacet &_ns)

virtual	~prop_convt ()

literalt	operator() (const exprt &expr)

virtual void	set_frozen (const bvt &)

virtual void	set_all_frozen ()

virtual bool	is_in_conflict (literalt l) const
	determine whether a variable is in the final conflict More...

virtual bool	has_is_in_conflict () const

virtual void	set_time_limit_seconds (uint32_t)

Public Member Functions inherited from decision_proceduret
	decision_proceduret (const namespacet &_ns)

virtual	~decision_proceduret ()

void	set_to_true (const exprt &expr)

void	set_to_false (const exprt &expr)

resultt	operator() ()

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`. More...

Protected Member Functions
resultt	read_result (std::istream &in)

Protected Member Functions inherited from smt2_convt
void	write_header ()

void	write_footer (std::ostream &)

bool	use_array_theory (const exprt &)

void	flatten_array (const exprt &)
	produce a flat bit-vector for a given array of fixed size More...

void	unflatten_array (const exprt &)

void	convert_byte_update (const byte_update_exprt &expr)

void	convert_byte_extract (const byte_extract_exprt &expr)

void	convert_typecast (const typecast_exprt &expr)

void	convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

void	convert_struct (const struct_exprt &expr)

void	convert_union (const union_exprt &expr)

void	convert_constant (const constant_exprt &expr)

void	convert_relation (const exprt &expr)

void	convert_is_dynamic_object (const exprt &expr)

void	convert_plus (const plus_exprt &expr)

void	convert_minus (const minus_exprt &expr)

void	convert_div (const div_exprt &expr)

void	convert_mult (const mult_exprt &expr)

void	convert_rounding_mode_FPA (const exprt &expr)
	Converting a constant or symbolic rounding mode to SMT-LIB. More...

void	convert_floatbv_plus (const ieee_float_op_exprt &expr)

void	convert_floatbv_minus (const ieee_float_op_exprt &expr)

void	convert_floatbv_div (const ieee_float_op_exprt &expr)

void	convert_floatbv_mult (const ieee_float_op_exprt &expr)

void	convert_mod (const mod_exprt &expr)

void	convert_index (const index_exprt &expr)

void	convert_member (const member_exprt &expr)

void	convert_overflow (const exprt &expr)

void	convert_with (const with_exprt &expr)

void	convert_update (const exprt &expr)

std::string	convert_identifier (const irep_idt &identifier)

exprt	convert_operands (const exprt &)

void	find_symbols (const exprt &expr)

void	find_symbols (const typet &type)

void	find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)

exprt	letify (exprt &expr)

exprt	letify_rec (exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i)

void	collect_bindings (exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)

exprt	substitute_let (exprt &expr, const seen_expressionst &map)

constant_exprt	parse_literal (const irept &, const typet &type)

exprt	parse_struct (const irept &s, const struct_typet &type)

exprt	parse_union (const irept &s, const union_typet &type)

exprt	parse_array (const irept &s, const array_typet &type)

exprt	parse_rec (const irept &s, const typet &type)

void	convert_floatbv (const exprt &expr)

std::string	type2id (const typet &) const

std::string	floatbv_suffix (const exprt &) const

const smt2_symbolt &	to_smt2_symbol (const exprt &expr)

void	flatten2bv (const exprt &)

void	unflatten (wheret, const typet &, unsigned nesting=0)

void	convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)

void	define_object_size (const irep_idt &id, const exprt &expr)

	smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)

virtual	~smt2_convt ()

virtual literalt	convert (const exprt &expr)

virtual void	set_frozen (literalt)

virtual void	set_to (const exprt &expr, bool value)

virtual exprt	get (const exprt &expr) const

virtual void	print_assignment (std::ostream &out) const

virtual tvt	l_get (literalt l) const

virtual void	set_assumptions (const bvt &bv)

void	convert_expr (const exprt &)

void	convert_type (const typet &)

void	convert_literal (const literalt)

Protected Member Functions inherited from prop_convt
	prop_convt (const namespacet &_ns)

virtual	~prop_convt ()

literalt	operator() (const exprt &expr)

virtual void	set_frozen (const bvt &)

virtual void	set_all_frozen ()

virtual bool	is_in_conflict (literalt l) const
	determine whether a variable is in the final conflict More...

virtual bool	has_is_in_conflict () const

virtual void	set_time_limit_seconds (uint32_t)

Protected Member Functions inherited from decision_proceduret
	decision_proceduret (const namespacet &_ns)

virtual	~decision_proceduret ()

void	set_to_true (const exprt &expr)

void	set_to_false (const exprt &expr)

resultt	operator() ()

Protected Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`. More...

Additional Inherited Members
Public Types inherited from smt2_convt
enum	solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 }

Public Types inherited from decision_proceduret
enum	resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }

Public Types inherited from messaget
enum	message_levelt { M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6, M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Static Public Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Public Attributes inherited from smt2_convt
bool	use_FPA_theory

bool	use_datatypes

bool	use_array_of_bool

bool	emit_set_logic

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

Protected Types inherited from smt2_convt
enum	wheret { wheret::BEGIN, wheret::END }

typedef irep_hash_mapt< exprt, let_count_idt >	seen_expressionst

typedef std::unordered_map< irep_idt, identifiert >	identifier_mapt

typedef std::map< typet, std::string >	datatype_mapt

typedef std::map< exprt, irep_idt >	defined_expressionst

typedef std::set< std::string >	smt2_identifierst

enum	solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 }

Protected Types inherited from decision_proceduret
enum	resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }

Protected Types inherited from messaget
enum	message_levelt { M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6, M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Static Protected Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Protected Attributes inherited from smt2_stringstreamt
std::stringstream	stringstream

Protected Attributes inherited from smt2_convt
std::ostream &	out

std::string	benchmark

std::string	notes

std::string	logic

solvert	solver

bvt	assumptions

boolbv_widtht	boolbv_width

std::size_t	let_id_count

std::set< irep_idt >	bvfp_set

pointer_logict	pointer_logic

identifier_mapt	identifier_map

datatype_mapt	datatype_map

defined_expressionst	defined_expressions

defined_expressionst	object_sizes

smt2_identifierst	smt2_identifiers

std::size_t	no_boolean_variables

std::vector< bool >	boolean_assignment

bool	use_FPA_theory

bool	use_datatypes

bool	use_array_of_bool

bool	emit_set_logic

Protected Attributes inherited from decision_proceduret
const namespacet &	ns

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Static Protected Attributes inherited from smt2_convt
static const std::size_t	LET_COUNT = 2

Static Protected Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

Detailed Description

Decision procedure interface for various SMT 2.x solvers.

Definition at line 25 of file smt2_dec.h.

Constructor & Destructor Documentation

◆ smt2_dect()

smt2_dect::smt2_dect	(	const namespacet &	_ns,
		const std::string &	_benchmark,
		const std::string &	_notes,
		const std::string &	_logic,
		solvert	_solver
	)

inline

Definition at line 28 of file smt2_dec.h.

Member Function Documentation

◆ dec_solve()

decision_proceduret::resultt smt2_dect::dec_solve ( )

virtual

Reimplemented from smt2_convt.

Definition at line 37 of file smt2_dec.cpp.

◆ decision_procedure_text()

std::string smt2_dect::decision_procedure_text ( ) const

virtual

Reimplemented from smt2_convt.

Definition at line 21 of file smt2_dec.cpp.

◆ has_set_assumptions()

virtual bool smt2_dect::has_set_assumptions ( ) const

inlinevirtual

Reimplemented from prop_convt.

Definition at line 42 of file smt2_dec.h.

◆ read_result()

decision_proceduret::resultt smt2_dect::read_result ( std::istream & in )

protected

Definition at line 131 of file smt2_dec.cpp.

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

solvers/smt2/smt2_dec.h
solvers/smt2/smt2_dec.cpp

Public Member Functions

Protected Member Functions

Additional Inherited Members