\hypertarget{classgymbosat_1_1Expr}{}\doxysection{gymbosat\+::Expr Class Reference}
\label{classgymbosat_1_1Expr}\index{gymbosat::Expr@{gymbosat::Expr}}


Base class for representing logical expressions.  




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



Inheritance diagram for gymbosat\+::Expr\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=350pt]{classgymbosat_1_1Expr__inherit__graph}
\end{center}
\end{figure}


Collaboration diagram for gymbosat\+::Expr\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=193pt]{classgymbosat_1_1Expr__coll__graph}
\end{center}
\end{figure}
\doxysubsection*{Public Member Functions}
\begin{DoxyCompactItemize}
\item 
virtual \mbox{\hyperlink{classgymbosat_1_1Expr_af468583262a2936a1df0329a6331abb7}{$\sim$\+Expr}} ()
\begin{DoxyCompactList}\small\item\em Destructor for the \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} class. \end{DoxyCompactList}\item 
virtual std\+::string \mbox{\hyperlink{classgymbosat_1_1Expr_a85bcfafb66b9e5fde802840c213fbcec}{to\+\_\+string}} ()=0
\begin{DoxyCompactList}\small\item\em Convert the logical expression to a string representation. \end{DoxyCompactList}\item 
virtual bool \mbox{\hyperlink{classgymbosat_1_1Expr_ac1a7a99cbd57909be8d51e70524d156b}{evaluate}} ()=0
\begin{DoxyCompactList}\small\item\em Evaluate the logical expression. \end{DoxyCompactList}\item 
virtual bool \mbox{\hyperlink{classgymbosat_1_1Expr_a462170452606863e487f0807be83a96a}{un\+Const}} ()=0
\begin{DoxyCompactList}\small\item\em Check if the logical expression can be simplified by removing constants. \end{DoxyCompactList}\item 
virtual std\+::pair$<$ bool, std\+::string $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a92753531910a25ff11c257e0044436fd}{free\+Var}} ()=0
\begin{DoxyCompactList}\small\item\em Identify and return free variables in the logical expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a4d946a615d7d11020d5c9f0ee8fff135}{guess\+Var}} (std\+::string var, bool val)=0
\begin{DoxyCompactList}\small\item\em Make a guess for a variable\textquotesingle{}s value and return the resulting expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a480cdd6cc0f3750b2b801e33b8950628}{simplify}} ()=0
\begin{DoxyCompactList}\small\item\em Simplify the logical expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a2375384f892329d64455a54c7e3ddb27}{fix\+Negations}} ()=0
\begin{DoxyCompactList}\small\item\em Fix negations in the logical expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a5c20f014cd61f3849fa5426747314008}{distribute}} ()=0
\begin{DoxyCompactList}\small\item\em Distribute operations in the logical expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a18774dd94770cedef7544c47a6ead2f9}{get\+Left}} ()=0
\begin{DoxyCompactList}\small\item\em Get the left child expression. \end{DoxyCompactList}\item 
virtual std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_ab4433deb961131f650ce86fb32136cad}{get\+Right}} ()=0
\begin{DoxyCompactList}\small\item\em Get the right child expression. \end{DoxyCompactList}\item 
virtual std\+::unordered\+\_\+set$<$ std\+::string $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_aa7775d2a1555fd55529b1ed699ca84ea}{literals}} ()=0
\begin{DoxyCompactList}\small\item\em Get the literals present in the logical expression. \end{DoxyCompactList}\item 
virtual std\+::unordered\+\_\+map$<$ std\+::string, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{Polarity}} $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_adea7d5e5285df79237a4b72a8b82c66d}{literal\+Polarity}} (std\+::string var)=0
\begin{DoxyCompactList}\small\item\em Get the polarities of literals with respect to a specific variable. \end{DoxyCompactList}\item 
virtual std\+::pair$<$ std\+::string, bool $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a766c9fc6f0ac28161a19e7a7184f61b6}{unit\+Clause}} ()=0
\begin{DoxyCompactList}\small\item\em Get a unit clause from the logical expression. \end{DoxyCompactList}\item 
virtual std\+::vector$<$ std\+::shared\+\_\+ptr$<$ \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} $>$ $>$ \mbox{\hyperlink{classgymbosat_1_1Expr_a2546fb8aae5d6557ff7b7063dcc94562}{clauses}} ()=0
\begin{DoxyCompactList}\small\item\em Get a vector of clauses present in the logical expression. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Public Attributes}
\begin{DoxyCompactItemize}
\item 
\mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}{Op\+Code}} \mbox{\hyperlink{classgymbosat_1_1Expr_aa84655ea020547722c7433af5c009d27}{opcode}}
\item 
std\+::string \mbox{\hyperlink{classgymbosat_1_1Expr_ad4a359e63fbd7d3fe3cb598300a1c61e}{name}}
\end{DoxyCompactItemize}


