<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://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"/>
<title>CVC3: xchaff_solver.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">xchaff_solver.h</div> </div>
</div>
<div class="contents">
<a href="xchaff__solver_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */</span>
<a name="l00002"></a>00002
<a name="l00003"></a>00003 <span class="comment">/*********************************************************************</span>
<a name="l00004"></a>00004 <span class="comment"> Copyright 2000-2001, Princeton University. All rights reserved.</span>
<a name="l00005"></a>00005 <span class="comment"> By using this software the USER indicates that he or she has read,</span>
<a name="l00006"></a>00006 <span class="comment"> understood and will comply with the following:</span>
<a name="l00007"></a>00007 <span class="comment"></span>
<a name="l00008"></a>00008 <span class="comment"> --- Princeton University hereby grants USER nonexclusive permission</span>
<a name="l00009"></a>00009 <span class="comment"> to use, copy and/or modify this software for internal, noncommercial,</span>
<a name="l00010"></a>00010 <span class="comment"> research purposes only. Any distribution, including commercial sale</span>
<a name="l00011"></a>00011 <span class="comment"> or license, of this software, copies of the software, its associated</span>
<a name="l00012"></a>00012 <span class="comment"> documentation and/or modifications of either is strictly prohibited</span>
<a name="l00013"></a>00013 <span class="comment"> without the prior consent of Princeton University. Title to copyright</span>
<a name="l00014"></a>00014 <span class="comment"> to this software and its associated documentation shall at all times</span>
<a name="l00015"></a>00015 <span class="comment"> remain with Princeton University. Appropriate copyright notice shall</span>
<a name="l00016"></a>00016 <span class="comment"> be placed on all software copies, and a complete copy of this notice</span>
<a name="l00017"></a>00017 <span class="comment"> shall be included in all copies of the associated documentation.</span>
<a name="l00018"></a>00018 <span class="comment"> No right is granted to use in advertising, publicity or otherwise</span>
<a name="l00019"></a>00019 <span class="comment"> any trademark, service mark, or the name of Princeton University.</span>
<a name="l00020"></a>00020 <span class="comment"></span>
<a name="l00021"></a>00021 <span class="comment"></span>
<a name="l00022"></a>00022 <span class="comment"> --- This software and any associated documentation is provided "as is"</span>
<a name="l00023"></a>00023 <span class="comment"></span>
<a name="l00024"></a>00024 <span class="comment"> PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS</span>
<a name="l00025"></a>00025 <span class="comment"> OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A</span>
<a name="l00026"></a>00026 <span class="comment"> PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR</span>
<a name="l00027"></a>00027 <span class="comment"> ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,</span>
<a name="l00028"></a>00028 <span class="comment"> TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.</span>
<a name="l00029"></a>00029 <span class="comment"></span>
<a name="l00030"></a>00030 <span class="comment"> Princeton University shall not be liable under any circumstances for</span>
<a name="l00031"></a>00031 <span class="comment"> any direct, indirect, special, incidental, or consequential damages</span>
<a name="l00032"></a>00032 <span class="comment"> with respect to any claim by USER or any third party on account of</span>
<a name="l00033"></a>00033 <span class="comment"> or arising from the use, or inability to use, this software or its</span>
<a name="l00034"></a>00034 <span class="comment"> associated documentation, even if Princeton University has been advised</span>
<a name="l00035"></a>00035 <span class="comment"> of the possibility of those damages.</span>
<a name="l00036"></a>00036 <span class="comment">*********************************************************************/</span>
<a name="l00037"></a>00037
<a name="l00038"></a>00038
<a name="l00039"></a>00039
<a name="l00040"></a>00040 <span class="preprocessor">#ifndef __SAT_SOLVER__</span>
<a name="l00041"></a>00041 <span class="preprocessor"></span><span class="preprocessor">#define __SAT_SOLVER__</span>
<a name="l00042"></a>00042 <span class="preprocessor"></span>
<a name="l00043"></a>00043 <span class="preprocessor">#include <sys/time.h></span>
<a name="l00044"></a>00044 <span class="preprocessor">#include <sys/resource.h></span>
<a name="l00045"></a>00045 <span class="preprocessor">#include <stdlib.h></span>
<a name="l00046"></a>00046
<a name="l00047"></a>00047 <span class="preprocessor">#include "<a class="code" href="xchaff__utils_8h.html">xchaff_utils.h</a>"</span>
<a name="l00048"></a>00048 <span class="preprocessor">#include "<a class="code" href="xchaff__dbase_8h.html">xchaff_dbase.h</a>"</span>
<a name="l00049"></a>00049
<a name="l00050"></a>00050 <span class="preprocessor">#ifndef __SAT_STATUS__</span>
<a name="l00051"></a><a class="code" href="xchaff__solver_8h.html#aae57d20f93eb1c7fc0d595c26a61a0ec">00051</a> <span class="preprocessor"></span><span class="preprocessor">#define __SAT_STATUS__</span>
<a name="l00052"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87b">00052</a> <span class="preprocessor"></span><span class="keyword">enum</span> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87b">SAT_StatusT</a> {
<a name="l00053"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baf6adbbdb69d80588184f30a38895b43e">00053</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baf6adbbdb69d80588184f30a38895b43e">UNDETERMINED</a>,
<a name="l00054"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">00054</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>,
<a name="l00055"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baa6a5c07f8c320f440ebc34fed65eb550">00055</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baa6a5c07f8c320f440ebc34fed65eb550">SATISFIABLE</a>,
<a name="l00056"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba52acca9974adc722d8bdd782fec68b55">00056</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba52acca9974adc722d8bdd782fec68b55">TIME_OUT</a>,
<a name="l00057"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baff91e7382744a3692b5e8b812c24f9dd">00057</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baff91e7382744a3692b5e8b812c24f9dd">MEM_OUT</a>,
<a name="l00058"></a><a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba3ae09818606786b529d9ca89180fa29a">00058</a> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba3ae09818606786b529d9ca89180fa29a">ABORTED</a>
<a name="l00059"></a>00059 };
<a name="l00060"></a>00060 <span class="preprocessor">#endif</span>
<a name="l00061"></a>00061 <span class="preprocessor"></span>
<a name="l00062"></a><a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25">00062</a> <span class="keyword">enum</span> <a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25">SAT_DeductionT</a> {
<a name="l00063"></a><a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">00063</a> <a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>,
<a name="l00064"></a><a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a7980b2b643aebe4041a43b90e652c3fc">00064</a> <a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a7980b2b643aebe4041a43b90e652c3fc">NO_CONFLICT</a>
<a name="l00065"></a>00065 };
<a name="l00066"></a>00066
<a name="l00067"></a><a class="code" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">00067</a> <span class="keyword">typedef</span> void(*<a class="code" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a>)(<span class="keywordtype">void</span> *) ;<span class="comment"></span>
<a name="l00068"></a>00068 <span class="comment">/**Struct**********************************************************************</span>
<a name="l00069"></a>00069 <span class="comment"></span>
<a name="l00070"></a>00070 <span class="comment"> Synopsis [Sat solver parameters ]</span>
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> Description []</span>
<a name="l00073"></a>00073 <span class="comment"></span>
<a name="l00074"></a>00074 <span class="comment"> SeeAlso []</span>
<a name="l00075"></a>00075 <span class="comment"></span>
<a name="l00076"></a>00076 <span class="comment">******************************************************************************/</span>
<a name="l00077"></a><a class="code" href="structCSolverParameters.html">00077</a> <span class="keyword">struct </span><a class="code" href="structCSolverParameters.html">CSolverParameters</a> {
<a name="l00078"></a><a class="code" href="structCSolverParameters.html#a1904f8790a16c706e0d2ba51ce11c364">00078</a> <span class="keywordtype">float</span> <a class="code" href="structCSolverParameters.html#a1904f8790a16c706e0d2ba51ce11c364">time_limit</a>;
<a name="l00079"></a>00079
<a name="l00080"></a><a class="code" href="structCSolverParameters.html#aa5fb349b73577a3b99014ca90ce34e55">00080</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#aa5fb349b73577a3b99014ca90ce34e55">decision_strategy</a>;
<a name="l00081"></a><a class="code" href="structCSolverParameters.html#a714385448e9041b135391f9548ed6efa">00081</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a714385448e9041b135391f9548ed6efa">preprocess_strategy</a>;
<a name="l00082"></a>00082
<a name="l00083"></a><a class="code" href="structCSolverParameters.html#aa4c80dc600b3dcd9f64ef0c602dd59da">00083</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverParameters.html#aa4c80dc600b3dcd9f64ef0c602dd59da">allow_clause_deletion</a>;
<a name="l00084"></a><a class="code" href="structCSolverParameters.html#a5cbdbad62f42fd6f41ba5a4ed6f40af6">00084</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a5cbdbad62f42fd6f41ba5a4ed6f40af6">clause_deletion_interval</a>;
<a name="l00085"></a><a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">00085</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a>;
<a name="l00086"></a><a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">00086</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a>;
<a name="l00087"></a><a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">00087</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a>;
<a name="l00088"></a><a class="code" href="structCSolverParameters.html#ae358e7fe29489f48a00c012fb02a3778">00088</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#ae358e7fe29489f48a00c012fb02a3778">bubble_init_step</a>;
<a name="l00089"></a>00089
<a name="l00090"></a><a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">00090</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a>;
<a name="l00091"></a><a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">00091</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a>;
<a name="l00092"></a>00092
<a name="l00093"></a><a class="code" href="structCSolverParameters.html#a0040f5ae79dd7e8a478f60f3d02b1a6d">00093</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverParameters.html#a0040f5ae79dd7e8a478f60f3d02b1a6d">allow_restart</a>;
<a name="l00094"></a><a class="code" href="structCSolverParameters.html#a4fec1add4989095c31fab9ec2a29f824">00094</a> <span class="keywordtype">float</span> <a class="code" href="structCSolverParameters.html#a4fec1add4989095c31fab9ec2a29f824">next_restart_time</a>;
<a name="l00095"></a><a class="code" href="structCSolverParameters.html#a22f43c87a3a8cdfdfd35bd400f3f0b59">00095</a> <span class="keywordtype">float</span> <a class="code" href="structCSolverParameters.html#a22f43c87a3a8cdfdfd35bd400f3f0b59">restart_time_increment</a>;
<a name="l00096"></a><a class="code" href="structCSolverParameters.html#a914448885e9e2aedefd743f6428552d8">00096</a> <span class="keywordtype">float</span> <a class="code" href="structCSolverParameters.html#a914448885e9e2aedefd743f6428552d8">restart_time_incr_incr</a>;
<a name="l00097"></a><a class="code" href="structCSolverParameters.html#ac1a694498478fc1c1e164e81881ea61f">00097</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#ac1a694498478fc1c1e164e81881ea61f">next_restart_backtrack</a>;
<a name="l00098"></a><a class="code" href="structCSolverParameters.html#a319ab0a9a6646af75828ff1a1f9a33b6">00098</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a319ab0a9a6646af75828ff1a1f9a33b6">restart_backtrack_incr</a>;
<a name="l00099"></a><a class="code" href="structCSolverParameters.html#a8b11bde6fb341437589e70a1b419d846">00099</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#a8b11bde6fb341437589e70a1b419d846">restart_backtrack_incr_incr</a>;
<a name="l00100"></a><a class="code" href="structCSolverParameters.html#ac22c8353981fed418be2df36b64e635e">00100</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#ac22c8353981fed418be2df36b64e635e">restart_randomness</a>;
<a name="l00101"></a><a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">00101</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">base_randomness</a>;
<a name="l00102"></a>00102
<a name="l00103"></a><a class="code" href="structCSolverParameters.html#a3e90abca92fa570f9d1dc5ce49b01daa">00103</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverParameters.html#a3e90abca92fa570f9d1dc5ce49b01daa">back_track_complete</a>;
<a name="l00104"></a><a class="code" href="structCSolverParameters.html#acb3ae3f751542d16fa162fbb4a9478b6">00104</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverParameters.html#acb3ae3f751542d16fa162fbb4a9478b6">conflict_analysis_method</a>;
<a name="l00105"></a><a class="code" href="structCSolverParameters.html#a4543f7d64cbab749e5e1998b83d1e1d2">00105</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverParameters.html#a4543f7d64cbab749e5e1998b83d1e1d2">allow_multiple_conflict</a>;
<a name="l00106"></a><a class="code" href="structCSolverParameters.html#a9d1be4fd22f1ee134702028a980c2d1b">00106</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverParameters.html#a9d1be4fd22f1ee134702028a980c2d1b">allow_multiple_conflict_clause</a>;
<a name="l00107"></a>00107 };<span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment">/**Struct**********************************************************************</span>
<a name="l00109"></a>00109 <span class="comment"></span>
<a name="l00110"></a>00110 <span class="comment"> Synopsis [Sat solver statistics ]</span>
<a name="l00111"></a>00111 <span class="comment"></span>
<a name="l00112"></a>00112 <span class="comment"> Description []</span>
<a name="l00113"></a>00113 <span class="comment"></span>
<a name="l00114"></a>00114 <span class="comment"> SeeAlso []</span>
<a name="l00115"></a>00115 <span class="comment"></span>
<a name="l00116"></a>00116 <span class="comment">******************************************************************************/</span>
<a name="l00117"></a><a class="code" href="structCSolverStats.html">00117</a> <span class="keyword">struct </span><a class="code" href="structCSolverStats.html">CSolverStats</a> {
<a name="l00118"></a><a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">00118</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a>;
<a name="l00119"></a><a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">00119</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a>;
<a name="l00120"></a>00120
<a name="l00121"></a><a class="code" href="structCSolverStats.html#ab5c8d00ed96f235136c96197230a09c7">00121</a> <span class="keywordtype">bool</span> <a class="code" href="structCSolverStats.html#ab5c8d00ed96f235136c96197230a09c7">is_mem_out</a>; <span class="comment">//this flag will be set if memory out</span>
<a name="l00122"></a>00122
<a name="l00123"></a><a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">00123</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a>;
<a name="l00124"></a><a class="code" href="structCSolverStats.html#a60bcfaf8308075781464cf18477fc3e4">00124</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#a60bcfaf8308075781464cf18477fc3e4">last_cpu_time</a>;
<a name="l00125"></a><a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">00125</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">finish_cpu_time</a>;
<a name="l00126"></a><a class="code" href="structCSolverStats.html#ab42200e7e324f1f59e4ae2452fa22c6f">00126</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#ab42200e7e324f1f59e4ae2452fa22c6f">start_world_time</a>;
<a name="l00127"></a><a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">00127</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">finish_world_time</a>;
<a name="l00128"></a>00128
<a name="l00129"></a><a class="code" href="structCSolverStats.html#a7adfa10784b5c1866e8e3ab08bf68da2">00129</a> <span class="keywordtype">long</span> <a class="code" href="structCSolverStats.html#a7adfa10784b5c1866e8e3ab08bf68da2">total_bubble_move</a>;
<a name="l00130"></a>00130
<a name="l00131"></a><a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">00131</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a>;
<a name="l00132"></a><a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">00132</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">num_backtracks</a>;
<a name="l00133"></a><a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">00133</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a>;
<a name="l00134"></a><a class="code" href="structCSolverStats.html#ae5581743416ca4828eb017c92a4e91a4">00134</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#ae5581743416ca4828eb017c92a4e91a4">num_implications</a>;
<a name="l00135"></a><a class="code" href="structCSolverStats.html#aaa0ec761ac703cd4d1ebd9446d1dcaf1">00135</a> <span class="keywordtype">int</span> <a class="code" href="structCSolverStats.html#aaa0ec761ac703cd4d1ebd9446d1dcaf1">num_free_variables</a>;
<a name="l00136"></a>00136 };
<a name="l00137"></a>00137 <span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment">/**Class**********************************************************************</span>
<a name="l00139"></a>00139 <span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> Synopsis [Sat Solver]</span>
<a name="l00141"></a>00141 <span class="comment"></span>
<a name="l00142"></a>00142 <span class="comment"> Description [This class contains the process and datastructrues to solve</span>
<a name="l00143"></a>00143 <span class="comment"> the Sat problem.]</span>
<a name="l00144"></a>00144 <span class="comment"></span>
<a name="l00145"></a>00145 <span class="comment"> SeeAlso []</span>
<a name="l00146"></a>00146 <span class="comment"></span>
<a name="l00147"></a>00147 <span class="comment">******************************************************************************/</span>
<a name="l00148"></a><a class="code" href="classCSolver.html">00148</a> <span class="keyword">class </span><a class="code" href="classCSolver.html">CSolver</a>:<span class="keyword">public</span> <a class="code" href="classCDatabase.html">CDatabase</a>
<a name="l00149"></a>00149 {
<a name="l00150"></a>00150 <span class="keyword">protected</span>:
<a name="l00151"></a><a class="code" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">00151</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a>; <span class="comment">//current decision elvel</span>
<a name="l00152"></a><a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">00152</a> vector<vector<int> *> <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>;
<a name="l00153"></a><a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">00153</a> queue<pair<int,ClauseIdx> > <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>;
<a name="l00154"></a><a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">00154</a> <a class="code" href="structCSolverParameters.html">CSolverParameters</a> <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>;
<a name="l00155"></a><a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">00155</a> <a class="code" href="structCSolverStats.html">CSolverStats</a> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>;
<a name="l00156"></a>00156
<a name="l00157"></a><a class="code" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">00157</a> vector<pair<int,pair< HookFunPtrT, int> > > <a class="code" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a>;
<a name="l00158"></a>00158
<a name="l00159"></a>00159 <span class="comment">//these are for decision making</span>
<a name="l00160"></a><a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">00160</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a>;
<a name="l00161"></a><a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">00161</a> vector<int> <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[2];
<a name="l00162"></a><a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">00162</a> vector<pair<int,int> ><a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>;
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="comment">//these are for conflict analysis</span>
<a name="l00165"></a><a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">00165</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a>; <span class="comment">//used when constructing conflict clauses</span>
<a name="l00166"></a><a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">00166</a> vector<ClauseIdx> <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>; <span class="comment">//the conflict clauses</span>
<a name="l00167"></a><a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">00167</a> vector<long> <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>; <span class="comment">//used when constructing conflict clauses</span>
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <span class="comment">//these are for the extended API</span>
<a name="l00170"></a><a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">00170</a> void (*<a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a>)(<span class="keywordtype">void</span> *, int);
<a name="l00171"></a><a class="code" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">00171</a> int (*<a class="code" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a>)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *);
<a name="l00172"></a><a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">00172</a> void (*<a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a>)(<span class="keywordtype">void</span> *, int, int);
<a name="l00173"></a><a class="code" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">00173</a> void (*<a class="code" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a>)(<span class="keywordtype">void</span> *);
<a name="l00174"></a><a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">00174</a> <span class="keywordtype">void</span> *<a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a>;
<a name="l00175"></a><a class="code" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">00175</a> <span class="keywordtype">void</span> *<a class="code" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a>;
<a name="l00176"></a><a class="code" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">00176</a> <span class="keywordtype">void</span> *<a class="code" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a>;
<a name="l00177"></a><a class="code" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">00177</a> <span class="keywordtype">void</span> *<a class="code" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a>;
<a name="l00178"></a>00178
<a name="l00179"></a>00179 <span class="comment">//needed to support dynamic adding of unit clauses</span>
<a name="l00180"></a><a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">00180</a> vector<ClauseIdx> <a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>;
<a name="l00181"></a>00181
<a name="l00182"></a>00182 <span class="keyword">protected</span>:
<a name="l00183"></a>00183 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a>(<span class="keywordtype">void</span>);
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">preprocess</a>(<span class="keywordtype">bool</span> allowNewClauses);
<a name="l00186"></a>00186
<a name="l00187"></a>00187 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a>(<span class="keywordtype">void</span>);
<a name="l00188"></a>00188
<a name="l00189"></a>00189 <span class="keywordtype">bool</span> <a class="code" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">decide_next_branch</a>(<span class="keywordtype">void</span>);
<a name="l00190"></a>00190
<a name="l00191"></a>00191 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">analyze_conflicts</a>(<span class="keywordtype">void</span>);
<a name="l00192"></a>00192 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a3bc2008b3318b4796cf2cd34fa446dee">conflict_analysis_grasp</a> (<span class="keywordtype">void</span>);
<a name="l00193"></a>00193 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">conflict_analysis_zchaff</a> (<span class="keywordtype">void</span>);
<a name="l00194"></a>00194
<a name="l00195"></a>00195 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a>(<span class="keywordtype">int</span> level);
<a name="l00196"></a>00196
<a name="l00197"></a>00197 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">init</a>(<span class="keywordtype">void</span>);
<a name="l00198"></a>00198 <span class="comment">//for conflict analysis</span>
<a name="l00199"></a>00199 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">mark_vars_at_level</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl,
<a name="l00200"></a>00200 <span class="keywordtype">int</span> var_idx,
<a name="l00201"></a>00201 <span class="keywordtype">int</span> dl);
<a name="l00202"></a>00202
<a name="l00203"></a>00203 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl); <span class="comment">//the max dlevel of all the assigned lits in this clause</span>
<a name="l00204"></a>00204
<a name="l00205"></a>00205 <span class="comment">//for bcp</span>
<a name="l00206"></a>00206 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">set_var_value</a>(<span class="keywordtype">int</span> var,
<a name="l00207"></a>00207 <span class="keywordtype">int</span> value,
<a name="l00208"></a>00208 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante,
<a name="l00209"></a>00209 <span class="keywordtype">int</span> dl);
<a name="l00210"></a>00210 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">set_var_value_not_current_dl</a>(<span class="keywordtype">int</span> v,
<a name="l00211"></a>00211 vector<CLitPoolElement *> & neg_ht_clauses);
<a name="l00212"></a>00212 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">set_var_value_with_current_dl</a>(<span class="keywordtype">int</span> v,
<a name="l00213"></a>00213 vector<CLitPoolElement*> & neg_ht_clauses);
<a name="l00214"></a>00214 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">unset_var_value</a>(<span class="keywordtype">int</span> var);
<a name="l00215"></a>00215
<a name="l00216"></a>00216 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">run_periodic_functions</a> (<span class="keywordtype">void</span>);
<a name="l00217"></a>00217 <span class="comment">//misc functions</span>
<a name="l00218"></a>00218 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a>(<span class="keywordtype">void</span>);
<a name="l00219"></a>00219
<a name="l00220"></a>00220 <span class="keywordtype">bool</span> <a class="code" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">time_out</a>(<span class="keywordtype">void</span>);
<a name="l00221"></a>00221
<a name="l00222"></a>00222 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">delete_unrelevant_clauses</a>(<span class="keywordtype">void</span>);
<a name="l00223"></a>00223 <span class="keyword">public</span>:
<a name="l00224"></a>00224 <span class="comment">//constructors and destructors</span>
<a name="l00225"></a>00225 <a class="code" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">CSolver</a>() ;
<a name="l00226"></a>00226 <a class="code" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">~CSolver</a>();
<a name="l00227"></a>00227 <span class="comment">//member access function</span>
<a name="l00228"></a><a class="code" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">00228</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a19c6655c87bd6117db6510183dad2893">set_time_limit</a>(<span class="keywordtype">float</span> t)
<a name="l00229"></a>00229 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a1904f8790a16c706e0d2ba51ce11c364">time_limit</a> = t; }
<a name="l00230"></a><a class="code" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">00230</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">set_mem_limit</a>(<span class="keywordtype">int</span> s) {
<a name="l00231"></a>00231 <a class="code" href="classCSolver.html#a069343e0391a7b95510634c9c96bb66f">CDatabase::set_mem_limit</a>(s);
<a name="l00232"></a>00232 }
<a name="l00233"></a><a class="code" href="classCSolver.html#adc4bf726c678250a85fef5a600d5e1d7">00233</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#adc4bf726c678250a85fef5a600d5e1d7">set_decision_strategy</a>(<span class="keywordtype">int</span> s)
<a name="l00234"></a>00234 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#aa5fb349b73577a3b99014ca90ce34e55">decision_strategy</a> = s; }
<a name="l00235"></a><a class="code" href="classCSolver.html#a771e7780c8a112317bfd437599e2af22">00235</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a771e7780c8a112317bfd437599e2af22">set_preprocess_strategy</a>(<span class="keywordtype">int</span> s)
<a name="l00236"></a>00236 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a714385448e9041b135391f9548ed6efa">preprocess_strategy</a> = s; }
<a name="l00237"></a><a class="code" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">00237</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ad61a4e50bc8640852b7cd9d2cbd423d0">enable_cls_deletion</a>(<span class="keywordtype">bool</span> allow)
<a name="l00238"></a>00238 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#aa4c80dc600b3dcd9f64ef0c602dd59da">allow_clause_deletion</a> = allow; }
<a name="l00239"></a><a class="code" href="classCSolver.html#a31f9c112bb7ee8b3b334618d847d3d1f">00239</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a31f9c112bb7ee8b3b334618d847d3d1f">set_cls_del_interval</a>(<span class="keywordtype">int</span> n)
<a name="l00240"></a>00240 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a5cbdbad62f42fd6f41ba5a4ed6f40af6">clause_deletion_interval</a> = n; }
<a name="l00241"></a><a class="code" href="classCSolver.html#a72cf182c0c2c1dccb61c837765ea56f3">00241</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a72cf182c0c2c1dccb61c837765ea56f3">set_max_unrelevance</a>(<span class="keywordtype">int</span> n )
<a name="l00242"></a>00242 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> = n; }
<a name="l00243"></a><a class="code" href="classCSolver.html#a5778d83eeb8c5ad0d34120c3b472cde9">00243</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a5778d83eeb8c5ad0d34120c3b472cde9">set_min_num_clause_lits_for_delete</a>(<span class="keywordtype">int</span> n)
<a name="l00244"></a>00244 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> = n; }
<a name="l00245"></a><a class="code" href="classCSolver.html#aa3bb06628177a7a003957e00f9584351">00245</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#aa3bb06628177a7a003957e00f9584351">set_max_conflict_clause_length</a>(<span class="keywordtype">int</span> l)
<a name="l00246"></a>00246 { <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> = l; }
<a name="l00247"></a><a class="code" href="classCSolver.html#adcfb8dcb69c2221d25be0cd5ad6c43ff">00247</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#adcfb8dcb69c2221d25be0cd5ad6c43ff">set_allow_multiple_conflict</a>( <span class="keywordtype">bool</span> b = <span class="keyword">false</span>) {
<a name="l00248"></a>00248 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a4543f7d64cbab749e5e1998b83d1e1d2">allow_multiple_conflict</a> = b ;
<a name="l00249"></a>00249 }
<a name="l00250"></a><a class="code" href="classCSolver.html#a9713537c85c12024d85d5b25ab2cb844">00250</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a9713537c85c12024d85d5b25ab2cb844">set_allow_multiple_conflict_clause</a>( <span class="keywordtype">bool</span> b = <span class="keyword">false</span>) {
<a name="l00251"></a>00251 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a9d1be4fd22f1ee134702028a980c2d1b">allow_multiple_conflict_clause</a> = b;
<a name="l00252"></a>00252 }
<a name="l00253"></a><a class="code" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">00253</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a17438ece1aeb9736e73bc25b96def58d">set_randomness</a>(<span class="keywordtype">int</span> n) {
<a name="l00254"></a>00254 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">base_randomness</a> = n;
<a name="l00255"></a>00255 }
<a name="l00256"></a><a class="code" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">00256</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a6765f3784e94ebde4c86447845e67c1d">set_random_seed</a>(<span class="keywordtype">int</span> seed) {
<a name="l00257"></a>00257 <span class="keywordflow">if</span> (seed < 0)
<a name="l00258"></a>00258 srand ( <a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>() );
<a name="l00259"></a>00259 <span class="keywordflow">else</span>
<a name="l00260"></a>00260 srand (seed);
<a name="l00261"></a>00261 }
<a name="l00262"></a>00262
<a name="l00263"></a>00263 <span class="comment">//these are for the extended API</span>
<a name="l00264"></a><a class="code" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">00264</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">RegisterDLevelHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">int</span>), <span class="keywordtype">void</span> *cookie)
<a name="l00265"></a>00265 { <a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a> = f; <a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a> = cookie; }
<a name="l00266"></a><a class="code" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">00266</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">RegisterDecisionHook</a>(<span class="keywordtype">int</span> (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">bool</span> *), <span class="keywordtype">void</span> *cookie)
<a name="l00267"></a>00267 { <a class="code" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a> = f; <a class="code" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a> = cookie; }
<a name="l00268"></a><a class="code" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">00268</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">RegisterAssignmentHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *, <span class="keywordtype">int</span>, <span class="keywordtype">int</span>), <span class="keywordtype">void</span> *cookie)
<a name="l00269"></a>00269 { <a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a> = f; <a class="code" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a> = cookie; }
<a name="l00270"></a><a class="code" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">00270</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">RegisterDeductionHook</a>(<span class="keywordtype">void</span> (*f)(<span class="keywordtype">void</span> *), <span class="keywordtype">void</span> *cookie)
<a name="l00271"></a>00271 { <a class="code" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a> = f;
<a name="l00272"></a>00272 <a class="code" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a> = cookie; }
<a name="l00273"></a>00273
<a name="l00274"></a><a class="code" href="classCSolver.html#af7b4ed5bb5be8b7c56e4aa5f1913979b">00274</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#af7b4ed5bb5be8b7c56e4aa5f1913979b">outcome</a> () { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a>; }
<a name="l00275"></a><a class="code" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">00275</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a1d592aab62ad4f2943e0687916a34397">num_decisions</a>() { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a>; }
<a name="l00276"></a><a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">00276</a> <span class="keywordtype">int</span> & <a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>() {
<a name="l00277"></a>00277 <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#aaa0ec761ac703cd4d1ebd9446d1dcaf1">num_free_variables</a>;
<a name="l00278"></a>00278 }
<a name="l00279"></a><a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">00279</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>() { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a>; }
<a name="l00280"></a><a class="code" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">00280</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#ac1c4a48d4db9e61bc657a633b7230b88">num_implications</a>() { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae5581743416ca4828eb017c92a4e91a4">num_implications</a>; }
<a name="l00281"></a><a class="code" href="classCSolver.html#ae8d515c8e764ad65b870d5703b51c847">00281</a> <span class="keywordtype">long</span> <a class="code" href="classCSolver.html#ae8d515c8e764ad65b870d5703b51c847">total_bubble_move</a>(<span class="keywordtype">void</span>) { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7adfa10784b5c1866e8e3ab08bf68da2">total_bubble_move</a>; }
<a name="l00282"></a>00282
<a name="l00283"></a><a class="code" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">00283</a> <span class="keyword">const</span> <span class="keywordtype">char</span> * <a class="code" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">version</a>(<span class="keywordtype">void</span>){
<a name="l00284"></a>00284 <span class="keywordflow">return</span> <span class="stringliteral">"Z2001.2.17"</span>;
<a name="l00285"></a>00285 }
<a name="l00286"></a>00286
<a name="l00287"></a><a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">00287</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>(<span class="keywordtype">void</span>) {
<a name="l00288"></a>00288 <span class="keyword">struct </span>rusage ru;
<a name="l00289"></a>00289 getrusage(RUSAGE_SELF, &ru);
<a name="l00290"></a>00290 <span class="keywordflow">return</span> ( ru.ru_utime.tv_sec*1000 +
<a name="l00291"></a>00291 ru.ru_utime.tv_usec/1000+
<a name="l00292"></a>00292 ru.ru_stime.tv_sec*1000 +
<a name="l00293"></a>00293 ru.ru_stime.tv_usec/1000 );
<a name="l00294"></a>00294 }
<a name="l00295"></a>00295
<a name="l00296"></a><a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">00296</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>(<span class="keywordtype">void</span>) {
<a name="l00297"></a>00297 <span class="keyword">struct </span>timeval tv;
<a name="l00298"></a>00298 <span class="keyword">struct </span>timezone tz;
<a name="l00299"></a>00299 gettimeofday(&tv,&tz);
<a name="l00300"></a>00300 <span class="keywordflow">return</span> (tv.tv_sec * 1000 + tv.tv_usec/1000) ;
<a name="l00301"></a>00301 }
<a name="l00302"></a>00302
<a name="l00303"></a><a class="code" href="classCSolver.html#a66d960cb2bd8f5642afe1bf581d64f97">00303</a> <span class="keywordtype">float</span> <a class="code" href="classCSolver.html#a66d960cb2bd8f5642afe1bf581d64f97">elapsed_cpu_time</a>() {
<a name="l00304"></a>00304 <span class="keywordtype">int</span> current = <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>();
<a name="l00305"></a>00305 <span class="keywordtype">int</span> diff = current - <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a60bcfaf8308075781464cf18477fc3e4">last_cpu_time</a>;
<a name="l00306"></a>00306 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a60bcfaf8308075781464cf18477fc3e4">last_cpu_time</a> = current;
<a name="l00307"></a>00307 <span class="keywordflow">return</span> diff/1000.0;
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309
<a name="l00310"></a><a class="code" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">00310</a> <span class="keywordtype">float</span> <a class="code" href="classCSolver.html#afde50f1cee0bab34e2464b17693d59f7">total_run_time</a>() {
<a name="l00311"></a>00311 <span class="keywordflow">if</span> (!<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a>) <span class="keywordflow">return</span> 0;
<a name="l00312"></a>00312 <span class="keywordflow">return</span> (<a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>() -
<a name="l00313"></a>00313 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a>)/1000.0 ;
<a name="l00314"></a>00314 }
<a name="l00315"></a>00315
<a name="l00316"></a><a class="code" href="classCSolver.html#ace35bd2316cbf7b72d942c7a672374e3">00316</a> <span class="keywordtype">float</span> <a class="code" href="classCSolver.html#ace35bd2316cbf7b72d942c7a672374e3">cpu_run_time</a>() {
<a name="l00317"></a>00317 <span class="keywordflow">return</span> (<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">finish_cpu_time</a> -
<a name="l00318"></a>00318 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a>)/1000.0 ;
<a name="l00319"></a>00319 }
<a name="l00320"></a>00320
<a name="l00321"></a><a class="code" href="classCSolver.html#aa181acac744c04062df328ee5eac38f9">00321</a> <span class="keywordtype">float</span> <a class="code" href="classCSolver.html#aa181acac744c04062df328ee5eac38f9">world_run_time</a>() {
<a name="l00322"></a>00322 <span class="keywordflow">return</span> (<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">finish_world_time</a> -
<a name="l00323"></a>00323 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab42200e7e324f1f59e4ae2452fa22c6f">start_world_time</a>) / 1000.0 ;
<a name="l00324"></a>00324 }
<a name="l00325"></a>00325
<a name="l00326"></a><a class="code" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">00326</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">estimate_mem_usage</a>() {
<a name="l00327"></a>00327 <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a6a7cefe78a6f785c2c51950a74dde6d8">CDatabase::estimate_mem_usage</a>();
<a name="l00328"></a>00328 }
<a name="l00329"></a><a class="code" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">00329</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">mem_usage</a>(<span class="keywordtype">void</span>) {
<a name="l00330"></a>00330 <span class="keywordtype">int</span> mem_dbase = <a class="code" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">CDatabase::mem_usage</a>();
<a name="l00331"></a>00331 <span class="keywordtype">int</span> mem_assignment = 0;
<a name="l00332"></a>00332 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0; i< <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a>; ++i)
<a name="l00333"></a>00333 mem_assignment += <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i]->capacity() * <span class="keyword">sizeof</span>(int);
<a name="l00334"></a>00334 mem_assignment += <span class="keyword">sizeof</span>(vector<int>)* <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>.size();
<a name="l00335"></a>00335 <span class="keywordflow">return</span> mem_dbase + mem_assignment;
<a name="l00336"></a>00336 }
<a name="l00337"></a><a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">00337</a> <span class="keywordtype">int</span> & <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() { <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a>; }
<a name="l00338"></a>00338
<a name="l00339"></a>00339 <span class="comment">//top level function</span>
<a name="l00340"></a><a class="code" href="classCSolver.html#ade3fe6d285fbae6d71d09051e0e4637b">00340</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ade3fe6d285fbae6d71d09051e0e4637b">add_hook</a>( <a class="code" href="xchaff__solver_8h.html#a4288f2865a52bcea1f6cd0afa93a7898">HookFunPtrT</a> fun, <span class="keywordtype">int</span> interval) {
<a name="l00341"></a>00341 pair<HookFunPtrT, int> a(fun, interval);
<a name="l00342"></a>00342 <a class="code" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a>.push_back(pair<<span class="keywordtype">int</span>, pair<HookFunPtrT, int> > (0, a));
<a name="l00343"></a>00343 }
<a name="l00344"></a>00344
<a name="l00345"></a><a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">00345</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a> (<span class="keywordtype">int</span> lit, <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante_clause) {
<a name="l00346"></a>00346 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"\t\t\t\t\t\tQueueing "</span> << (lit&0x01?<span class="stringliteral">" -"</span>:<span class="stringliteral">" +"</span>) << (lit>>1) ;
<a name="l00347"></a>00347 cout << <span class="stringliteral">" because of "</span> << ante_clause << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; );
<a name="l00348"></a>00348 <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.push(pair<int, ClauseIdx>(lit, ante_clause));
<a name="l00349"></a>00349 }
<a name="l00350"></a>00350
<a name="l00351"></a>00351 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">add_variables</a>(<span class="keywordtype">int</span> new_vars);
<a name="l00352"></a>00352
<a name="l00353"></a>00353 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="code" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a>(vector<long>& lits, <span class="keywordtype">bool</span> addConflicts=<span class="keyword">true</span>);
<a name="l00354"></a>00354
<a name="l00355"></a>00355 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>(<span class="keywordtype">void</span>);
<a name="l00356"></a>00356
<a name="l00357"></a>00357 <span class="comment">// ClauseIdx add_clause_with_order_adjustment(int * lits, int n_lits);</span>
<a name="l00358"></a><a class="code" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">00358</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a> (<span class="keywordtype">void</span>){
<a name="l00359"></a>00359 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a> > 1 )
<a name="l00360"></a>00360 cout << <span class="stringliteral">"Restarting ... "</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00361"></a>00361 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() > 1) {
<a name="l00362"></a>00362 <span class="comment">//clean up the original var_stats.</span>
<a name="l00363"></a>00363 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=1; i<<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size(); ++i) {
<a name="l00364"></a>00364 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(i).<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(0) = 0;
<a name="l00365"></a>00365 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(i).<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(1) = 0;
<a name="l00366"></a>00366 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[0][i] = 0;
<a name="l00367"></a>00367 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[1][i] = 0;
<a name="l00368"></a>00368 }
<a name="l00369"></a>00369 <a class="code" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a>();
<a name="l00370"></a>00370 <a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a>(1); <span class="comment">//backtrack to level 0. restart.</span>
<a name="l00371"></a>00371 }
<a name="l00372"></a>00372 }
<a name="l00373"></a>00373
<a name="l00374"></a>00374 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">solve</a>(<span class="keywordtype">bool</span> allowNewClauses);
<a name="l00375"></a>00375 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">continueCheck</a>();
<a name="l00376"></a>00376
<a name="l00377"></a>00377 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a>(ostream & os = cout);
<a name="l00378"></a>00378
<a name="l00379"></a>00379 <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#adf342158bf2d06241a075a8c22a1ee73">output_current_stats</a>(<span class="keywordtype">void</span>);
<a name="l00380"></a>00380
<a name="l00381"></a><a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">00381</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>(ostream & os = cout ) {
<a name="l00382"></a>00382 <a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">CDatabase::dump</a>(os);
<a name="l00383"></a>00383 <a class="code" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a>(os);
<a name="l00384"></a>00384 }
<a name="l00385"></a>00385 };
<a name="l00386"></a>00386 <span class="preprocessor">#endif</span>
<a name="l00387"></a>00387 <span class="preprocessor"></span>
<a name="l00388"></a>00388
<a name="l00389"></a>00389
<a name="l00390"></a>00390
<a name="l00391"></a>00391
<a name="l00392"></a>00392
<a name="l00393"></a>00393
<a name="l00394"></a>00394
<a name="l00395"></a>00395
<a name="l00396"></a>00396
<a name="l00397"></a>00397
<a name="l00398"></a>00398
<a name="l00399"></a>00399
<a name="l00400"></a>00400
<a name="l00401"></a>00401
<a name="l00402"></a>00402
<a name="l00403"></a>00403
<a name="l00404"></a>00404
<a name="l00405"></a>00405
<a name="l00406"></a>00406
<a name="l00407"></a>00407
<a name="l00408"></a>00408
<a name="l00409"></a>00409
<a name="l00410"></a>00410
<a name="l00411"></a>00411
<a name="l00412"></a>00412
<a name="l00413"></a>00413
<a name="l00414"></a>00414
<a name="l00415"></a>00415
<a name="l00416"></a>00416
<a name="l00417"></a>00417
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
