\hypertarget{structgymbo_1_1SExecutor}{}\doxysection{gymbo\+::SExecutor Struct Reference}
\label{structgymbo_1_1SExecutor}\index{gymbo::SExecutor@{gymbo::SExecutor}}


Represents a derived class for symbolic execution engine for deterministic programs.  




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



Inheritance diagram for gymbo\+::SExecutor\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=202pt]{structgymbo_1_1SExecutor__inherit__graph}
\end{center}
\end{figure}


Collaboration diagram for gymbo\+::SExecutor\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=202pt]{structgymbo_1_1SExecutor__coll__graph}
\end{center}
\end{figure}
\doxysubsection*{Public Member Functions}
\begin{DoxyCompactItemize}
\item 
bool \mbox{\hyperlink{structgymbo_1_1SExecutor_a59f5891ef952677a333d5040978cddfd}{solve}} (bool is\+\_\+target, int pc, \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&state)
\begin{DoxyCompactList}\small\item\em Solves path constraints and updates the cache. \end{DoxyCompactList}\item 
\mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} \mbox{\hyperlink{structgymbo_1_1SExecutor_a51286f8002b2465f71bf648b94b646cc}{run}} (\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&prog, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&state, int max\+Depth=256)
\begin{DoxyCompactList}\small\item\em Symbolically Execute a Program with Gradient Descent Optimization. \end{DoxyCompactList}\item 
\mbox{\hyperlink{structgymbo_1_1SExecutor_ac50697ded09001c18e10a7ef980b1d8e}{Base\+Executor}} (\mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a5be3e38314fe7cea470837a7ddea6f92}{optimizer}}, int \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a824a4c52632a08005a8a0264308a7372}{max\+SAT}}=256, int \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a4fff090ea20da5638a9c6801bc6d0a67}{max\+UNSAT}}=256, int \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a11bcbb9c82b00bc4c96481198464fea9}{max\+\_\+num\+\_\+trials}}=10, bool \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a4be9366c810f0d7cc89a53f2763c5eff}{ignore\+\_\+memory}}=false, bool \mbox{\hyperlink{structgymbo_1_1BaseExecutor_afcf1a585351b645d5ca9294a6e791ef4}{use\+\_\+dpll}}=false, int \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a8955bd4fe56d26bda2324b95f3700829}{verbose\+\_\+level}}=0, bool \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a467faae223c1e02ced0eab62650e43db}{return\+\_\+trace}}=false)
\begin{DoxyCompactList}\small\item\em Constructor for \mbox{\hyperlink{structgymbo_1_1BaseExecutor}{Base\+Executor}}. \end{DoxyCompactList}\end{DoxyCompactItemize}
\doxysubsection*{Public Attributes}
\begin{DoxyCompactItemize}
\item 
\mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \mbox{\hyperlink{structgymbo_1_1SExecutor_acfa19f2c340c7a057f5c9457af201feb}{constraints\+\_\+cache}}
\begin{DoxyCompactList}\small\item\em Cache for storing and reusing path constraints. \end{DoxyCompactList}\end{DoxyCompactItemize}


\doxysubsection{Detailed Description}
Represents a derived class for symbolic execution engine for deterministic programs. 

\doxysubsection{Member Function Documentation}
\mbox{\Hypertarget{structgymbo_1_1SExecutor_ac50697ded09001c18e10a7ef980b1d8e}\label{structgymbo_1_1SExecutor_ac50697ded09001c18e10a7ef980b1d8e}} 
\index{gymbo::SExecutor@{gymbo::SExecutor}!BaseExecutor@{BaseExecutor}}
\index{BaseExecutor@{BaseExecutor}!gymbo::SExecutor@{gymbo::SExecutor}}
\doxysubsubsection{\texorpdfstring{BaseExecutor()}{BaseExecutor()}}
{\footnotesize\ttfamily gymbo\+::\+Base\+Executor\+::\+Base\+Executor\hspace{0.3cm}{\ttfamily [inline]}}



Constructor for \mbox{\hyperlink{structgymbo_1_1BaseExecutor}{Base\+Executor}}. 


