\hypertarget{sat_8h}{}\doxysection{libgymbo/sat.h File Reference}
\label{sat_8h}\index{libgymbo/sat.h@{libgymbo/sat.h}}


Implementation of SAT solver.  


{\ttfamily \#include $<$memory$>$}\newline
{\ttfamily \#include \char`\"{}type.\+h\char`\"{}}\newline
Include dependency graph for sat.\+h\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=350pt]{sat_8h__incl}
\end{center}
\end{figure}
This graph shows which files directly or indirectly include this file\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=205pt]{sat_8h__dep__incl}
\end{center}
\end{figure}
\doxysubsection*{Classes}
\begin{DoxyCompactItemize}
\item 
class \mbox{\hyperlink{classgymbosat_1_1Expr}{gymbosat\+::\+Expr}}
\begin{DoxyCompactList}\small\item\em Base class for representing logical expressions. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Var}{gymbosat\+::\+Var}}
\begin{DoxyCompactList}\small\item\em Class representing a variable in a logical expression. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1And}{gymbosat\+::\+And}}
\begin{DoxyCompactList}\small\item\em Class representing the logical AND operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Or}{gymbosat\+::\+Or}}
\begin{DoxyCompactList}\small\item\em Class representing the logical OR operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Not}{gymbosat\+::\+Not}}
\begin{DoxyCompactList}\small\item\em Class representing the logical NOT operation. \end{DoxyCompactList}\item 
class \mbox{\hyperlink{classgymbosat_1_1Const}{gymbosat\+::\+Const}}
\begin{DoxyCompactList}\small\item\em Class representing a boolean constant in a logical expression. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Namespaces}
\begin{DoxyCompactItemize}
\item 
 \mbox{\hyperlink{namespacegymbosat}{gymbosat}}
\end{DoxyCompactItemize}
\doxysubsection*{Enumerations}
\begin{DoxyCompactItemize}
\item 
enum \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024}{gymbosat\+::\+Op\+Code}} \{ \newline
\mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a783aa8811c0d97c103452691317996a5}{gymbosat\+::\+VAR}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024ad2e14235bea46219c69d69b818deda51}{gymbosat\+::\+AND}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa707761460979d2894359f95295f922d}{gymbosat\+::\+OR}}
, \mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024aa1aa2298eeb70aab521df090792f029e}{gymbosat\+::\+NOT}}
, \newline
\mbox{\hyperlink{namespacegymbosat_a6d86d55f55f58425a61afe7f71066024a8ff08a99249527948f9bbe6633e8f5b3}{gymbosat\+::\+CONST}}
 \}
\begin{DoxyCompactList}\small\item\em Enum representing different logical operation codes. \end{DoxyCompactList}\item 
enum \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2}{gymbosat\+::\+Polarity}} \{ \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2a339b3ba4e7e766359538835c6e30c883}{gymbosat\+::\+Positive}}
, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2af58cec105a8a618a79c888a3bef6a293}{gymbosat\+::\+Negative}}
, \mbox{\hyperlink{namespacegymbosat_ab93a240afc8d89ec25d1bb528545f6d2aa41fd20cf2100eceb7f63242f216503a}{gymbosat\+::\+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$<$ Expr $>$ \mbox{\hyperlink{namespacegymbosat_aee3ea3ef6116322c249d4f557b51326d}{gymbosat\+::cnf}} (std\+::shared\+\_\+ptr$<$ Expr $>$ expr)
\begin{DoxyCompactList}\small\item\em Convert a logical expression to conjunctive normal form (CNF). \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ Expr $>$ \mbox{\hyperlink{namespacegymbosat_a39eb2e94bf479cf70e9f4f20ae1b7ed4}{gymbosat\+::literal\+Elimination}} (std\+::shared\+\_\+ptr$<$ 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}{gymbosat\+::all\+Unit\+Clauses}} (std\+::shared\+\_\+ptr$<$ Expr $>$ expr)
\begin{DoxyCompactList}\small\item\em Extract all unit clauses from a logical expression. \end{DoxyCompactList}\item 
std\+::shared\+\_\+ptr$<$ Expr $>$ \mbox{\hyperlink{namespacegymbosat_a900a3e916b5f594baf9598112ff29db9}{gymbosat\+::unit\+Propagation}} (std\+::shared\+\_\+ptr$<$ 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}{gymbosat\+::satisfiable\+DPLL}} (std\+::shared\+\_\+ptr$<$ 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$<$ Expr $>$ \mbox{\hyperlink{namespacegymbosat_a03e10dde5ead3c1638a3959f61df655a}{gymbosat\+::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$<$ Expr $>$ \mbox{\hyperlink{namespacegymbosat_a6f0b9965254e8e0a97d6ce893d01cd06}{gymbosat\+::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{Detailed Description}
Implementation of SAT solver. 

\begin{DoxyAuthor}{Author}
Hideaki Takahashi 
\end{DoxyAuthor}
