Deploying to gh-pages from @ 7629097 🚀

pr-preview/4919/accessor_8h_source.html

@@ -136,28 +136,28 @@
 <div class="foldopen" id="foldopen00011" data-start="{" data-end="};">
 <div class="line"><a id="l00011" name="l00011"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html">   11</a></span><span class="keyword">class </span><a class="code hl_class" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html">Z3SolverAccessor</a> {</div>
 <div class="line"><a id="l00012" name="l00012"></a><span class="lineno">   12</span> <span class="keyword">public</span>:</div>
-<div class="line"><a id="l00014" name="l00014"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#aad67aa50f0b1cda205a6c653d5db551a">   14</a></span>    <span class="keyword">explicit</span> <a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#aad67aa50f0b1cda205a6c653d5db551a">Z3SolverAccessor</a>(<a class="code hl_class" href="class_p4_1_1_p4_tools_1_1_z3_solver.html">Z3Solver</a> &amp;solver) : solver(solver) {}</div>
+<div class="line"><a id="l00014" name="l00014"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#aad67aa50f0b1cda205a6c653d5db551a">   14</a></span>    <span class="keyword">explicit</span> <a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#aad67aa50f0b1cda205a6c653d5db551a">Z3SolverAccessor</a>(<a class="code hl_class" href="class_p4_1_1_p4_tools_1_1_z3_solver.html">Z3Solver</a> &amp;<a class="code hl_namespace" href="namespacesolver.html">solver</a>) : <a class="code hl_namespace" href="namespacesolver.html">solver</a>(<a class="code hl_namespace" href="namespacesolver.html">solver</a>) {}</div>
 <div class="line"><a id="l00015" name="l00015"></a><span class="lineno">   15</span> </div>
 <div class="foldopen" id="foldopen00017" data-start="{" data-end="}">
 <div class="line"><a id="l00017" name="l00017"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a1e85bc456750a2bc7b7eb71c5b78c0ab">   17</a></span>    z3::expr_vector <a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a1e85bc456750a2bc7b7eb71c5b78c0ab">getAssertions</a>(std::optional&lt;bool&gt; assertionType = std::nullopt) {</div>
 <div class="line"><a id="l00018" name="l00018"></a><span class="lineno">   18</span>        <span class="keywordflow">if</span> (!assertionType) {</div>
-<div class="line"><a id="l00019" name="l00019"></a><span class="lineno">   19</span>            <span class="keywordflow">return</span> solver.isIncremental ? solver.z3solver.assertions() : solver.z3Assertions;</div>
+<div class="line"><a id="l00019" name="l00019"></a><span class="lineno">   19</span>            <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.isIncremental ? <a class="code hl_namespace" href="namespacesolver.html">solver</a>.z3solver.assertions() : <a class="code hl_namespace" href="namespacesolver.html">solver</a>.z3Assertions;</div>
 <div class="line"><a id="l00020" name="l00020"></a><span class="lineno">   20</span>        }</div>
 <div class="line"><a id="l00021" name="l00021"></a><span class="lineno">   21</span>        <span class="keywordflow">if</span> (assertionType.value()) {</div>
-<div class="line"><a id="l00022" name="l00022"></a><span class="lineno">   22</span>            <span class="keywordflow">return</span> solver.z3solver.assertions();</div>
+<div class="line"><a id="l00022" name="l00022"></a><span class="lineno">   22</span>            <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.z3solver.assertions();</div>
 <div class="line"><a id="l00023" name="l00023"></a><span class="lineno">   23</span>        }</div>
-<div class="line"><a id="l00024" name="l00024"></a><span class="lineno">   24</span>        <span class="keywordflow">return</span> solver.z3Assertions;</div>
+<div class="line"><a id="l00024" name="l00024"></a><span class="lineno">   24</span>        <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.z3Assertions;</div>
 <div class="line"><a id="l00025" name="l00025"></a><span class="lineno">   25</span>    }</div>
 </div>
 <div class="line"><a id="l00026" name="l00026"></a><span class="lineno">   26</span> </div>
-<div class="line"><a id="l00028" name="l00028"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a94b2f94d637dd7ae83f60c629620bf0e">   28</a></span>    <a class="code hl_class" href="class_p4_1_1safe__vector.html">safe_vector&lt;const Constraint *&gt;</a> <a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a94b2f94d637dd7ae83f60c629620bf0e">getP4Assertions</a>() { <span class="keywordflow">return</span> solver.p4Assertions; }</div>
+<div class="line"><a id="l00028" name="l00028"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a94b2f94d637dd7ae83f60c629620bf0e">   28</a></span>    <a class="code hl_class" href="class_p4_1_1safe__vector.html">safe_vector&lt;const Constraint *&gt;</a> <a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a94b2f94d637dd7ae83f60c629620bf0e">getP4Assertions</a>() { <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.p4Assertions; }</div>
 <div class="line"><a id="l00029" name="l00029"></a><span class="lineno">   29</span> </div>
-<div class="line"><a id="l00031" name="l00031"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a4965364ef2d055ae00d94c7f1996cf63">   31</a></span>    <span class="keyword">const</span> z3::context &amp;<a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a4965364ef2d055ae00d94c7f1996cf63">getContext</a>() { <span class="keywordflow">return</span> solver.<a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver.html#af9600eb5e2ce02995b2678d3dd59598f">getZ3Ctx</a>(); }</div>
+<div class="line"><a id="l00031" name="l00031"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a4965364ef2d055ae00d94c7f1996cf63">   31</a></span>    <span class="keyword">const</span> z3::context &amp;<a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a4965364ef2d055ae00d94c7f1996cf63">getContext</a>() { <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.getZ3Ctx(); }</div>
 <div class="line"><a id="l00032" name="l00032"></a><span class="lineno">   32</span> </div>
-<div class="line"><a id="l00034" name="l00034"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a75d8ce158e882c61c9b8f5a119d3df64">   34</a></span>    std::vector&lt;size_t&gt; &amp;<a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a75d8ce158e882c61c9b8f5a119d3df64">getCheckpoints</a>() { <span class="keywordflow">return</span> solver.checkpoints; }</div>
+<div class="line"><a id="l00034" name="l00034"></a><span class="lineno"><a class="line" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a75d8ce158e882c61c9b8f5a119d3df64">   34</a></span>    std::vector&lt;size_t&gt; &amp;<a class="code hl_function" href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a75d8ce158e882c61c9b8f5a119d3df64">getCheckpoints</a>() { <span class="keywordflow">return</span> <a class="code hl_namespace" href="namespacesolver.html">solver</a>.checkpoints; }</div>
 <div class="line"><a id="l00035" name="l00035"></a><span class="lineno">   35</span> </div>
 <div class="line"><a id="l00036" name="l00036"></a><span class="lineno">   36</span> <span class="keyword">private</span>:</div>
-<div class="line"><a id="l00038" name="l00038"></a><span class="lineno">   38</span>    <a class="code hl_class" href="class_p4_1_1_p4_tools_1_1_z3_solver.html">Z3Solver</a> &amp;solver;</div>
+<div class="line"><a id="l00038" name="l00038"></a><span class="lineno">   38</span>    <a class="code hl_class" href="class_p4_1_1_p4_tools_1_1_z3_solver.html">Z3Solver</a> &amp;<a class="code hl_namespace" href="namespacesolver.html">solver</a>;</div>
 <div class="line"><a id="l00039" name="l00039"></a><span class="lineno">   39</span>};</div>
 </div>
 <div class="line"><a id="l00040" name="l00040"></a><span class="lineno">   40</span> </div>
@@ -171,9 +171,9 @@
 <div class="ttc" id="aclass_p4_1_1_p4_tools_1_1_z3_solver_accessor_html_a94b2f94d637dd7ae83f60c629620bf0e"><div class="ttname"><a href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#a94b2f94d637dd7ae83f60c629620bf0e">P4::P4Tools::Z3SolverAccessor::getP4Assertions</a></div><div class="ttdeci">safe_vector&lt; const Constraint * &gt; getP4Assertions()</div><div class="ttdoc">Gets all P4 assertions. Used by GTests only.</div><div class="ttdef"><b>Definition</b> accessor.h:28</div></div>
 <div class="ttc" id="aclass_p4_1_1_p4_tools_1_1_z3_solver_accessor_html_aad67aa50f0b1cda205a6c653d5db551a"><div class="ttname"><a href="class_p4_1_1_p4_tools_1_1_z3_solver_accessor.html#aad67aa50f0b1cda205a6c653d5db551a">P4::P4Tools::Z3SolverAccessor::Z3SolverAccessor</a></div><div class="ttdeci">Z3SolverAccessor(Z3Solver &amp;solver)</div><div class="ttdoc">Default constructor.</div><div class="ttdef"><b>Definition</b> accessor.h:14</div></div>
 <div class="ttc" id="aclass_p4_1_1_p4_tools_1_1_z3_solver_html"><div class="ttname"><a href="class_p4_1_1_p4_tools_1_1_z3_solver.html">P4::P4Tools::Z3Solver</a></div><div class="ttdoc">A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context.</div><div class="ttdef"><b>Definition</b> z3_solver.h:28</div></div>
-<div class="ttc" id="aclass_p4_1_1_p4_tools_1_1_z3_solver_html_af9600eb5e2ce02995b2678d3dd59598f"><div class="ttname"><a href="class_p4_1_1_p4_tools_1_1_z3_solver.html#af9600eb5e2ce02995b2678d3dd59598f">P4::P4Tools::Z3Solver::getZ3Ctx</a></div><div class="ttdeci">const z3::context &amp; getZ3Ctx() const</div><div class="ttdoc">Get the actual Z3 context that this class uses.</div><div class="ttdef"><b>Definition</b> z3_solver.cpp:332</div></div>
 <div class="ttc" id="aclass_p4_1_1safe__vector_html"><div class="ttname"><a href="class_p4_1_1safe__vector.html">P4::safe_vector</a></div><div class="ttdef"><b>Definition</b> safe_vector.h:27</div></div>
 <div class="ttc" id="anamespace_p4_1_1_p4_tools_html"><div class="ttname"><a href="namespace_p4_1_1_p4_tools.html">P4::P4Tools</a></div><div class="ttdef"><b>Definition</b> common/compiler/compiler_result.cpp:3</div></div>
+<div class="ttc" id="anamespacesolver_html"><div class="ttname"><a href="namespacesolver.html">solver</a></div><div class="ttdef"><b>Definition</b> phv/solver/action_constraint_solver.cpp:33</div></div>
 </div><!-- fragment --></div><!-- contents -->
 </div><!-- doc-content -->
 <!-- HTML footer for doxygen 1.12.0-->

pr-preview/4919/action_8h_source.html

@@ -169,12 +169,12 @@
 <div class="line"><a id="l00042" name="l00042"></a><span class="lineno">   42</span> </div>
 <div class="line"><a id="l00043" name="l00043"></a><span class="lineno">   43</span><span class="preprocessor">#endif </span><span class="comment">/* BACKENDS_BMV2_COMMON_ACTION_H_ */</span><span class="preprocessor"></span></div>
 <div class="ttc" id="aclass_p4_1_1_b_m_v2_1_1_action_converter_html"><div class="ttname"><a href="class_p4_1_1_b_m_v2_1_1_action_converter.html">P4::BMV2::ActionConverter</a></div><div class="ttdef"><b>Definition</b> action.h:25</div></div>
-<div class="ttc" id="aclass_p4_1_1_i_r_1_1_vector_html"><div class="ttname"><a href="class_p4_1_1_i_r_1_1_vector.html">P4::IR::Vector</a></div><div class="ttdef"><b>Definition</b> vector.h:58</div></div>
+<div class="ttc" id="aclass_p4_1_1_i_r_1_1_vector_html"><div class="ttname"><a href="class_p4_1_1_i_r_1_1_vector.html">P4::IR::Vector</a></div><div class="ttdef"><b>Definition</b> vector.h:59</div></div>
 <div class="ttc" id="aclass_p4_1_1_inspector_html"><div class="ttname"><a href="class_p4_1_1_inspector.html">P4::Inspector</a></div><div class="ttdef"><b>Definition</b> visitor.h:400</div></div>
 <div class="ttc" id="aclass_p4_1_1_util_1_1_json_array_html"><div class="ttname"><a href="class_p4_1_1_util_1_1_json_array.html">P4::Util::JsonArray</a></div><div class="ttdef"><b>Definition</b> json.h:115</div></div>
 <div class="ttc" id="aclass_p4_1_1cstring_html"><div class="ttname"><a href="class_p4_1_1cstring.html">P4::cstring</a></div><div class="ttdef"><b>Definition</b> cstring.h:85</div></div>
 <div class="ttc" id="anamespace_p4_1_1_b_m_v2_html"><div class="ttname"><a href="namespace_p4_1_1_b_m_v2.html">P4::BMV2</a></div><div class="ttdoc">TODO: this is not really specific to BMV2, it should reside somewhere else.</div><div class="ttdef"><b>Definition</b> action.cpp:21</div></div>
-<div class="ttc" id="astruct_p4_1_1_b_m_v2_1_1_conversion_context_html"><div class="ttname"><a href="struct_p4_1_1_b_m_v2_1_1_conversion_context.html">P4::BMV2::ConversionContext</a></div><div class="ttdef"><b>Definition</b> helpers.h:297</div></div>
+<div class="ttc" id="astruct_p4_1_1_b_m_v2_1_1_conversion_context_html"><div class="ttname"><a href="struct_p4_1_1_b_m_v2_1_1_conversion_context.html">P4::BMV2::ConversionContext</a></div><div class="ttdef"><b>Definition</b> bmv2/common/helpers.h:297</div></div>
 </div><!-- fragment --></div><!-- contents -->
 </div><!-- doc-content -->
 <!-- HTML footer for doxygen 1.12.0-->