\begin{DoxyParams}{Parameters}
{\em optimizer} & The gradient descent optimizer for parameter optimization. \\
\hline
{\em max\+SAT} & The maximum number of SAT constraints to collect. \\
\hline
{\em max\+UNSAT} & The maximum number of UNSAT constraints to collect. \\
\hline
{\em max\+\_\+num\+\_\+trials} & The maximum number of trials for each gradient descent. \\
\hline
{\em ignore\+\_\+memory} & If set to true, constraints derived from memory will be ignored. \\
\hline
{\em use\+\_\+dpll} & If set to true, use DPLL to decide the initial assignment for each term. \\
\hline
{\em verbose\+\_\+level} & The level of verbosity. \\
\hline
{\em return\+\_\+trace} & If set to true, save the trace at each pc and return them (default false). \\
\hline
\end{DoxyParams}
\mbox{\Hypertarget{structgymbo_1_1SExecutor_a51286f8002b2465f71bf648b94b646cc}\label{structgymbo_1_1SExecutor_a51286f8002b2465f71bf648b94b646cc}} 
\index{gymbo::SExecutor@{gymbo::SExecutor}!run@{run}}
\index{run@{run}!gymbo::SExecutor@{gymbo::SExecutor}}
\doxysubsubsection{\texorpdfstring{run()}{run()}}
{\footnotesize\ttfamily \mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} gymbo\+::\+SExecutor\+::run (\begin{DoxyParamCaption}\item[{\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&}]{prog,  }\item[{std\+::unordered\+\_\+set$<$ int $>$ \&}]{target\+\_\+pcs,  }\item[{\mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&}]{state,  }\item[{int}]{max\+Depth = {\ttfamily 256} }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [virtual]}}



Symbolically Execute a Program with Gradient Descent Optimization. 

This function conducts symbolic execution of a given program while simultaneously optimizing the path constraints using the provided gradient descent optimizer, {\ttfamily \mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}}}.


\begin{DoxyParams}{Parameters}
{\em prog} & The program to symbolically execute. \\
\hline
{\em target\+\_\+pcs} & The set of pc where gymbo executes path-\/constraints solving. If this set is empty or contains -\/1, gymbo solves all path-\/constraints. \\
\hline
{\em state} & The initial symbolic state of the program. \\
\hline
{\em max\+Depth} & The maximum depth of symbolic exploration. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
A trace of the symbolic execution. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{structgymbo_1_1BaseExecutor_a7df59ba85914f0e054a8f0b503711351}{gymbo\+::\+Base\+Executor}}.

\mbox{\Hypertarget{structgymbo_1_1SExecutor_a59f5891ef952677a333d5040978cddfd}\label{structgymbo_1_1SExecutor_a59f5891ef952677a333d5040978cddfd}} 
\index{gymbo::SExecutor@{gymbo::SExecutor}!solve@{solve}}
\index{solve@{solve}!gymbo::SExecutor@{gymbo::SExecutor}}
\doxysubsubsection{\texorpdfstring{solve()}{solve()}}
{\footnotesize\ttfamily bool gymbo\+::\+SExecutor\+::solve (\begin{DoxyParamCaption}\item[{bool}]{is\+\_\+target,  }\item[{int}]{pc,  }\item[{\mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&}]{state }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}, {\ttfamily [virtual]}}



Solves path constraints and updates the cache. 

This function solves path constraints, updates the cache, and prints verbose information if conditions are met.


\begin{DoxyParams}{Parameters}
{\em is\+\_\+target} & Flag indicating whether the program counter is a target. \\
\hline
{\em pc} & The program counter. \\
\hline
{\em state} & Reference to the symbolic state. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
The flag indicating satisfifiability. 
\end{DoxyReturn}


Implements \mbox{\hyperlink{structgymbo_1_1BaseExecutor_ab075472095a48ab173af2121f8156e21}{gymbo\+::\+Base\+Executor}}.



\doxysubsection{Member Data Documentation}
\mbox{\Hypertarget{structgymbo_1_1SExecutor_acfa19f2c340c7a057f5c9457af201feb}\label{structgymbo_1_1SExecutor_acfa19f2c340c7a057f5c9457af201feb}} 
\index{gymbo::SExecutor@{gymbo::SExecutor}!constraints\_cache@{constraints\_cache}}
\index{constraints\_cache@{constraints\_cache}!gymbo::SExecutor@{gymbo::SExecutor}}
\doxysubsubsection{\texorpdfstring{constraints\_cache}{constraints\_cache}}
{\footnotesize\ttfamily \mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} gymbo\+::\+SExecutor\+::constraints\+\_\+cache}



Cache for storing and reusing path constraints. 



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