\doxysubsection{Detailed Description}
Base class for representing logical expressions. 

\doxysubsection{Constructor \& Destructor Documentation}
\mbox{\Hypertarget{classgymbosat_1_1Expr_af468583262a2936a1df0329a6331abb7}\label{classgymbosat_1_1Expr_af468583262a2936a1df0329a6331abb7}} 
\index{gymbosat::Expr@{gymbosat::Expr}!````~Expr@{$\sim$Expr}}
\index{````~Expr@{$\sim$Expr}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{$\sim$Expr()}{~Expr()}}
{\footnotesize\ttfamily virtual gymbosat\+::\+Expr\+::$\sim$\+Expr (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [virtual]}}



Destructor for the \mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}} class. 



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



Get a vector of clauses present in the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a5b81da3a3fac35e316a2ab81ee899fb0}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_ae44c912be809762fbeeeba4326bd0f2f}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a57c5ad72cfd5375e997287ca5bea83f5}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a393effa3189dea8e54379d5bf6353084}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a02163d40505204998ef8f84dd256c2a5}{gymbosat\+::\+Var}}.

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



Distribute operations in the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_abb5336fa2d34c9b96493302fc8225afe}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a4e0167e2446c6877737d08a70c2935a6}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a02a435b65b082c0afeb430b27acb20cd}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_aa5e8fec05e8684b366c9157963ebd06f}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a9aa0f8574edf2af2a2fb9bff7b235eb0}{gymbosat\+::\+Var}}.

\mbox{\Hypertarget{classgymbosat_1_1Expr_ac1a7a99cbd57909be8d51e70524d156b}\label{classgymbosat_1_1Expr_ac1a7a99cbd57909be8d51e70524d156b}} 
\index{gymbosat::Expr@{gymbosat::Expr}!evaluate@{evaluate}}
\index{evaluate@{evaluate}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{evaluate()}{evaluate()}}
{\footnotesize\ttfamily virtual bool gymbosat\+::\+Expr\+::evaluate (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [pure virtual]}}



Evaluate the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_ad70b99655f5a1126b860c57e17b8baf3}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_af385cdf6a30697616f06076a9296f76b}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a9d75efd2db1509d9f5a3a984645ab25f}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a0e393520eb9044e3e2ff5e8d75317c8a}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_afc1c37653dcc96843e60eb4f858acdcf}{gymbosat\+::\+Var}}.

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



Fix negations in the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a3e70a24e7e46b4bbea0650e6b4ed6a2e}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_af1617752e83d03bcfab93d5d0d31aa37}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_ab27b62b002cc6b5f0082ac0e0924e1c4}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_afba83f1734fa1c7399dcf57de543321f}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_add2327d5589081e788e3d9e6d9ad0bc4}{gymbosat\+::\+Var}}.

