|
Gymbo
|
Class representing the logical OR operation. More...
#include <sat.h>


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 |
Class representing the logical OR operation.
Constructor for the Or class.
| left | Left child expression. |
| right | Right child expression. |
|
inlineoverridevirtual |
Get a vector of clauses present in the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Distribute operations in the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Evaluate the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Fix negations in the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Identify and return free variables in the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Get the left child expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Get the right child expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Make a guess for a variable's value and return the resulting expression.
| var | Variable name. |
| val | Guessed value for the variable. |
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Get the polarities of literals with respect to a specific variable.
| var | Variable name. |
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Get the literals present in the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Simplify the logical expression.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Convert the logical expression to a string representation.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Check if the logical expression can be simplified by removing constants.
Implements gymbosat::Expr.
|
inlineoverridevirtual |
Get a unit clause from the logical expression.
Implements gymbosat::Expr.
|
private |
|
private |