-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ 5df1914 🚀
- Loading branch information
1 parent
1543a28
commit 2ce2790
Showing
9,416 changed files
with
943,678 additions
and
1,131 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,167 @@ | ||
<!-- HTML header for doxygen 1.9.1--> | ||
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> | ||
<html xmlns="http://www.w3.org/1999/xhtml"> | ||
<head> | ||
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/> | ||
<meta http-equiv="X-UA-Compatible" content="IE=9"/> | ||
<meta name="generator" content="Doxygen 1.9.1"/> | ||
<meta name="viewport" content="width=device-width, initial-scale=1"/> | ||
<title>P4C: /home/runner/work/P4c-Documentation-Hosting/P4c-Documentation-Hosting/backends/p4tools/modules/testgen/test/z3-solver/accessor.h Source File</title> | ||
<link href="tabs.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="jquery.js"></script> | ||
<script type="text/javascript" src="dynsections.js"></script> | ||
<link href="navtree.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="resize.js"></script> | ||
<script type="text/javascript" src="navtreedata.js"></script> | ||
<script type="text/javascript" src="navtree.js"></script> | ||
<link href="search/search.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="search/searchdata.js"></script> | ||
<script type="text/javascript" src="search/search.js"></script> | ||
<link href="doxygen.css" rel="stylesheet" type="text/css" /> | ||
<link href="doxygen-awesome.css" rel="stylesheet" type="text/css"/> | ||
<!-- DARK MODE BUTTON --> | ||
<script type="text/javascript" src="doxygen-awesome-darkmode-toggle.js"></script> | ||
<!-- CODE COPY BUTTON --> | ||
<script type="text/javascript" src="doxygen-awesome-fragment-copy-button.js"></script> | ||
<!-- link PARAGRAPH --> | ||
<script type="text/javascript" src="doxygen-awesome-paragraph-link.js"></script> | ||
<!--TABLE OF CONTENT --> | ||
<script type="text/javascript" src="doxygen-awesome-interactive-toc.js"></script> | ||
<script type="text/javascript"> | ||
DoxygenAwesomeInteractiveToc.init() | ||
DoxygenAwesomeParagraphLink.init() | ||
DoxygenAwesomeFragmentCopyButton.init() | ||
DoxygenAwesomeDarkModeToggle.init() | ||
</script> | ||
</head> | ||
<body> | ||
<div id="top"><!-- do not remove this div, it is closed by doxygen! --> | ||
<div id="titlearea"> | ||
<table cellspacing="0" cellpadding="0"> | ||
<tbody> | ||
<tr style="height: 56px;"> | ||
<td id="projectlogo"><img alt="Logo" src="p4-logo2.png"/></td> | ||
<td id="projectalign" style="padding-left: 0.5em;"> | ||
<div id="projectname">P4C | ||
</div> | ||
<div id="projectbrief">The P4 Compiler</div> | ||
</td> | ||
</tr> | ||
</tbody> | ||
</table> | ||
</div> | ||
<!-- end header part --> | ||
<!-- Generated by Doxygen 1.9.1 --> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
var searchBox = new SearchBox("searchBox", "search",false,'Search','.html'); | ||
/* @license-end */ | ||
</script> | ||
<script type="text/javascript" src="menudata.js"></script> | ||
<script type="text/javascript" src="menu.js"></script> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
$(function() { | ||
initMenu('',true,false,'search.php','Search'); | ||
$(document).ready(function() { init_search(); }); | ||
}); | ||
/* @license-end */</script> | ||
<div id="main-nav"></div> | ||
</div><!-- top --> | ||
<div id="side-nav" class="ui-resizable side-nav-resizable"> | ||
<div id="nav-tree"> | ||
<div id="nav-tree-contents"> | ||
<div id="nav-sync" class="sync"></div> | ||
</div> | ||
</div> | ||
<div id="splitbar" style="-moz-user-select:none;" | ||
class="ui-resizable-handle"> | ||
</div> | ||
</div> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
$(document).ready(function(){initNavTree('accessor_8h_source.html',''); initResizable(); }); | ||
/* @license-end */ | ||
</script> | ||
<div id="doc-content"> | ||
<!-- window showing the filter options --> | ||
<div id="MSearchSelectWindow" | ||
onmouseover="return searchBox.OnSearchSelectShow()" | ||
onmouseout="return searchBox.OnSearchSelectHide()" | ||
onkeydown="return searchBox.OnSearchSelectKey(event)"> | ||
</div> | ||
|
||
<!-- iframe showing the search results (closed by default) --> | ||
<div id="MSearchResultsWindow"> | ||
<iframe src="javascript:void(0)" frameborder="0" | ||
name="MSearchResults" id="MSearchResults"> | ||
</iframe> | ||
</div> | ||
|
||
<div class="header"> | ||
<div class="headertitle"> | ||
<div class="title">accessor.h</div> </div> | ||
</div><!--header--> | ||
<div class="contents"> | ||
<div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="preprocessor">#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_</span></div> | ||
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="preprocessor">#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_</span></div> | ||
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span>  </div> | ||
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="preprocessor">#include <vector></span></div> | ||
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span>  </div> | ||
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="preprocessor">#include "backends/p4tools/common/core/z3_solver.h"</span></div> | ||
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span>  </div> | ||
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="keyword">namespace </span><a class="code" href="namespace_p4_tools.html">P4Tools</a> {</div> | ||
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span>  </div> | ||
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment">// The main class for access to a private members</span></div> | ||
<div class="line"><a name="l00011"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html"> 11</a></span> <span class="keyword">class </span><a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html">Z3SolverAccessor</a> {</div> | ||
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span>  <span class="keyword">public</span>:</div> | ||
<div class="line"><a name="l00014"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html#aec5ffd4296c1a8ae9ef24ed0ee3897cd"> 14</a></span>  <span class="keyword">explicit</span> <a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html#aec5ffd4296c1a8ae9ef24ed0ee3897cd">Z3SolverAccessor</a>(<a class="code" href="class_p4_tools_1_1_z3_solver.html">Z3Solver</a> &solver) : solver(solver) {}</div> | ||
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span>  </div> | ||
<div class="line"><a name="l00017"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html#a559c4f32f70ec2aaff732a1a4963f66a"> 17</a></span>  z3::expr_vector <a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html#a559c4f32f70ec2aaff732a1a4963f66a">getAssertions</a>(std::optional<bool> assertionType = std::nullopt) {</div> | ||
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span>  <span class="keywordflow">if</span> (!assertionType) {</div> | ||
<div class="line"><a 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 name="l00020"></a><span class="lineno"> 20</span>  }</div> | ||
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span>  <span class="keywordflow">if</span> (assertionType.value()) {</div> | ||
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span>  <span class="keywordflow">return</span> solver.z3solver.assertions();</div> | ||
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span>  }</div> | ||
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span>  <span class="keywordflow">return</span> solver.z3Assertions;</div> | ||
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span>  }</div> | ||
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span>  </div> | ||
<div class="line"><a name="l00028"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html#af0c48784be3117d564e4c120277715c4"> 28</a></span>  <a class="code" href="classsafe__vector.html">safe_vector<const Constraint *></a> <a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html#af0c48784be3117d564e4c120277715c4">getP4Assertions</a>() { <span class="keywordflow">return</span> solver.p4Assertions; }</div> | ||
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span>  </div> | ||
<div class="line"><a name="l00031"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html#a3ba609111c692a23091507f10ab4b766"> 31</a></span>  <span class="keyword">const</span> z3::context &<a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html#a3ba609111c692a23091507f10ab4b766">getContext</a>() { <span class="keywordflow">return</span> solver.<a class="code" href="class_p4_tools_1_1_z3_solver.html#a658ecbd58127afa1013df70549e31b27">getZ3Ctx</a>(); }</div> | ||
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span>  </div> | ||
<div class="line"><a name="l00034"></a><span class="lineno"><a class="line" href="class_p4_tools_1_1_z3_solver_accessor.html#ac4955496c26ea5cc35f7a2ab90b8756f"> 34</a></span>  std::vector<size_t> &<a class="code" href="class_p4_tools_1_1_z3_solver_accessor.html#ac4955496c26ea5cc35f7a2ab90b8756f">getCheckpoints</a>() { <span class="keywordflow">return</span> solver.checkpoints; }</div> | ||
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span>  </div> | ||
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span>  <span class="keyword">private</span>:</div> | ||
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span>  <a class="code" href="class_p4_tools_1_1_z3_solver.html">Z3Solver</a> &solver;</div> | ||
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> };</div> | ||
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span>  </div> | ||
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> } <span class="comment">// namespace P4Tools</span></div> | ||
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span>  </div> | ||
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="preprocessor">#endif </span><span class="comment">/* BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_ */</span><span class="preprocessor"></span></div> | ||
<div class="ttc" id="aclass_p4_tools_1_1_z3_solver_accessor_html"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html">P4Tools::Z3SolverAccessor</a></div><div class="ttdef"><b>Definition:</b> accessor.h:11</div></div> | ||
<div class="ttc" id="aclass_p4_tools_1_1_z3_solver_accessor_html_a3ba609111c692a23091507f10ab4b766"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html#a3ba609111c692a23091507f10ab4b766">P4Tools::Z3SolverAccessor::getContext</a></div><div class="ttdeci">const z3::context & getContext()</div><div class="ttdoc">Get Z3 context. Used by GTests only.</div><div class="ttdef"><b>Definition:</b> accessor.h:31</div></div> | ||
<div class="ttc" id="aclass_p4_tools_1_1_z3_solver_accessor_html_a559c4f32f70ec2aaff732a1a4963f66a"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html#a559c4f32f70ec2aaff732a1a4963f66a">P4Tools::Z3SolverAccessor::getAssertions</a></div><div class="ttdeci">z3::expr_vector getAssertions(std::optional< bool > assertionType=std::nullopt)</div><div class="ttdoc">Gets all assertions. Used by GTests only.</div><div class="ttdef"><b>Definition:</b> accessor.h:17</div></div> | ||
<div class="ttc" id="aclass_p4_tools_1_1_z3_solver_accessor_html_ac4955496c26ea5cc35f7a2ab90b8756f"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html#ac4955496c26ea5cc35f7a2ab90b8756f">P4Tools::Z3SolverAccessor::getCheckpoints</a></div><div class="ttdeci">std::vector< size_t > & getCheckpoints()</div><div class="ttdoc">Gets checkpoints that have been made. Used by GTests only.</div><div class="ttdef"><b>Definition:</b> accessor.h:34</div></div> | ||
<div class="ttc" id="aclass_p4_tools_1_1_z3_solver_accessor_html_aec5ffd4296c1a8ae9ef24ed0ee3897cd"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html#aec5ffd4296c1a8ae9ef24ed0ee3897cd">P4Tools::Z3SolverAccessor::Z3SolverAccessor</a></div><div class="ttdeci">Z3SolverAccessor(Z3Solver &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_tools_1_1_z3_solver_accessor_html_af0c48784be3117d564e4c120277715c4"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver_accessor.html#af0c48784be3117d564e4c120277715c4">P4Tools::Z3SolverAccessor::getP4Assertions</a></div><div class="ttdeci">safe_vector< const Constraint * > 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_tools_1_1_z3_solver_html"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver.html">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_tools_1_1_z3_solver_html_a658ecbd58127afa1013df70549e31b27"><div class="ttname"><a href="class_p4_tools_1_1_z3_solver.html#a658ecbd58127afa1013df70549e31b27">P4Tools::Z3Solver::getZ3Ctx</a></div><div class="ttdeci">const z3::context & 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:340</div></div> | ||
<div class="ttc" id="aclasssafe__vector_html"><div class="ttname"><a href="classsafe__vector.html">safe_vector< const Constraint * ></a></div></div> | ||
<div class="ttc" id="anamespace_p4_tools_html"><div class="ttname"><a href="namespace_p4_tools.html">P4Tools</a></div><div class="ttdef"><b>Definition:</b> compiler_target.cpp:19</div></div> | ||
</div><!-- fragment --></div><!-- contents --> | ||
</div><!-- doc-content --> | ||
<!-- HTML footer for doxygen 1.8.12--> | ||
<!-- start footer part --> | ||
<div id="nav-path" class="navpath"><!-- id is needed for treeview function! --> | ||
<ul> | ||
<li class="navelem"><a class="el" href="dir_dec21994cd756836ecefab773235960a.html">backends</a></li><li class="navelem"><a class="el" href="dir_1841efd42c9265a4a72e4d07d8561569.html">p4tools</a></li><li class="navelem"><a class="el" href="dir_741b27cf8f7bebc8151bbfef823d7c1d.html">modules</a></li><li class="navelem"><a class="el" href="dir_83a8e6017e6647ab2aa86dac60c1c317.html">testgen</a></li><li class="navelem"><a class="el" href="dir_1853de99ada774e8fbdf5bc39f5620bf.html">test</a></li><li class="navelem"><a class="el" href="dir_e7078a92dbccbf2d34725a0bb9335f72.html">z3-solver</a></li><li class="navelem"><b>accessor.h</b></li> | ||
<li class="footer">Generated on Sat May 11 2024 for | ||
<a href="http://p4.org/spec"> | ||
<!-- <img class="footer" src="p4-logo2.png" alt="P4 Org" /></a></li> --> | ||
P4 Organization</a></li> | ||
</ul> | ||
</div> | ||
</body> | ||
</html> |
Oops, something went wrong.