\mbox{\Hypertarget{classgymbosat_1_1Expr_a92753531910a25ff11c257e0044436fd}\label{classgymbosat_1_1Expr_a92753531910a25ff11c257e0044436fd}} 
\index{gymbosat::Expr@{gymbosat::Expr}!freeVar@{freeVar}}
\index{freeVar@{freeVar}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{freeVar()}{freeVar()}}
{\footnotesize\ttfamily virtual std\+::pair$<$bool, std\+::string$>$ gymbosat\+::\+Expr\+::free\+Var (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [pure 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}


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a636afe7d321b1a27efca6ab550445fee}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a1a3cf41e3c56d6d9e34596ee197113f4}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a5b8bca08d6fd49a998e38b78f149ca1d}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a0ac6ad39f548de338e61b73351428919}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a9e013c99cdc05adb8fd2d046290a7688}{gymbosat\+::\+Var}}.

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



Get the left child expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_ade85fc3299d47c1e0b2214a9c4f317dc}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a9411b71780dbf0939b2dd05bfbd72c16}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_ae1162068c99cac1e5e7e8b851ed492a4}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a44d1c80f33935e02f99d417f5cd2440a}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_ac17b0f31d32f20b86becd38ea546f223}{gymbosat\+::\+Var}}.

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



Get the right child expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a0d4342830b7401b595ac5481939eefe4}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a402c8546fa63d62322f4dc3b31e62545}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_add362d07c64cf42697b11f5b869b7d36}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a0c8442aaf1c872b959f1465e52b74ab5}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a46c34d8f668e561c6c78279a1246ccef}{gymbosat\+::\+Var}}.

\mbox{\Hypertarget{classgymbosat_1_1Expr_a4d946a615d7d11020d5c9f0ee8fff135}\label{classgymbosat_1_1Expr_a4d946a615d7d11020d5c9f0ee8fff135}} 
\index{gymbosat::Expr@{gymbosat::Expr}!guessVar@{guessVar}}
\index{guessVar@{guessVar}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{guessVar()}{guessVar()}}
{\footnotesize\ttfamily virtual std\+::shared\+\_\+ptr$<$\mbox{\hyperlink{classgymbosat_1_1Expr}{Expr}}$>$ gymbosat\+::\+Expr\+::guess\+Var (\begin{DoxyParamCaption}\item[{std\+::string}]{var,  }\item[{bool}]{val }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [pure 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}


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a0ba707c7cdda3b55db862df111ce25ab}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a4b17bfb2c1ff0c48922a9366dd124f84}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a77f3492efad433a53d29c273683a2bcd}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_ac7dc6c2a220f0474cb1e6b11f4775d2a}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a3c80f5b944b13a7300fd1369a38575bc}{gymbosat\+::\+Var}}.

\mbox{\Hypertarget{classgymbosat_1_1Expr_adea7d5e5285df79237a4b72a8b82c66d}\label{classgymbosat_1_1Expr_adea7d5e5285df79237a4b72a8b82c66d}} 
\index{gymbosat::Expr@{gymbosat::Expr}!literalPolarity@{literalPolarity}}
\index{literalPolarity@{literalPolarity}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{literalPolarity()}{literalPolarity()}}
{\footnotesize\ttfamily virtual std\+::unordered\+\_\+map$<$std\+::string, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{Polarity}}$>$ gymbosat\+::\+Expr\+::literal\+Polarity (\begin{DoxyParamCaption}\item[{std\+::string}]{var }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [pure 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}


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_ae8fa89dfc3b3a4549be4e4d2b212dbe3}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a72d8ea4e686aae68caa22145edb196b1}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a69ee05e12c00509993fa9dd687cd01ac}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a761328ffc63044ff03ac0f937dce2641}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a4429d6094daba3dd3278166676540a01}{gymbosat\+::\+Var}}.

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



