#include <smt_lib_solver.h>

Inheritance diagram for mcrl2::data::detail::SMT_LIB_Solver:

Public Member Functions
	SMT_LIB_Solver ()=default

	~SMT_LIB_Solver () override=default

Public Member Functions inherited from mcrl2::data::detail::SMT_Solver
virtual	~SMT_Solver ()=default

virtual bool	is_satisfiable (const data_expression_list &a_formula)=0

Protected Member Functions
void	translate (data_expression_list a_formula)

Protected Attributes
std::string	f_benchmark

Private Member Functions
const data_expression &	left (const data_expression &x) const

const data_expression &	right (const data_expression &x) const

const data_expression &	arg (const data_expression &x) const

void	declare_sorts ()

void	declare_operators ()

void	declare_variables ()

void	declare_predicates ()

void	produce_notes_for_sorts ()

void	produce_notes_for_operators ()

void	produce_notes_for_predicates ()

void	translate_clause (const data_expression &a_clause, const bool a_expecting_predicate)

void	add_bool2pred_and_translate_clause (const data_expression &a_clause)

void	translate_not (const data_expression &a_clause)

void	translate_equality (const data_expression &a_clause)

void	translate_inequality (const data_expression &a_clause)

void	translate_greater_than (const data_expression &a_clause)

void	translate_greater_than_or_equal (const data_expression &a_clause)

void	translate_less_than (const data_expression &a_clause)

void	translate_less_than_or_equal (const data_expression &a_clause)

void	translate_plus (const data_expression &a_clause)

void	translate_unary_minus (const data_expression &a_clause)

void	translate_binary_minus (const data_expression &a_clause)

void	translate_multiplication (const data_expression &a_clause)

void	translate_max (const data_expression &a_clause)

void	translate_min (const data_expression &a_clause)

void	translate_abs (const data_expression &a_clause)

void	translate_succ (const data_expression &a_clause)

void	translate_pred (const data_expression &a_clause)

void	translate_add_c (const data_expression &a_clause)

void	translate_c_nat (const data_expression &a_clause)

void	translate_c_int (const data_expression &a_clause)

void	translate_unknown_operator (const data_expression &a_clause)

void	translate_variable (const variable &a_clause)

void	translate_nat_variable (const variable &a_clause)

void	translate_pos_variable (const variable &a_clause)

void	translate_int_constant (const data_expression &a_clause)

void	translate_nat_constant (const data_expression &a_clause)

void	translate_pos_constant (const data_expression &a_clause)

void	translate_true ()

void	translate_false ()

void	translate_function_symbol (const data_expression &a_clause)

void	add_nat_clauses ()

void	add_pos_clauses ()

Private Attributes
std::string	f_sorts_notes

std::string	f_operators_notes

std::string	f_predicates_notes

std::string	f_extrasorts

std::string	f_operators_extrafuns

std::string	f_variables_extrafuns

std::string	f_extrapreds

std::string	f_formula

std::map< sort_expression, std::size_t >	f_sorts

std::map< function_symbol, std::size_t >	f_operators

std::set< variable >	f_variables

std::set< variable >	f_nat_variables

std::set< variable >	f_pos_variables

bool	f_bool2pred = false

Detailed Description

