Gymbo

Public Member Functions | Public Attributes | List of all members
gymbosat::Expr Class Referenceabstract

Base class for representing logical expressions. More...

`#include <sat.h>`

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

## 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