Option for Saving Traces (#31)

* add option to discard traces * update docs
Koukyosyumei · Dec 7, 2023 · 0feb645 · 0feb645
1 parent 8adc179
commit 0feb645
Show file tree

Hide file tree

Showing 14 changed files with 450 additions and 426 deletions.
diff --git a/docs/index.html b/docs/index.html
@@ -177,14 +177,14 @@ <h1><a class="anchor" id="cli_sec"></a>
 <div class="line"><a class="code" href="namespacegymbo.html#a1af6d97f4c122833601a9b054a23009a">gymbo::compile_ast</a>(code, prg);</div>
 <div class="line"> </div>
 <div class="line"><span class="comment">// execute gradient-based symbolie execution</span></div>
-<div class="line"><a class="code" href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">gymbo::run_gymbo</a>(prg, optimizer, init, cache_constraints, ...);</div>
+<div class="line"><a class="code" href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">gymbo::run_gymbo</a>(prg, optimizer, init, cache_constraints, ...);</div>
 <div class="ttc" id="acompiler_8h_html"><div class="ttname"><a href="compiler_8h.html">compiler.h</a></div><div class="ttdoc">Implementation of compiler.</div></div>
 <div class="ttc" id="agd_8h_html"><div class="ttname"><a href="gd_8h.html">gd.h</a></div><div class="ttdoc">Implementation of gradient descent optimizer.</div></div>
 <div class="ttc" id="anamespacegymbo_html_a1af6d97f4c122833601a9b054a23009a"><div class="ttname"><a href="namespacegymbo.html#a1af6d97f4c122833601a9b054a23009a">gymbo::compile_ast</a></div><div class="ttdeci">void compile_ast(std::vector&lt; Node * &gt; code, Prog &amp;prg)</div><div class="ttdoc">Compile the Abstract Syntax Tree (AST) into a sequence of instructions.</div><div class="ttdef"><b>Definition:</b> compiler.h:133</div></div>
 <div class="ttc" id="anamespacegymbo_html_a5e7728b7fbac9bf79ae665cf9b94f443"><div class="ttname"><a href="namespacegymbo.html#a5e7728b7fbac9bf79ae665cf9b94f443">gymbo::generate_ast</a></div><div class="ttdeci">void generate_ast(Token *&amp;token, char *user_input, std::vector&lt; Node * &gt; &amp;code)</div><div class="ttdoc">Parses a C-like language program into an AST.</div><div class="ttdef"><b>Definition:</b> parser.h:439</div></div>
 <div class="ttc" id="anamespacegymbo_html_a89c8cb7e3b04d3d02f0cba69ab593981"><div class="ttname"><a href="namespacegymbo.html#a89c8cb7e3b04d3d02f0cba69ab593981">gymbo::tokenize</a></div><div class="ttdeci">Token * tokenize(char *user_input, std::unordered_map&lt; std::string, int &gt; &amp;var_counter)</div><div class="ttdoc">Tokenizes a given string and returns a linked list of tokens.</div><div class="ttdef"><b>Definition:</b> tokenizer.h:222</div></div>
-<div class="ttc" id="anamespacegymbo_html_a8aa21505f18c246fc0adafb360939fe0"><div class="ttname"><a href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">gymbo::run_gymbo</a></div><div class="ttdeci">Trace run_gymbo(Prog &amp;prog, GDOptimizer &amp;optimizer, SymState &amp;state, std::unordered_set&lt; int &gt; &amp;taregt_pcs, PathConstraintsTable &amp;constraints_cache, int maxDepth, int &amp;maxSAT, int &amp;maxUNSAT, int max_num_trials, bool ignore_memory, bool use_dpll, int verbose_level)</div><div class="ttdoc">Symbolically Execute a Program with Gradient Descent Optimization.</div><div class="ttdef"><b>Definition:</b> symbolic.h:65</div></div>
 <div class="ttc" id="anamespacegymbo_html_a9b6a88c2be45a5e3fd3f053681f89733"><div class="ttname"><a href="namespacegymbo.html#a9b6a88c2be45a5e3fd3f053681f89733">gymbo::Prog</a></div><div class="ttdeci">std::vector&lt; Instr &gt; Prog</div><div class="ttdoc">Alias for a program, represented as a vector of instructions.</div><div class="ttdef"><b>Definition:</b> type.h:144</div></div>
+<div class="ttc" id="anamespacegymbo_html_aa13abbc332896d34bc320950bdacfdf9"><div class="ttname"><a href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">gymbo::run_gymbo</a></div><div class="ttdeci">Trace run_gymbo(Prog &amp;prog, GDOptimizer &amp;optimizer, SymState &amp;state, std::unordered_set&lt; int &gt; &amp;taregt_pcs, PathConstraintsTable &amp;constraints_cache, int maxDepth, int &amp;maxSAT, int &amp;maxUNSAT, int max_num_trials, bool ignore_memory, bool use_dpll, int verbose_level, bool return_trace)</div><div class="ttdoc">Symbolically Execute a Program with Gradient Descent Optimization.</div><div class="ttdef"><b>Definition:</b> symbolic.h:68</div></div>
 <div class="ttc" id="anamespacegymbo_html_aea0120f1cdc1417f9b6b8480ac562389"><div class="ttname"><a href="namespacegymbo.html#aea0120f1cdc1417f9b6b8480ac562389">gymbo::PathConstraintsTable</a></div><div class="ttdeci">std::unordered_map&lt; std::string, std::pair&lt; bool, std::unordered_map&lt; int, float &gt; &gt;&gt; PathConstraintsTable</div><div class="ttdoc">Alias for a table of path constraints. The key is the string representation of the constraint and the...</div><div class="ttdef"><b>Definition:</b> type.h:159</div></div>
 <div class="ttc" id="aparser_8h_html"><div class="ttname"><a href="parser_8h.html">parser.h</a></div><div class="ttdoc">Implementation of parser.</div></div>
 <div class="ttc" id="astructgymbo_1_1GDOptimizer_html"><div class="ttname"><a href="structgymbo_1_1GDOptimizer.html">gymbo::GDOptimizer</a></div><div class="ttdoc">Gradient Descent Optimizer for Symbolic Path Constraints.</div><div class="ttdef"><b>Definition:</b> gd.h:28</div></div>

diff --git a/docs/latex/index.tex b/docs/latex/index.tex
@@ -121,7 +121,7 @@
 \DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a1af6d97f4c122833601a9b054a23009a}{gymbo::compile\_ast}}(code, prg);}
 \DoxyCodeLine{}
 \DoxyCodeLine{\textcolor{comment}{// execute gradient-\/based symbolie execution}}
-\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_a8aa21505f18c246fc0adafb360939fe0}{gymbo::run\_gymbo}}(prg, optimizer, init, cache\_constraints, ...);}
+\DoxyCodeLine{\mbox{\hyperlink{namespacegymbo_aa13abbc332896d34bc320950bdacfdf9}{gymbo::run\_gymbo}}(prg, optimizer, init, cache\_constraints, ...);}
 
 \end{DoxyCode}
 \hypertarget{index_python_sec}{}\doxysection{Python API}\label{index_python_sec}

