smt2_solvert Class Reference

Inheritance diagram for smt2_solvert:

Collaboration diagram for smt2_solvert:

Public Member Functions
	smt2_solvert (std::istream &_in, decision_proceduret &_solver)
Public Member Functions inherited from smt2_parsert
	smt2_parsert (std::istream &_in)
bool	parse () override
Public Member Functions inherited from smt2_tokenizert
	smt2_tokenizert (std::istream &_in)
	operator bool ()
Public Member Functions inherited from parsert
virtual void	clear ()
	parsert ()
virtual	~parsert ()
bool	read (char &ch)
bool	eof ()
void	parse_error (const std::string &message, const std::string &before)
void	inc_line_no ()
void	set_line_no (unsigned _line_no)
void	set_file (const irep_idt &file)
irep_idt	get_file () const
unsigned	get_line_no () const
unsigned	get_column () const
void	set_column (unsigned _column)
void	set_source_location (exprt &e)
void	set_function (const irep_idt &function)
void	advance_column (unsigned token_width)
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 mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...

Protected Member Functions
void	command (const std::string &) override
void	define_constants (const exprt &)
void	expand_function_applications (exprt &)
Protected Member Functions inherited from smt2_parsert
void	command_sequence ()
irep_idt	get_fresh_id (const irep_idt &)
irep_idt	rename_id (const irep_idt &) const
void	ignore_command ()
exprt	expression ()
exprt	function_application ()
typet	sort ()
exprt::operandst	operands ()
typet	function_signature_declaration ()
typet	function_signature_definition ()
exprt	multi_ary (irep_idt, const exprt::operandst &)
exprt	binary_predicate (irep_idt, const exprt::operandst &)
exprt	binary (irep_idt, const exprt::operandst &)
exprt	unary (irep_idt, const exprt::operandst &)
exprt	let_expression ()
exprt	quantifier_expression (irep_idt)
exprt	function_application (const irep_idt &identifier, const exprt::operandst &op)
exprt::operandst	cast_bv_to_signed (const exprt::operandst &)
	Apply typecast to signedbv to expressions in vector. More...
exprt	cast_bv_to_unsigned (const exprt &)
	Apply typecast to unsignedbv to given expression. More...
Protected Member Functions inherited from smt2_tokenizert
tokent	next_token ()
tokent	peek ()
mstreamt &	error ()

Protected Attributes
decision_proceduret &	solver
std::set< irep_idt >	constants_done
Protected Attributes inherited from smt2_parsert
bool	exit
renaming_mapt	renaming_map
renaming_counterst	renaming_counters
Protected Attributes inherited from smt2_tokenizert
std::string	buffer
bool	ok
bool	peeked
tokent	token
Protected Attributes inherited from parsert
source_locationt	source_location
unsigned	line_no
unsigned	previous_line_no
unsigned	column
Protected Attributes inherited from messaget
message_handlert *	message_handler
mstreamt	mstream

Additional Inherited Members
Public Types inherited from smt2_parsert
using	id_mapt = std::map< irep_idt, idt >
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 mstreamt &	eom (mstreamt &m)
static mstreamt &	endl (mstreamt &m)
Public Attributes inherited from smt2_parsert
id_mapt	id_map
Public Attributes inherited from parsert
std::istream *	in
std::string	this_line
std::string	last_line
std::vector< exprt >	stack
Protected Types inherited from smt2_parsert
using	renaming_mapt = std::map< irep_idt, irep_idt >
using	renaming_counterst = std::map< irep_idt, unsigned >
Protected Types inherited from smt2_tokenizert
using	tokent = enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL, NUMERAL, SYMBOL, OPEN, CLOSE }

Detailed Description

Definition at line 23 of file smt2_solver.cpp.

Constructor & Destructor Documentation

smt2_solvert()

smt2_solvert::smt2_solvert ( std::istream &  _in, decision_proceduret &  _solver  )

inline

Definition at line 26 of file smt2_solver.cpp.

Member Function Documentation

command()

void smt2_solvert::command ( const std::string &  c )

overrideprotectedvirtual

Reimplemented from smt2_parsert.

Definition at line 123 of file smt2_solver.cpp.

References smt2_parsert::command(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, define_constants(), smt2_tokenizert::error(), smt2_parsert::exit, expand_function_applications(), smt2_parsert::expression(), irept::is_not_nil(), irept::pretty(), decision_proceduret::set_to_true(), simplify_expr(), solver, and smt2_parsert::sort().

define_constants()

void smt2_solvert::define_constants ( const exprt &  expr )

protected

Definition at line 44 of file smt2_solver.cpp.

References constants_done, expand_function_applications(), symbol_exprt::get_identifier(), irept::id(), smt2_parsert::id_map, exprt::operands(), decision_proceduret::set_to_true(), solver, and to_symbol_expr().

Referenced by command().

expand_function_applications()

void smt2_solvert::expand_function_applications ( exprt &  expr )

protected

Definition at line 77 of file smt2_solver.cpp.

References DATA_INVARIANT, irept::id(), smt2_parsert::id_map, exprt::operands(), to_function_application_expr(), and to_mathematical_function_type().

Referenced by command(), and define_constants().

Member Data Documentation

constants_done

std::set<irep_idt> smt2_solvert::constants_done

protected

Definition at line 41 of file smt2_solver.cpp.

Referenced by define_constants().

solver

decision_proceduret& smt2_solvert::solver

protected

Definition at line 35 of file smt2_solver.cpp.

Referenced by command(), and define_constants().

---

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

• solvers/smt2/smt2_solver.cpp