The class SMT_LIB_Solver is a base class for SMT solvers that read the SMT-LIB format [Silvio Ranise and Cesare Tinelli. The SMT-LIB Standard: Version 1.1. Technical Report, Department of Computer Science, The University of Iowa, 2005. (Available at http://goedel.cs.uiowa.edu/smtlib)]. It inherits from the class SMT_Solver.

The method SMT_LIB_Solver::translate receives an expression of sort Bool in conjunctive normal form as parameter a_formula and translates it to a benchmark in SMT-LIB format. The result is saved as field std::string f_benchmark.

Definition at line 34 of file smt_lib_solver.h.

Constructor & Destructor Documentation

◆ SMT_LIB_Solver()

mcrl2::data::detail::SMT_LIB_Solver::SMT_LIB_Solver ( )

default

◆ ~SMT_LIB_Solver()

mcrl2::data::detail::SMT_LIB_Solver::~SMT_LIB_Solver ( )

overridedefault

Member Function Documentation

◆ add_bool2pred_and_translate_clause()

void mcrl2::data::detail::SMT_LIB_Solver::add_bool2pred_and_translate_clause ( const data_expression & a_clause )

inlineprivate

Definition at line 418 of file smt_lib_solver.h.

◆ add_nat_clauses()

void mcrl2::data::detail::SMT_LIB_Solver::add_nat_clauses ( )

inlineprivate

Definition at line 746 of file smt_lib_solver.h.

◆ add_pos_clauses()

void mcrl2::data::detail::SMT_LIB_Solver::add_pos_clauses ( )

inlineprivate

Definition at line 755 of file smt_lib_solver.h.

◆ arg()

const data_expression & mcrl2::data::detail::SMT_LIB_Solver::arg ( const data_expression & x ) const

inlineprivate

Definition at line 64 of file smt_lib_solver.h.

◆ declare_operators()

void mcrl2::data::detail::SMT_LIB_Solver::declare_operators ( )

inlineprivate

Definition at line 92 of file smt_lib_solver.h.

◆ declare_predicates()

void mcrl2::data::detail::SMT_LIB_Solver::declare_predicates ( )

inlineprivate

Definition at line 217 of file smt_lib_solver.h.

◆ declare_sorts()

void mcrl2::data::detail::SMT_LIB_Solver::declare_sorts ( )

inlineprivate

Definition at line 70 of file smt_lib_solver.h.

◆ declare_variables()

void mcrl2::data::detail::SMT_LIB_Solver::declare_variables ( )

inlineprivate

Definition at line 165 of file smt_lib_solver.h.

◆ left()

const data_expression & mcrl2::data::detail::SMT_LIB_Solver::left ( const data_expression & x ) const

inlineprivate

Definition at line 52 of file smt_lib_solver.h.

◆ produce_notes_for_operators()

void mcrl2::data::detail::SMT_LIB_Solver::produce_notes_for_operators ( )

inlineprivate

Definition at line 249 of file smt_lib_solver.h.

◆ produce_notes_for_predicates()

void mcrl2::data::detail::SMT_LIB_Solver::produce_notes_for_predicates ( )

inlineprivate

Definition at line 266 of file smt_lib_solver.h.

◆ produce_notes_for_sorts()

void mcrl2::data::detail::SMT_LIB_Solver::produce_notes_for_sorts ( )

inlineprivate

Definition at line 232 of file smt_lib_solver.h.

◆ right()

const data_expression & mcrl2::data::detail::SMT_LIB_Solver::right ( const data_expression & x ) const

inlineprivate

Definition at line 58 of file smt_lib_solver.h.

◆ translate()

void mcrl2::data::detail::SMT_LIB_Solver::translate ( data_expression_list a_formula )

inlineprotected

precondition: The argument passed as parameter a_formula is a list of expressions of sort Bool in internal mCRL2 format. The argument represents a formula in conjunctive normal form, where the elements of the list represent the clauses

Definition at line 770 of file smt_lib_solver.h.

◆ translate_abs()

void mcrl2::data::detail::SMT_LIB_Solver::translate_abs ( const data_expression & a_clause )

inlineprivate

Definition at line 571 of file smt_lib_solver.h.

◆ translate_add_c()

void mcrl2::data::detail::SMT_LIB_Solver::translate_add_c ( const data_expression & a_clause )

inlineprivate

Definition at line 599 of file smt_lib_solver.h.

◆ translate_binary_minus()

void mcrl2::data::detail::SMT_LIB_Solver::translate_binary_minus ( const data_expression & a_clause )

inlineprivate

Definition at line 519 of file smt_lib_solver.h.

◆ translate_c_int()

void mcrl2::data::detail::SMT_LIB_Solver::translate_c_int ( const data_expression & a_clause )

inlineprivate

Definition at line 626 of file smt_lib_solver.h.

◆ translate_c_nat()

void mcrl2::data::detail::SMT_LIB_Solver::translate_c_nat ( const data_expression & a_clause )

inlineprivate

Definition at line 620 of file smt_lib_solver.h.

◆ translate_clause()

void mcrl2::data::detail::SMT_LIB_Solver::translate_clause	(	const data_expression &	a_clause,
		const bool	a_expecting_predicate
	)

inlineprivate

Definition at line 277 of file smt_lib_solver.h.

◆ translate_equality()

void mcrl2::data::detail::SMT_LIB_Solver::translate_equality ( const data_expression & a_clause )

inlineprivate

Definition at line 434 of file smt_lib_solver.h.

◆ translate_false()

void mcrl2::data::detail::SMT_LIB_Solver::translate_false ( )

inlineprivate

Definition at line 721 of file smt_lib_solver.h.

◆ translate_function_symbol()

void mcrl2::data::detail::SMT_LIB_Solver::translate_function_symbol ( const data_expression & a_clause )

inlineprivate

Definition at line 726 of file smt_lib_solver.h.

◆ translate_greater_than()

void mcrl2::data::detail::SMT_LIB_Solver::translate_greater_than ( const data_expression & a_clause )

inlineprivate

Definition at line 456 of file smt_lib_solver.h.

◆ translate_greater_than_or_equal()

void mcrl2::data::detail::SMT_LIB_Solver::translate_greater_than_or_equal ( const data_expression & a_clause )

inlineprivate

Definition at line 467 of file smt_lib_solver.h.

◆ translate_inequality()

void mcrl2::data::detail::SMT_LIB_Solver::translate_inequality ( const data_expression & a_clause )

inlineprivate

Definition at line 445 of file smt_lib_solver.h.

◆ translate_int_constant()

void mcrl2::data::detail::SMT_LIB_Solver::translate_int_constant ( const data_expression & a_clause )

inlineprivate

Definition at line 690 of file smt_lib_solver.h.

◆ translate_less_than()

void mcrl2::data::detail::SMT_LIB_Solver::translate_less_than ( const data_expression & a_clause )

inlineprivate

Definition at line 478 of file smt_lib_solver.h.

◆ translate_less_than_or_equal()

void mcrl2::data::detail::SMT_LIB_Solver::translate_less_than_or_equal ( const data_expression & a_clause )

inlineprivate

Definition at line 489 of file smt_lib_solver.h.

◆ translate_max()

void mcrl2::data::detail::SMT_LIB_Solver::translate_max ( const data_expression & a_clause )

inlineprivate

Definition at line 541 of file smt_lib_solver.h.

◆ translate_min()

void mcrl2::data::detail::SMT_LIB_Solver::translate_min ( const data_expression & a_clause )

inlineprivate

Definition at line 556 of file smt_lib_solver.h.

◆ translate_multiplication()

void mcrl2::data::detail::SMT_LIB_Solver::translate_multiplication ( const data_expression & a_clause )

inlineprivate

Definition at line 530 of file smt_lib_solver.h.

◆ translate_nat_constant()

void mcrl2::data::detail::SMT_LIB_Solver::translate_nat_constant ( const data_expression & a_clause )

inlineprivate

Definition at line 704 of file smt_lib_solver.h.

◆ translate_nat_variable()

void mcrl2::data::detail::SMT_LIB_Solver::translate_nat_variable ( const variable & a_clause )

inlineprivate

Definition at line 672 of file smt_lib_solver.h.

◆ translate_not()

void mcrl2::data::detail::SMT_LIB_Solver::translate_not ( const data_expression & a_clause )

inlineprivate

Definition at line 426 of file smt_lib_solver.h.

◆ translate_plus()

void mcrl2::data::detail::SMT_LIB_Solver::translate_plus ( const data_expression & a_clause )

inlineprivate

Definition at line 500 of file smt_lib_solver.h.

◆ translate_pos_constant()

void mcrl2::data::detail::SMT_LIB_Solver::translate_pos_constant ( const data_expression & a_clause )

inlineprivate

Definition at line 710 of file smt_lib_solver.h.

◆ translate_pos_variable()

void mcrl2::data::detail::SMT_LIB_Solver::translate_pos_variable ( const variable & a_clause )

inlineprivate

Definition at line 681 of file smt_lib_solver.h.

◆ translate_pred()

void mcrl2::data::detail::SMT_LIB_Solver::translate_pred ( const data_expression & a_clause )

inlineprivate

Definition at line 591 of file smt_lib_solver.h.

◆ translate_succ()

void mcrl2::data::detail::SMT_LIB_Solver::translate_succ ( const data_expression & a_clause )

inlineprivate

Definition at line 583 of file smt_lib_solver.h.

◆ translate_true()

void mcrl2::data::detail::SMT_LIB_Solver::translate_true ( )

inlineprivate

Definition at line 716 of file smt_lib_solver.h.

◆ translate_unary_minus()

void mcrl2::data::detail::SMT_LIB_Solver::translate_unary_minus ( const data_expression & a_clause )

inlineprivate

Definition at line 511 of file smt_lib_solver.h.

◆ translate_unknown_operator()

void mcrl2::data::detail::SMT_LIB_Solver::translate_unknown_operator ( const data_expression & a_clause )

inlineprivate

Definition at line 633 of file smt_lib_solver.h.

◆ translate_variable()

void mcrl2::data::detail::SMT_LIB_Solver::translate_variable ( const variable & a_clause )

inlineprivate

Definition at line 664 of file smt_lib_solver.h.

Member Data Documentation

◆ f_benchmark

std::string mcrl2::data::detail::SMT_LIB_Solver::f_benchmark

protected

Definition at line 765 of file smt_lib_solver.h.

◆ f_bool2pred

bool mcrl2::data::detail::SMT_LIB_Solver::f_bool2pred = false

private

Definition at line 50 of file smt_lib_solver.h.

◆ f_extrapreds

std::string mcrl2::data::detail::SMT_LIB_Solver::f_extrapreds

private

Definition at line 43 of file smt_lib_solver.h.

◆ f_extrasorts

std::string mcrl2::data::detail::SMT_LIB_Solver::f_extrasorts

private

Definition at line 40 of file smt_lib_solver.h.

◆ f_formula

std::string mcrl2::data::detail::SMT_LIB_Solver::f_formula

private

Definition at line 44 of file smt_lib_solver.h.

◆ f_nat_variables

std::set< variable > mcrl2::data::detail::SMT_LIB_Solver::f_nat_variables

private

Definition at line 48 of file smt_lib_solver.h.

◆ f_operators

std::map< function_symbol, std::size_t > mcrl2::data::detail::SMT_LIB_Solver::f_operators

private

Definition at line 46 of file smt_lib_solver.h.

◆ f_operators_extrafuns

std::string mcrl2::data::detail::SMT_LIB_Solver::f_operators_extrafuns

private

Definition at line 41 of file smt_lib_solver.h.

◆ f_operators_notes

std::string mcrl2::data::detail::SMT_LIB_Solver::f_operators_notes

private

Definition at line 38 of file smt_lib_solver.h.

◆ f_pos_variables

std::set< variable > mcrl2::data::detail::SMT_LIB_Solver::f_pos_variables

private

Definition at line 49 of file smt_lib_solver.h.

◆ f_predicates_notes

std::string mcrl2::data::detail::SMT_LIB_Solver::f_predicates_notes

private

Definition at line 39 of file smt_lib_solver.h.

◆ f_sorts

std::map< sort_expression, std::size_t > mcrl2::data::detail::SMT_LIB_Solver::f_sorts

private

Definition at line 45 of file smt_lib_solver.h.

◆ f_sorts_notes

std::string mcrl2::data::detail::SMT_LIB_Solver::f_sorts_notes

private

Definition at line 37 of file smt_lib_solver.h.

◆ f_variables

std::set< variable > mcrl2::data::detail::SMT_LIB_Solver::f_variables

private

Definition at line 47 of file smt_lib_solver.h.

◆ f_variables_extrafuns

std::string mcrl2::data::detail::SMT_LIB_Solver::f_variables_extrafuns

private

Definition at line 42 of file smt_lib_solver.h.

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

data/include/mcrl2/data/detail/prover/smt_lib_solver.h

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ SMT_LIB_Solver()

◆ ~SMT_LIB_Solver()

Member Function Documentation

◆ add_bool2pred_and_translate_clause()

◆ add_nat_clauses()

◆ add_pos_clauses()

◆ arg()

◆ declare_operators()

◆ declare_predicates()

◆ declare_sorts()

◆ declare_variables()

◆ left()

◆ produce_notes_for_operators()

◆ produce_notes_for_predicates()

◆ produce_notes_for_sorts()

◆ right()

◆ translate()

◆ translate_abs()

◆ translate_add_c()

◆ translate_binary_minus()

◆ translate_c_int()

◆ translate_c_nat()

◆ translate_clause()

◆ translate_equality()

◆ translate_false()

◆ translate_function_symbol()

◆ translate_greater_than()

◆ translate_greater_than_or_equal()

◆ translate_inequality()

◆ translate_int_constant()

◆ translate_less_than()

◆ translate_less_than_or_equal()

◆ translate_max()

◆ translate_min()

◆ translate_multiplication()

◆ translate_nat_constant()

◆ translate_nat_variable()

◆ translate_not()

◆ translate_plus()

◆ translate_pos_constant()

◆ translate_pos_variable()

◆ translate_pred()

◆ translate_succ()

◆ translate_true()

◆ translate_unary_minus()

◆ translate_unknown_operator()

◆ translate_variable()

Member Data Documentation

◆ f_benchmark

◆ f_bool2pred

◆ f_extrapreds

◆ f_extrasorts

◆ f_formula

◆ f_nat_variables

◆ f_operators

◆ f_operators_extrafuns

◆ f_operators_notes

◆ f_pos_variables

◆ f_predicates_notes

◆ f_sorts

◆ f_sorts_notes

◆ f_variables

◆ f_variables_extrafuns