diff --git a/docs/latex/namespacegymbo.tex b/docs/latex/namespacegymbo.tex
@@ -160,7 +160,7 @@
 \begin{DoxyCompactList}\small\item\em Compiles user input into a program, returning variable counts and the compiled program. \end{DoxyCompactList}\item 
 \mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \mbox{\hyperlink{namespacegymbo_af40a70afb521e856bda968808b2b492e}{gexecute}} (\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&prg, \mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \&optimizer, \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&init, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, int max\+\_\+depth, int max\+SAT, int max\+UNSAT, int max\+\_\+num\+\_\+trials, bool ignore\+\_\+memory, bool use\+\_\+dpll, int verbose\+\_\+level)
 \begin{DoxyCompactList}\small\item\em Symbolically Executes a Program with Gradient Descent Optimization. \end{DoxyCompactList}\item 
-\mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} \mbox{\hyperlink{namespacegymbo_a8aa21505f18c246fc0adafb360939fe0}{run\+\_\+gymbo}} (\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&prog, \mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \&optimizer, \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&state, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, \mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \&constraints\+\_\+cache, int max\+Depth, int \&max\+SAT, int \&max\+UNSAT, int max\+\_\+num\+\_\+trials, bool ignore\+\_\+memory, bool use\+\_\+dpll, int verbose\+\_\+level)
+\mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} \mbox{\hyperlink{namespacegymbo_aa13abbc332896d34bc320950bdacfdf9}{run\+\_\+gymbo}} (\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&prog, \mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \&optimizer, \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&state, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, \mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \&constraints\+\_\+cache, int max\+Depth, int \&max\+SAT, int \&max\+UNSAT, int max\+\_\+num\+\_\+trials, bool ignore\+\_\+memory, bool use\+\_\+dpll, int verbose\+\_\+level, bool return\+\_\+trace=false)
 \begin{DoxyCompactList}\small\item\em Symbolically Execute a Program with Gradient Descent Optimization. \end{DoxyCompactList}\item 
 void \mbox{\hyperlink{namespacegymbo_a70694fc6a91234300048503b2fe15a9b}{sym\+Step}} (\mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&state, \mbox{\hyperlink{classgymbo_1_1Instr}{Instr}} instr, std\+::vector$<$ \mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} $>$ \&result)
 \begin{DoxyCompactList}\small\item\em Symbolically Execute a Single Instruction of a Program. \end{DoxyCompactList}\item 
