The class formula checker takes a data specification in mCRL2 format and a list of expressions. More...

#include <formula_checker.h>

Public Member Functions
	Formula_Checker (mcrl2::data::data_specification a_data_spec, mcrl2::data::rewriter::strategy a_rewrite_strategy=mcrl2::data::jitty, int a_time_limit=0, bool a_path_eliminator=false, mcrl2::data::detail::smt_solver_type a_solver_type=mcrl2::data::detail::solver_type_cvc, bool a_apply_induction=false, bool a_counter_example=false, bool a_witness=false, char const *a_dot_file_name=nullptr)
	Constructor that initializes Formula_Checker::f_counter_example, Formula_Checker::f_witness,.

	~Formula_Checker ()=default
	Destructor without any specific functionality.

void	check_formulas (const data_expression_list &a_formulas)
	Checks the formulas in the list a_formulas. precondition: the parameter a_formulas is a list of expressions of sort Bool in internal mCRL2 format.

Private Member Functions
void	print_witness ()
	Displays a witness.

void	print_counter_example ()
	Displays a counter-example.

void	save_dot_file (int a_formula_number)
	Writes the BDD corresponding to the formula with number a_formula_number to a dot file.

Private Attributes
mcrl2::data::detail::BDD_Prover	f_bdd_prover
	BDD based prover.

BDD2Dot	f_bdd2dot
	Class that outputs BDDs in dot format.

bool	f_counter_example
	Flag indicating whether or not counter-examples are displayed.

bool	f_witness
	Flag indicating whether or not witnesses are displayed.

std::string	f_dot_file_name
	Prefix for the names of the files containing BDDs in dot format.

Detailed Description

The class formula checker takes a data specification in mCRL2 format and a list of expressions.

of sort Bool in the mCRL2 format and determines whether or not these expersions are tautologies or

contradictions. The class Formula_Checker is initialized with a specification of data equations in internal mCRL2 format using the

Constructor Formula_Checker::Formula_Checker. After initialization, the function Formula_Checker::check_formulas can be called any number of times to check whether the expressions of sort Bool in internal mCRL2 format in the list passed as parameter a_formulas are tautologies or contradictions.

The class Formula_Checker uses an instance of the class BDD_Prover to prove a number of propositional formulas. The prover is initialized with the parameters a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction and a_lps. The parameter a_rewrite_strategy specifies which rewrite strategy is used by the prover's rewriter. It can be set to either GS_REWR_JITTY or GS_REWR_JITTYC. The parameter a_time_limit specifies the maximum amount of time in seconds to be spent by the prover on proving a single formula. If a_time_limit is set to 0, no time limit will be enforced. The parameter a_path_eliminator specifies whether or not path elimination is applied. When path elimination is applied, the prover uses an SMT solver to remove inconsistent paths from BDDs. The parameter a_solver_type specifies which SMT solver is used for path elimination. Either the SMT solver ario (http://www.eecs.umich.edu/~ario/) or cvc-lite (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path. If the parameter a_path_eliminator is set to false, the parameter a_solver_type is ignored. The parameter a_time_limit specifies the data equations used by the prover's rewriter. The parameter a_apply_induction indicates whether or not induction on list will be applied.

The parameter a_dot_file_name specifies whether a file in dot format of the resulting BDD is saved each time the prover cannot determine whether an expression of sort Bool is a contradiction or a tautology. If the parameter is set to 0, no .dot files are saved. If a string is passed as parameter a_dot_file_name, this string will be used as the prefix of the filenames. An instance of the class BDD2Dot is used to save these files in dot format.

If the parameter a_counter_example is set to true, a so called counter example is printed to stderr each time an expression is encountered that is neither a contradiction nor a tautology. A counter example is a valuation for which the expression does not hold.

If the parameter a_witness is set to false, a so called witness is printed to stderr each time such an expression is encountered. A witness is a valuation for which the expression holds.

