Gymbo

Classes | Enumerations | Functions
gymbosat Namespace Reference

## Classes
class | Expr
| Base class for representing logical expressions. More...
class | Var
| Class representing a variable in a logical expression. More...
class | And
| Class representing the logical AND operation. More...
class | Or
| Class representing the logical OR operation. More...
class | Not
| Class representing the logical NOT operation. More...
class | Const
| Class representing a boolean constant in a logical expression. More...

## Enumerations
enum | OpCode { VAR , AND , OR , NOT , CONST }
| Enum representing different logical operation codes. More...
enum | Polarity { Positive , Negative , Mixed }
| Enum representing different polarities in logical expressions. More...

## Functions
std::shared_ptr< Expr > | cnf (std::shared_ptr< Expr > expr)
| Convert a logical expression to conjunctive normal form (CNF). More...
std::shared_ptr< Expr > | literalElimination (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
| Eliminate literals in a logical expression based on assignments. More...
std::vector< std::pair< std::string, bool > > | allUnitClauses (std::shared_ptr< Expr > expr)
| Extract all unit clauses from a logical expression. More...
std::shared_ptr< Expr > | unitPropagation (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
| Perform unit propagation on a logical expression based on assignments. More...
bool | satisfiableDPLL (std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
| Check satisfiability of a logical expression using the DPLL algorithm. More...
std::shared_ptr< Expr > | sym2expr (gymbo::Sym *sym, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map)
| Convert a symbolic expression to a logical expression. More...
std::shared_ptr< Expr > | pathconstraints2expr (std::vector< gymbo::Sym > &constraints, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map)
| Convert a vector of symbolic path constraints to a logical expression. More...

## Enumeration Type Documentation

## ◆ OpCode

enum gymbosat::OpCode

Enum representing different logical operation codes.

Enumerator
VAR |
AND |
OR |
NOT |
CONST |

## ◆ Polarity

enum gymbosat::Polarity

Enum representing different polarities in logical expressions.

Enumerator
Positive |
Negative |
Mixed |

## Function Documentation

## ◆ allUnitClauses()

std::vector<std::pair<std::string, bool> > gymbosat::allUnitClauses | ( | std::shared_ptr< Expr > | expr | ) |
| inline

Extract all unit clauses from a logical expression.

Parameters

  expr | Shared pointer to the logical expression.

Returns
  Vector of pairs representing unit clauses: (literal, value).

## ◆ cnf()

std::shared_ptr<Expr> gymbosat::cnf | ( | std::shared_ptr< Expr > | expr | ) |
| inline

Convert a logical expression to conjunctive normal form (CNF).

Parameters

  expr | Shared pointer to the logical expression.

Returns
  Shared pointer to the expression in CNF.

## ◆ literalElimination()

std::shared_ptr<Expr> gymbosat::literalElimination | ( | std::shared_ptr< Expr > | expr,
|  | std::unordered_map< std::string, bool > & | assignments_map
| ) |  |
| inline

Eliminate literals in a logical expression based on assignments.

Parameters

  expr | Shared pointer to the logical expression.
  assignments_map | Reference to an unordered map of variable assignments.

Returns
  Shared pointer to the modified logical expression.

## ◆ pathconstraints2expr()

std::shared_ptr<Expr> gymbosat::pathconstraints2expr | ( | std::vector< gymbo::Sym > & | constraints,
|  | std::unordered_map< std::string, gymbo::Sym * > & | unique_sym_map
| ) |  |
| inline

Convert a vector of symbolic path constraints to a logical expression.

Parameters

  constraints | Vector of symbolic path constraints.
  unique_sym_map | Reference to an unordered map of unique symbolic expressions.

Returns
  Shared pointer to the logical expression representing the path constraints.

## ◆ satisfiableDPLL()

bool gymbosat::satisfiableDPLL | ( | std::shared_ptr< Expr > | expr,
|  | std::unordered_map< std::string, bool > & | assignments_map
| ) |  |
| inline

Check satisfiability of a logical expression using the DPLL algorithm.

Parameters

  expr | Shared pointer to the logical expression.
  assignments_map | Reference to an unordered map of variable assignments.

Returns
  True if the expression is satisfiable, false otherwise.

## ◆ sym2expr()

std::shared_ptr<Expr> gymbosat::sym2expr | ( | gymbo::Sym * | sym,
|  | std::unordered_map< std::string, gymbo::Sym * > & | unique_sym_map
| ) |  |
| inline

Convert a symbolic expression to a logical expression.

Parameters

  sym | Pointer to the symbolic expression.
  unique_sym_map | Reference to an unordered map of unique symbolic expressions.

Returns
  Shared pointer to the corresponding logical expression.

## ◆ unitPropagation()

std::shared_ptr<Expr> gymbosat::unitPropagation | ( | std::shared_ptr< Expr > | expr,
|  | std::unordered_map< std::string, bool > & | assignments_map
| ) |  |
| inline

Perform unit propagation on a logical expression based on assignments.

Parameters

  expr | Shared pointer to the logical expression.
  assignments_map | Reference to an unordered map of variable assignments.

Returns
  Shared pointer to the modified logical expression.