gymbosat::Expr Class Reference

Base class for representing logical expressions. More...

#include <sat.h>

Inheritance diagram for gymbosat::Expr:

Collaboration diagram for gymbosat::Expr:

Public Member Functions
virtual	~Expr ()
	Destructor for the Expr class. More...
virtual std::string	to_string ()=0
	Convert the logical expression to a string representation. More...
virtual bool	evaluate ()=0
	Evaluate the logical expression. More...
virtual bool	unConst ()=0
	Check if the logical expression can be simplified by removing constants. More...
virtual std::pair< bool, std::string >	freeVar ()=0
	Identify and return free variables in the logical expression. More...
virtual std::shared_ptr< Expr >	guessVar (std::string var, bool val)=0
	Make a guess for a variable's value and return the resulting expression. More...
virtual std::shared_ptr< Expr >	simplify ()=0
	Simplify the logical expression. More...
virtual std::shared_ptr< Expr >	fixNegations ()=0
	Fix negations in the logical expression. More...
virtual std::shared_ptr< Expr >	distribute ()=0
	Distribute operations in the logical expression. More...
virtual std::shared_ptr< Expr >	getLeft ()=0
	Get the left child expression. More...
virtual std::shared_ptr< Expr >	getRight ()=0
	Get the right child expression. More...
virtual std::unordered_set< std::string >	literals ()=0
	Get the literals present in the logical expression. More...
virtual std::unordered_map< std::string, Polarity >	literalPolarity (std::string var)=0
	Get the polarities of literals with respect to a specific variable. More...
virtual std::pair< std::string, bool >	unitClause ()=0
	Get a unit clause from the logical expression. More...
virtual std::vector< std::shared_ptr< Expr > >	clauses ()=0
	Get a vector of clauses present in the logical expression. More...

Public Attributes
OpCode	opcode
std::string	name

Detailed Description

Base class for representing logical expressions.

Constructor & Destructor Documentation

~Expr()

virtual gymbosat::Expr::~Expr ( )

inlinevirtual

Destructor for the Expr class.

Member Function Documentation

clauses()

virtual std::vector<std::shared_ptr<Expr> > gymbosat::Expr::clauses ( )

pure virtual

Get a vector of clauses present in the logical expression.

Returns

Vector of shared pointers to clause expressions.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

distribute()

virtual std::shared_ptr<Expr> gymbosat::Expr::distribute ( )

pure virtual

Distribute operations in the logical expression.

Returns

Shared pointer to the logical expression with distributed operations.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

evaluate()

virtual bool gymbosat::Expr::evaluate ( )

pure virtual

Evaluate the logical expression.

Returns

Result of the logical evaluation.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

fixNegations()

virtual std::shared_ptr<Expr> gymbosat::Expr::fixNegations ( )

pure virtual

Fix negations in the logical expression.

Returns

Shared pointer to the logical expression with fixed negations.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

freeVar()

virtual std::pair<bool, std::string> gymbosat::Expr::freeVar ( )

pure virtual

Identify and return free variables in the logical expression.

Returns

Pair indicating if there are free variables and the first free variable found.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

getLeft()

virtual std::shared_ptr<Expr> gymbosat::Expr::getLeft ( )

pure virtual

Get the left child expression.

Returns

Shared pointer to the left child expression.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

getRight()

virtual std::shared_ptr<Expr> gymbosat::Expr::getRight ( )

pure virtual

Get the right child expression.

Returns

Shared pointer to the right child expression.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

guessVar()

virtual std::shared_ptr<Expr> gymbosat::Expr::guessVar ( std::string  var, bool  val  )

pure virtual

Make a guess for a variable's value and return the resulting expression.

Parameters

var	Variable name.
val	Guessed value for the variable.

Returns

Shared pointer to the resulting logical expression.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

literalPolarity()

virtual std::unordered_map<std::string, Polarity> gymbosat::Expr::literalPolarity ( std::string  var )

pure virtual

Get the polarities of literals with respect to a specific variable.

Parameters

var	Variable name.

Returns

Unordered map of literals to their polarities.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

literals()

virtual std::unordered_set<std::string> gymbosat::Expr::literals ( )

pure virtual

Get the literals present in the logical expression.

Returns

Unordered set of literals.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

simplify()

virtual std::shared_ptr<Expr> gymbosat::Expr::simplify ( )

pure virtual

Simplify the logical expression.

Returns

Shared pointer to the simplified logical expression.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

to_string()

virtual std::string gymbosat::Expr::to_string ( )

pure virtual

Convert the logical expression to a string representation.

Returns

String representation of the logical expression.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

unConst()

virtual bool gymbosat::Expr::unConst ( )

pure virtual

Check if the logical expression can be simplified by removing constants.

Returns

True if the expression can be simplified, false otherwise.

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

unitClause()

virtual std::pair<std::string, bool> gymbosat::Expr::unitClause ( )

pure virtual

Get a unit clause from the logical expression.

Returns

Pair representing a unit clause: (literal, value).

Implemented in gymbosat::Const, gymbosat::Not, gymbosat::Or, gymbosat::And, and gymbosat::Var.

Member Data Documentation

name

std::string gymbosat::Expr::name

Name associated with the expression.

opcode

OpCode gymbosat::Expr::opcode

Operation code for the expression.

---

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

• libgymbo/sat.h