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

#include <smt1_dec.h>

Inheritance diagram for smt1_dect:

Collaboration diagram for smt1_dect:

Classes
struct	valuet

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

virtual resultt	dec_solve ()

virtual std::string	decision_procedure_text () const

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

virtual	~smt1_convt ()

virtual literalt	convert (const exprt &expr)

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

virtual exprt	get (const exprt &expr) const

virtual tvt	l_get (literalt) const

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

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

virtual	~prop_convt ()

literalt	operator() (const exprt &expr)

virtual void	set_frozen (literalt a)

virtual void	set_frozen (const bvt &)

virtual void	set_assumptions (const bvt &_assumptions)

virtual bool	has_set_assumptions () const

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

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

void	set_to_true (const exprt &expr)

void	set_to_false (const exprt &expr)

resultt	operator() ()

virtual bool	in_core (const exprt &expr)

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 (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level)

mstreamt &	error ()

mstreamt &	warning ()

mstreamt &	result ()

mstreamt &	status ()

mstreamt &	statistics ()

mstreamt &	progress ()

mstreamt &	debug ()

Protected Member Functions
resultt	read_result_boolector (std::istream &in)
	read model produced by Boolector More...

resultt	read_result_cvc3 (std::istream &in)

resultt	read_result_opensmt (std::istream &in)

resultt	read_result_mathsat (std::istream &in)

resultt	read_result_yices (std::istream &in)

resultt	read_result_z3 (std::istream &in)

bool	string_to_expr_z3 (const typet &type, const std::string &value, exprt &e) const

std::string	mathsat_value (const std::string &src)

Protected Member Functions inherited from smt1_temp_filet
	smt1_temp_filet ()

	~smt1_temp_filet ()

Protected Member Functions inherited from smt1_convt
void	write_header ()

void	write_footer ()

void	convert_expr (const exprt &expr, bool bool_as_bv)

void	convert_type (const typet &type)

void	convert_byte_update (const exprt &expr, bool bool_as_bv)

void	convert_byte_extract (const byte_extract_exprt &expr, bool bool_as_bv)

void	convert_typecast (const typecast_exprt &expr, bool bool_as_bv)

void	convert_struct (const exprt &expr)

void	convert_union (const exprt &expr)

void	convert_constant (const constant_exprt &expr, bool bool_as_bv)

void	convert_relation (const exprt &expr, bool bool_as_bv)

void	convert_is_dynamic_object (const exprt &expr, bool bool_as_bv)

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_floatbv_plus (const exprt &expr)

void	convert_floatbv_minus (const exprt &expr)

void	convert_floatbv_div (const exprt &expr)

void	convert_floatbv_mult (const exprt &expr)

void	convert_mod (const mod_exprt &expr)

void	convert_index (const index_exprt &expr, bool bool_as_bv)

void	convert_member (const member_exprt &expr, bool bool_as_bv)

void	convert_overflow (const exprt &expr)

void	convert_with (const exprt &expr)

void	convert_update (const exprt &expr)

std::string	convert_identifier (const irep_idt &identifier)

void	convert_literal (const literalt l)

void	find_symbols (const exprt &expr)

void	find_symbols (const typet &type)

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

void	flatten_array (const exprt &op)

void	from_bv_begin (const typet &type, bool bool_as_bv)

void	from_bv_end (const typet &type, bool bool_as_bv)

void	from_bool_begin (const typet &type, bool bool_as_bv)

void	from_bool_end (const typet &type, bool bool_as_bv)

typet	array_index_type () const

void	array_index (const exprt &expr)

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

void	set_value (identifiert &identifier, const std::string &index, const std::string &value)

exprt	ce_value (const typet &type, const std::string &index, const std::string &v, bool in_struct) const

exprt	binary2struct (const struct_typet &type, const std::string &binary) const

exprt	binary2union (const union_typet &type, const std::string &binary) const

void	convert_nary (const exprt &expr, const irep_idt op_string, bool bool_as_bv)

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

virtual	~smt1_convt ()

virtual literalt	convert (const exprt &expr)

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

virtual exprt	get (const exprt &expr) const

virtual tvt	l_get (literalt) const

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

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

virtual	~prop_convt ()

literalt	operator() (const exprt &expr)

virtual void	set_frozen (literalt a)

virtual void	set_frozen (const bvt &)

virtual void	set_assumptions (const bvt &_assumptions)

virtual bool	has_set_assumptions () const

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

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

void	set_to_true (const exprt &expr)

void	set_to_false (const exprt &expr)

resultt	operator() ()

virtual bool	in_core (const exprt &expr)

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 (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level)

mstreamt &	error ()

mstreamt &	warning ()

mstreamt &	result ()

mstreamt &	status ()

mstreamt &	statistics ()

mstreamt &	progress ()

mstreamt &	debug ()

Protected Attributes
std::string	logic

bool	dec_solve_was_called

Protected Attributes inherited from smt1_temp_filet
std::ofstream	temp_out

std::string	temp_out_filename

std::string	temp_result_filename

Protected Attributes inherited from smt1_convt
std::string	benchmark

std::string	source

std::string	logic

solvert	solver

std::ostream &	out

boolbv_widtht	boolbv_width

std::set< irep_idt >	quantified_symbols

pointer_logict	pointer_logic

identifier_mapt	identifier_map

unsigned	array_index_bits

array_of_mapt	array_of_map

array_expr_mapt	array_expr_map

string2array_mapt	string2array_map

unsigned	no_boolean_variables

std::vector< bool >	boolean_assignment

Protected Attributes inherited from decision_proceduret
const namespacet &	ns

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Additional Inherited Members
Public Types inherited from smt1_convt
enum	solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::OPENSMT, 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 mstreamt &	eom (mstreamt &m)

