\hypertarget{structgymbo_1_1PSExecutor}{}\doxysection{gymbo\+::PSExecutor Struct Reference}
\label{structgymbo_1_1PSExecutor}\index{gymbo::PSExecutor@{gymbo::PSExecutor}}


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




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



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


Collaboration diagram for gymbo\+::PSExecutor\+:\nopagebreak
\begin{figure}[H]
\begin{center}
\leavevmode
\includegraphics[width=202pt]{structgymbo_1_1PSExecutor__coll__graph}
\end{center}
\end{figure}
\doxysubsection*{Public Member Functions}
\begin{DoxyCompactItemize}
\item 
void \mbox{\hyperlink{structgymbo_1_1PSExecutor_a4a37d705557ea3bb094f65a376c4c919}{register\+\_\+random\+\_\+var}} (int var\+\_\+id)
\item 
bool \mbox{\hyperlink{structgymbo_1_1PSExecutor_ad20d28e31b9411155eeeeabf5abaeac2}{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 symbolic state. \end{DoxyCompactList}\item 
\mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} \mbox{\hyperlink{structgymbo_1_1PSExecutor_a180bdab3a4656e692125dc345fe887bd}{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 Run probabilistic symbolic execution on a program. \end{DoxyCompactList}\item 
\mbox{\hyperlink{structgymbo_1_1PSExecutor_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 
std\+::unordered\+\_\+set$<$ int $>$ \mbox{\hyperlink{structgymbo_1_1PSExecutor_a17671e8308b45544fae07dcbd1c1aa6c}{random\+\_\+vars}}
\begin{DoxyCompactList}\small\item\em Set of random variables\textquotesingle{}IDs. \end{DoxyCompactList}\item 
\mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \mbox{\hyperlink{structgymbo_1_1PSExecutor_a2539e874335ed3a4932b970b56c68731}{constraints\+\_\+cache}}
\begin{DoxyCompactList}\small\item\em Cache for storing and reusing path constraints. \end{DoxyCompactList}\item 
\mbox{\hyperlink{namespacegymbo_a035e6fe34f819db35a5662ae0cf427d3}{Prob\+Path\+Constraints\+Table}} \mbox{\hyperlink{structgymbo_1_1PSExecutor_acce527624db36d3db3c92c7c60047140}{prob\+\_\+constraints\+\_\+table}}
\end{DoxyCompactItemize}


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

\doxysubsection{Member Function Documentation}
\mbox{\Hypertarget{structgymbo_1_1PSExecutor_ac50697ded09001c18e10a7ef980b1d8e}\label{structgymbo_1_1PSExecutor_ac50697ded09001c18e10a7ef980b1d8e}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!BaseExecutor@{BaseExecutor}}
\index{BaseExecutor@{BaseExecutor}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\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_1PSExecutor_a4a37d705557ea3bb094f65a376c4c919}\label{structgymbo_1_1PSExecutor_a4a37d705557ea3bb094f65a376c4c919}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!register\_random\_var@{register\_random\_var}}
\index{register\_random\_var@{register\_random\_var}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\doxysubsubsection{\texorpdfstring{register\_random\_var()}{register\_random\_var()}}
{\footnotesize\ttfamily void gymbo\+::\+PSExecutor\+::register\+\_\+random\+\_\+var (\begin{DoxyParamCaption}\item[{int}]{var\+\_\+id }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}

\mbox{\Hypertarget{structgymbo_1_1PSExecutor_a180bdab3a4656e692125dc345fe887bd}\label{structgymbo_1_1PSExecutor_a180bdab3a4656e692125dc345fe887bd}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!run@{run}}
\index{run@{run}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\doxysubsubsection{\texorpdfstring{run()}{run()}}
{\footnotesize\ttfamily \mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} gymbo\+::\+PSExecutor\+::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]}}



Run probabilistic symbolic execution on a program. 

This function performs probabilistic symbolic execution on a given program, considering variable distributions, symbolic states, and path constraints. It explores different execution paths and updates the constraints and probabilities accordingly.


\begin{DoxyParams}{Parameters}
{\em prog} & The program to symbolically execute. \\
\hline
{\em target\+\_\+pcs} & 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 for execution. \\
\hline
{\em max\+Depth} & Maximum exploration depth during symbolic execution. \\
\hline
\end{DoxyParams}
\begin{DoxyReturn}{Returns}
The symbolic execution trace containing states and child traces. 
\end{DoxyReturn}


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

\mbox{\Hypertarget{structgymbo_1_1PSExecutor_ad20d28e31b9411155eeeeabf5abaeac2}\label{structgymbo_1_1PSExecutor_ad20d28e31b9411155eeeeabf5abaeac2}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!solve@{solve}}
\index{solve@{solve}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\doxysubsubsection{\texorpdfstring{solve()}{solve()}}
{\footnotesize\ttfamily bool gymbo\+::\+PSExecutor\+::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 symbolic state. 

This function checks the satisfiability of the path constraints using an SMT solver or a probabilistic branching algorithm. It updates the symbolic state based on the result and stores the solution in a cache for future use.


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


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



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



Cache for storing and reusing path constraints. 

\mbox{\Hypertarget{structgymbo_1_1PSExecutor_acce527624db36d3db3c92c7c60047140}\label{structgymbo_1_1PSExecutor_acce527624db36d3db3c92c7c60047140}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!prob\_constraints\_table@{prob\_constraints\_table}}
\index{prob\_constraints\_table@{prob\_constraints\_table}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\doxysubsubsection{\texorpdfstring{prob\_constraints\_table}{prob\_constraints\_table}}
{\footnotesize\ttfamily \mbox{\hyperlink{namespacegymbo_a035e6fe34f819db35a5662ae0cf427d3}{Prob\+Path\+Constraints\+Table}} gymbo\+::\+PSExecutor\+::prob\+\_\+constraints\+\_\+table}

Table for storing probabilistic path constraints. \mbox{\Hypertarget{structgymbo_1_1PSExecutor_a17671e8308b45544fae07dcbd1c1aa6c}\label{structgymbo_1_1PSExecutor_a17671e8308b45544fae07dcbd1c1aa6c}} 
\index{gymbo::PSExecutor@{gymbo::PSExecutor}!random\_vars@{random\_vars}}
\index{random\_vars@{random\_vars}!gymbo::PSExecutor@{gymbo::PSExecutor}}
\doxysubsubsection{\texorpdfstring{random\_vars}{random\_vars}}
{\footnotesize\ttfamily std\+::unordered\+\_\+set$<$int$>$ gymbo\+::\+PSExecutor\+::random\+\_\+vars}



Set of random variables\textquotesingle{}IDs. 



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