\hypertarget{classgymbosat_1_1And}{}\doxysection{gymbosat\+::And Class Reference}
\label{classgymbosat_1_1And}\index{gymbosat::And@{gymbosat::And}}


Class representing the logical AND operation.  




{\ttfamily \#include $<$sat.\+h$>$}



Inheritance diagram for gymbosat\+::And\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=193pt]{classgymbosat_1_1And__inherit__graph}
\end{center}
\end{figure}


Collaboration diagram for gymbosat\+::And\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=193pt]{classgymbosat_1_1And__coll__graph}
\end{center}
\end{figure}
\doxysubsection*{Public Member Functions}
\begin{DoxyCompactItemize}
\item 
\mbox{\hyperlink{classgymbosat_1_1And_abffddbe0886529402c55100f0ed9765c}{And}} (std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a28c449aee5c9a0427778049cc94d3ce3}{left}}, std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a751c47c6f6de6bd1b5808460daaa6980}{right}})
\begin{DoxyCompactList}\small\item\em Constructor for the \mbox{\hyperlink{classgymbosat_1_1And}{And}} class. \end{DoxyCompactList}\item 
std\+::string \mbox{\hyperlink{classgymbosat_1_1And_affbe88b38fe18ca450ca074b6cfd135e}{to\+\_\+string}} () override
\begin{DoxyCompactList}\small\item\em Convert the logical expression to a string representation. \end{DoxyCompactList}\item 
bool \mbox{\hyperlink{classgymbosat_1_1And_a0e393520eb9044e3e2ff5e8d75317c8a}{evaluate}} () override
\begin{DoxyCompactList}\small\item\em Evaluate the logical expression. \end{DoxyCompactList}\item 
std\+::pair$<$ bool, std\+::string $>$ \mbox{\hyperlink{classgymbosat_1_1And_a0ac6ad39f548de338e61b73351428919}{free\+Var}} () override
\begin{DoxyCompactList}\small\item\em Identify and return free variables in the logical expression. \end{DoxyCompactList}\item 
bool \mbox{\hyperlink{classgymbosat_1_1And_a6d4e1f0b5d1d9379e90ed5d80e0fcf3a}{un\+Const}} () override
\begin{DoxyCompactList}\small\item\em Check if the logical expression can be simplified by removing constants. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_afba83f1734fa1c7399dcf57de543321f}{fix\+Negations}} () override
\begin{DoxyCompactList}\small\item\em Fix negations in the logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_aa5e8fec05e8684b366c9157963ebd06f}{distribute}} () override
\begin{DoxyCompactList}\small\item\em Distribute operations in the logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a44d1c80f33935e02f99d417f5cd2440a}{get\+Left}} () override
\begin{DoxyCompactList}\small\item\em Get the left child expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a0c8442aaf1c872b959f1465e52b74ab5}{get\+Right}} () override
\begin{DoxyCompactList}\small\item\em Get the right child expression. \end{DoxyCompactList}\item 
std\+::unordered\+\_\+set$<$ std\+::string $>$ \mbox{\hyperlink{classgymbosat_1_1And_a537ddf4b5192e2747744e7ad2108b11e}{literals}} () override
\begin{DoxyCompactList}\small\item\em Get the literals present in the logical expression. \end{DoxyCompactList}\item 
std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{Polarity}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a761328ffc63044ff03ac0f937dce2641}{literal\+Polarity}} (std\+::string var) override
\begin{DoxyCompactList}\small\item\em Get the polarities of literals with respect to a specific variable. \end{DoxyCompactList}\item 
std\+::pair$<$ std\+::string, bool $>$ \mbox{\hyperlink{classgymbosat_1_1And_afffae51480f5b0ffe99d27bc0a60ec90}{unit\+Clause}} () override
\begin{DoxyCompactList}\small\item\em Get a unit clause from the logical expression. \end{DoxyCompactList}\item 
std\+::vector$<$ std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ $>$ \mbox{\hyperlink{classgymbosat_1_1And_a393effa3189dea8e54379d5bf6353084}{clauses}} () override
\begin{DoxyCompactList}\small\item\em Get a vector of clauses present in the logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_ac7dc6c2a220f0474cb1e6b11f4775d2a}{guess\+Var}} (std\+::string var, bool val) override
\begin{DoxyCompactList}\small\item\em Make a guess for a variable\textquotesingle{}s value and return the resulting expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a6455aa50fd64ad0d9071a3e97955069d}{simplify}} () override
\begin{DoxyCompactList}\small\item\em Simplify the logical expression. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Private Attributes}
\begin{DoxyCompactItemize}
\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a28c449aee5c9a0427778049cc94d3ce3}{left}}
\item 
std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1And_a751c47c6f6de6bd1b5808460daaa6980}{right}}
\end{DoxyCompactItemize}
\doxysubsection*{Additional Inherited Members}


