#include <bdd_prover.h>

Inheritance diagram for mcrl2::data::detail::BDD_Prover:

Public Types
typedef rewriter::substitution_type	substitution_type

Public Member Functions
	BDD_Prover (const data_specification &data_spec, const used_data_equation_selector &equations_selector, mcrl2::data::rewriter::strategy a_rewrite_strategy=mcrl2::data::jitty, int a_time_limit=0, bool a_path_eliminator=false, smt_solver_type a_solver_type=solver_type_cvc, bool a_apply_induction=false)

	BDD_Prover (const rewriter &r, int time_limit=0, bool apply_induction=false)

	~BDD_Prover ()
	Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.

void	set_substitution (substitution_type &sigma)
	Set the substitution to be used to construct the BDD.

void	set_substitution_internal (substitution_type &sigma)
	Set the substitution in internal format to be used to construct the BDD.

Answer	is_tautology ()
	Indicates whether or not the formula Prover::f_formula is a tautology.

Answer	is_contradiction ()
	Indicates whether or not the formula Prover::f_formula is a contradiction.

data_expression	get_bdd ()
	Returns the BDD BDD_Prover::f_bdd.

data_expression	get_witness ()
	Returns all the guards on a path in the BDD that leads to a leaf labelled "true", if such a leaf exists.

data_expression	get_counter_example ()
	Returns all the guards on a path in the BDD that leads to a leaf labelled "false", if such a leaf exists.

std::shared_ptr< detail::Rewriter >	get_rewriter ()
	Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).

strategy	rewriter_strategy () const
	Returns the strategy of the rewriter used inside this proving rewriter.

void	set_formula (const data_expression &formula)
	Sets Prover::f_formula to formula. precondition: the argument passed as parameter formula is an expression of sort Bool.

BDD_Prover	clone ()

void	thread_initialise ()

Protected Attributes
data_expression	f_formula
	An expression of sort Bool.

const Info	f_info = Info(f_full, f_reverse)
	A class that provides information about expressions.

Manipulator	f_manipulator = Manipulator(f_info)
	A class that can be used to manipulate expressions.

bool	f_processed = false
	A flag that indicates whether or not the formala Prover::f_formula has been processed.

Answer	f_tautology
	A flag that indicates whether or not the formala Prover::f_formula is a tautology.

Answer	f_contradiction
	A flag that indicates whether or not the formala Prover::f_formula is a contradiction.

const int	f_time_limit
	An integer representing the maximal amount of seconds to be spent on processing a formula.

time_t	f_deadline
	A timestamp representing the moment when the maximal amount of seconds has been spent on processing the current formula.

substitution_type	bdd_sigma
	A binary decision diagram in the internal representation of the rewriter.

data_expression	f_bdd
	A binary decision diagram in the internal representation of mCRL2.

Protected Attributes inherited from mcrl2::data::basic_rewriter< data_expression >
std::shared_ptr< detail::Rewriter >	m_rewriter
	The wrapped Rewriter.

Private Member Functions
void	build_bdd ()
	Constructs the EQ-BDD corresponding to the formula Prover::f_formula.

std::string	indent (size_t n)

data_expression	bdd_down (const data_expression &formula, const size_t a_indent=0)
	Creates the EQ-BDD corresponding to the formula formula.

void	eliminate_paths ()
	Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.

void	update_answers ()
	Updates the values of Prover::f_tautology and Prover::f_contradiction.

bool	smallest (const data_expression &formula, data_expression &result)
	Returns the smallest guard in the formula formula.

bool	get_branch (const data_expression &a_bdd, const bool a_polarity, data_expression &result)
	Returns branch of the BDD a_bdd, depending on the polarity a_polarity.

Private Attributes
bool	f_apply_induction
	A flag indicating whether or not induction on lists is applied.

std::unordered_map< data_expression, data_expression >	f_formula_to_bdd
	A data specification.

std::unordered_map< data_expression, data_expression >	f_smallest
	A hashtable that maps formulas to the smallest guard occuring in those formulas.

std::shared_ptr< BDD_Simplifier >	f_bdd_simplifier
	Class that simplifies a BDD.

Induction	f_induction
	Class that creates all statements needed to prove a given property using induction.

Static Private Attributes
static constexpr bool	f_reverse = true
	Flag indicating whether or not the result of the comparison between the first two arguments.

static constexpr bool	f_full = true
	Flag indicating whether or not the arguments of equality functions are taken into account.

Additional Inherited Members
Protected Types inherited from mcrl2::data::rewriter
typedef basic_rewriter< data_expression >::substitution_type	substitution_type

