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.