Gymbo

Public Member Functions | Private Attributes | List of all members
gymbosat::Or Class Reference

Class representing the logical OR operation. More...

`#include <sat.h>`

Inheritance diagram for gymbosat::Or:
[legend]
Collaboration diagram for gymbosat::Or:
[legend]

## Public Member Functions
| Or (std::shared_ptr< Expr > left, std::shared_ptr< Expr > right)
| Constructor for the Or 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...
bool | unConst () override
| Check if the logical expression can be simplified by removing constants. 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...
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 > | left
std::shared_ptr< Expr > | right

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

## Detailed Description

Class representing the logical OR operation.

## Constructor & Destructor Documentation

## ◆ Or()

gymbosat::Or::Or | ( | std::shared_ptr< Expr > | left,
|  | std::shared_ptr< Expr > | right
| ) |  |
| inline

Constructor for the Or class.

Parameters

  left | Left child expression.
  right | Right child expression.

## Member Function Documentation

## ◆ clauses()

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

Distribute operations in the logical expression.

Returns
  Shared pointer to the logical expression with distributed operations.

Implements gymbosat::Expr.

## ◆ evaluate()

bool gymbosat::Or::evaluate | ( |  | ) |
| inlineoverridevirtual

Evaluate the logical expression.

Returns
  Result of the logical evaluation.

Implements gymbosat::Expr.

## ◆ fixNegations()

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

Get the left child expression.

Returns
  Shared pointer to the left child expression.

Implements gymbosat::Expr.

## ◆ getRight()

std::shared_ptr<Expr> gymbosat::Or::getRight | ( |  | ) |
| inlineoverridevirtual

Get the right child expression.

Returns
  Shared pointer to the right child expression.

Implements gymbosat::Expr.

## ◆ guessVar()

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

Get the literals present in the logical expression.

Returns
  Unordered set of literals.

Implements gymbosat::Expr.

## ◆ simplify()

std::shared_ptr< Expr > gymbosat::Or::simplify | ( |  | ) |
| inlineoverridevirtual

Simplify the logical expression.

Returns
  Shared pointer to the simplified logical expression.

Implements gymbosat::Expr.

## ◆ to_string()

std::string gymbosat::Or::to_string | ( |  | ) |
| inlineoverridevirtual

Convert the logical expression to a string representation.

Returns
  String representation of the logical expression.

Implements gymbosat::Expr.

## ◆ unConst()

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

Get a unit clause from the logical expression.

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

Implements gymbosat::Expr.

## Member Data Documentation

## ◆ left

std::shared_ptr<Expr> gymbosat::Or::left
| private

## ◆ right

std::shared_ptr<Expr> gymbosat::Or::right
| private

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

- libgymbo/sat.h