@@ -1162,11 +1162,11 @@
 \begin{DoxyReturn}{Returns}
 An AST node representing the relational expression. 
 \end{DoxyReturn}
-\mbox{\Hypertarget{namespacegymbo_a8aa21505f18c246fc0adafb360939fe0}\label{namespacegymbo_a8aa21505f18c246fc0adafb360939fe0}} 
+\mbox{\Hypertarget{namespacegymbo_aa13abbc332896d34bc320950bdacfdf9}\label{namespacegymbo_aa13abbc332896d34bc320950bdacfdf9}} 
 \index{gymbo@{gymbo}!run\_gymbo@{run\_gymbo}}
 \index{run\_gymbo@{run\_gymbo}!gymbo@{gymbo}}
 \doxysubsubsection{\texorpdfstring{run\_gymbo()}{run\_gymbo()}}
-{\footnotesize\ttfamily \mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} gymbo\+::run\+\_\+gymbo (\begin{DoxyParamCaption}\item[{\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&}]{prog,  }\item[{\mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \&}]{optimizer,  }\item[{\mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&}]{state,  }\item[{std\+::unordered\+\_\+set$<$ int $>$ \&}]{target\+\_\+pcs,  }\item[{\mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \&}]{constraints\+\_\+cache,  }\item[{int}]{max\+Depth,  }\item[{int \&}]{max\+SAT,  }\item[{int \&}]{max\+UNSAT,  }\item[{int}]{max\+\_\+num\+\_\+trials,  }\item[{bool}]{ignore\+\_\+memory,  }\item[{bool}]{use\+\_\+dpll,  }\item[{int}]{verbose\+\_\+level }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}
+{\footnotesize\ttfamily \mbox{\hyperlink{structgymbo_1_1Trace}{Trace}} gymbo\+::run\+\_\+gymbo (\begin{DoxyParamCaption}\item[{\mbox{\hyperlink{namespacegymbo_a9b6a88c2be45a5e3fd3f053681f89733}{Prog}} \&}]{prog,  }\item[{\mbox{\hyperlink{structgymbo_1_1GDOptimizer}{GDOptimizer}} \&}]{optimizer,  }\item[{\mbox{\hyperlink{structgymbo_1_1SymState}{Sym\+State}} \&}]{state,  }\item[{std\+::unordered\+\_\+set$<$ int $>$ \&}]{target\+\_\+pcs,  }\item[{\mbox{\hyperlink{namespacegymbo_aea0120f1cdc1417f9b6b8480ac562389}{Path\+Constraints\+Table}} \&}]{constraints\+\_\+cache,  }\item[{int}]{max\+Depth,  }\item[{int \&}]{max\+SAT,  }\item[{int \&}]{max\+UNSAT,  }\item[{int}]{max\+\_\+num\+\_\+trials,  }\item[{bool}]{ignore\+\_\+memory,  }\item[{bool}]{use\+\_\+dpll,  }\item[{int}]{verbose\+\_\+level,  }\item[{bool}]{return\+\_\+trace = {\ttfamily false} }\end{DoxyParamCaption})\hspace{0.3cm}{\ttfamily [inline]}}
 
 
 