Protected Types inherited from mcrl2::data::basic_rewriter< data_expression >
typedef data::mutable_indexed_substitution	substitution_type
	The type for the substitution that is used internally.

typedef data_expression	term_type
	The type for expressions manipulated by the rewriter.

typedef rewrite_strategy	strategy
	The rewrite strategies of the rewriter.

Protected Member Functions inherited from mcrl2::data::rewriter
	rewriter (const std::shared_ptr< detail::Rewriter > &r)
	Constructor for internal use.

	rewriter (const rewriter &r)=default
	Constructor.

	rewriter (const data_specification &d=rewriter::default_specification(), const strategy s=jitty)
	Constructor.

template<typename EquationSelector >
	rewriter (const data_specification &d, const EquationSelector &selector, const strategy s=jitty)
	Constructor.

rewriter	clone ()
	Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.

void	thread_initialise ()
	Initialises this rewriter with thread dependent information.

data_expression	operator() (const data_expression &d) const
	Rewrites a data expression.

template<typename SubstitutionFunction >
data_expression	operator() (const data_expression &d, const SubstitutionFunction &sigma) const
	Rewrites the data expression d, and on the fly applies a substitution function. to data variables.

template<typename SubstitutionFunction >
void	operator() (data_expression &result, const data_expression &d, const SubstitutionFunction &sigma) const
	Rewrites the data expression d, and on the fly applies a substitution function. to data variables.

data_expression	operator() (const data_expression &d, substitution_type &sigma) const
	Rewrites the data expression d, and on the fly applies a substitution function to data variables.

void	operator() (data_expression &result, const data_expression &d, substitution_type &sigma) const
	Rewrites the data expression d, and on the fly applies a substitution function to data variables.

	~rewriter ()

Protected Member Functions inherited from mcrl2::data::basic_rewriter< data_expression >
	basic_rewriter (const std::shared_ptr< detail::Rewriter > &r)
	Constructor.

	basic_rewriter (const basic_rewriter &other)=default
	Copy Constructor.

	basic_rewriter (const data_specification &d, const strategy s=jitty)
	Constructor.

	basic_rewriter (const data_specification &d, const used_data_equation_selector &equation_selector, const strategy s=jitty)
	Constructor.

basic_rewriter &	operator= (const basic_rewriter &other)=default
	Assignment operator.

Static Protected Member Functions inherited from mcrl2::data::rewriter
static substitution_type &	empty_substitution ()

static const data_specification &	default_specification ()
	Default specification used if no specification is specified at construction.

Detailed Description

Definition at line 85 of file bdd_prover.h.

Member Typedef Documentation

◆ substitution_type

typedef rewriter::substitution_type mcrl2::data::detail::BDD_Prover::substitution_type

Definition at line 88 of file bdd_prover.h.

Constructor & Destructor Documentation

◆ BDD_Prover() [1/2]

mcrl2::data::detail::BDD_Prover::BDD_Prover	(	const data_specification &	data_spec,
		const used_data_equation_selector &	equations_selector,
		mcrl2::data::rewriter::strategy	a_rewrite_strategy = `mcrl2::data::jitty`,
		int	a_time_limit = `0`,
		bool	a_path_eliminator = `false`,
		smt_solver_type	a_solver_type = `solver_type_cvc`,
		bool	a_apply_induction = `false`
	)

inline

Definition at line 465 of file bdd_prover.h.

◆ BDD_Prover() [2/2]

mcrl2::data::detail::BDD_Prover::BDD_Prover	(	const rewriter &	r,
		int	time_limit = `0`,
		bool	apply_induction = `false`
	)

inline

Definition at line 509 of file bdd_prover.h.

◆ ~BDD_Prover()

mcrl2::data::detail::BDD_Prover::~BDD_Prover ( )

inline

Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.

Definition at line 519 of file bdd_prover.h.

Member Function Documentation

◆ bdd_down()

data_expression mcrl2::data::detail::BDD_Prover::bdd_down	(	const data_expression &	formula,
		const size_t	a_indent = `0`
	)

inlineprivate

Creates the EQ-BDD corresponding to the formula formula.

Definition at line 185 of file bdd_prover.h.

◆ build_bdd()

void mcrl2::data::detail::BDD_Prover::build_bdd ( )

inlineprivate

Constructs the EQ-BDD corresponding to the formula Prover::f_formula.

Definition at line 148 of file bdd_prover.h.

◆ clone()

BDD_Prover mcrl2::data::detail::BDD_Prover::clone ( )