Get the literals present in the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_ad62fdd34c799d434b18e25841099e04a}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a63945cef5d7a9392692fa66d161f8503}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_aef8f1ea74f0ee165bfa3c52ea9eba111}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a537ddf4b5192e2747744e7ad2108b11e}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a695a80ac8aea702f65bbc5ba0d34ab60}{gymbosat\+::\+Var}}.

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



Simplify the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a06ed122848ceb557bae8fe66783061a0}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a4f169fc86479de1a37f7866fe5b8a015}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a5b53d02a2cdb06adc724e709b89dac3f}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a6455aa50fd64ad0d9071a3e97955069d}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_acf837760d8d850b190c7ad753e4523db}{gymbosat\+::\+Var}}.

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



Convert the logical expression to a string representation. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_acaf729ec5f8cd7ed3b6c81cb23b7f9af}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a438829c52493f67c99cd4a85e78f03d6}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a257ff6c08e5289ed6bd02b3b5d50ee4c}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_affbe88b38fe18ca450ca074b6cfd135e}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_ab22296034c16195902c0bb01799722e1}{gymbosat\+::\+Var}}.

\mbox{\Hypertarget{classgymbosat_1_1Expr_a462170452606863e487f0807be83a96a}\label{classgymbosat_1_1Expr_a462170452606863e487f0807be83a96a}} 
\index{gymbosat::Expr@{gymbosat::Expr}!unConst@{unConst}}
\index{unConst@{unConst}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{unConst()}{unConst()}}
{\footnotesize\ttfamily virtual bool gymbosat\+::\+Expr\+::un\+Const (\begin{DoxyParamCaption}{ }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [pure 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}


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a3b3a3ef47d754c53d913ec0cebf6ec36}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a5d09bc42cae0a9bf522c5375d7ba8f70}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a84aa719f774ffd20a78a4cfa4a931c7a}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_a6d4e1f0b5d1d9379e90ed5d80e0fcf3a}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_a48452af858f886d121455123176cbb63}{gymbosat\+::\+Var}}.

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



Get a unit clause from the logical expression. 

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


Implemented in \mbox{\hyperlink{classgymbosat_1_1Const_a32e2e08c72ef3820c5e6cb92cef05d2c}{gymbosat\+::\+Const}}, \mbox{\hyperlink{classgymbosat_1_1Not_a4118ba387b374d8e8940a64db34941f9}{gymbosat\+::\+Not}}, \mbox{\hyperlink{classgymbosat_1_1Or_a2538710166c753dec215727198866b66}{gymbosat\+::\+Or}}, \mbox{\hyperlink{classgymbosat_1_1And_afffae51480f5b0ffe99d27bc0a60ec90}{gymbosat\+::\+And}}, and \mbox{\hyperlink{classgymbosat_1_1Var_aa59b38a82e6b503c295635c0dc68adef}{gymbosat\+::\+Var}}.



\doxysubsection{Member Data Documentation}
\mbox{\Hypertarget{classgymbosat_1_1Expr_ad4a359e63fbd7d3fe3cb598300a1c61e}\label{classgymbosat_1_1Expr_ad4a359e63fbd7d3fe3cb598300a1c61e}} 
\index{gymbosat::Expr@{gymbosat::Expr}!name@{name}}
\index{name@{name}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{name}{name}}
{\footnotesize\ttfamily std\+::string gymbosat\+::\+Expr\+::name}

Name associated with the expression. \mbox{\Hypertarget{classgymbosat_1_1Expr_aa84655ea020547722c7433af5c009d27}\label{classgymbosat_1_1Expr_aa84655ea020547722c7433af5c009d27}} 
\index{gymbosat::Expr@{gymbosat::Expr}!opcode@{opcode}}
\index{opcode@{opcode}!gymbosat::Expr@{gymbosat::Expr}}
\doxysubsubsection{\texorpdfstring{opcode}{opcode}}
{\footnotesize\ttfamily \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}{Op\+Code}} gymbosat\+::\+Expr\+::opcode}

Operation code for the expression. 

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