@@ -1200,6 +1200,8 @@
 \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}
 \begin{DoxyReturn}{Returns}
 A trace of the symbolic execution. 

diff --git a/docs/latex/symbolic_8h.tex b/docs/latex/symbolic_8h.tex
@@ -29,7 +29,7 @@
 \doxysubsection*{Functions}
 \begin{DoxyCompactItemize}
 \item 
-Trace \mbox{\hyperlink{namespacegymbo_a8aa21505f18c246fc0adafb360939fe0}{gymbo\+::run\+\_\+gymbo}} (Prog \&prog, GDOptimizer \&optimizer, Sym\+State \&state, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, Path\+Constraints\+Table \&constraints\+\_\+cache, int max\+Depth, int \&max\+SAT, int \&max\+UNSAT, int max\+\_\+num\+\_\+trials, bool ignore\+\_\+memory, bool use\+\_\+dpll, int verbose\+\_\+level)
+Trace \mbox{\hyperlink{namespacegymbo_aa13abbc332896d34bc320950bdacfdf9}{gymbo\+::run\+\_\+gymbo}} (Prog \&prog, GDOptimizer \&optimizer, Sym\+State \&state, std\+::unordered\+\_\+set$<$ int $>$ \&target\+\_\+pcs, Path\+Constraints\+Table \&constraints\+\_\+cache, int max\+Depth, int \&max\+SAT, int \&max\+UNSAT, int max\+\_\+num\+\_\+trials, bool ignore\+\_\+memory, bool use\+\_\+dpll, int verbose\+\_\+level, bool return\+\_\+trace=false)
 \begin{DoxyCompactList}\small\item\em Symbolically Execute a Program with Gradient Descent Optimization. \end{DoxyCompactList}\item 
 void \mbox{\hyperlink{namespacegymbo_a70694fc6a91234300048503b2fe15a9b}{gymbo\+::sym\+Step}} (Sym\+State \&state, Instr instr, std\+::vector$<$ Sym\+State $>$ \&result)
 \begin{DoxyCompactList}\small\item\em Symbolically Execute a Single Instruction of a Program. \end{DoxyCompactList}\item 