\doxysubsection{Detailed Description}
Class representing the logical AND operation. 

\doxysubsection{Constructor \& Destructor Documentation}
\mbox{\Hypertarget{classgymbosat_1_1And_abffddbe0886529402c55100f0ed9765c}\label{classgymbosat_1_1And_abffddbe0886529402c55100f0ed9765c}} 
\index{gymbosat::And@{gymbosat::And}!And@{And}}
\index{And@{And}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{And()}{And()}}
{\footnotesize\ttfamily gymbosat\+::\+And\+::\+And (\begin{DoxyParamCaption}\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{left,  }\item[{std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$}]{right }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}



Constructor for the \mbox{\hyperlink{classgymbosat_1_1And}{And}} class. 


\begin{DoxyParams}{Parameters}
{\em left} & Left child expression. \\
\hline
{\em right} & Right child expression. \\
\hline
\end{DoxyParams}


\doxysubsection{Member Function Documentation}
\mbox{\Hypertarget{classgymbosat_1_1And_a393effa3189dea8e54379d5bf6353084}\label{classgymbosat_1_1And_a393effa3189dea8e54379d5bf6353084}} 
\index{gymbosat::And@{gymbosat::And}!clauses@{clauses}}
\index{clauses@{clauses}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{clauses()}{clauses()}}
{\footnotesize\ttfamily std\+::vector$<$std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ $>$ gymbosat\+::\+And\+::clauses (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get a vector of clauses present in the logical expression. 

\begin{DoxyReturn}{Returns}
Vector of shared pointers to clause expressions. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a2546fb8aae5d6557ff7b7063dcc94562}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_aa5e8fec05e8684b366c9157963ebd06f}\label{classgymbosat_1_1And_aa5e8fec05e8684b366c9157963ebd06f}} 
\index{gymbosat::And@{gymbosat::And}!distribute@{distribute}}
\index{distribute@{distribute}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{distribute()}{distribute()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::distribute (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Distribute operations in the logical expression. 

\begin{DoxyReturn}{Returns}
Shared pointer to the logical expression with distributed operations. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a5c20f014cd61f3849fa5426747314008}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a0e393520eb9044e3e2ff5e8d75317c8a}\label{classgymbosat_1_1And_a0e393520eb9044e3e2ff5e8d75317c8a}} 
\index{gymbosat::And@{gymbosat::And}!evaluate@{evaluate}}
\index{evaluate@{evaluate}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{evaluate()}{evaluate()}}
{\footnotesize\ttfamily bool gymbosat\+::\+And\+::evaluate (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Evaluate the logical expression. 

\begin{DoxyReturn}{Returns}
Result of the logical evaluation. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_ac1a7a99cbd57909be8d51e70524d156b}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_afba83f1734fa1c7399dcf57de543321f}\label{classgymbosat_1_1And_afba83f1734fa1c7399dcf57de543321f}} 
\index{gymbosat::And@{gymbosat::And}!fixNegations@{fixNegations}}
\index{fixNegations@{fixNegations}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{fixNegations()}{fixNegations()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::fix\+Negations (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Fix negations in the logical expression. 

\begin{DoxyReturn}{Returns}
Shared pointer to the logical expression with fixed negations. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a2375384f892329d64455a54c7e3ddb27}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a0ac6ad39f548de338e61b73351428919}\label{classgymbosat_1_1And_a0ac6ad39f548de338e61b73351428919}} 
\index{gymbosat::And@{gymbosat::And}!freeVar@{freeVar}}
\index{freeVar@{freeVar}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{freeVar()}{freeVar()}}
{\footnotesize\ttfamily std\+::pair$<$bool, std\+::string$>$ gymbosat\+::\+And\+::free\+Var (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Identify and return free variables in the logical expression. 

\begin{DoxyReturn}{Returns}
Pair indicating if there are free variables and the first free variable found. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a92753531910a25ff11c257e0044436fd}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a44d1c80f33935e02f99d417f5cd2440a}\label{classgymbosat_1_1And_a44d1c80f33935e02f99d417f5cd2440a}} 
\index{gymbosat::And@{gymbosat::And}!getLeft@{getLeft}}
\index{getLeft@{getLeft}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{getLeft()}{getLeft()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::get\+Left (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get the left child expression. 

\begin{DoxyReturn}{Returns}
Shared pointer to the left child expression. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a18774dd94770cedef7544c47a6ead2f9}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a0c8442aaf1c872b959f1465e52b74ab5}\label{classgymbosat_1_1And_a0c8442aaf1c872b959f1465e52b74ab5}} 
\index{gymbosat::And@{gymbosat::And}!getRight@{getRight}}
\index{getRight@{getRight}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{getRight()}{getRight()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::get\+Right (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get the right child expression. 

\begin{DoxyReturn}{Returns}
Shared pointer to the right child expression. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_ab4433deb961131f650ce86fb32136cad}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_ac7dc6c2a220f0474cb1e6b11f4775d2a}\label{classgymbosat_1_1And_ac7dc6c2a220f0474cb1e6b11f4775d2a}} 
\index{gymbosat::And@{gymbosat::And}!guessVar@{guessVar}}
\index{guessVar@{guessVar}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{guessVar()}{guessVar()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ gymbosat\+::\+And\+::guess\+Var (\begin{DoxyParamCaption}\item[{std\+::string}]{var,  }\item[{bool}]{val }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Make a guess for a variable\textquotesingle{}s value and return the resulting expression. 


\begin{DoxyParams}{Parameters}
{\em var} & Variable name. \\
\hline
{\em val} & Guessed value for the variable. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Shared pointer to the resulting logical expression. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a4d946a615d7d11020d5c9f0ee8fff135}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a761328ffc63044ff03ac0f937dce2641}\label{classgymbosat_1_1And_a761328ffc63044ff03ac0f937dce2641}} 
\index{gymbosat::And@{gymbosat::And}!literalPolarity@{literalPolarity}}
\index{literalPolarity@{literalPolarity}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{literalPolarity()}{literalPolarity()}}
{\footnotesize\ttfamily std\+::unordered\+\_\+map$<$std\+::string, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{Polarity}}$>$ gymbosat\+::\+And\+::literal\+Polarity (\begin{DoxyParamCaption}\item[{std\+::string}]{var }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get the polarities of literals with respect to a specific variable. 


\begin{DoxyParams}{Parameters}
{\em var} & Variable name. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
Unordered map of literals to their polarities. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_adea7d5e5285df79237a4b72a8b82c66d}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a537ddf4b5192e2747744e7ad2108b11e}\label{classgymbosat_1_1And_a537ddf4b5192e2747744e7ad2108b11e}} 
\index{gymbosat::And@{gymbosat::And}!literals@{literals}}
\index{literals@{literals}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{literals()}{literals()}}
{\footnotesize\ttfamily std\+::unordered\+\_\+set$<$std\+::string$>$ gymbosat\+::\+And\+::literals (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get the literals present in the logical expression. 

\begin{DoxyReturn}{Returns}
Unordered set of literals. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_aa7775d2a1555fd55529b1ed699ca84ea}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a6455aa50fd64ad0d9071a3e97955069d}\label{classgymbosat_1_1And_a6455aa50fd64ad0d9071a3e97955069d}} 
\index{gymbosat::And@{gymbosat::And}!simplify@{simplify}}
\index{simplify@{simplify}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{simplify()}{simplify()}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ gymbosat\+::\+And\+::simplify (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Simplify the logical expression. 

\begin{DoxyReturn}{Returns}
Shared pointer to the simplified logical expression. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a480cdd6cc0f3750b2b801e33b8950628}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_affbe88b38fe18ca450ca074b6cfd135e}\label{classgymbosat_1_1And_affbe88b38fe18ca450ca074b6cfd135e}} 
\index{gymbosat::And@{gymbosat::And}!to\_string@{to\_string}}
\index{to\_string@{to\_string}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{to\_string()}{to\_string()}}
{\footnotesize\ttfamily std\+::string gymbosat\+::\+And\+::to\+\_\+string (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Convert the logical expression to a string representation. 

\begin{DoxyReturn}{Returns}
String representation of the logical expression. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a85bcfafb66b9e5fde802840c213fbcec}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_a6d4e1f0b5d1d9379e90ed5d80e0fcf3a}\label{classgymbosat_1_1And_a6d4e1f0b5d1d9379e90ed5d80e0fcf3a}} 
\index{gymbosat::And@{gymbosat::And}!unConst@{unConst}}
\index{unConst@{unConst}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{unConst()}{unConst()}}
{\footnotesize\ttfamily bool gymbosat\+::\+And\+::un\+Const (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Check if the logical expression can be simplified by removing constants. 

\begin{DoxyReturn}{Returns}
True if the expression can be simplified, false otherwise. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a462170452606863e487f0807be83a96a}{gymbosat\+::\+Expr}}.