inline

Definition at line 635 of file bdd_prover.h.

◆ eliminate_paths()

void mcrl2::data::detail::BDD_Prover::eliminate_paths ( )

inlineprivate

Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.

Definition at line 249 of file bdd_prover.h.

◆ get_bdd()

data_expression mcrl2::data::detail::BDD_Prover::get_bdd ( )

inline

Returns the BDD BDD_Prover::f_bdd.

Definition at line 552 of file bdd_prover.h.

◆ get_branch()

bool mcrl2::data::detail::BDD_Prover::get_branch	(	const data_expression &	a_bdd,
		const bool	a_polarity,
		data_expression &	result
	)

inlineprivate

Returns branch of the BDD a_bdd, depending on the polarity a_polarity.

Definition at line 418 of file bdd_prover.h.

◆ get_counter_example()

data_expression mcrl2::data::detail::BDD_Prover::get_counter_example ( )

inline

Returns all the guards on a path in the BDD that leads to a leaf labelled "false", if such a leaf exists.

Definition at line 587 of file bdd_prover.h.

◆ get_rewriter()

std::shared_ptr< detail::Rewriter > mcrl2::data::detail::BDD_Prover::get_rewriter ( )

inline

Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).

Definition at line 615 of file bdd_prover.h.

◆ get_witness()

data_expression mcrl2::data::detail::BDD_Prover::get_witness ( )

inline

Returns all the guards on a path in the BDD that leads to a leaf labelled "true", if such a leaf exists.

Definition at line 559 of file bdd_prover.h.

◆ indent()

std::string mcrl2::data::detail::BDD_Prover::indent ( size_t n )

inlineprivate

Definition at line 179 of file bdd_prover.h.

◆ is_contradiction()

Answer mcrl2::data::detail::BDD_Prover::is_contradiction ( )

inline

Indicates whether or not the formula Prover::f_formula is a contradiction.

Definition at line 545 of file bdd_prover.h.

◆ is_tautology()

Answer mcrl2::data::detail::BDD_Prover::is_tautology ( )

inline

Indicates whether or not the formula Prover::f_formula is a tautology.

Definition at line 538 of file bdd_prover.h.

◆ rewriter_strategy()

strategy mcrl2::data::detail::BDD_Prover::rewriter_strategy ( ) const

inline

Returns the strategy of the rewriter used inside this proving rewriter.

Definition at line 621 of file bdd_prover.h.

◆ set_formula()

void mcrl2::data::detail::BDD_Prover::set_formula ( const data_expression & formula )

inline

Sets Prover::f_formula to formula. precondition: the argument passed as parameter formula is an expression of sort Bool.

Definition at line 628 of file bdd_prover.h.

◆ set_substitution()

void mcrl2::data::detail::BDD_Prover::set_substitution ( substitution_type & sigma )

inline

Set the substitution to be used to construct the BDD.

Definition at line 526 of file bdd_prover.h.

◆ set_substitution_internal()

void mcrl2::data::detail::BDD_Prover::set_substitution_internal ( substitution_type & sigma )

inline

Set the substitution in internal format to be used to construct the BDD.

Definition at line 532 of file bdd_prover.h.

◆ smallest()

bool mcrl2::data::detail::BDD_Prover::smallest	(	const data_expression &	formula,
		data_expression &	result
	)

inlineprivate

Returns the smallest guard in the formula formula.

Definition at line 336 of file bdd_prover.h.

◆ thread_initialise()

void mcrl2::data::detail::BDD_Prover::thread_initialise ( )

inline

Definition at line 640 of file bdd_prover.h.

◆ update_answers()

void mcrl2::data::detail::BDD_Prover::update_answers ( )

inlineprivate

Updates the values of Prover::f_tautology and Prover::f_contradiction.

Definition at line 264 of file bdd_prover.h.

Member Data Documentation

◆ bdd_sigma

substitution_type mcrl2::data::detail::BDD_Prover::bdd_sigma

protected

A binary decision diagram in the internal representation of the rewriter.

Definition at line 459 of file bdd_prover.h.

◆ f_apply_induction

bool mcrl2::data::detail::BDD_Prover::f_apply_induction

private

A flag indicating whether or not induction on lists is applied.

Definition at line 128 of file bdd_prover.h.

◆ f_bdd

data_expression mcrl2::data::detail::BDD_Prover::f_bdd

protected

A binary decision diagram in the internal representation of mCRL2.

Definition at line 462 of file bdd_prover.h.

◆ f_bdd_simplifier