diff --git a/docs/namespacegymbo.html b/docs/namespacegymbo.html
@@ -270,9 +270,9 @@
 <tr class="memitem:af40a70afb521e856bda968808b2b492e"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespacegymbo.html#aea0120f1cdc1417f9b6b8480ac562389">PathConstraintsTable</a>&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="namespacegymbo.html#af40a70afb521e856bda968808b2b492e">gexecute</a> (<a class="el" href="namespacegymbo.html#a9b6a88c2be45a5e3fd3f053681f89733">Prog</a> &amp;prg, <a class="el" href="structgymbo_1_1GDOptimizer.html">GDOptimizer</a> &amp;optimizer, <a class="el" href="structgymbo_1_1SymState.html">SymState</a> &amp;init, std::unordered_set&lt; int &gt; &amp;target_pcs, int max_depth, int maxSAT, int maxUNSAT, int max_num_trials, bool ignore_memory, bool use_dpll, int verbose_level)</td></tr>
 <tr class="memdesc:af40a70afb521e856bda968808b2b492e"><td class="mdescLeft">&#160;</td><td class="mdescRight">Symbolically Executes a Program with Gradient Descent Optimization.  <a href="namespacegymbo.html#af40a70afb521e856bda968808b2b492e">More...</a><br /></td></tr>
 <tr class="separator:af40a70afb521e856bda968808b2b492e"><td class="memSeparator" colspan="2">&#160;</td></tr>
-<tr class="memitem:a8aa21505f18c246fc0adafb360939fe0"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structgymbo_1_1Trace.html">Trace</a>&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">run_gymbo</a> (<a class="el" href="namespacegymbo.html#a9b6a88c2be45a5e3fd3f053681f89733">Prog</a> &amp;prog, <a class="el" href="structgymbo_1_1GDOptimizer.html">GDOptimizer</a> &amp;optimizer, <a class="el" href="structgymbo_1_1SymState.html">SymState</a> &amp;state, std::unordered_set&lt; int &gt; &amp;target_pcs, <a class="el" href="namespacegymbo.html#aea0120f1cdc1417f9b6b8480ac562389">PathConstraintsTable</a> &amp;constraints_cache, int maxDepth, int &amp;maxSAT, int &amp;maxUNSAT, int max_num_trials, bool ignore_memory, bool use_dpll, int verbose_level)</td></tr>
-<tr class="memdesc:a8aa21505f18c246fc0adafb360939fe0"><td class="mdescLeft">&#160;</td><td class="mdescRight">Symbolically Execute a Program with Gradient Descent Optimization.  <a href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">More...</a><br /></td></tr>
-<tr class="separator:a8aa21505f18c246fc0adafb360939fe0"><td class="memSeparator" colspan="2">&#160;</td></tr>
+<tr class="memitem:aa13abbc332896d34bc320950bdacfdf9"><td class="memItemLeft" align="right" valign="top"><a class="el" href="structgymbo_1_1Trace.html">Trace</a>&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">run_gymbo</a> (<a class="el" href="namespacegymbo.html#a9b6a88c2be45a5e3fd3f053681f89733">Prog</a> &amp;prog, <a class="el" href="structgymbo_1_1GDOptimizer.html">GDOptimizer</a> &amp;optimizer, <a class="el" href="structgymbo_1_1SymState.html">SymState</a> &amp;state, std::unordered_set&lt; int &gt; &amp;target_pcs, <a class="el" href="namespacegymbo.html#aea0120f1cdc1417f9b6b8480ac562389">PathConstraintsTable</a> &amp;constraints_cache, int maxDepth, int &amp;maxSAT, int &amp;maxUNSAT, int max_num_trials, bool ignore_memory, bool use_dpll, int verbose_level, bool return_trace=false)</td></tr>
+<tr class="memdesc:aa13abbc332896d34bc320950bdacfdf9"><td class="mdescLeft">&#160;</td><td class="mdescRight">Symbolically Execute a Program with Gradient Descent Optimization.  <a href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">More...</a><br /></td></tr>
+<tr class="separator:aa13abbc332896d34bc320950bdacfdf9"><td class="memSeparator" colspan="2">&#160;</td></tr>
 <tr class="memitem:a70694fc6a91234300048503b2fe15a9b"><td class="memItemLeft" align="right" valign="top">void&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="namespacegymbo.html#a70694fc6a91234300048503b2fe15a9b">symStep</a> (<a class="el" href="structgymbo_1_1SymState.html">SymState</a> &amp;state, <a class="el" href="classgymbo_1_1Instr.html">Instr</a> instr, std::vector&lt; <a class="el" href="structgymbo_1_1SymState.html">SymState</a> &gt; &amp;result)</td></tr>
 <tr class="memdesc:a70694fc6a91234300048503b2fe15a9b"><td class="mdescLeft">&#160;</td><td class="mdescRight">Symbolically Execute a Single Instruction of a Program.  <a href="namespacegymbo.html#a70694fc6a91234300048503b2fe15a9b">More...</a><br /></td></tr>
 <tr class="separator:a70694fc6a91234300048503b2fe15a9b"><td class="memSeparator" colspan="2">&#160;</td></tr>