The function Formula_Checker::check_formulas prints information to stderr indicating whether the expressions in the list of formulas passed as parameter a_formulas are tautologies or contradictions. In some cases the BDD based prover may be unable to determine whether an expression is a tautology or a contradiction. If this is the case, the function Formula_Checker::check_formulas will print information to stderr indicating this fact.

Definition at line 59 of file formula_checker.h.

Constructor & Destructor Documentation

◆ Formula_Checker()

mcrl2::data::detail::Formula_Checker::Formula_Checker	(	mcrl2::data::data_specification	a_data_spec,
		mcrl2::data::rewriter::strategy	a_rewrite_strategy = `mcrl2::data::jitty`,
		int	a_time_limit = `0`,
		bool	a_path_eliminator = `false`,
		mcrl2::data::detail::smt_solver_type	a_solver_type = `mcrl2::data::detail::solver_type_cvc`,
		bool	a_apply_induction = `false`,
		bool	a_counter_example = `false`,
		bool	a_witness = `false`,
		char const *	a_dot_file_name = `nullptr`
	)

inline

Constructor that initializes Formula_Checker::f_counter_example, Formula_Checker::f_witness,.

Formula_Checker::f_bdd_prover and Formula_Checker::f_dot_file_name. precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal to 0, no time limit will be enforced

Definition at line 131 of file formula_checker.h.

◆ ~Formula_Checker()

mcrl2::data::detail::Formula_Checker::~Formula_Checker ( )

default

Destructor without any specific functionality.

Member Function Documentation

◆ check_formulas()

void mcrl2::data::detail::Formula_Checker::check_formulas ( const data_expression_list & a_formulas )

inline

Checks the formulas in the list a_formulas. precondition: the parameter a_formulas is a list of expressions of sort Bool in internal mCRL2 format.

Definition at line 158 of file formula_checker.h.

◆ print_counter_example()

void mcrl2::data::detail::Formula_Checker::print_counter_example ( )

inlineprivate

Displays a counter-example.

Definition at line 98 of file formula_checker.h.

◆ print_witness()

void mcrl2::data::detail::Formula_Checker::print_witness ( )

inlineprivate

Displays a witness.

Definition at line 78 of file formula_checker.h.

◆ save_dot_file()

void mcrl2::data::detail::Formula_Checker::save_dot_file ( int a_formula_number )

inlineprivate

Writes the BDD corresponding to the formula with number a_formula_number to a dot file.

Definition at line 118 of file formula_checker.h.

Member Data Documentation

◆ f_bdd2dot

BDD2Dot mcrl2::data::detail::Formula_Checker::f_bdd2dot

private

Class that outputs BDDs in dot format.

Definition at line 66 of file formula_checker.h.

◆ f_bdd_prover

mcrl2::data::detail::BDD_Prover mcrl2::data::detail::Formula_Checker::f_bdd_prover

private

BDD based prover.

Definition at line 63 of file formula_checker.h.

◆ f_counter_example

bool mcrl2::data::detail::Formula_Checker::f_counter_example

private

Flag indicating whether or not counter-examples are displayed.

Definition at line 69 of file formula_checker.h.

◆ f_dot_file_name

std::string mcrl2::data::detail::Formula_Checker::f_dot_file_name

private

Prefix for the names of the files containing BDDs in dot format.

Definition at line 75 of file formula_checker.h.

◆ f_witness

bool mcrl2::data::detail::Formula_Checker::f_witness

private

Flag indicating whether or not witnesses are displayed.

Definition at line 72 of file formula_checker.h.

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

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

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Formula_Checker()

◆ ~Formula_Checker()

Member Function Documentation

◆ check_formulas()

◆ print_counter_example()

◆ print_witness()

◆ save_dot_file()

Member Data Documentation

◆ f_bdd2dot

◆ f_bdd_prover

◆ f_counter_example

◆ f_dot_file_name

◆ f_witness