Public Member Functions
	EquivalenceChecker (std::unique_ptr< storm::solver::SmtSolver > &&smtSolver, boost::optional< storm::expressions::Expression > const &constraint=boost::none)
	Creates an equivalence checker with the given solver and constraint.

void	addConstraints (std::vector< storm::expressions::Expression > const &constraints)

bool	areEquivalent (storm::expressions::Expression const &first, storm::expressions::Expression const &second)

bool	areEquivalentModuloNegation (storm::expressions::Expression const &first, storm::expressions::Expression const &second)

Detailed Description

Definition at line 13 of file EquivalenceChecker.h.

Constructor & Destructor Documentation

storm::expressions::EquivalenceChecker::EquivalenceChecker	(	std::unique_ptr< storm::solver::SmtSolver > &&	smtSolver,
		boost::optional< storm::expressions::Expression > const &	constraint = `boost::none`
	)

Creates an equivalence checker with the given solver and constraint.

Parameters

smtSolver	The solver to use.
constraint	An additional constraint. Must be satisfiable.

Definition at line 10 of file EquivalenceChecker.cpp.

void storm::expressions::EquivalenceChecker::addConstraints ( std::vector< storm::expressions::Expression > const & constraints )

Definition at line 17 of file EquivalenceChecker.cpp.

bool storm::expressions::EquivalenceChecker::areEquivalent	(	storm::expressions::Expression const &	first,
		storm::expressions::Expression const &	second
	)

Definition at line 23 of file EquivalenceChecker.cpp.

bool storm::expressions::EquivalenceChecker::areEquivalentModuloNegation	(	storm::expressions::Expression const &	first,
		storm::expressions::Expression const &	second
	)

Definition at line 31 of file EquivalenceChecker.cpp.

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