@@ -1890,8 +1890,8 @@ <h2 class="memtitle"><span class="permalink"><a href="#a7782376e331d91dd967f5a7b
 
 </div>
 </div>
-<a id="a8aa21505f18c246fc0adafb360939fe0"></a>
-<h2 class="memtitle"><span class="permalink"><a href="#a8aa21505f18c246fc0adafb360939fe0">&#9670;&nbsp;</a></span>run_gymbo()</h2>
+<a id="aa13abbc332896d34bc320950bdacfdf9"></a>
+<h2 class="memtitle"><span class="permalink"><a href="#aa13abbc332896d34bc320950bdacfdf9">&#9670;&nbsp;</a></span>run_gymbo()</h2>
 
 <div class="memitem">
 <div class="memproto">
@@ -1969,7 +1969,13 @@ <h2 class="memtitle"><span class="permalink"><a href="#a8aa21505f18c246fc0adafb3
           <td class="paramkey"></td>
           <td></td>
           <td class="paramtype">int&#160;</td>
-          <td class="paramname"><em>verbose_level</em>&#160;</td>
+          <td class="paramname"><em>verbose_level</em>, </td>
+        </tr>
+        <tr>
+          <td class="paramkey"></td>
+          <td></td>
+          <td class="paramtype">bool&#160;</td>
+          <td class="paramname"><em>return_trace</em> = <code>false</code>&#160;</td>
         </tr>
         <tr>
           <td></td>
@@ -2000,6 +2006,7 @@ <h2 class="memtitle"><span class="permalink"><a href="#a8aa21505f18c246fc0adafb3
     <tr><td class="paramname">ignore_memory</td><td>If set to true, constraints derived from memory will be ignored. </td></tr>
     <tr><td class="paramname">use_dpll</td><td>If set to true, use DPLL to decide the initial assignment for each term. </td></tr>
     <tr><td class="paramname">verbose_level</td><td>The level of verbosity. </td></tr>
+    <tr><td class="paramname">return_trace</td><td>If set to true, save the trace at each pc and return them (default false). </td></tr>
   </table>
   </dd>
 </dl>

diff --git a/docs/namespacemembers.html b/docs/namespacemembers.html
@@ -300,7 +300,7 @@ <h3><a id="index_r"></a>- r -</h3><ul>
 : <a class="el" href="namespacegymbo.html#a7782376e331d91dd967f5a7b1c23c1ba">gymbo</a>
 </li>
 <li>run_gymbo()
-: <a class="el" href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">gymbo</a>
+: <a class="el" href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">gymbo</a>
 </li>
 </ul>
 

diff --git a/docs/namespacemembers_func.html b/docs/namespacemembers_func.html
@@ -200,7 +200,7 @@ <h3><a id="index_r"></a>- r -</h3><ul>
 : <a class="el" href="namespacegymbo.html#a7782376e331d91dd967f5a7b1c23c1ba">gymbo</a>
 </li>
 <li>run_gymbo()
-: <a class="el" href="namespacegymbo.html#a8aa21505f18c246fc0adafb360939fe0">gymbo</a>
+: <a class="el" href="namespacegymbo.html#aa13abbc332896d34bc320950bdacfdf9">gymbo</a>
 </li>
 </ul>