\mbox{\Hypertarget{classgymbosat_1_1And_afffae51480f5b0ffe99d27bc0a60ec90}\label{classgymbosat_1_1And_afffae51480f5b0ffe99d27bc0a60ec90}} 
\index{gymbosat::And@{gymbosat::And}!unitClause@{unitClause}}
\index{unitClause@{unitClause}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{unitClause()}{unitClause()}}
{\footnotesize\ttfamily std\+::pair$<$std\+::string, bool$>$ gymbosat\+::\+And\+::unit\+Clause (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [override]}, {\ttfamily [virtual]}}



Get a unit clause from the logical expression. 

\begin{DoxyReturn}{Returns}
Pair representing a unit clause\+: (literal, value). 
\end{DoxyReturn}


Implements \mbox{\hyperlink{classgymbosat_1_1Expr_a766c9fc6f0ac28161a19e7a7184f61b6}{gymbosat\+::\+Expr}}.



\doxysubsection{Member Data Documentation}
\mbox{\Hypertarget{classgymbosat_1_1And_a28c449aee5c9a0427778049cc94d3ce3}\label{classgymbosat_1_1And_a28c449aee5c9a0427778049cc94d3ce3}} 
\index{gymbosat::And@{gymbosat::And}!left@{left}}
\index{left@{left}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{left}{left}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::left\hspace{0.3cm}{\ttfamily [private]}}

\mbox{\Hypertarget{classgymbosat_1_1And_a751c47c6f6de6bd1b5808460daaa6980}\label{classgymbosat_1_1And_a751c47c6f6de6bd1b5808460daaa6980}} 
\index{gymbosat::And@{gymbosat::And}!right@{right}}
\index{right@{right}!gymbosat::And@{gymbosat::And}}
\doxysubsubsection{\texorpdfstring{right}{right}}
{\footnotesize\ttfamily std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+And\+::right\hspace{0.3cm}{\ttfamily [private]}}



The documentation for this class was generated from the following file\+:\begin{DoxyCompactItemize}
\item 
libgymbo/\mbox{\hyperlink{sat_8h}{sat.\+h}}\end{DoxyCompactItemize}
