Class representing a boolean constant in a logical expression.
More...
#include <sat.h>
|
| | Const (bool value) |
| | Constructor for the Const 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 > | simplify () override |
| | Simplify the logical expression. 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::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::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...
|
| |
| virtual | ~Expr () |
| | Destructor for the Expr class. More...
|
| |
Class representing a boolean constant in a logical expression.
◆ Const()
| gymbosat::Const::Const |
( |
bool |
value | ) |
|
|
inline |
Constructor for the Const class.
- Parameters
-
| value | Boolean value of the constant. |
◆ clauses()
| std::vector<std::shared_ptr<Expr> > gymbosat::Const::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::Const::distribute |
( |
| ) |
|
|
inlineoverridevirtual |
Distribute operations in the logical expression.
- Returns
- Shared pointer to the logical expression with distributed operations.
Implements gymbosat::Expr.
◆ evaluate()
| bool gymbosat::Const::evaluate |
( |
| ) |
|
|
inlineoverridevirtual |
Evaluate the logical expression.
- Returns
- Result of the logical evaluation.
Implements gymbosat::Expr.
◆ fixNegations()
| std::shared_ptr<Expr> gymbosat::Const::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::Const::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::Const::getLeft |
( |
| ) |
|
|
inlineoverridevirtual |
Get the left child expression.
- Returns
- Shared pointer to the left child expression.
Implements gymbosat::Expr.
◆ getRight()
| std::shared_ptr<Expr> gymbosat::Const::getRight |
( |
| ) |
|
|
inlineoverridevirtual |
Get the right child expression.
- Returns
- Shared pointer to the right child expression.
Implements gymbosat::Expr.
◆ guessVar()
| std::shared_ptr< Expr > gymbosat::Const::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::Const::literalPolarity |
( |
std::string |
var | ) |
|
|
inlineoverridevirtual |
Get the polarities of literals with respect to a specific variable.
- Parameters
-
- Returns
- Unordered map of literals to their polarities.
Implements gymbosat::Expr.
◆ literals()
| std::unordered_set<std::string> gymbosat::Const::literals |
( |
| ) |
|
|
inlineoverridevirtual |
Get the literals present in the logical expression.
- Returns
- Unordered set of literals.
Implements gymbosat::Expr.
◆ simplify()
| std::shared_ptr<Expr> gymbosat::Const::simplify |
( |
| ) |
|
|
inlineoverridevirtual |
Simplify the logical expression.
- Returns
- Shared pointer to the simplified logical expression.
Implements gymbosat::Expr.
◆ to_string()
| std::string gymbosat::Const::to_string |
( |
| ) |
|
|
inlineoverridevirtual |
Convert the logical expression to a string representation.
- Returns
- String representation of the logical expression.
Implements gymbosat::Expr.
◆ unConst()
| bool gymbosat::Const::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::Const::unitClause |
( |
| ) |
|
|
inlineoverridevirtual |
Get a unit clause from the logical expression.
- Returns
- Pair representing a unit clause: (literal, value).
Implements gymbosat::Expr.
◆ value
| bool gymbosat::Const::value |
|
private |
The documentation for this class was generated from the following file: