\hypertarget{namespacegymbosat}{}\doxysection{gymbosat Namespace Reference}
\label{namespacegymbosat}\index{gymbosat@{gymbosat}}
\doxysubsection*{Classes}
\begin{DoxyCompactItemize}
\item 
class \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}
\begin{DoxyCompactList}\small\item\em Base class for representing logical expressions. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Var}{Var}}
\begin{DoxyCompactList}\small\item\em Class representing a variable in a logical expression. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1And}{And}}
\begin{DoxyCompactList}\small\item\em Class representing the logical AND operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Or}{Or}}
\begin{DoxyCompactList}\small\item\em Class representing the logical OR operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Not}{Not}}
\begin{DoxyCompactList}\small\item\em Class representing the logical NOT operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Const}{Const}}
\begin{DoxyCompactList}\small\item\em Class representing a boolean constant in a logical expression. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Enumerations}
\begin{DoxyCompactItemize}
\item 
enum \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}{Op\+Code}} \{ \newline
\mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a783aa8811c0d97c103452691317996a5}{VAR}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024ad2e14235bea46219c69d69b818deda51}{AND}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa707761460979d2894359f95295f922d}{OR}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa1aa2298eeb70aab521df090792f029e}{NOT}}
, \newline
\mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a8ff08a99249527948f9bbe6633e8f5b3}{CONST}}
 \}
\begin{DoxyCompactList}\small\item\em Enum representing different logical operation codes. \end{DoxyCompactList}\item 
enum \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{Polarity}} \{ \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2a339b3ba4e7e766359538835c6e30c883}{Positive}}
, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2af58cec105a8a618a79c888a3bef6a293}{Negative}}
, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2aa41fd20cf2100eceb7f63242f216503a}{Mixed}}
 \}
\begin{DoxyCompactList}\small\item\em Enum representing different polarities in logical expressions. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Functions}
\begin{DoxyCompactItemize}
\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{namespacegymbosat_aee3ea3ef6116322c249d4f557b51326d}{cnf}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ expr)
\begin{DoxyCompactList}\small\item\em Convert a logical expression to conjunctive normal form (CNF). \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{namespacegymbosat_a39eb2e94bf479cf70e9f4f20ae1b7ed4}{literal\+Elimination}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ expr, std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&assignments\+\_\+map)
\begin{DoxyCompactList}\small\item\em Eliminate literals in a logical expression based on assignments. \end{DoxyCompactList}\item 
std\+::vector$<$ std\+::pair$<$ std\+::string, bool $>$ $>$ \mbox{\hyperlink{namespacegymbosat_a53351856c441258f036913048a7777c4}{all\+Unit\+Clauses}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ expr)
\begin{DoxyCompactList}\small\item\em Extract all unit clauses from a logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{namespacegymbosat_a900a3e916b5f594baf9598112ff29db9}{unit\+Propagation}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ expr, std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&assignments\+\_\+map)
\begin{DoxyCompactList}\small\item\em Perform unit propagation on a logical expression based on assignments. \end{DoxyCompactList}\item 
bool \mbox{\hyperlink{namespacegymbosat_a1b9fe029a32c35b69482f3d410b5e649}{satisfiable\+DPLL}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ expr, std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&assignments\+\_\+map)
\begin{DoxyCompactList}\small\item\em Check satisfiability of a logical expression using the DPLL algorithm. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{namespacegymbosat_a03e10dde5ead3c1638a3959f61df655a}{sym2expr}} (\mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$sym, std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$ $>$ \&unique\+\_\+sym\+\_\+map)
\begin{DoxyCompactList}\small\item\em Convert a symbolic expression to a logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{namespacegymbosat_a6f0b9965254e8e0a97d6ce893d01cd06}{pathconstraints2expr}} (std\+::vector$<$ \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $>$ \&constraints, std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$ $>$ \&unique\+\_\+sym\+\_\+map)
\begin{DoxyCompactList}\small\item\em Convert a vector of symbolic path constraints to a logical expression. \end{DoxyCompactList}\end{DoxyCompactItemize}


\doxysubsection{Enumeration Type Documentation}
\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}} 
\index{gymbosat@{gymbosat}!OpCode@{OpCode}}
\index{OpCode@{OpCode}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{OpCode}{OpCode}}
{\footnotesize\ttfamily enum \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}{gymbosat\+::\+Op\+Code}}}



Enum representing different logical operation codes. 

\begin{DoxyEnumFields}{Enumerator}
\raisebox{\heightof{T}}[0pt][0pt]{\index{VAR@{VAR}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!VAR@{VAR}}}\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a783aa8811c0d97c103452691317996a5}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a783aa8811c0d97c103452691317996a5}} 
VAR&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{AND@{AND}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!AND@{AND}}}\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024ad2e14235bea46219c69d69b818deda51}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024ad2e14235bea46219c69d69b818deda51}} 
AND&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{OR@{OR}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!OR@{OR}}}\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa707761460979d2894359f95295f922d}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa707761460979d2894359f95295f922d}} 
OR&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{NOT@{NOT}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!NOT@{NOT}}}\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa1aa2298eeb70aab521df090792f029e}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa1aa2298eeb70aab521df090792f029e}} 
NOT&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{CONST@{CONST}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!CONST@{CONST}}}\mbox{\Hypertarget{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a8ff08a99249527948f9bbe6633e8f5b3}\label{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a8ff08a99249527948f9bbe6633e8f5b3}} 
CONST&\\
\hline

\end{DoxyEnumFields}
\mbox{\Hypertarget{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}\label{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}} 
\index{gymbosat@{gymbosat}!Polarity@{Polarity}}
\index{Polarity@{Polarity}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{Polarity}{Polarity}}
{\footnotesize\ttfamily enum \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{gymbosat\+::\+Polarity}}}



Enum representing different polarities in logical expressions. 

\begin{DoxyEnumFields}{Enumerator}
\raisebox{\heightof{T}}[0pt][0pt]{\index{Positive@{Positive}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!Positive@{Positive}}}\mbox{\Hypertarget{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2a339b3ba4e7e766359538835c6e30c883}\label{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2a339b3ba4e7e766359538835c6e30c883}} 
Positive&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{Negative@{Negative}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!Negative@{Negative}}}\mbox{\Hypertarget{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2af58cec105a8a618a79c888a3bef6a293}\label{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2af58cec105a8a618a79c888a3bef6a293}} 
Negative&\\
\hline

\raisebox{\heightof{T}}[0pt][0pt]{\index{Mixed@{Mixed}!gymbosat@{gymbosat}}\index{gymbosat@{gymbosat}!Mixed@{Mixed}}}\mbox{\Hypertarget{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2aa41fd20cf2100eceb7f63242f216503a}\label{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2aa41fd20cf2100eceb7f63242f216503a}} 
Mixed&\\
\hline

\end{DoxyEnumFields}


