<!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.cpp 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.cpp</div> </div>
</div>
<div class="contents">
<a href="xchaff__solver_8cpp.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 <span class="preprocessor">#include "<a class="code" href="xchaff__solver_8h.html">xchaff_solver.h</a>"</span>
<a name="l00040"></a>00040 <span class="preprocessor">#include <algorithm></span>
<a name="l00041"></a>00041
<a name="l00042"></a>00042
<a name="l00043"></a><a class="code" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">00043</a> <a class="code" href="classCSolver.html#afa1c51e0570e7a835fae6ba187f9d09b">CSolver::CSolver</a>(<span class="keywordtype">void</span>)
<a name="l00044"></a>00044 {
<a name="l00045"></a>00045 <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>()=0;
<a name="l00046"></a>00046 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a1904f8790a16c706e0d2ba51ce11c364">time_limit</a> = 3600 * 48; <span class="comment">//2 days</span>
<a name="l00047"></a>00047 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#aa5fb349b73577a3b99014ca90ce34e55">decision_strategy</a> = 0;
<a name="l00048"></a>00048 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a714385448e9041b135391f9548ed6efa">preprocess_strategy</a> = 0;
<a name="l00049"></a>00049 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#aa4c80dc600b3dcd9f64ef0c602dd59da">allow_clause_deletion</a> = true ;
<a name="l00050"></a>00050 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a5cbdbad62f42fd6f41ba5a4ed6f40af6">clause_deletion_interval</a> = 5000;
<a name="l00051"></a>00051 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> = 20;
<a name="l00052"></a>00052 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> = 100;
<a name="l00053"></a>00053 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> = 5000;
<a name="l00054"></a>00054 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ae358e7fe29489f48a00c012fb02a3778">bubble_init_step</a> = 32;
<a name="l00055"></a>00055
<a name="l00056"></a>00056 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a> = 0;
<a name="l00057"></a>00057 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a> = 0;
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a3e90abca92fa570f9d1dc5ce49b01daa">back_track_complete</a> = <span class="keyword">true</span>;
<a name="l00060"></a>00060 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a4543f7d64cbab749e5e1998b83d1e1d2">allow_multiple_conflict</a> = <span class="keyword">false</span>;
<a name="l00061"></a>00061 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a9d1be4fd22f1ee134702028a980c2d1b">allow_multiple_conflict_clause</a> = <span class="keyword">false</span>;
<a name="l00062"></a>00062
<a name="l00063"></a>00063 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a0040f5ae79dd7e8a478f60f3d02b1a6d">allow_restart</a> = <span class="keyword">true</span>;
<a name="l00064"></a>00064 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a4fec1add4989095c31fab9ec2a29f824">next_restart_time</a> = 50; <span class="comment">//this set the first restart time (in seconds)</span>
<a name="l00065"></a>00065 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a22f43c87a3a8cdfdfd35bd400f3f0b59">restart_time_increment</a> = 0;
<a name="l00066"></a>00066 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a914448885e9e2aedefd743f6428552d8">restart_time_incr_incr</a> = 0;
<a name="l00067"></a>00067
<a name="l00068"></a>00068 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ac1a694498478fc1c1e164e81881ea61f">next_restart_backtrack</a>= 0;
<a name="l00069"></a>00069 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a319ab0a9a6646af75828ff1a1f9a33b6">restart_backtrack_incr</a>= 40000;
<a name="l00070"></a>00070 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8b11bde6fb341437589e70a1b419d846">restart_backtrack_incr_incr</a> = 100;
<a name="l00071"></a>00071
<a name="l00072"></a>00072 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ac22c8353981fed418be2df36b64e635e">restart_randomness</a> = 0;
<a name="l00073"></a>00073 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">base_randomness</a> = 0;
<a name="l00074"></a>00074 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a> = 0;
<a name="l00075"></a>00075
<a name="l00076"></a>00076 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a> = <span class="keyword">false</span>;
<a name="l00077"></a>00077 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>;
<a name="l00078"></a>00078 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab5c8d00ed96f235136c96197230a09c7">is_mem_out</a> = <span class="keyword">false</span>;
<a name="l00079"></a>00079 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a> = 0;
<a name="l00080"></a>00080 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">finish_cpu_time</a> = 0;
<a name="l00081"></a>00081 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a60bcfaf8308075781464cf18477fc3e4">last_cpu_time</a> = 0;
<a name="l00082"></a>00082
<a name="l00083"></a>00083 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab42200e7e324f1f59e4ae2452fa22c6f">start_world_time</a> = 0;
<a name="l00084"></a>00084 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">finish_world_time</a> = 0;
<a name="l00085"></a>00085
<a name="l00086"></a>00086 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a> = 0;
<a name="l00087"></a>00087 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">num_backtracks</a> = 0;
<a name="l00088"></a>00088 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a> = 0;
<a name="l00089"></a>00089 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae5581743416ca4828eb017c92a4e91a4">num_implications</a> = 0;
<a name="l00090"></a>00090
<a name="l00091"></a>00091 <a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a> = 0;
<a name="l00092"></a>00092 <a class="code" href="classCSolver.html#a65a9481261bf9d9d90ff36de99992094">_dlevel</a> = 0;
<a name="l00093"></a>00093 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7adfa10784b5c1866e8e3ab08bf68da2">total_bubble_move</a> = 0;
<a name="l00094"></a>00094
<a name="l00095"></a>00095 <a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a> = NULL;
<a name="l00096"></a>00096 <a class="code" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a> = NULL;
<a name="l00097"></a>00097 <a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a> = NULL;
<a name="l00098"></a>00098 <a class="code" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a> = NULL;
<a name="l00099"></a>00099 }
<a name="l00100"></a>00100
<a name="l00101"></a><a class="code" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">00101</a> <a class="code" href="classCSolver.html#af3c9bd8a7dede30ca60e24bf30073206">CSolver::~CSolver</a>()
<a name="l00102"></a>00102 {
<a name="l00103"></a>00103 <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>) {
<a name="l00104"></a>00104 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i<<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size(); ++i)
<a name="l00105"></a>00105 <span class="keyword">delete</span> <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i];
<a name="l00106"></a>00106 }
<a name="l00107"></a>00107 }
<a name="l00108"></a>00108
<a name="l00109"></a><a class="code" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">00109</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">CSolver::run_periodic_functions</a>(<span class="keywordtype">void</span>)
<a name="l00110"></a>00110 {
<a name="l00111"></a>00111 <span class="comment">//a. clause deletion</span>
<a name="l00112"></a>00112 <span class="keywordflow">if</span> ( <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#aa4c80dc600b3dcd9f64ef0c602dd59da">allow_clause_deletion</a> &&
<a name="l00113"></a>00113 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">num_backtracks</a> % <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a5cbdbad62f42fd6f41ba5a4ed6f40af6">clause_deletion_interval</a> == 0)
<a name="l00114"></a>00114 <a class="code" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">delete_unrelevant_clauses</a>();
<a name="l00115"></a>00115 <span class="comment">//b. restart</span>
<a name="l00116"></a>00116 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a0040f5ae79dd7e8a478f60f3d02b1a6d">allow_restart</a> && <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">num_backtracks</a> > <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ac1a694498478fc1c1e164e81881ea61f">next_restart_backtrack</a>) {
<a name="l00117"></a>00117 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ac1a694498478fc1c1e164e81881ea61f">next_restart_backtrack</a> += <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a319ab0a9a6646af75828ff1a1f9a33b6">restart_backtrack_incr</a>;
<a name="l00118"></a>00118 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a319ab0a9a6646af75828ff1a1f9a33b6">restart_backtrack_incr</a> += <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8b11bde6fb341437589e70a1b419d846">restart_backtrack_incr_incr</a>;
<a name="l00119"></a>00119 <span class="keywordtype">float</span> current = <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>()/1000;
<a name="l00120"></a>00120 <span class="keywordflow">if</span> (current > <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a4fec1add4989095c31fab9ec2a29f824">next_restart_time</a>) {
<a name="l00121"></a>00121 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a> > 1) cout << <span class="stringliteral">"restart..."</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00122"></a>00122 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a4fec1add4989095c31fab9ec2a29f824">next_restart_time</a> = current + <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a22f43c87a3a8cdfdfd35bd400f3f0b59">restart_time_increment</a>;
<a name="l00123"></a>00123 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a22f43c87a3a8cdfdfd35bd400f3f0b59">restart_time_increment</a> += <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a914448885e9e2aedefd743f6428552d8">restart_time_incr_incr</a>;
<a name="l00124"></a>00124 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a> = <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#ac22c8353981fed418be2df36b64e635e">restart_randomness</a>;
<a name="l00125"></a>00125 <a class="code" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a>();
<a name="l00126"></a>00126 }
<a name="l00127"></a>00127 }
<a name="l00128"></a>00128 <span class="comment">//c. update var stats for decision</span>
<a name="l00129"></a>00129 <span class="keywordflow">if</span> ((<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a> % 0xff)==0)
<a name="l00130"></a>00130 <a class="code" href="classCSolver.html#acc181946a5845c647818631415c22c22">update_var_stats</a>();
<a name="l00131"></a>00131 <span class="comment">//d. run hook functions</span>
<a name="l00132"></a>00132 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< <a class="code" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a>.size(); ++i) {
<a name="l00133"></a>00133 pair<int,pair<HookFunPtrT, int> > & hook = <a class="code" href="classCSolver.html#a49509a796f28911569176b2cc6d4a0a0">_hooks</a>[i];
<a name="l00134"></a>00134 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a> >= hook.first) {
<a name="l00135"></a>00135 hook.first += hook.second.second;
<a name="l00136"></a>00136 hook.second.first((<span class="keywordtype">void</span> *) <span class="keyword">this</span>);
<a name="l00137"></a>00137 }
<a name="l00138"></a>00138 }
<a name="l00139"></a>00139 }
<a name="l00140"></a>00140
<a name="l00141"></a>00141
<a name="l00142"></a><a class="code" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">00142</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">CSolver::init</a>(<span class="keywordtype">void</span>)
<a name="l00143"></a>00143 {
<a name="l00144"></a>00144 <a class="code" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">CDatabase::init</a>();
<a name="l00145"></a>00145
<a name="l00146"></a>00146 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a> = <span class="keyword">true</span>;
<a name="l00147"></a>00147 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a> = <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>();
<a name="l00148"></a>00148 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab42200e7e324f1f59e4ae2452fa22c6f">start_world_time</a> = <a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>();
<a name="l00149"></a>00149 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#aaa0ec761ac703cd4d1ebd9446d1dcaf1">num_free_variables</a> = <a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>();
<a name="l00150"></a>00150 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i<<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size(); ++i)
<a name="l00151"></a>00151 <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>.push_back(<span class="keyword">new</span> vector<int>);
<a name="l00152"></a>00152
<a name="l00153"></a>00153 <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.resize( <a class="code" href="classCDatabase.html#ac95e4d7648334447162c0fb4e3de28d7">num_variables</a>());
<a name="l00154"></a>00154 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[0].resize(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size());
<a name="l00155"></a>00155 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[1].resize(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size());
<a name="l00156"></a>00156 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00157"></a>00157 }
<a name="l00158"></a>00158
<a name="l00159"></a>00159
<a name="l00160"></a><a class="code" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">00160</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a1b1f7e9d95712bd0852366c044a5829f">CSolver::add_variables</a>(<span class="keywordtype">int</span> new_vars)
<a name="l00161"></a>00161 {
<a name="l00162"></a>00162 <span class="keywordtype">int</span> old_num_vars = <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size();
<a name="l00163"></a>00163 <span class="keywordtype">int</span> num_vars = old_num_vars + new_vars;
<a name="l00164"></a>00164 <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().resize(num_vars) ;
<a name="l00165"></a>00165 <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>) {
<a name="l00166"></a>00166 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#aaa0ec761ac703cd4d1ebd9446d1dcaf1">num_free_variables</a> += new_vars;
<a name="l00167"></a>00167
<a name="l00168"></a>00168 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=old_num_vars; i<num_vars; ++i) {
<a name="l00169"></a>00169 <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>.push_back(<span class="keyword">new</span> vector<int>);
<a name="l00170"></a>00170 <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.push_back(pair<int, int>(i,0));
<a name="l00171"></a>00171 }
<a name="l00172"></a>00172 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[0].resize(num_vars);
<a name="l00173"></a>00173 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[1].resize(num_vars);
<a name="l00174"></a>00174 }
<a name="l00175"></a>00175 <span class="keywordflow">return</span> old_num_vars;
<a name="l00176"></a>00176 }
<a name="l00177"></a>00177
<a name="l00178"></a>00178
<a name="l00179"></a><a class="code" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">00179</a> <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> <a class="code" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">CSolver::add_clause</a>(vector<long>& lits, <span class="keywordtype">bool</span> addConflicts) {
<a name="l00180"></a>00180 <span class="keywordtype">int</span> new_cl;
<a name="l00181"></a>00181 <span class="keywordtype">int</span> n_lits = lits.size();
<a name="l00182"></a>00182 <span class="comment">//a. do we need to enlarge lits pool?</span>
<a name="l00183"></a>00183 <span class="keywordflow">while</span> (<a class="code" href="classCDatabase.html#ac66c5172be66fa260f8f6d5fd41ca295">lit_pool_free_space</a>() <= n_lits + 1) {
<a name="l00184"></a>00184 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ae121408a92221766e9139e7cf40ab7de">enlarge_lit_pool</a>()==<span class="keyword">false</span>)
<a name="l00185"></a>00185 <span class="keywordflow">return</span> -1; <span class="comment">//mem out, can't enlarge lit pool, because </span>
<a name="l00186"></a>00186 <span class="comment">//ClauseIdx can't be -1, so it shows error.</span>
<a name="l00187"></a>00187 }
<a name="l00188"></a>00188 <span class="comment">//b. get a free cl index;</span>
<a name="l00189"></a>00189 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>.empty()) {
<a name="l00190"></a>00190 new_cl = <a class="code" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">_clauses</a>.size();
<a name="l00191"></a>00191 <a class="code" href="classCDatabase.html#a6adefe9983a5487fca8fc26cf8d9573f">_clauses</a>.resize(new_cl + 1);
<a name="l00192"></a>00192 }
<a name="l00193"></a>00193 <span class="keywordflow">else</span> {
<a name="l00194"></a>00194 new_cl = <a class="code" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>.front();
<a name="l00195"></a>00195 <a class="code" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>.pop();
<a name="l00196"></a>00196 }
<a name="l00197"></a>00197 <span class="comment">//c. add the clause lits to lits pool</span>
<a name="l00198"></a>00198 <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(new_cl).<a class="code" href="classCClause.html#a9dea20f5f7e41be18dfbe01105c58f2c">init</a>(<a class="code" href="classCDatabase.html#a3217dc6be8cff75fd418fbd4ff2e5763">lit_pool_end</a>(), n_lits);
<a name="l00199"></a>00199
<a name="l00200"></a>00200 <span class="comment">//I want to verify added clauses are either all free or all 0</span>
<a name="l00201"></a>00201 <span class="keywordtype">bool</span> satisfied = <span class="keyword">false</span>, is_unit = <span class="keyword">false</span>, <a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a> = <span class="keyword">false</span>;
<a name="l00202"></a>00202 <span class="keywordtype">int</span> num_unknown = 0;
<a name="l00203"></a>00203 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0; i< n_lits; ++i){
<a name="l00204"></a>00204 <span class="keywordtype">int</span> var_idx = lits[i]>>1;
<a name="l00205"></a>00205 <span class="keywordflow">if</span> ((<span class="keywordtype">unsigned</span>)var_idx >= <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size()) {
<a name="l00206"></a>00206 assert(<span class="keyword">false</span>);
<a name="l00207"></a>00207 }
<a name="l00208"></a>00208 <span class="keywordtype">int</span> var_sign = lits[i]&0x1;
<a name="l00209"></a>00209 <a class="code" href="classCDatabase.html#a7fa3358fa63aa02cae8055c0dfe832b7">lit_pool_push_back</a>( ((var_idx<<1) + var_sign) << 2);
<a name="l00210"></a>00210 ++<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(var_idx).<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(var_sign);
<a name="l00211"></a>00211 <span class="keywordtype">int</span> lit_value = <a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(new_cl).literal(i));
<a name="l00212"></a>00212
<a name="l00213"></a>00213 <span class="keywordflow">if</span> (lit_value == 1) {
<a name="l00214"></a>00214 satisfied = <span class="keyword">true</span>;
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (lit_value != 0) {
<a name="l00217"></a>00217 ++num_unknown;
<a name="l00218"></a>00218 }
<a name="l00219"></a>00219 }
<a name="l00220"></a>00220 <a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a> = !satisfied && (num_unknown == 0);
<a name="l00221"></a>00221 is_unit = !satisfied && (num_unknown == 1);
<a name="l00222"></a>00222 assert(<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a> || num_unknown == n_lits);
<a name="l00223"></a>00223 <a class="code" href="classCDatabase.html#a7fa3358fa63aa02cae8055c0dfe832b7">lit_pool_push_back</a>(-new_cl); <span class="comment">//push in the clause idx in the end</span>
<a name="l00224"></a>00224 <span class="comment">//d. set the head/tail pointers</span>
<a name="l00225"></a>00225 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(new_cl).num_lits() > 1) {
<a name="l00226"></a>00226 <span class="comment">//add the ht. note: ht must be the last free var</span>
<a name="l00227"></a>00227 <span class="keywordtype">int</span> max_idx = -1, max_dl = -1;
<a name="l00228"></a>00228 <a class="code" href="classCClause.html">CClause</a> & cl = <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(new_cl);
<a name="l00229"></a>00229 <span class="keywordtype">int</span> i, sz = cl.<a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>();
<a name="l00230"></a>00230 <span class="keywordtype">int</span> other_ht_idx;
<a name="l00231"></a>00231 <span class="keywordflow">for</span> (i=0; i< sz; ++i) {
<a name="l00232"></a>00232 <span class="keywordtype">int</span> v_idx = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00233"></a>00233 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).value()==<a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) {
<a name="l00234"></a>00234 <span class="keywordtype">int</span> v_sign = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">var_sign</a>();
<a name="l00235"></a>00235 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(v_sign).push_back( & cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i]);
<a name="l00236"></a>00236 cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">set_ht</a>(1);
<a name="l00237"></a>00237 other_ht_idx = i;
<a name="l00238"></a>00238 <span class="keywordflow">break</span>;
<a name="l00239"></a>00239 }
<a name="l00240"></a>00240 <span class="keywordflow">else</span> {
<a name="l00241"></a>00241 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() > max_dl) {
<a name="l00242"></a>00242 max_dl = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a>();
<a name="l00243"></a>00243 max_idx = i;
<a name="l00244"></a>00244 }
<a name="l00245"></a>00245 }
<a name="l00246"></a>00246 }
<a name="l00247"></a>00247 <span class="keywordflow">if</span> (i >= sz) {
<a name="l00248"></a>00248 <span class="comment">//no unknown literals. so use the max dl literal</span>
<a name="l00249"></a>00249 <span class="keywordtype">int</span> v_idx = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00250"></a>00250 <span class="keywordtype">int</span> v_sign = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">var_sign</a>();
<a name="l00251"></a>00251 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(v_sign).push_back( & cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx]);
<a name="l00252"></a>00252 cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">set_ht</a>(1);
<a name="l00253"></a>00253 other_ht_idx = max_idx;
<a name="l00254"></a>00254 }
<a name="l00255"></a>00255 max_idx = -1; max_dl = -1;
<a name="l00256"></a>00256 <span class="keywordflow">for</span> (i=sz-1; i>=0; --i) {
<a name="l00257"></a>00257 <span class="keywordflow">if</span> (i==other_ht_idx ) <span class="keywordflow">continue</span>;
<a name="l00258"></a>00258 <span class="keywordtype">int</span> v_idx = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00259"></a>00259 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).value()==<a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) {
<a name="l00260"></a>00260 <span class="keywordtype">int</span> v_sign = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">var_sign</a>();
<a name="l00261"></a>00261 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(v_sign).push_back( & cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i]);
<a name="l00262"></a>00262 cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">set_ht</a>(-1);
<a name="l00263"></a>00263 <span class="keywordflow">break</span>;
<a name="l00264"></a>00264 }
<a name="l00265"></a>00265 <span class="keywordflow">else</span> {
<a name="l00266"></a>00266 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() > max_dl) {
<a name="l00267"></a>00267 max_dl = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a>();
<a name="l00268"></a>00268 max_idx = i;
<a name="l00269"></a>00269 }
<a name="l00270"></a>00270 }
<a name="l00271"></a>00271 }
<a name="l00272"></a>00272 <span class="keywordflow">if</span> (i < 0) {
<a name="l00273"></a>00273 <span class="keywordtype">int</span> v_idx = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00274"></a>00274 <span class="keywordtype">int</span> v_sign = cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">var_sign</a>();
<a name="l00275"></a>00275 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * lit_ptr = & cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx];
<a name="l00276"></a>00276 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v_idx).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(v_sign).push_back(lit_ptr);
<a name="l00277"></a>00277 cl.<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[max_idx].<a class="code" href="classCLitPoolElement.html#a61ae125841707c699b3587e0f5a668bc">set_ht</a>(-1);
<a name="l00278"></a>00278 }
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280 <span class="comment">//update some statistics</span>
<a name="l00281"></a>00281 ++<a class="code" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a>.<a class="code" href="structCDatabaseStats.html#a2350a97ea7c7333870732c83772fb1f9">num_added_clauses</a>;
<a name="l00282"></a>00282 <a class="code" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a>.<a class="code" href="structCDatabaseStats.html#ad7baf06bf924ed8d6d9b9f73d734ef74">num_added_literals</a> += n_lits;
<a name="l00283"></a>00283 <span class="keywordflow">if</span> (is_unit && <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae8963018c0dcb967130c5d9867922b4d">is_solver_started</a>) {
<a name="l00284"></a>00284 <span class="keywordflow">if</span> (n_lits == 1) <a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>.push_back(new_cl);
<a name="l00285"></a>00285 <span class="keywordtype">int</span> lit = <a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(new_cl);
<a name="l00286"></a>00286 assert(lit);
<a name="l00287"></a>00287 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(lit, new_cl);
<a name="l00288"></a>00288 }
<a name="l00289"></a>00289 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (addConflicts && <a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a>) {
<a name="l00290"></a>00290 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.push_back(new_cl);
<a name="l00291"></a>00291 }
<a name="l00292"></a>00292 <span class="keywordflow">return</span> new_cl;
<a name="l00293"></a>00293 }
<a name="l00294"></a>00294
<a name="l00295"></a>00295
<a name="l00296"></a><a class="code" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">00296</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">CSolver::set_var_value</a>(<span class="keywordtype">int</span> v, <span class="keywordtype">int</span> value, <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante, <span class="keywordtype">int</span> dl)
<a name="l00297"></a>00297 {
<a name="l00298"></a>00298 assert (value == 0 || value == 1);
<a name="l00299"></a>00299 <a class="code" href="xchaff__utils_8h.html#a6683569480fcdbf7931a984f2738731c">CHECK_FULL</a>(<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00300"></a>00300 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(<a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>());
<a name="l00301"></a>00301 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"Setting\t"</span> << (value>0?<span class="stringliteral">"+"</span>:<span class="stringliteral">"-"</span>) << v
<a name="l00302"></a>00302 << <span class="stringliteral">" at "</span> << dl << <span class="stringliteral">" because "</span> << ante<< <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00303"></a>00303 ++<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ae5581743416ca4828eb017c92a4e91a4">num_implications</a> ;
<a name="l00304"></a>00304 --<a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>();
<a name="l00305"></a>00305 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a>) {
<a name="l00306"></a>00306 (*_assignment_hook)(<a class="code" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a>, v, value);
<a name="l00307"></a>00307 }
<a name="l00308"></a>00308 <a class="code" href="classCVariable.html">CVariable</a> & var = <a class="code" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>[v];
<a name="l00309"></a>00309 assert (var.<a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>);
<a name="l00310"></a>00310 var.<a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a>() = dl;
<a name="l00311"></a>00311 var.<a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() = value;
<a name="l00312"></a>00312 var.<a class="code" href="classCVariable.html#ab10578bfddce9b0dfb959b84395d799c">set_antecedence</a>(ante);
<a name="l00313"></a>00313 vector<CLitPoolElement *> & ht_ptrs = var.<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(value);
<a name="l00314"></a>00314 <span class="keywordflow">if</span> (dl == <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>())
<a name="l00315"></a>00315 <a class="code" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">set_var_value_with_current_dl</a>(v, ht_ptrs);
<a name="l00316"></a>00316 <span class="keywordflow">else</span>
<a name="l00317"></a>00317 <a class="code" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">set_var_value_not_current_dl</a>(v, ht_ptrs);
<a name="l00318"></a>00318 }
<a name="l00319"></a>00319
<a name="l00320"></a>00320
<a name="l00321"></a><a class="code" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">00321</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac497f97142b2f82acf8f43ba191feb08">CSolver::set_var_value_with_current_dl</a>(<span class="keywordtype">int</span> v, vector<CLitPoolElement *> & ht_ptrs)
<a name="l00322"></a>00322 {
<a name="l00323"></a>00323 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl_idx;
<a name="l00324"></a>00324 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * ht_ptr, * other_ht_ptr = NULL, * ptr;
<a name="l00325"></a>00325 <span class="keywordtype">int</span> dir;
<a name="l00326"></a>00326 <span class="keywordflow">for</span> (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); itr != ht_ptrs.end(); ++itr) {
<a name="l00327"></a>00327 ht_ptr = *itr;
<a name="l00328"></a>00328 dir = ht_ptr-><a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">direction</a>();
<a name="l00329"></a>00329 ptr = ht_ptr;
<a name="l00330"></a>00330 <span class="keywordflow">while</span>(1) {
<a name="l00331"></a>00331 ptr += dir;
<a name="l00332"></a>00332 <span class="keywordflow">if</span> (ptr->val() <= 0) {
<a name="l00333"></a>00333 <span class="keywordflow">if</span> (dir == 1)
<a name="l00334"></a>00334 cl_idx = - ptr-><a class="code" href="classCLitPoolElement.html#a253daa80c6f47528feb0b69e1a5c4623">val</a>();
<a name="l00335"></a>00335 <span class="keywordflow">if</span> (dir == ht_ptr-><a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">direction</a>()) {
<a name="l00336"></a>00336 ptr = ht_ptr;
<a name="l00337"></a>00337 dir = -dir;
<a name="l00338"></a>00338 <span class="keywordflow">continue</span>;
<a name="l00339"></a>00339 }
<a name="l00340"></a>00340 <span class="keywordtype">int</span> the_value = <a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a> (*other_ht_ptr);
<a name="l00341"></a>00341 <span class="keywordflow">if</span> (the_value == 0) <span class="comment">//a conflict</span>
<a name="l00342"></a>00342 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.push_back(cl_idx);
<a name="l00343"></a>00343 <span class="keywordflow">else</span> <span class="keywordflow">if</span> ( the_value != 1) <span class="comment">//e.g. unknown</span>
<a name="l00344"></a>00344 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a> (other_ht_ptr-><a class="code" href="classCLitPoolElement.html#a19281557172f9102172f404bf9f69cbc">s_var</a>(), cl_idx);
<a name="l00345"></a>00345 <span class="keywordflow">break</span>;
<a name="l00346"></a>00346 }
<a name="l00347"></a>00347 <span class="keywordflow">if</span> (ptr->is_ht()) {
<a name="l00348"></a>00348 other_ht_ptr = ptr;
<a name="l00349"></a>00349 <span class="keywordflow">continue</span>;
<a name="l00350"></a>00350 }
<a name="l00351"></a>00351 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(*ptr) == 0)
<a name="l00352"></a>00352 <span class="keywordflow">continue</span>;
<a name="l00353"></a>00353 <span class="comment">//now it's value is either 1 or unknown</span>
<a name="l00354"></a>00354 <span class="keywordtype">int</span> v1 = ptr-><a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00355"></a>00355 <span class="keywordtype">int</span> sign = ptr->var_sign();
<a name="l00356"></a>00356 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v1).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(sign).push_back(ptr);
<a name="l00357"></a>00357 ht_ptr-><a class="code" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">unset_ht</a>();
<a name="l00358"></a>00358 ptr->set_ht(dir);
<a name="l00359"></a>00359
<a name="l00360"></a>00360 *itr = ht_ptrs.back();
<a name="l00361"></a>00361 ht_ptrs.pop_back();
<a name="l00362"></a>00362 --itr;
<a name="l00363"></a>00363 <span class="keywordflow">break</span>;
<a name="l00364"></a>00364 }
<a name="l00365"></a>00365 }
<a name="l00366"></a>00366 }
<a name="l00367"></a>00367
<a name="l00368"></a><a class="code" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">00368</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a4617b5f40d47a1ac33135a76669994a4">CSolver::set_var_value_not_current_dl</a>(<span class="keywordtype">int</span> v, vector<CLitPoolElement *> & ht_ptrs)
<a name="l00369"></a>00369 {
<a name="l00370"></a>00370 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl_idx;
<a name="l00371"></a>00371 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * ht_ptr, * other_ht_ptr = NULL, * ptr, * max_ptr = NULL;
<a name="l00372"></a>00372 <span class="keywordtype">int</span> dir,max_dl;
<a name="l00373"></a>00373
<a name="l00374"></a>00374 <span class="keywordflow">for</span> (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin();
<a name="l00375"></a>00375 itr != ht_ptrs.end(); ++itr) {
<a name="l00376"></a>00376 max_dl = -1;
<a name="l00377"></a>00377 ht_ptr = *itr;
<a name="l00378"></a>00378 dir = ht_ptr-><a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">direction</a>();
<a name="l00379"></a>00379 ptr = ht_ptr;
<a name="l00380"></a>00380 <span class="keywordflow">while</span>(1) {
<a name="l00381"></a>00381 ptr += dir;
<a name="l00382"></a>00382 <span class="keywordflow">if</span> (ptr->val() <= 0) {
<a name="l00383"></a>00383 <span class="keywordflow">if</span> (dir == 1)
<a name="l00384"></a>00384 cl_idx = - ptr-><a class="code" href="classCLitPoolElement.html#a253daa80c6f47528feb0b69e1a5c4623">val</a>();
<a name="l00385"></a>00385 <span class="keywordflow">if</span> (dir == ht_ptr-><a class="code" href="classCLitPoolElement.html#a5810e79233dd5430fa52f56e5ef1f3ed">direction</a>()) {
<a name="l00386"></a>00386 ptr = ht_ptr;
<a name="l00387"></a>00387 dir = -dir;
<a name="l00388"></a>00388 <span class="keywordflow">continue</span>;
<a name="l00389"></a>00389 }
<a name="l00390"></a>00390 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(ht_ptr-><a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>()).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() < max_dl) {
<a name="l00391"></a>00391 <span class="keywordtype">int</span> v1 = max_ptr-><a class="code" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">var_index</a>();
<a name="l00392"></a>00392 <span class="keywordtype">int</span> sign = max_ptr->var_sign();
<a name="l00393"></a>00393 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v1).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(sign).push_back(max_ptr);
<a name="l00394"></a>00394 ht_ptr-><a class="code" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">unset_ht</a>();
<a name="l00395"></a>00395 max_ptr->set_ht(dir);
<a name="l00396"></a>00396 *itr = ht_ptrs.back();
<a name="l00397"></a>00397 ht_ptrs.pop_back();
<a name="l00398"></a>00398 --itr;
<a name="l00399"></a>00399 }
<a name="l00400"></a>00400 <span class="keywordtype">int</span> the_value = <a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a> (*other_ht_ptr);
<a name="l00401"></a>00401 <span class="keywordflow">if</span> (the_value == 0) <span class="comment">//a conflict</span>
<a name="l00402"></a>00402 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.push_back(cl_idx);
<a name="l00403"></a>00403 <span class="keywordflow">else</span> <span class="keywordflow">if</span> ( the_value != 1) <span class="comment">//e.g. unknown</span>
<a name="l00404"></a>00404 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a> (other_ht_ptr-><a class="code" href="classCLitPoolElement.html#a19281557172f9102172f404bf9f69cbc">s_var</a>(), cl_idx);
<a name="l00405"></a>00405 <span class="keywordflow">break</span>;
<a name="l00406"></a>00406 }
<a name="l00407"></a>00407 <span class="keywordflow">if</span> (ptr->is_ht()) {
<a name="l00408"></a>00408 other_ht_ptr = ptr;
<a name="l00409"></a>00409 <span class="keywordflow">continue</span>;
<a name="l00410"></a>00410 }
<a name="l00411"></a>00411 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(*ptr) == 0) {
<a name="l00412"></a>00412 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(ptr->var_index()).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() > max_dl) {
<a name="l00413"></a>00413 max_dl = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(ptr->var_index()).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>();
<a name="l00414"></a>00414 max_ptr = ptr;
<a name="l00415"></a>00415 }
<a name="l00416"></a>00416 <span class="keywordflow">continue</span>;
<a name="l00417"></a>00417 }
<a name="l00418"></a>00418 <span class="comment">//now it's value is either 1 or unknown</span>
<a name="l00419"></a>00419 <span class="keywordtype">int</span> v1 = ptr->var_index();
<a name="l00420"></a>00420 <span class="keywordtype">int</span> sign = ptr->var_sign();
<a name="l00421"></a>00421 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v1).<a class="code" href="classCVariable.html#aef0698f402345545601284fa7682e6f5">ht_ptr</a>(sign).push_back(ptr);
<a name="l00422"></a>00422 ht_ptr-><a class="code" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">unset_ht</a>();
<a name="l00423"></a>00423 ptr->set_ht(dir);
<a name="l00424"></a>00424
<a name="l00425"></a>00425 *itr = ht_ptrs.back();
<a name="l00426"></a>00426 ht_ptrs.pop_back();
<a name="l00427"></a>00427 --itr;
<a name="l00428"></a>00428 <span class="keywordflow">break</span>;
<a name="l00429"></a>00429 }
<a name="l00430"></a>00430 }
<a name="l00431"></a>00431 }
<a name="l00432"></a>00432
<a name="l00433"></a><a class="code" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">00433</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">CSolver::unset_var_value</a>(<span class="keywordtype">int</span> v)
<a name="l00434"></a>00434 {
<a name="l00435"></a>00435 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(cout <<<span class="stringliteral">"Unset var "</span> << (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).value()?<span class="stringliteral">"+"</span>:<span class="stringliteral">"-"</span>) << v << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00436"></a>00436 <a class="code" href="classCVariable.html">CVariable</a> & var = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v);
<a name="l00437"></a>00437 <span class="keywordflow">if</span> (var.var_score_pos() < <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a>)
<a name="l00438"></a>00438 <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a> = var.var_score_pos();
<a name="l00439"></a>00439 var.value() = <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>;
<a name="l00440"></a>00440 var.set_antecedence(<a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>);
<a name="l00441"></a>00441 var.dlevel() = -1;
<a name="l00442"></a>00442 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a66cffc281bb01002d1b30e01f6e90a28">_assignment_hook</a>) {
<a name="l00443"></a>00443 (*_assignment_hook)(<a class="code" href="classCSolver.html#a0de6dbd6e4d7f30c4ee841f15b8ae5e4">_assignment_hook_cookie</a>, v, -1);
<a name="l00444"></a>00444 }
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446
<a name="l00447"></a><a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">00447</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">CSolver::find_max_clause_dlevel</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<a name="l00448"></a>00448 {
<a name="l00449"></a>00449 <span class="comment">//if cl has single literal, then dlevel should be 0 </span>
<a name="l00450"></a>00450 <span class="keywordtype">int</span> max_level = 0;
<a name="l00451"></a>00451 <span class="keywordflow">if</span> (cl == <a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a> || cl == <a class="code" href="xchaff__base_8h.html#aa5981a99705aebbb4ca38799d15e0e79">FLIPPED</a>)
<a name="l00452"></a>00452 <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>();
<a name="l00453"></a>00453 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz= <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).num_lits(); i<sz; ++i) {
<a name="l00454"></a>00454 <span class="keywordtype">int</span> var_idx =((<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>())[i]).var_index();
<a name="l00455"></a>00455 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>[var_idx].value() != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) {
<a name="l00456"></a>00456 <span class="keywordflow">if</span> (max_level < <a class="code" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>[var_idx].<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>())
<a name="l00457"></a>00457 max_level = <a class="code" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>[var_idx].dlevel();
<a name="l00458"></a>00458 }
<a name="l00459"></a>00459 }
<a name="l00460"></a>00460 <span class="keywordflow">return</span> max_level;
<a name="l00461"></a>00461 }
<a name="l00462"></a>00462
<a name="l00463"></a><a class="code" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">00463</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">CSolver::dump_assignment_stack</a>(ostream & os) {
<a name="l00464"></a>00464 cout << <span class="stringliteral">"Assignment Stack: "</span>;
<a name="l00465"></a>00465 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0; i<= <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>(); ++i) {
<a name="l00466"></a>00466 <span class="keywordflow">if</span> ((*<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i]).size() > 0)
<a name="l00467"></a>00467 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>( (*<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i])[0]>>1).<a class="code" href="classCVariable.html#a92a4c6ae0e4b566d1f664add2aeb39e9">get_antecedence</a>()==<a class="code" href="xchaff__base_8h.html#aa5981a99705aebbb4ca38799d15e0e79">FLIPPED</a>)
<a name="l00468"></a>00468 cout << <span class="stringliteral">"*"</span> ;
<a name="l00469"></a>00469 cout << <span class="stringliteral">"("</span> <<i << <span class="stringliteral">":"</span>;
<a name="l00470"></a>00470 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> j=0; j<(*<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i]).size(); ++j )
<a name="l00471"></a>00471 cout << ((*<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i])[j]&0x1?<span class="stringliteral">"-"</span>:<span class="stringliteral">"+"</span>)
<a name="l00472"></a>00472 << ((*<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i])[j] >> 1) << <span class="stringliteral">" "</span>;
<a name="l00473"></a>00473 cout << <span class="stringliteral">") "</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00474"></a>00474 }
<a name="l00475"></a>00475 cout << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00476"></a>00476 }
<a name="l00477"></a>00477
<a name="l00478"></a>00478
<a name="l00479"></a><a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">00479</a> <span class="keywordtype">bool</span> <a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">CDatabase::is_conflict</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<a name="l00480"></a>00480 {
<a name="l00481"></a>00481 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * lits = <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>();
<a name="l00482"></a>00482 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz= <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).num_lits(); i<sz; ++i)
<a name="l00483"></a>00483 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(lits[i]) != 0)
<a name="l00484"></a>00484 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00485"></a>00485 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487
<a name="l00488"></a><a class="code" href="classCDatabase.html#a85e3fc325b5e311c4081e5ac05e4ac5c">00488</a> <span class="keywordtype">bool</span> <a class="code" href="classCDatabase.html#a85e3fc325b5e311c4081e5ac05e4ac5c">CDatabase::is_satisfied</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<a name="l00489"></a>00489 {
<a name="l00490"></a>00490 <a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * lits = <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>();
<a name="l00491"></a>00491 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz= <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).num_lits(); i<sz; ++i)
<a name="l00492"></a>00492 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a>(lits[i]) == 1)
<a name="l00493"></a>00493 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00494"></a>00494 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00495"></a>00495 }
<a name="l00496"></a>00496
<a name="l00497"></a><a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">00497</a> <span class="keywordtype">int</span> <a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">CDatabase::find_unit_literal</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl)
<a name="l00498"></a>00498 {
<a name="l00499"></a>00499 <span class="comment">//if it's not unit, return 0.</span>
<a name="l00500"></a>00500 <span class="keywordtype">int</span> unassigned = 0;
<a name="l00501"></a>00501 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz= <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).num_lits(); i<sz; ++i) {
<a name="l00502"></a>00502 <span class="keywordtype">int</span> var_idx =((<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>())[i]).var_index();
<a name="l00503"></a>00503 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#a0bc13af9359ede872eefe8e1f44b3069">_variables</a>[var_idx].value() == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) {
<a name="l00504"></a>00504 <span class="keywordflow">if</span> (unassigned == 0)
<a name="l00505"></a>00505 unassigned = <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).<a class="code" href="classCClause.html#a8254175660df4f73f485f9227becaf14">literals</a>()[i].<a class="code" href="classCLitPoolElement.html#a19281557172f9102172f404bf9f69cbc">s_var</a>();
<a name="l00506"></a>00506 <span class="keywordflow">else</span> <span class="comment">//more than one unassigned</span>
<a name="l00507"></a>00507 <span class="keywordflow">return</span> 0;
<a name="l00508"></a>00508 }
<a name="l00509"></a>00509 }
<a name="l00510"></a>00510 <span class="keywordflow">return</span> unassigned;
<a name="l00511"></a>00511 }
<a name="l00512"></a>00512
<a name="l00513"></a><a class="code" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">00513</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a09834f0e5025b7a748bc24bf113b0f9e">CSolver::delete_unrelevant_clauses</a>(<span class="keywordtype">void</span>)
<a name="l00514"></a>00514 {
<a name="l00515"></a>00515 <a class="code" href="xchaff__utils_8h.html#a6683569480fcdbf7931a984f2738731c">CHECK_FULL</a> (<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00516"></a>00516 <span class="keywordtype">int</span> original_num_deleted = <a class="code" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a>();
<a name="l00517"></a>00517 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a>.mem_used_up) {
<a name="l00518"></a>00518 <a class="code" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a>.<a class="code" href="structCDatabaseStats.html#ab317cc5ad2da6a68cdec37e71fd80f4f">mem_used_up</a> = <span class="keyword">false</span>;
<a name="l00519"></a>00519 <span class="keywordflow">if</span> (++<a class="code" href="classCDatabase.html#abb17b94a5d63adc740acbe28adb537dd">CDatabase::_stats</a>.mem_used_up_counts < 5) {
<a name="l00520"></a>00520 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> = (int) (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> * 0.8);
<a name="l00521"></a>00521 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> < 4)
<a name="l00522"></a>00522 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a> = 4;
<a name="l00523"></a>00523 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> = (int) (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a>* 0.8);
<a name="l00524"></a>00524 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> < 10)
<a name="l00525"></a>00525 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> = 10;
<a name="l00526"></a>00526 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> = (int) (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a>*0.8);
<a name="l00527"></a>00527 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> < 50 )
<a name="l00528"></a>00528 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> = 50;
<a name="l00529"></a>00529 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(
<a name="l00530"></a>00530 cout << <span class="stringliteral">"Forced to reduce unrelevance in clause deletion. "</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00531"></a>00531 cout <<<span class="stringliteral">"MaxUnrel: "</span> << <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a>
<a name="l00532"></a>00532 << <span class="stringliteral">" MinLenDel: "</span> << <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a>
<a name="l00533"></a>00533 << <span class="stringliteral">" MaxLenCL : "</span> << <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00534"></a>00534 );
<a name="l00535"></a>00535 }
<a name="l00536"></a>00536 }
<a name="l00537"></a>00537 <span class="comment">//first find out the clause to delete and mark them</span>
<a name="l00538"></a>00538 <span class="keywordflow">for</span> (vector<CClause>::iterator itr = <a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().begin() + <a class="code" href="classCDatabase.html#a25c0a024183a09bf973942b1e4865501">init_num_clauses</a>();
<a name="l00539"></a>00539 itr != <a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().end(); ++itr) {
<a name="l00540"></a>00540 <a class="code" href="classCClause.html">CClause</a> & cl = * itr;
<a name="l00541"></a>00541 <span class="keywordflow">if</span> (!cl.<a class="code" href="classCClause.html#accc3ecb433cd7ba00affc3180b0911d4">in_use</a>() || cl.<a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>() < <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a8747b9ca39f6cf7312f081d223634194">min_num_clause_lits_for_delete</a> ) <span class="keywordflow">continue</span>;
<a name="l00542"></a>00542 <span class="keywordtype">int</span> val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
<a name="l00543"></a>00543 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0; i< cl.<a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>(); ++i) {
<a name="l00544"></a>00544 <span class="keywordtype">int</span> lit_value = <a class="code" href="classCDatabase.html#ab0c8f1826cf8c92fc01943ab62d223df">literal_value</a> (cl.<a class="code" href="classCClause.html#aa9e91f96e80b94da2b28e3ab381b9acc">literal</a>(i));
<a name="l00545"></a>00545 <span class="keywordflow">if</span> (lit_value == 0 ) ++val_0_lits;
<a name="l00546"></a>00546 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (lit_value == 1) ++val_1_lits;
<a name="l00547"></a>00547 <span class="keywordflow">else</span> ++unknown_lits;
<a name="l00548"></a>00548 <span class="keywordflow">if</span> (unknown_lits + val_1_lits > <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a97c37504943c58e8cf1afc406018b027">max_unrelevance</a>) {
<a name="l00549"></a>00549 <a class="code" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">mark_clause_deleted</a>(cl);
<a name="l00550"></a>00550 <a class="code" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>.push(itr - <a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().begin());
<a name="l00551"></a>00551 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"Deleting Unrelevant clause: "</span> << cl << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00552"></a>00552 <span class="keywordflow">break</span>;
<a name="l00553"></a>00553 }
<a name="l00554"></a>00554 <span class="keywordflow">if</span> (cl.<a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>() > <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#af82455d9df59584dbf9f400cf6f918b1">max_conflict_clause_length</a> &&
<a name="l00555"></a>00555 (unknown_lits+val_1_lits > 1) ) { <span class="comment">//to make sure it's not generating an implication</span>
<a name="l00556"></a>00556 <span class="comment">//and it's not an antecedence for other var assignment</span>
<a name="l00557"></a>00557 <a class="code" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">mark_clause_deleted</a>(cl);
<a name="l00558"></a>00558 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"Deleting too large clause: "</span> << cl << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00559"></a>00559 <a class="code" href="classCDatabase.html#ae238340b46c3fc75854c4c244ae96d28">_unused_clause_idx_queue</a>.push(itr - <a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().begin());
<a name="l00560"></a>00560 <span class="keywordflow">break</span>;
<a name="l00561"></a>00561 }
<a name="l00562"></a>00562 }
<a name="l00563"></a>00563 }
<a name="l00564"></a>00564 <span class="comment">//now delete the index from variables</span>
<a name="l00565"></a>00565 <span class="keywordflow">if</span> (original_num_deleted == <a class="code" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a>())
<a name="l00566"></a>00566 return ; <span class="comment">//didn't delete anything</span>
<a name="l00567"></a>00567 <span class="keywordflow">for</span> (vector<CVariable>::iterator itr = <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().begin();
<a name="l00568"></a>00568 itr != <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().end(); ++ itr) {
<a name="l00569"></a>00569 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0; i<2; ++i) { <span class="comment">//for each phase</span>
<a name="l00570"></a>00570 <span class="comment">//delete the h_t index from the vars</span>
<a name="l00571"></a>00571 vector<CLitPoolElement *> & ht_ptr = (*itr).ht_ptr(i);
<a name="l00572"></a>00572 <span class="keywordflow">for</span> (vector<CLitPoolElement *>::iterator my_itr = ht_ptr.begin();
<a name="l00573"></a>00573 my_itr != ht_ptr.end(); ++my_itr) {
<a name="l00574"></a>00574 <span class="keywordflow">if</span> ( (*my_itr)->val() <= 0) {
<a name="l00575"></a>00575 *my_itr = ht_ptr.back();
<a name="l00576"></a>00576 ht_ptr.pop_back();
<a name="l00577"></a>00577 --my_itr;
<a name="l00578"></a>00578 }
<a name="l00579"></a>00579 }
<a name="l00580"></a>00580 }
<a name="l00581"></a>00581 }
<a name="l00582"></a>00582 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(cout << <span class="stringliteral">"Deleting "</span> << <a class="code" href="classCDatabase.html#ad386f2990781ab78ebbe6eb83b7c365e">num_deleted_clauses</a>() - original_num_deleted << <span class="stringliteral">" Clause "</span>;
<a name="l00583"></a>00583 cout << <span class="stringliteral">" and "</span> << <a class="code" href="classCDatabase.html#a3e0c56c9059f90ce0b3ba0f94e2aeed2">num_deleted_literals</a>() - original_del_lits << <span class="stringliteral">" Literals "</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00584"></a>00584 <a class="code" href="xchaff__utils_8h.html#a6683569480fcdbf7931a984f2738731c">CHECK_FULL</a> (<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00585"></a>00585 }
<a name="l00586"></a>00586 <span class="comment">//============================================================================================</span>
<a name="l00587"></a><a class="code" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">00587</a> <span class="keywordtype">bool</span> <a class="code" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">CSolver::time_out</a>(<span class="keywordtype">void</span>)
<a name="l00588"></a>00588 {
<a name="l00589"></a>00589 <span class="keywordflow">if</span> ( (<a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>() - <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#acf5b03d1d0c79232a13fcf20419a6e2c">start_cpu_time</a>)/1000.0 > <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a1904f8790a16c706e0d2ba51ce11c364">time_limit</a> )
<a name="l00590"></a>00590 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00591"></a>00591 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00592"></a>00592 }
<a name="l00593"></a>00593
<a name="l00594"></a><a class="code" href="xchaff__solver_8cpp.html#a044c6cf23b7a89698e33df8aae6ff024">00594</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="xchaff__solver_8cpp.html#a044c6cf23b7a89698e33df8aae6ff024">compare_var_stat</a>(<span class="keyword">const</span> pair<int, int> & v1,
<a name="l00595"></a>00595 <span class="keyword">const</span> pair<int, int> & v2)
<a name="l00596"></a>00596 {
<a name="l00597"></a>00597 <span class="keywordflow">if</span> (v1.second > v2.second) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00598"></a>00598 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00599"></a>00599 }
<a name="l00600"></a>00600
<a name="l00601"></a><a class="code" href="classCSolver.html#acc181946a5845c647818631415c22c22">00601</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#acc181946a5845c647818631415c22c22">CSolver::update_var_stats</a>(<span class="keywordtype">void</span>)
<a name="l00602"></a>00602 {
<a name="l00603"></a>00603 <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="l00604"></a>00604 <a class="code" href="classCVariable.html">CVariable</a> & var = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(i);
<a name="l00605"></a>00605 var.<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(0) = var.<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(0)/2 + var.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(0) - <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[0][i];
<a name="l00606"></a>00606 var.<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(1) = var.<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(1)/2 + var.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(1) - <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[1][i];
<a name="l00607"></a>00607 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[0][i] = var.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(0);
<a name="l00608"></a>00608 <a class="code" href="classCSolver.html#aec6d0a9cf59ad2da0dad717bea16efcb">_last_var_lits_count</a>[1][i] = var.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(1);
<a name="l00609"></a>00609 <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>[i-1] = pair<int, int>(i, var.<a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>());
<a name="l00610"></a>00610 }
<a name="l00611"></a>00611 ::stable_sort(<a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.begin(), <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.end(), <a class="code" href="xchaff__solver_8cpp.html#a044c6cf23b7a89698e33df8aae6ff024">compare_var_stat</a>);
<a name="l00612"></a>00612 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i<<a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.size(); ++i)
<a name="l00613"></a>00613 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(<a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>[i].first).<a class="code" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">var_score_pos</a>() = i;
<a name="l00614"></a>00614 <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a> = 0;
<a name="l00615"></a>00615 }
<a name="l00616"></a>00616
<a name="l00617"></a><a class="code" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">00617</a> <span class="keywordtype">bool</span> <a class="code" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">CSolver::decide_next_branch</a>(<span class="keywordtype">void</span>)
<a name="l00618"></a>00618 {
<a name="l00619"></a>00619 ++<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ac277ac957d61a2f1810ca0db1814b1c9">num_decisions</a>;
<a name="l00620"></a>00620 <span class="keywordflow">if</span> (!<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty()) {
<a name="l00621"></a>00621 <span class="comment">//some hook function did a decision, so skip my own decision making.</span>
<a name="l00622"></a>00622 <span class="comment">//if the front of implication queue is 0, that means it's finished</span>
<a name="l00623"></a>00623 <span class="comment">//because var index start from 1, so 2 *vid + sign won't be 0. </span>
<a name="l00624"></a>00624 <span class="comment">//else it's a valid decision.</span>
<a name="l00625"></a>00625 <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a> = 0; <span class="comment">//reset the max_score_position.</span>
<a name="l00626"></a>00626 <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.front().first;
<a name="l00627"></a>00627 }
<a name="l00628"></a>00628
<a name="l00629"></a>00629 <span class="keywordtype">int</span> s_var = 0, s_var2;
<a name="l00630"></a>00630 <span class="keywordtype">bool</span> done = <span class="keyword">false</span>;
<a name="l00631"></a>00631
<a name="l00632"></a>00632 <span class="keywordtype">unsigned</span> i, var_idx, sign;
<a name="l00633"></a>00633 <a class="code" href="classCVariable.html">CVariable</a> * ptr;
<a name="l00634"></a>00634
<a name="l00635"></a>00635 <span class="keywordflow">for</span> (i=<a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a>; i<<a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>.size(); ++i) {
<a name="l00636"></a>00636 var_idx = <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>[i].first;
<a name="l00637"></a>00637 ptr = &(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>()[var_idx]);
<a name="l00638"></a>00638 <span class="keywordflow">if</span> (ptr-><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>()==<a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) {
<a name="l00639"></a>00639 <span class="comment">//move th max score position pointer</span>
<a name="l00640"></a>00640 <a class="code" href="classCSolver.html#ae7e25a4d85f75c17d55cf64e26056920">_max_score_pos</a> = i;
<a name="l00641"></a>00641 <span class="comment">//make some randomness happen</span>
<a name="l00642"></a>00642 <span class="keywordflow">if</span> (--<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a> < <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">base_randomness</a>)
<a name="l00643"></a>00643 <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a> = <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adde3fd4026e6ce1a5598ac2766326e04">base_randomness</a>;
<a name="l00644"></a>00644
<a name="l00645"></a>00645 <span class="keywordtype">int</span> randomness = <a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a2c4888b23c0f7ea4a3a2ec654ddf83b5">randomness</a>;
<a name="l00646"></a>00646 <span class="keywordflow">if</span> (randomness >= <a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>())
<a name="l00647"></a>00647 randomness = <a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>() - 1;
<a name="l00648"></a>00648 <span class="keywordtype">int</span> skip =random()%(1+randomness);
<a name="l00649"></a>00649 <span class="keywordtype">int</span> index = i;
<a name="l00650"></a>00650 <span class="keywordflow">while</span> (skip > 0) {
<a name="l00651"></a>00651 ++index;
<a name="l00652"></a>00652 var_idx = <a class="code" href="classCSolver.html#a40c08e5478f016f460d6adec977c2446">_var_order</a>[index].first;
<a name="l00653"></a>00653 ptr = &(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>()[var_idx]);
<a name="l00654"></a>00654 <span class="keywordflow">if</span> (ptr-><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>()==<a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>)
<a name="l00655"></a>00655 --skip;
<a name="l00656"></a>00656 }
<a name="l00657"></a>00657 assert (ptr-><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>);
<a name="l00658"></a>00658 sign = ptr-><a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(0) > ptr-><a class="code" href="classCVariable.html#acf5cbd17ee39aa733dd5445c5836ec81">score</a>(1) ? 0 : 1;
<a name="l00659"></a>00659 s_var = var_idx + var_idx + sign;
<a name="l00660"></a>00660 <span class="keywordflow">break</span>;
<a name="l00661"></a>00661 }
<a name="l00662"></a>00662 }
<a name="l00663"></a>00663 <span class="keywordflow">if</span> (s_var < 2) done = <span class="keyword">true</span>;
<a name="l00664"></a>00664
<a name="l00665"></a>00665 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#af74159b82e953b3b766001d27b8b7981">_decision_hook</a>) {
<a name="l00666"></a>00666 decide:
<a name="l00667"></a>00667 s_var2 = (*_decision_hook)(<a class="code" href="classCSolver.html#a2a02aeed8e6eefe8b1d8a661c7e94c45">_decision_hook_cookie</a>, &done);
<a name="l00668"></a>00668 <span class="keywordflow">if</span> (done) {
<a name="l00669"></a>00669 <span class="keywordflow">if</span> (s_var2 == -1) {
<a name="l00670"></a>00670 <span class="comment">// No more decisions</span>
<a name="l00671"></a>00671 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00672"></a>00672 }
<a name="l00673"></a>00673 <span class="keywordflow">else</span> {
<a name="l00674"></a>00674 <span class="comment">// check for more work</span>
<a name="l00675"></a>00675 <span class="keywordflow">if</span> (!<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty() ||
<a name="l00676"></a>00676 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size() != 0)
<a name="l00677"></a>00677 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00678"></a>00678 <span class="keywordflow">else</span> <span class="keywordflow">goto</span> decide;
<a name="l00679"></a>00679 }
<a name="l00680"></a>00680 }
<a name="l00681"></a>00681 <span class="keywordflow">else</span> {
<a name="l00682"></a>00682 <span class="keywordflow">if</span> (s_var2 == -1) {
<a name="l00683"></a>00683 <span class="comment">// use SAT choice</span>
<a name="l00684"></a>00684 }
<a name="l00685"></a>00685 <span class="keywordflow">else</span> {
<a name="l00686"></a>00686 <span class="comment">// use decision</span>
<a name="l00687"></a>00687 s_var = s_var2;
<a name="l00688"></a>00688 }
<a name="l00689"></a>00689 }
<a name="l00690"></a>00690 }
<a name="l00691"></a>00691
<a name="l00692"></a>00692 <span class="keywordflow">if</span> (s_var<2) <span class="comment">//no more free vars, solution found, quit</span>
<a name="l00693"></a>00693 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00694"></a>00694 ++<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>();
<a name="l00695"></a>00695 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a>) {
<a name="l00696"></a>00696 (*_dlevel_hook)(<a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a>, 1);
<a name="l00697"></a>00697 }
<a name="l00698"></a>00698 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() > <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a>) <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a859161eb057e8035f34ea5fca4d65075">max_dlevel</a> = <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>();
<a name="l00699"></a>00699 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"**Decision at Level "</span> << <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() ;
<a name="l00700"></a>00700 cout <<<span class="stringliteral">": "</span> << s_var << <span class="stringliteral">"\te.g. "</span> << (s_var&0x1?<span class="stringliteral">"-"</span>:<span class="stringliteral">" "</span>) ;
<a name="l00701"></a>00701 cout <<(s_var>>1) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; );
<a name="l00702"></a>00702 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(s_var, <a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>);
<a name="l00703"></a>00703 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00704"></a>00704 }
<a name="l00705"></a>00705
<a name="l00706"></a><a class="code" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">00706</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">CSolver::preprocess</a>(<span class="keywordtype">bool</span> allowNewClauses)
<a name="l00707"></a>00707 {
<a name="l00708"></a>00708 <span class="comment">//1. detect all the unused variables</span>
<a name="l00709"></a>00709 <span class="keywordflow">if</span> (!allowNewClauses) {
<a name="l00710"></a>00710 vector<int> un_used;
<a name="l00711"></a>00711 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=1, sz=<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size(); i<sz; ++i) {
<a name="l00712"></a>00712 <a class="code" href="classCVariable.html">CVariable</a> & v = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(i);
<a name="l00713"></a>00713 <span class="keywordflow">if</span> (v.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(0) == 0 && v.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(1) == 0) {
<a name="l00714"></a>00714 un_used.push_back(i);
<a name="l00715"></a>00715 v.<a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() = 1;
<a name="l00716"></a>00716 v.<a class="code" href="classCVariable.html#aedac20571208b480adb2aff58797981a">dlevel</a>() = -1;
<a name="l00717"></a>00717 }
<a name="l00718"></a>00718 }
<a name="l00719"></a>00719 <a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>() -= un_used.size();
<a name="l00720"></a>00720 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a>>1 && un_used.size() > 0) {
<a name="l00721"></a>00721 cout << un_used.size()<< <span class="stringliteral">" Variables are defined but not used "</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00722"></a>00722 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a> > 2) {
<a name="l00723"></a>00723 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< un_used.size(); ++i)
<a name="l00724"></a>00724 cout << un_used[i] << <span class="stringliteral">" "</span>;
<a name="l00725"></a>00725 cout << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00726"></a>00726 }
<a name="l00727"></a>00727 }
<a name="l00728"></a>00728 <span class="comment">//2. detect all variables with only one phase occuring</span>
<a name="l00729"></a>00729 vector<int> uni_phased;
<a name="l00730"></a>00730 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=1, sz=<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>().size(); i<sz; ++i) {
<a name="l00731"></a>00731 <a class="code" href="classCVariable.html">CVariable</a> & v = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(i);
<a name="l00732"></a>00732 <span class="keywordflow">if</span> (v.<a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>)
<a name="l00733"></a>00733 <span class="keywordflow">continue</span>;
<a name="l00734"></a>00734 <span class="keywordflow">if</span> (v.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(0) == 0){ <span class="comment">//no positive phased lits.</span>
<a name="l00735"></a>00735 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>( i+i+1, <a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>);
<a name="l00736"></a>00736 uni_phased.push_back(-i);
<a name="l00737"></a>00737 }
<a name="l00738"></a>00738 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (v.<a class="code" href="classCVariable.html#a200c0dd2b0b7cadd109b662fb20ec889">lits_count</a>(1) == 0){ <span class="comment">//no negative phased lits.</span>
<a name="l00739"></a>00739 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>( i+i, <a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>);
<a name="l00740"></a>00740 uni_phased.push_back(i);
<a name="l00741"></a>00741 }
<a name="l00742"></a>00742 }
<a name="l00743"></a>00743 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a>>1 && uni_phased.size() > 0) {
<a name="l00744"></a>00744 cout << uni_phased.size()<< <span class="stringliteral">" Variables only appear in one phase."</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00745"></a>00745 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#adaaa1d95214368e99b13ac36cbb16dea">verbosity</a> > 2) {
<a name="l00746"></a>00746 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< uni_phased.size(); ++i)
<a name="l00747"></a>00747 cout << uni_phased[i] << <span class="stringliteral">" "</span>;
<a name="l00748"></a>00748 cout <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00749"></a>00749 }
<a name="l00750"></a>00750 }
<a name="l00751"></a>00751 }
<a name="l00752"></a>00752 <span class="comment">//3. detect all the unit clauses</span>
<a name="l00753"></a>00753 <span class="keywordflow">for</span> (<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> i=0, sz=<a class="code" href="classCDatabase.html#a0c2329a20ee0a2672475933c3edd888e">clauses</a>().size(); i<sz; ++i) {
<a name="l00754"></a>00754 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(i).<a class="code" href="classCClause.html#ae4f9f5a951b75aab530b5b05a3232082">num_lits</a>() == 1){ <span class="comment">//unit clause</span>
<a name="l00755"></a>00755 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(<a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(i), i);
<a name="l00756"></a>00756 }
<a name="l00757"></a>00757 }
<a name="l00758"></a>00758
<a name="l00759"></a>00759 <span class="keywordflow">if</span>(<a class="code" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a>()==<a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>) <span class="keywordflow">return</span> <a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>;
<a name="l00760"></a>00760 <span class="keywordflow">return</span> <a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a7980b2b643aebe4041a43b90e652c3fc">NO_CONFLICT</a>;
<a name="l00761"></a>00761 }
<a name="l00762"></a>00762
<a name="l00763"></a><a class="code" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">00763</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">CSolver::real_solve</a>(<span class="keywordtype">void</span>)
<a name="l00764"></a>00764 {
<a name="l00765"></a>00765 <span class="keywordflow">while</span>(1) {
<a name="l00766"></a>00766 <a class="code" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">run_periodic_functions</a>();
<a name="l00767"></a>00767 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a752f7912bef54fb9f310cbeeabc34543">decide_next_branch</a>() || !<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty() ||
<a name="l00768"></a>00768 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size() != 0) {
<a name="l00769"></a>00769 <span class="keywordflow">while</span> (<a class="code" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">deduce</a>()==<a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>) {
<a name="l00770"></a>00770 <span class="keywordtype">int</span> blevel = <a class="code" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">analyze_conflicts</a>();
<a name="l00771"></a>00771 <span class="keywordflow">if</span> (blevel <= 0) {
<a name="l00772"></a>00772 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>;
<a name="l00773"></a>00773 <span class="keywordflow">return</span>;
<a name="l00774"></a>00774 }
<a name="l00775"></a>00775 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>.size()) {
<a name="l00776"></a>00776 <span class="comment">// reassert added unit clauses</span>
<a name="l00777"></a>00777 <span class="keywordtype">unsigned</span> idx = <a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>.size()-1;
<a name="l00778"></a>00778 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl = <a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>.back();
<a name="l00779"></a>00779 <span class="keywordtype">int</span> lit = <a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(cl);
<a name="l00780"></a>00780 <span class="keywordflow">while</span> (lit != 0) {
<a name="l00781"></a>00781 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(lit, cl);
<a name="l00782"></a>00782 <span class="keywordflow">if</span> (idx == 0) <span class="keywordflow">break</span>;
<a name="l00783"></a>00783 cl = <a class="code" href="classCSolver.html#a6b12fb5fcb0e279221c4047b3a61d99e">_addedUnitClauses</a>[--idx];
<a name="l00784"></a>00784 lit = <a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(cl);
<a name="l00785"></a>00785 }
<a name="l00786"></a>00786 }
<a name="l00787"></a>00787 }
<a name="l00788"></a>00788 }
<a name="l00789"></a>00789 <span class="keywordflow">else</span> {
<a name="l00790"></a>00790 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baa6a5c07f8c320f440ebc34fed65eb550">SATISFIABLE</a>;
<a name="l00791"></a>00791 <span class="keywordflow">return</span>;
<a name="l00792"></a>00792 }
<a name="l00793"></a>00793 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#af3b17269840c1a07e21303c1fca4e5a0">time_out</a>()) {
<a name="l00794"></a>00794 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba52acca9974adc722d8bdd782fec68b55">TIME_OUT</a>;
<a name="l00795"></a>00795 <span class="keywordflow">return</span>;
<a name="l00796"></a>00796 }
<a name="l00797"></a>00797 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab5c8d00ed96f235136c96197230a09c7">is_mem_out</a>) {
<a name="l00798"></a>00798 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baff91e7382744a3692b5e8b812c24f9dd">MEM_OUT</a>;
<a name="l00799"></a>00799 <span class="keywordflow">return</span>;
<a name="l00800"></a>00800 }
<a name="l00801"></a>00801 }
<a name="l00802"></a>00802 }
<a name="l00803"></a>00803
<a name="l00804"></a><a class="code" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">00804</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a351fe372330bede0ada8c3723e844a8e">CSolver::solve</a>(<span class="keywordtype">bool</span> allowNewClauses)
<a name="l00805"></a>00805 {
<a name="l00806"></a>00806 <a class="code" href="classCSolver.html#a711b6b701409a5a5fa54dd54b609328b">init</a>();
<a name="l00807"></a>00807 <span class="comment">//preprocess </span>
<a name="l00808"></a>00808 <span class="keywordflow">if</span>(<a class="code" href="classCSolver.html#aef7418705a19f94876ab5c708e87e15c">preprocess</a>(allowNewClauses)==<a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>) {
<a name="l00809"></a>00809 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a457807a12c793c4ff53a56aefe246d51">outcome</a> = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>;
<a name="l00810"></a>00810 }
<a name="l00811"></a>00811 <span class="keywordflow">else</span> { <span class="comment">//the real search</span>
<a name="l00812"></a>00812 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a>) {
<a name="l00813"></a>00813 (*_dlevel_hook)(<a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a>, 1);
<a name="l00814"></a>00814 }
<a name="l00815"></a>00815 <a class="code" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a>();
<a name="l00816"></a>00816 }
<a name="l00817"></a>00817 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">finish_cpu_time</a> = <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>();
<a name="l00818"></a>00818 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">finish_world_time</a> = <a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>();
<a name="l00819"></a>00819 <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="l00820"></a>00820 }
<a name="l00821"></a>00821
<a name="l00822"></a><a class="code" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">00822</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a9119faa6145fead463e8b14ec2f7cf7b">CSolver::continueCheck</a>()
<a name="l00823"></a>00823 {
<a name="l00824"></a>00824 <a class="code" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">real_solve</a>();
<a name="l00825"></a>00825 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#af6278310a2420aa873287185f2625af8">finish_cpu_time</a> = <a class="code" href="classCSolver.html#a7d23251aefbab59adac9658723ac60ad">current_cpu_time</a>();
<a name="l00826"></a>00826 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a7e0257bf7aca5d36a9329827237ffd19">finish_world_time</a> = <a class="code" href="classCSolver.html#a4fc755c9adedc2769461bacfc8532f9e">current_world_time</a>();
<a name="l00827"></a>00827 <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="l00828"></a>00828 }
<a name="l00829"></a>00829
<a name="l00830"></a><a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">00830</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">CSolver::back_track</a>(<span class="keywordtype">int</span> blevel)
<a name="l00831"></a>00831 {
<a name="l00832"></a>00832 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a> (cout << <span class="stringliteral">"Back track to "</span> << blevel <<<span class="stringliteral">" ,currently in "</span><< <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() << <span class="stringliteral">" level"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;);
<a name="l00833"></a>00833 <a class="code" href="xchaff__utils_8h.html#a6683569480fcdbf7931a984f2738731c">CHECK_FULL</a> (<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00834"></a>00834 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(<a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>());
<a name="l00835"></a>00835 assert(blevel <= <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>());
<a name="l00836"></a>00836 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>(); i>= blevel; --i) {
<a name="l00837"></a>00837 vector<int> & assignments = *<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[i];
<a name="l00838"></a>00838 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> j=assignments.size()-1 ; j>=0; --j)
<a name="l00839"></a>00839 <a class="code" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">unset_var_value</a>(assignments[j]>>1);
<a name="l00840"></a>00840 <a class="code" href="classCSolver.html#a5b1c1a111284ece5745488b12baef8b2">num_free_variables</a>() += assignments.size();
<a name="l00841"></a>00841 assignments.clear();
<a name="l00842"></a>00842 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#ad517659e82e1b42617886d2b6758acd3">_dlevel_hook</a>) {
<a name="l00843"></a>00843 (*_dlevel_hook)(<a class="code" href="classCSolver.html#ad1e4bd711ad507a40d36d5815bdaa69c">_dlevel_hook_cookie</a>, -1);
<a name="l00844"></a>00844 }
<a name="l00845"></a>00845 }
<a name="l00846"></a>00846 <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() = blevel - 1;
<a name="l00847"></a>00847 ++<a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#a25040e610686ab4e75a582de624946db">num_backtracks</a>;
<a name="l00848"></a>00848 <a class="code" href="xchaff__utils_8h.html#a6683569480fcdbf7931a984f2738731c">CHECK_FULL</a> (<a class="code" href="classCSolver.html#a8804888a9795945f5b09c67c529b898d">dump</a>());
<a name="l00849"></a>00849 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(<a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>());
<a name="l00850"></a>00850 }
<a name="l00851"></a>00851
<a name="l00852"></a><a class="code" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">00852</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a769075f3a6ed6eab6e4ec9e93c964f89">CSolver::deduce</a>(<span class="keywordtype">void</span>)
<a name="l00853"></a>00853 {
<a name="l00854"></a>00854 <a class="code" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a>:
<a name="l00855"></a>00855 <span class="keywordflow">while</span> (!<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty() && <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size()==0) {
<a name="l00856"></a>00856 <span class="keywordtype">int</span> literal = <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.front().first;
<a name="l00857"></a>00857 <span class="keywordtype">int</span> variable_index = literal>>1;
<a name="l00858"></a>00858 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl = <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.front().second;
<a name="l00859"></a>00859 <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.pop();
<a name="l00860"></a>00860 <a class="code" href="classCVariable.html">CVariable</a> * the_var = &(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>()[variable_index]);
<a name="l00861"></a>00861 <span class="keywordflow">if</span> ( the_var-><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>) { <span class="comment">// an implication</span>
<a name="l00862"></a>00862 <span class="keywordtype">int</span> dl;
<a name="l00863"></a>00863 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a3e90abca92fa570f9d1dc5ce49b01daa">back_track_complete</a>)
<a name="l00864"></a>00864 dl = <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>();
<a name="l00865"></a>00865 <span class="keywordflow">else</span>
<a name="l00866"></a>00866 dl = <a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a>(cl);
<a name="l00867"></a>00867 <a class="code" href="classCSolver.html#ac06f1192d14de7730356cc102ebaee1b">set_var_value</a>(variable_index, !(literal&0x1), cl, dl);
<a name="l00868"></a>00868 the_var = &(<a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>()[variable_index]);
<a name="l00869"></a>00869 <a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[dl]->push_back(literal);
<a name="l00870"></a>00870 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(<a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">verify_integrity</a>());
<a name="l00871"></a>00871 }
<a name="l00872"></a>00872 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (the_var-><a class="code" href="classCVariable.html#a7319394585df665256e74df1282f992f">value</a>() == (literal&0x1) ) { <span class="comment">//a conflict</span>
<a name="l00873"></a>00873 <span class="comment">//note: literal & 0x1 == 1 means the literal is in negative phase</span>
<a name="l00874"></a>00874 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.push_back(cl);
<a name="l00875"></a>00875 }
<a name="l00876"></a>00876 }
<a name="l00877"></a>00877 <span class="keywordflow">if</span> (!<a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size() && <a class="code" href="classCSolver.html#ac30b332eb58a51d87d9e1f80f62754f8">_deduction_hook</a>) {
<a name="l00878"></a>00878 (*_deduction_hook)(<a class="code" href="classCSolver.html#aa2c250ed33c494f50d06122943ae280d">_deduction_hook_cookie</a>);
<a name="l00879"></a>00879 <span class="keywordflow">if</span> (!<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty()) <span class="keywordflow">goto</span> <a class="code" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">restart</a>;
<a name="l00880"></a>00880 }
<a name="l00881"></a>00881 <span class="keywordflow">while</span>(!<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty()) <a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.pop();
<a name="l00882"></a>00882 <span class="keywordflow">return</span> (<a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size()?<a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a3124eeef4801cbb117a96b9e4a0d7eb7">CONFLICT</a>:<a class="code" href="xchaff__solver_8h.html#a7b6c2d7ebb99756fa23352708c089b25a7980b2b643aebe4041a43b90e652c3fc">NO_CONFLICT</a>);
<a name="l00883"></a>00883 }
<a name="l00884"></a>00884
<a name="l00885"></a>00885
<a name="l00886"></a><a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">00886</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">CSolver::verify_integrity</a>(<span class="keywordtype">void</span>)
<a name="l00887"></a>00887 {
<a name="l00888"></a>00888 }
<a name="l00889"></a>00889
<a name="l00890"></a><a class="code" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">00890</a> <span class="keywordtype">void</span> <a class="code" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">CSolver::mark_vars_at_level</a>(<a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl, <span class="keywordtype">int</span> var_idx, <span class="keywordtype">int</span> dl)
<a name="l00891"></a>00891 {
<a name="l00892"></a>00892 <span class="keywordflow">for</span> (<a class="code" href="classCLitPoolElement.html">CLitPoolElement</a> * itr = <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl).literals(); (*itr).val() > 0 ; ++ itr) {
<a name="l00893"></a>00893 <span class="keywordtype">int</span> v = (*itr).var_index();
<a name="l00894"></a>00894 <span class="keywordflow">if</span> (v == var_idx)
<a name="l00895"></a>00895 <span class="keywordflow">continue</span>;
<a name="l00896"></a>00896 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() == dl) {
<a name="l00897"></a>00897 <span class="keywordflow">if</span> (!<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).is_marked()) {
<a name="l00898"></a>00898 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).<a class="code" href="classCVariable.html#a605e80794f39e7aa307d94fd13017431">set_marked</a>();
<a name="l00899"></a>00899 ++ <a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a>;
<a name="l00900"></a>00900 }
<a name="l00901"></a>00901 }
<a name="l00902"></a>00902 <span class="keywordflow">else</span> {
<a name="l00903"></a>00903 assert (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).<a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>() < dl);
<a name="l00904"></a>00904 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).in_new_cl() == -1){ <span class="comment">//it's not in the new cl</span>
<a name="l00905"></a>00905 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(v).<a class="code" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a>((*itr).var_sign());
<a name="l00906"></a>00906 <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.push_back((*itr).s_var());
<a name="l00907"></a>00907 }
<a name="l00908"></a>00908 }
<a name="l00909"></a>00909 }
<a name="l00910"></a>00910 }
<a name="l00911"></a>00911
<a name="l00912"></a><a class="code" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">00912</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a2d476175cdda3b0028fb0efd754630d6">CSolver::analyze_conflicts</a>(<span class="keywordtype">void</span>) {
<a name="l00913"></a>00913 <span class="keywordflow">return</span> <a class="code" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">conflict_analysis_zchaff</a>();
<a name="l00914"></a>00914 }
<a name="l00915"></a>00915
<a name="l00916"></a><a class="code" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">00916</a> <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a9329cbfb2ba31fe55352644822889242">CSolver::conflict_analysis_zchaff</a> (<span class="keywordtype">void</span>)
<a name="l00917"></a>00917 {
<a name="l00918"></a>00918 assert (<a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size());
<a name="l00919"></a>00919 assert (<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty());
<a name="l00920"></a>00920 assert (<a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a> == 0);
<a name="l00921"></a>00921 <span class="keywordtype">int</span> back_level = 0;
<a name="l00922"></a>00922 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> conflict_cl;
<a name="l00923"></a>00923 vector<ClauseIdx> added_conflict_clauses;
<a name="l00924"></a>00924 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz=<a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.size(); i<sz; ++i) {
<a name="l00925"></a>00925 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl = <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>[i];
<a name="l00926"></a>00926
<a name="l00927"></a>00927 <span class="keywordflow">if</span> (!<a class="code" href="classCDatabase.html#aeb01a55c31dfd135d9f19b561829e88d">is_conflict</a>(cl)) <span class="keywordflow">continue</span>;
<a name="l00928"></a>00928
<a name="l00929"></a>00929 back_level = 0; <span class="comment">// reset it</span>
<a name="l00930"></a>00930 <span class="keywordflow">while</span> (<a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.size()) {
<a name="l00931"></a>00931 <a class="code" href="classCVariable.html">CVariable</a> & var = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(<a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.back() >> 1);
<a name="l00932"></a>00932 <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.pop_back();
<a name="l00933"></a>00933 assert (var.<a class="code" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">in_new_cl</a>() != -1);
<a name="l00934"></a>00934 var.<a class="code" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a>(-1);
<a name="l00935"></a>00935 }
<a name="l00936"></a>00936 <span class="keywordtype">int</span> <a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a> = <a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a>(cl); <span class="comment">// find the max level, which is the back track level</span>
<a name="l00937"></a>00937 <span class="keywordtype">bool</span> first_time = <span class="keyword">true</span>; <span class="comment">//its the beginning</span>
<a name="l00938"></a>00938 <span class="keywordtype">bool</span> prev_is_uip = <span class="keyword">false</span>;
<a name="l00939"></a>00939 <a class="code" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">mark_vars_at_level</a> (cl, -1 <span class="comment">/*var*/</span>, max_dlevel);
<a name="l00940"></a>00940
<a name="l00941"></a>00941 vector <int> & assignments = *<a class="code" href="classCSolver.html#a6a21ab9d2ab20a5c4f103cc1a337e35f">_assignment_stack</a>[<a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>];
<a name="l00942"></a>00942 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> j = assignments.size() - 1; j >= 0; --j ) { <span class="comment">//now add conflict lits, and unassign vars</span>
<a name="l00943"></a>00943 <span class="keywordtype">int</span> assigned = assignments[j];
<a name="l00944"></a>00944 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(assigned>>1).<a class="code" href="classCVariable.html#a8be2f24a39402da9c9047c701c0e0486">is_marked</a>()) {
<a name="l00945"></a>00945 <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(assigned>>1).<a class="code" href="classCVariable.html#a474d619248f352afcaa3fd4fb6c8788d">clear_marked</a>();
<a name="l00946"></a>00946 -- <a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a>;
<a name="l00947"></a>00947 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> ante_cl = <a class="code" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">variables</a>()[assigned>>1].get_antecedence();
<a name="l00948"></a>00948
<a name="l00949"></a>00949 <span class="keywordflow">if</span> ( (<a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a> == 0 &&
<a name="l00950"></a>00950 (!first_time) &&
<a name="l00951"></a>00951 (prev_is_uip == <span class="keyword">false</span>))
<a name="l00952"></a>00952 || ante_cl==<a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a>) { <span class="comment">//conclude add clause</span>
<a name="l00953"></a>00953 assert (<a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(assigned>>1).in_new_cl()==-1);
<a name="l00954"></a>00954 <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.push_back(assigned^0x1); <span class="comment">// add this assignment's reverse, e.g. UIP</span>
<a name="l00955"></a>00955 <span class="keywordtype">int</span> conflict_cl = <a class="code" href="classCSolver.html#a5f90fcc1b1a7994a94fc8395d95cfb38">add_clause</a>(<a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>, <span class="keyword">false</span>);
<a name="l00956"></a>00956 <span class="keywordflow">if</span> (conflict_cl < 0 ) {
<a name="l00957"></a>00957 <a class="code" href="classCSolver.html#a5f656ea799ff4b4304b9f4f71a4df315">_stats</a>.<a class="code" href="structCSolverStats.html#ab5c8d00ed96f235136c96197230a09c7">is_mem_out</a> = <span class="keyword">true</span>;
<a name="l00958"></a>00958 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.clear();
<a name="l00959"></a>00959 assert (<a class="code" href="classCSolver.html#aeab7cd8f6085990a2a1ed518c9d75c6e">_implication_queue</a>.empty());
<a name="l00960"></a>00960 <span class="keywordflow">return</span> 1;
<a name="l00961"></a>00961 }
<a name="l00962"></a>00962 <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.pop_back(); <span class="comment">// remove for continue use of _conflict_lits</span>
<a name="l00963"></a>00963 added_conflict_clauses.push_back(conflict_cl);
<a name="l00964"></a>00964
<a name="l00965"></a>00965 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(cout <<<span class="stringliteral">"Conflict clause: "</span> << cl << <span class="stringliteral">" : "</span> << <a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(cl) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00966"></a>00966 cout << <span class="stringliteral">"**Add Clause "</span> <<conflict_cl<< <span class="stringliteral">" : "</span><<<a class="code" href="classCDatabase.html#a5af3586dfcd579ab14d37c6b6cf75e18">clause</a>(conflict_cl) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00967"></a>00967 );
<a name="l00968"></a>00968
<a name="l00969"></a>00969 prev_is_uip = <span class="keyword">true</span>;
<a name="l00970"></a>00970 <span class="keywordflow">break</span>; <span class="comment">//if do this, only one clause will be added.</span>
<a name="l00971"></a>00971 }
<a name="l00972"></a>00972 <span class="keywordflow">else</span> prev_is_uip = <span class="keyword">false</span>;
<a name="l00973"></a>00973
<a name="l00974"></a>00974 <span class="keywordflow">if</span> ( ante_cl != <a class="code" href="xchaff__base_8h.html#abd4c1edc3bf20c1f93ebaca33c9b2b64">NULL_CLAUSE</a> )
<a name="l00975"></a>00975 <a class="code" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">mark_vars_at_level</a>(ante_cl, assigned>>1<span class="comment">/*var*/</span>, max_dlevel);
<a name="l00976"></a>00976 <span class="keywordflow">else</span>
<a name="l00977"></a>00977 assert (j == 0);
<a name="l00978"></a>00978 first_time = <span class="keyword">false</span>;
<a name="l00979"></a>00979 }
<a name="l00980"></a>00980 }
<a name="l00981"></a>00981 back_level = <a class="code" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">max_dlevel</a>;
<a name="l00982"></a>00982 <a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a>(max_dlevel);
<a name="l00983"></a>00983 }
<a name="l00984"></a>00984 assert (<a class="code" href="classCSolver.html#a528d66d18534a7d6e73a2e7964103b1c">_num_marked</a> == 0);
<a name="l00985"></a>00985 <span class="keywordflow">if</span> (back_level==0) <span class="comment">//there are nothing to be done</span>
<a name="l00986"></a>00986 <span class="keywordflow">return</span> back_level;
<a name="l00987"></a>00987
<a name="l00988"></a>00988 <span class="keywordflow">if</span> (<a class="code" href="classCSolver.html#a30e5a80e5be76e6be4398340f3925818">_params</a>.<a class="code" href="structCSolverParameters.html#a3e90abca92fa570f9d1dc5ce49b01daa">back_track_complete</a>) {
<a name="l00989"></a>00989 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i=0; i< added_conflict_clauses.size(); ++i) {
<a name="l00990"></a>00990 <a class="code" href="xchaff__base_8h.html#a10b9683e115e9c10c0874794507db545">ClauseIdx</a> cl = added_conflict_clauses[i];
<a name="l00991"></a>00991 <span class="keywordflow">if</span> (<a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(cl)) { <span class="comment">//i.e. if it's a unit clause</span>
<a name="l00992"></a>00992 <span class="keywordtype">int</span> dl = <a class="code" href="classCSolver.html#a15a8ac75d8da0e7e47c0643870b3bcc9">find_max_clause_dlevel</a>(cl);
<a name="l00993"></a>00993 <span class="keywordflow">if</span> (dl < <a class="code" href="classCSolver.html#ad51e4ee566b488f8d3610890f3fa1bb7">dlevel</a>()) { <span class="comment">//thus make sure implied vars are at current dl.</span>
<a name="l00994"></a>00994 <a class="code" href="classCSolver.html#a48ffc1b95c078bcc0bb748f1068479fd">back_track</a>(dl+1);
<a name="l00995"></a>00995 }
<a name="l00996"></a>00996 }
<a name="l00997"></a>00997 }
<a name="l00998"></a>00998 }
<a name="l00999"></a>00999 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i=0, sz=added_conflict_clauses.size(); i<sz; ++i) {
<a name="l01000"></a>01000 conflict_cl = added_conflict_clauses[i];
<a name="l01001"></a>01001 <span class="keywordtype">int</span> lit = <a class="code" href="classCDatabase.html#a3e469952453c4b10f1040e9a19375f77">find_unit_literal</a>(conflict_cl);
<a name="l01002"></a>01002 <span class="keywordflow">if</span> (lit) {
<a name="l01003"></a>01003 <a class="code" href="classCSolver.html#a21e170987f92adbe179f39ffe3c861be">queue_implication</a>(lit, conflict_cl);
<a name="l01004"></a>01004 }
<a name="l01005"></a>01005 }
<a name="l01006"></a>01006
<a name="l01007"></a>01007 <a class="code" href="classCSolver.html#a6bba00c21025040cc46a0499eaea7f01">_conflicts</a>.clear();
<a name="l01008"></a>01008
<a name="l01009"></a>01009 <span class="keywordflow">while</span> (<a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.size()) {
<a name="l01010"></a>01010 <a class="code" href="classCVariable.html">CVariable</a> & var = <a class="code" href="classCDatabase.html#af421024d0ade14743332069684aba162">variable</a>(<a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.back() >> 1);
<a name="l01011"></a>01011 <a class="code" href="classCSolver.html#ab162797183d22466c24feb117fefc7d6">_conflict_lits</a>.pop_back();
<a name="l01012"></a>01012 assert (var.<a class="code" href="classCVariable.html#a106db2a07df4461da1ccfdf17faa8cdf">in_new_cl</a>() != -1);
<a name="l01013"></a>01013 var.<a class="code" href="classCVariable.html#a74c853f04808a514d7c99514a7583e2d">set_in_new_cl</a>(-1);
<a name="l01014"></a>01014 }
<a name="l01015"></a>01015 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>( <a class="code" href="classCSolver.html#a60c64d82a19286ac5774adce294aa16a">dump_assignment_stack</a>(););
<a name="l01016"></a>01016 <a class="code" href="xchaff__utils_8h.html#a763ffd798508592c5092ac77daa5a659">CHECK</a>(cout << <span class="stringliteral">"Conflict Analasis: conflict at level: "</span> << back_level;
<a name="l01017"></a>01017 cout << <span class="stringliteral">" Assertion Clause is "</span> << conflict_cl<< <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; );
<a name="l01018"></a>01018 <span class="keywordflow">return</span> back_level;
<a name="l01019"></a>01019 }
<a name="l01020"></a>01020
<a name="l01021"></a>01021
<a name="l01022"></a>01022
<a name="l01023"></a>01023
<a name="l01024"></a>01024
<a name="l01025"></a>01025
<a name="l01026"></a>01026
<a name="l01027"></a>01027
<a name="l01028"></a>01028
<a name="l01029"></a>01029
<a name="l01030"></a>01030
<a name="l01031"></a>01031
<a name="l01032"></a>01032
<a name="l01033"></a>01033
<a name="l01034"></a>01034
<a name="l01035"></a>01035
</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>