std::shared_ptr<BDD_Simplifier> mcrl2::data::detail::BDD_Prover::f_bdd_simplifier

private

Class that simplifies a BDD.

Definition at line 142 of file bdd_prover.h.

◆ f_contradiction

Answer mcrl2::data::detail::BDD_Prover::f_contradiction

protected

A flag that indicates whether or not the formala Prover::f_formula is a contradiction.

Definition at line 118 of file bdd_prover.h.

◆ f_deadline

time_t mcrl2::data::detail::BDD_Prover::f_deadline

protected

A timestamp representing the moment when the maximal amount of seconds has been spent on processing the current formula.

Definition at line 124 of file bdd_prover.h.

◆ f_formula

data_expression mcrl2::data::detail::BDD_Prover::f_formula

protected

An expression of sort Bool.

Definition at line 103 of file bdd_prover.h.

◆ f_formula_to_bdd

std::unordered_map< data_expression, data_expression > mcrl2::data::detail::BDD_Prover::f_formula_to_bdd

private

A data specification.

A hashtable that maps formulas to BDDs.

If the BDD of a formula is unknown, it maps this formula to 0.

Definition at line 135 of file bdd_prover.h.

◆ f_full

constexpr bool mcrl2::data::detail::BDD_Prover::f_full = true

staticconstexprprivate

Flag indicating whether or not the arguments of equality functions are taken into account.

when determining the order of expressions.

Definition at line 99 of file bdd_prover.h.

◆ f_induction

Induction mcrl2::data::detail::BDD_Prover::f_induction

private

Class that creates all statements needed to prove a given property using induction.

Definition at line 145 of file bdd_prover.h.

◆ f_info

const Info mcrl2::data::detail::BDD_Prover::f_info = Info(f_full, f_reverse)

protected

A class that provides information about expressions.

Definition at line 106 of file bdd_prover.h.

◆ f_manipulator

Manipulator mcrl2::data::detail::BDD_Prover::f_manipulator = Manipulator(f_info)

protected

A class that can be used to manipulate expressions.

Definition at line 109 of file bdd_prover.h.

◆ f_processed

bool mcrl2::data::detail::BDD_Prover::f_processed = false

protected

A flag that indicates whether or not the formala Prover::f_formula has been processed.

Definition at line 112 of file bdd_prover.h.

◆ f_reverse

constexpr bool mcrl2::data::detail::BDD_Prover::f_reverse = true

staticconstexprprivate

Flag indicating whether or not the result of the comparison between the first two arguments.

weighs stronger than the result of the comparison between the second pair of arguments of an

equation, when determining the order of expressions.

Definition at line 95 of file bdd_prover.h.

◆ f_smallest

std::unordered_map< data_expression, data_expression > mcrl2::data::detail::BDD_Prover::f_smallest

private

A hashtable that maps formulas to the smallest guard occuring in those formulas.

If the smallest guard of a formula is unknown, it maps this formula to 0.

Definition at line 139 of file bdd_prover.h.

◆ f_tautology

Answer mcrl2::data::detail::BDD_Prover::f_tautology

protected

A flag that indicates whether or not the formala Prover::f_formula is a tautology.

Definition at line 115 of file bdd_prover.h.

◆ f_time_limit

const int mcrl2::data::detail::BDD_Prover::f_time_limit

protected

An integer representing the maximal amount of seconds to be spent on processing a formula.

Definition at line 121 of file bdd_prover.h.

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

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

Public Types

Public Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Static Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ substitution_type

Constructor & Destructor Documentation

◆ BDD_Prover() [1/2]

◆ BDD_Prover() [2/2]

◆ ~BDD_Prover()

Member Function Documentation

◆ bdd_down()

◆ build_bdd()

◆ clone()

◆ eliminate_paths()

◆ get_bdd()

◆ get_branch()

◆ get_counter_example()

◆ get_rewriter()

◆ get_witness()

◆ indent()

◆ is_contradiction()

◆ is_tautology()

◆ rewriter_strategy()

◆ set_formula()

◆ set_substitution()

◆ set_substitution_internal()

◆ smallest()

◆ thread_initialise()

◆ update_answers()

Member Data Documentation

◆ bdd_sigma

◆ f_apply_induction

◆ f_bdd

◆ f_bdd_simplifier

◆ f_contradiction

◆ f_deadline

◆ f_formula

◆ f_formula_to_bdd

◆ f_full

◆ f_induction

◆ f_info

◆ f_manipulator

◆ f_processed

◆ f_reverse

◆ f_smallest

◆ f_tautology

◆ f_time_limit