\doxysubsection{Function Documentation}
\mbox{\Hypertarget{namespacegymbosat_a53351856c441258f036913048a7777c4}\label{namespacegymbosat_a53351856c441258f036913048a7777c4}} 
\index{gymbosat@{gymbosat}!allUnitClauses@{allUnitClauses}}
\index{allUnitClauses@{allUnitClauses}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{allUnitClauses()}{allUnitClauses()}}
{\footnotesize\ttfamily std\+::vector$<$std\+::pair$<$std\+::string, bool$>$ $>$ gymbosat\+::all\+Unit\+Clauses (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{expr }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Extract all unit clauses from a logical expression. 


\begin{DoxyParams}{Parameters}
{\em expr} & Shared pointer to the logical expression. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Vector of pairs representing unit clauses\+: (literal, value). 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_aee3ea3ef6116322c249d4f557b51326d}\label{namespacegymbosat_aee3ea3ef6116322c249d4f557b51326d}} 
\index{gymbosat@{gymbosat}!cnf@{cnf}}
\index{cnf@{cnf}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{cnf()}{cnf()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::cnf (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{expr }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



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


\begin{DoxyParams}{Parameters}
{\em expr} & Shared pointer to the logical expression. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the expression in CNF. 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_a39eb2e94bf479cf70e9f4f20ae1b7ed4}\label{namespacegymbosat_a39eb2e94bf479cf70e9f4f20ae1b7ed4}} 
\index{gymbosat@{gymbosat}!literalElimination@{literalElimination}}
\index{literalElimination@{literalElimination}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{literalElimination()}{literalElimination()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::literal\+Elimination (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{expr,  }\item[{std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&}]{assignments\+\_\+map }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Eliminate literals in a logical expression based on assignments. 


\begin{DoxyParams}{Parameters}
{\em expr} & Shared pointer to the logical expression. \\
\hline
{\em assignments\+\_\+map} & Reference to an unordered map of variable assignments. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the modified logical expression. 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_a6f0b9965254e8e0a97d6ce893d01cd06}\label{namespacegymbosat_a6f0b9965254e8e0a97d6ce893d01cd06}} 
\index{gymbosat@{gymbosat}!pathconstraints2expr@{pathconstraints2expr}}
\index{pathconstraints2expr@{pathconstraints2expr}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{pathconstraints2expr()}{pathconstraints2expr()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::pathconstraints2expr (\begin{DoxyParamCaption}\item[{std\+::vector$<$ \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $>$ \&}]{constraints,  }\item[{std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$ $>$ \&}]{unique\+\_\+sym\+\_\+map }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



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


\begin{DoxyParams}{Parameters}
{\em constraints} & Vector of symbolic path constraints. \\
\hline
{\em unique\+\_\+sym\+\_\+map} & Reference to an unordered map of unique symbolic expressions. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the logical expression representing the path constraints. 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_a1b9fe029a32c35b69482f3d410b5e649}\label{namespacegymbosat_a1b9fe029a32c35b69482f3d410b5e649}} 
\index{gymbosat@{gymbosat}!satisfiableDPLL@{satisfiableDPLL}}
\index{satisfiableDPLL@{satisfiableDPLL}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{satisfiableDPLL()}{satisfiableDPLL()}}
{\footnotesize\ttfamily bool gymbosat\+::satisfiable\+DPLL (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{expr,  }\item[{std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&}]{assignments\+\_\+map }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Check satisfiability of a logical expression using the DPLL algorithm. 


\begin{DoxyParams}{Parameters}
{\em expr} & Shared pointer to the logical expression. \\
\hline
{\em assignments\+\_\+map} & Reference to an unordered map of variable assignments. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
True if the expression is satisfiable, false otherwise. 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_a03e10dde5ead3c1638a3959f61df655a}\label{namespacegymbosat_a03e10dde5ead3c1638a3959f61df655a}} 
\index{gymbosat@{gymbosat}!sym2expr@{sym2expr}}
\index{sym2expr@{sym2expr}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{sym2expr()}{sym2expr()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::sym2expr (\begin{DoxyParamCaption}\item[{\mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$}]{sym,  }\item[{std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{structgymbo_1_1Sym}{gymbo\+::\+Sym}} $\ast$ $>$ \&}]{unique\+\_\+sym\+\_\+map }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Convert a symbolic expression to a logical expression. 


\begin{DoxyParams}{Parameters}
{\em sym} & Pointer to the symbolic expression. \\
\hline
{\em unique\+\_\+sym\+\_\+map} & Reference to an unordered map of unique symbolic expressions. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the corresponding logical expression. 
\end{DoxyReturn}
\mbox{\Hypertarget{namespacegymbosat_a900a3e916b5f594baf9598112ff29db9}\label{namespacegymbosat_a900a3e916b5f594baf9598112ff29db9}} 
\index{gymbosat@{gymbosat}!unitPropagation@{unitPropagation}}
\index{unitPropagation@{unitPropagation}!gymbosat@{gymbosat}}
\doxysubsubsection{\texorpdfstring{unitPropagation()}{unitPropagation()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::unit\+Propagation (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{expr,  }\item[{std\+::unordered\+\_\+map$<$ std\+::string, bool $>$ \&}]{assignments\+\_\+map }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Perform unit propagation on a logical expression based on assignments. 


\begin{DoxyParams}{Parameters}
{\em expr} & Shared pointer to the logical expression. \\
\hline
{\em assignments\+\_\+map} & Reference to an unordered map of variable assignments. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the modified logical expression. 
\end{DoxyReturn}
