Solver functions

Functions for solving expressions. More...

Functions
void	preprocess (std::shared_ptr< Expression > lhs, std::shared_ptr< Expression > rhs)
	Fill the map of equivalences to be applied to the expressions. Must be called before any other functions in this file.
std::vector< std::vector< std::string > >	proveEquivalence (std::shared_ptr< Expression > lhs, std::shared_ptr< Expression > rhs)
	Prove the expressions are equivalence using equivalence laws by solving the left hand side to the right hand side. Required that the expressions are actually equivalent for this to work.
void	generateNextSteps (std::shared_ptr< Expression > expr, std::shared_ptr< Expression > end, bool &found, std::queue< std::shared_ptr< Expression > > &queue, std::unordered_map< std::string, std::pair< std::string, std::string > > &visited)
	Generate the next expressions from the current expression. Creates a new expression for each law that can be applied to the current expression and adds it to the queue of steps to be processed if the expression has not already been visited.

Variables
std::unordered_map< EquivLaws::EquivLaw, std::string >	equivalences
	Map of equivalences to be applied to the expressions.
int	MAX_QUEUE_SIZE
	Maximum size of the queue of expressions to be processed.
int	MAX_EXPRESSION_LENGTH
	Maximum length of the expressions in the queue.

Detailed Description

Functions for solving expressions.

Function Documentation

generateNextSteps()

void generateNextSteps	(	std::shared_ptr< Expression >	expr,
		std::shared_ptr< Expression >	end,
		bool &	found,
		std::queue< std::shared_ptr< Expression > > &	queue,
		std::unordered_map< std::string, std::pair< std::string, std::string > > &	visited
	)

Generate the next expressions from the current expression. Creates a new expression for each law that can be applied to the current expression and adds it to the queue of steps to be processed if the expression has not already been visited.

Parameters

expr	pointer to the current expression
end	pointer to the end expression to reach. If the expression is found, the function will return early.
found	reference to a boolean that is set to true if the end expression is found
queue	reference to the queue of expressions to be for new expressions to be added to
visited	reference to the map of visited expressions. The key is the string representation of the new expression and the value is a pair of the string expression derived from and the law used to get to the expression

Definition at line 78 of file solver.cpp.

preprocess()

void preprocess	(	std::shared_ptr< Expression >	lhs,
		std::shared_ptr< Expression >	rhs
	)

Fill the map of equivalences to be applied to the expressions. Must be called before any other functions in this file.

Definition at line 13 of file solver.cpp.

proveEquivalence()

std::vector< std::vector< std::string > > proveEquivalence	(	std::shared_ptr< Expression >	lhs,
		std::shared_ptr< Expression >	rhs
	)

Prove the expressions are equivalence using equivalence laws by solving the left hand side to the right hand side. Required that the expressions are actually equivalent for this to work.

Parameters

lhs	pointer to left hand side expression
rhs	pointer to right hand side expression

Returns

vector of vector of strings of the steps to prove the equivalence: {{lhs, law},...}

See also

isEquivalent

Definition at line 34 of file solver.cpp.

Variable Documentation

equivalences

std::unordered_map<EquivLaws::EquivLaw, std::string> equivalences

extern

Map of equivalences to be applied to the expressions.

Definition at line 8 of file solver.cpp.

MAX_EXPRESSION_LENGTH

int MAX_EXPRESSION_LENGTH

extern

Maximum length of the expressions in the queue.

Definition at line 11 of file solver.cpp.

MAX_QUEUE_SIZE

int MAX_QUEUE_SIZE

extern

Maximum size of the queue of expressions to be processed.

Definition at line 10 of file solver.cpp.