gymbosat::Not Class Reference

Class representing the logical NOT operation. More...

#include <sat.h>

Inheritance diagram for gymbosat::Not:

Collaboration diagram for gymbosat::Not:

Public Member Functions
	Not (std::shared_ptr< Expr > expr)
	Constructor for the Not class. More...
std::string	to_string () override
	Convert the logical expression to a string representation. More...
bool	evaluate () override
	Evaluate the logical expression. More...
std::pair< bool, std::string >	freeVar () override
	Identify and return free variables in the logical expression. More...
std::shared_ptr< Expr >	distribute () override
	Distribute operations in the logical expression. More...
bool	unConst () override
	Check if the logical expression can be simplified by removing constants. 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...
std::shared_ptr< Expr >	fixNegations () override
	Fix negations in the logical expression. 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 >	simplify () override
	Simplify the logical expression. More...
Public Member Functions inherited from gymbosat::Expr
virtual	~Expr ()
	Destructor for the Expr class. More...

Private Attributes
std::shared_ptr< Expr >	expr

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

Detailed Description

Class representing the logical NOT operation.

Constructor & Destructor Documentation

Not()

gymbosat::Not::Not ( std::shared_ptr< Expr >  expr )

inline

Constructor for the Not class.

Parameters

expr	Child expression to negate.

Member Function Documentation

clauses()

std::vector<std::shared_ptr<Expr> > gymbosat::Not::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::Not::distribute ( )

inlineoverridevirtual

Distribute operations in the logical expression.

Returns

Shared pointer to the logical expression with distributed operations.

Implements gymbosat::Expr.

evaluate()

bool gymbosat::Not::evaluate ( )

inlineoverridevirtual

Evaluate the logical expression.

Returns

Result of the logical evaluation.

Implements gymbosat::Expr.

fixNegations()

std::shared_ptr< Expr > gymbosat::Not::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::Not::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::Not::getLeft ( )

inlineoverridevirtual

Get the left child expression.

Returns

Shared pointer to the left child expression.

Implements gymbosat::Expr.

getRight()

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

inlineoverridevirtual

Get the right child expression.

Returns

Shared pointer to the right child expression.

Implements gymbosat::Expr.

guessVar()

std::shared_ptr< Expr > gymbosat::Not::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::Not::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::Not::literals ( )

inlineoverridevirtual

Get the literals present in the logical expression.

Returns

Unordered set of literals.

Implements gymbosat::Expr.

simplify()

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

inlineoverridevirtual

Simplify the logical expression.

Returns

Shared pointer to the simplified logical expression.

Implements gymbosat::Expr.

to_string()

std::string gymbosat::Not::to_string ( )

inlineoverridevirtual

Convert the logical expression to a string representation.

Returns

String representation of the logical expression.

Implements gymbosat::Expr.

unConst()

bool gymbosat::Not::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::Not::unitClause ( )

inlineoverridevirtual

Get a unit clause from the logical expression.

Returns

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

Implements gymbosat::Expr.

Member Data Documentation

expr

std::shared_ptr<Expr> gymbosat::Not::expr

private

---

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

• libgymbo/sat.h