static mstreamt &	endl (mstreamt &m)

Protected Types inherited from smt1_convt
typedef std::unordered_map< irep_idt, identifiert, irep_id_hash >	identifier_mapt

typedef std::map< exprt, irep_idt >	array_of_mapt

typedef std::map< exprt, irep_idt >	array_expr_mapt

typedef std::map< exprt, exprt >	string2array_mapt

enum	solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::OPENSMT, 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 mstreamt &	eom (mstreamt &m)

static mstreamt &	endl (mstreamt &m)

Detailed Description

Decision procedure interface for various SMT 1.x solvers.

Definition at line 30 of file smt1_dec.h.

Constructor & Destructor Documentation

◆ smt1_dect()

smt1_dect::smt1_dect	(	const namespacet &	_ns,
		const std::string &	_benchmark,
		const std::string &	_source,
		const std::string &	_logic,
		solvert	_solver
	)

inline

Definition at line 33 of file smt1_dec.h.

Member Function Documentation

◆ dec_solve()

decision_proceduret::resultt smt1_dect::dec_solve ( )

virtual

Reimplemented from smt1_convt.

Definition at line 63 of file smt1_dec.cpp.

References decision_proceduret::D_ERROR, dec_solve_was_called, messaget::eom(), messaget::error(), get_temporary_file(), read_result_boolector(), read_result_cvc3(), read_result_mathsat(), read_result_opensmt(), read_result_yices(), read_result_z3(), smt1_convt::solver, smt1_temp_filet::temp_out, smt1_temp_filet::temp_out_filename, smt1_temp_filet::temp_result_filename, and smt1_convt::write_footer().

◆ decision_procedure_text()

std::string smt1_dect::decision_procedure_text ( ) const

virtual

Reimplemented from smt1_convt.

Definition at line 29 of file smt1_dec.cpp.

References logic, and smt1_convt::solver.

◆ mathsat_value()

std::string smt1_dect::mathsat_value ( const std::string & src )

protected

Definition at line 290 of file smt1_dec.cpp.

References integer2binary(), pos(), safe_string2unsigned(), and string2integer().

Referenced by read_result_mathsat().

◆ read_result_boolector()

decision_proceduret::resultt smt1_dect::read_result_boolector ( std::istream & in )

protected

read model produced by Boolector

Definition at line 182 of file smt1_dec.cpp.

References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), messaget::error(), smt1_convt::identifier_map, smt1_dect::valuet::index_value_map, smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and smt1_dect::valuet::value.

Referenced by dec_solve().

◆ read_result_cvc3()

decision_proceduret::resultt smt1_dect::read_result_cvc3 ( std::istream & in )

protected

Definition at line 549 of file smt1_dec.cpp.

References smt1_convt::array_of_map, smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, smt1_convt::identifier_map, integer2binary(), integer2unsigned(), smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and string2integer().

Referenced by dec_solve().

◆ read_result_mathsat()

decision_proceduret::resultt smt1_dect::read_result_mathsat ( std::istream & in )

protected

Definition at line 307 of file smt1_dec.cpp.

References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, has_prefix(), smt1_convt::identifier_map, mathsat_value(), smt1_convt::no_boolean_variables, and smt1_convt::set_value().

Referenced by dec_solve().

◆ read_result_opensmt()

decision_proceduret::resultt smt1_dect::read_result_opensmt ( std::istream & in )

protected

Definition at line 265 of file smt1_dec.cpp.

References decision_proceduret::D_ERROR.

Referenced by dec_solve().

◆ read_result_yices()

decision_proceduret::resultt smt1_dect::read_result_yices ( std::istream & in )

protected

Definition at line 270 of file smt1_dec.cpp.

References decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, messaget::eom(), and messaget::error().

Referenced by dec_solve().

◆ read_result_z3()

decision_proceduret::resultt smt1_dect::read_result_z3 ( std::istream & in )

protected

Definition at line 377 of file smt1_dec.cpp.

References smt1_convt::boolean_assignment, smt1_convt::convert_identifier(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, smt1_convt::identifier_map, smt1_convt::no_boolean_variables, pos(), smt1_convt::set_value(), and string_to_expr_z3().

Referenced by dec_solve().

◆ string_to_expr_z3()

bool smt1_dect::string_to_expr_z3	(	const typet &	type,
		const std::string &	value,
		exprt &	e
	)		const

protected

Definition at line 433 of file smt1_dec.cpp.

References smt1_convt::array_index_type(), smt1_convt::array_of_map, smt1_convt::binary2struct(), smt1_convt::binary2union(), irept::id(), integer2binary(), integer2unsigned(), messaget::result(), constant_exprt::set_value(), string2integer(), typet::subtype(), to_struct_type(), to_union_type(), exprt::type(), and array_of_exprt::what().

Referenced by read_result_z3().

Member Data Documentation

◆ dec_solve_was_called

bool smt1_dect::dec_solve_was_called

protected

Definition at line 51 of file smt1_dec.h.

Referenced by dec_solve().

◆ logic

std::string smt1_dect::logic

protected

Definition at line 50 of file smt1_dec.h.

Referenced by decision_procedure_text().

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

solvers/smt1/smt1_dec.h
solvers/smt1/smt1_dec.cpp

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ smt1_dect()

Member Function Documentation

◆ dec_solve()

◆ decision_procedure_text()

◆ mathsat_value()

◆ read_result_boolector()

◆ read_result_cvc3()

◆ read_result_mathsat()

◆ read_result_opensmt()

◆ read_result_yices()

◆ read_result_z3()

◆ string_to_expr_z3()

Member Data Documentation

◆ dec_solve_was_called

◆ logic