gymbosat::Var Class Reference

Class representing a variable in a logical expression. More...

#include <sat.h>

Inheritance diagram for gymbosat::Var:

Collaboration diagram for gymbosat::Var:

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

Private Attributes
std::string	name

Additional Inherited Members
Public Attributes inherited from gymbosat::Expr
OpCode	opcode
std::string	name

Detailed Description

Class representing a variable in a logical expression.

Constructor & Destructor Documentation

Var()

gymbosat::Var::Var ( std::string  name )

inline

Member Function Documentation

clauses()

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

inlineoverridevirtual

Get a vector of clauses present in the logical expression.

Returns

Vector of shared pointers to clause expressions.

Implements gymbosat::Expr.

distribute()

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

inlineoverridevirtual

Distribute operations in the logical expression.

Returns

Shared pointer to the logical expression with distributed operations.

Implements gymbosat::Expr.

evaluate()

bool gymbosat::Var::evaluate ( )

inlineoverridevirtual

Evaluate the logical expression.

Returns

Result of the logical evaluation.

Implements gymbosat::Expr.

fixNegations()

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

inlineoverridevirtual

Fix negations in the logical expression.

Returns

Shared pointer to the logical expression with fixed negations.

Implements gymbosat::Expr.

freeVar()

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

inlineoverridevirtual

Identify and return free variables in the logical expression.

Returns

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

Implements gymbosat::Expr.

getLeft()

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

inlineoverridevirtual

Get the left child expression.

Returns

Shared pointer to the left child expression.

Implements gymbosat::Expr.

getRight()

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

inlineoverridevirtual

Get the right child expression.

Returns

Shared pointer to the right child expression.

Implements gymbosat::Expr.

guessVar()

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

inlineoverridevirtual

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.

Implements gymbosat::Expr.

literalPolarity()

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

inlineoverridevirtual

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

Parameters

var	Variable name.

Returns

Unordered map of literals to their polarities.

Implements gymbosat::Expr.

literals()

std::unordered_set<std::string> gymbosat::Var::literals ( )

inlineoverridevirtual

Get the literals present in the logical expression.

Returns

Unordered set of literals.

Implements gymbosat::Expr.

simplify()

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

inlineoverridevirtual

Simplify the logical expression.

Returns

Shared pointer to the simplified logical expression.

Implements gymbosat::Expr.

to_string()

std::string gymbosat::Var::to_string ( )

inlineoverridevirtual

Convert the logical expression to a string representation.

Returns

String representation of the logical expression.

Implements gymbosat::Expr.

unConst()

bool gymbosat::Var::unConst ( )

inlineoverridevirtual

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

Returns

True if the expression can be simplified, false otherwise.

Implements gymbosat::Expr.

unitClause()

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

inlineoverridevirtual

Get a unit clause from the logical expression.

Returns

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

Implements gymbosat::Expr.

Member Data Documentation

name

std::string gymbosat::Var::name

private

---

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

• libgymbo/sat.h