// *********************************************************************// Copyright 2000-2004, Princeton University.  All rights reserved.// By using this software the USER indicates that he or she has read,// understood and will comply with the following://// --- Princeton University hereby grants USER nonexclusive permission// to use, copy and/or modify this software for internal, noncommercial,// research purposes only. Any distribution, including commercial sale// or license, of this software, copies of the software, its associated// documentation and/or modifications of either is strictly prohibited// without the prior consent of Princeton University.  Title to copyright// to this software and its associated documentation shall at all times// remain with Princeton University.  Appropriate copyright notice shall// be placed on all software copies, and a complete copy of this notice// shall be included in all copies of the associated documentation.// No right is  granted to use in advertising, publicity or otherwise// any trademark, service mark, or the name of Princeton University.////// --- This software and any associated documentation is provided "as is"//// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A// PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.//// Princeton University shall not be liable under any circumstances for// any direct, indirect, special, incidental, or consequential damages// with respect to any claim by USER or any third party on account of// or arising from the use, or inability to use, this software or its// associated documentation, even if Princeton University has been advised// of the possibility of those damages.// ********************************************************************#include <iostream>#include <algorithm>#include <fstream>#include <vector>#include <map>#include <set>#include <queue>using namespace std;#include "zchaff_solver.h"// #define VERIFY_ON#ifdef VERIFY_ONofstream verify_out("resolve_trace");#endifvoid CSolver::re_init_stats(void) {  _stats.is_mem_out           = false;  _stats.outcome              = UNDETERMINED;  _stats.next_restart         = _params.restart.first_restart;  _stats.restart_incr         = _params.restart.backtrack_incr;  _stats.next_cls_deletion    = _params.cls_deletion.interval;  _stats.next_var_score_decay = _params.decision.decay_period;  _stats.current_randomness   = _params.decision.base_randomness;  _stats.total_bubble_move            = 0;  _stats.num_decisions                = 0;  _stats.num_decisions_stack_conf     = 0;  _stats.num_decisions_vsids          = 0;  _stats.num_decisions_shrinking      = 0;  _stats.num_backtracks               = 0;  _stats.max_dlevel                   = 0;  _stats.num_implications             = 0;  _stats.num_restarts                 = 0;  _stats.num_del_orig_cls             = 0;  _stats.num_shrinkings               = 0;  _stats.start_cpu_time               = get_cpu_time();  _stats.finish_cpu_time              = 0;  _stats.random_seed                  = 0;}void CSolver::init_stats(void) {  re_init_stats();  _stats.been_reset                   = true;  _stats.num_free_variables           = 0;  _stats.num_free_branch_vars         = 0;}void CSolver::init_parameters(void) {  _params.verbosity                           = 0;  _params.time_limit                          = 3600 * 24;  // a day  _params.shrinking.size                      = 95;  _params.shrinking.enable                    = true;  _params.shrinking.upper_bound               = 800;  _params.shrinking.lower_bound               = 600;  _params.shrinking.upper_delta               = -5;  _params.shrinking.lower_delta               = 10;  _params.shrinking.window_width              = 20;  _params.shrinking.bound_update_frequency    = 20;  _params.decision.base_randomness            = 0;  _params.decision.decay_period               = 40;  _params.decision.bubble_init_step           = 0x400;  _params.cls_deletion.enable                 = true ;  _params.cls_deletion.head_activity          = 500;  _params.cls_deletion.tail_activity          = 10;  _params.cls_deletion.head_num_lits          = 6;  _params.cls_deletion.tail_num_lits          = 45;  _params.cls_deletion.tail_vs_head           = 16;  _params.cls_deletion.interval               = 600;  _params.restart.enable                      = true;  _params.restart.interval                    = 700;  _params.restart.first_restart               = 7000;  _params.restart.backtrack_incr              = 700;}CSolver::CSolver(void) {  init_parameters();  init_stats();  _dlevel                       = 0;  _force_terminate              = false;  _implication_id               = 0;  _num_marked                   = 0;  _num_in_new_cl                = 0;  _outside_constraint_hook      = NULL;  _sat_hook                     = NULL;}CSolver::~CSolver(void) {  while (!_assignment_stack.empty()) {    delete _assignment_stack.back();    _assignment_stack.pop_back();  }}void CSolver::set_time_limit(float t) {  _params.time_limit = t;}float CSolver::elapsed_cpu_time(void) {  return get_cpu_time() - _stats.start_cpu_time;}float CSolver::cpu_run_time(void) {  return (_stats.finish_cpu_time - _stats.start_cpu_time);}void CSolver::set_variable_number(int n) {  assert(num_variables() == 0);  CDatabase::set_variable_number(n);  _stats.num_free_variables = num_variables();  while (_assignment_stack.size() <= num_variables())    _assignment_stack.push_back(new vector<int>);  assert(_assignment_stack.size() == num_variables() + 1);}int CSolver::add_variable(void) {  int num = CDatabase::add_variable();  ++_stats.num_free_variables;  while (_assignment_stack.size() <= num_variables())    _assignment_stack.push_back(new vector<int>);  assert(_assignment_stack.size() == num_variables() + 1);  return num;}void CSolver::set_mem_limit(int s) {  CDatabase::set_mem_limit(s);}void CSolver::set_randomness(int n) {  _params.decision.base_randomness = n;}void CSolver::set_random_seed(int seed) {  srand(seed);}void CSolver::enable_cls_deletion(bool allow) {  _params.cls_deletion.enable = allow;}void CSolver::add_hook(HookFunPtrT fun, int interval) {  pair<HookFunPtrT, int> a(fun, interval);  _hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a));}void CSolver::run_periodic_functions(void) {  // a. restart  if (_params.restart.enable && _stats.num_backtracks > _stats.next_restart &&      _shrinking_cls.empty()) {    _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;    delete_unrelevant_clauses();    restart();    if (_stats.num_restarts % 5 == 1)      compact_lit_pool();    cout << "\rDecision: " << _assignment_stack[0]->size() << "/"         <<num_variables() << "\tTime: " << get_cpu_time() -           _stats.start_cpu_time << "/" << _params.time_limit << flush;  }  // b. decay variable score  if (_stats.num_backtracks > _stats.next_var_score_decay) {    _stats.next_var_score_decay = _stats.num_backtracks +                                  _params.decision.decay_period;    decay_variable_score();  }  // c. run hook functions  for (unsigned i = 0; i< _hooks.size(); ++i) {    pair<int, pair<HookFunPtrT, int> > & hook = _hooks[i];    if (_stats.num_decisions >= hook.first) {      hook.first += hook.second.second;      hook.second.first((void *) this);    }  }}void CSolver::init_solve(void) {  CDatabase::init_stats();  re_init_stats();  _stats.been_reset = false;  assert(_conflicts.empty());  assert(_conflict_lits.empty());  assert(_num_marked == 0);  assert(_num_in_new_cl == 0);  assert(_dlevel == 0);  for (unsigned i = 0, sz = variables()->size(); i < sz; ++i) {    variable(i).score(0) = variable(i).lits_count(0);    variable(i).score(1) = variable(i).lits_count(1);  }  _ordered_vars.resize(num_variables());  update_var_score();  set_random_seed(_stats.random_seed);  top_unsat_cls = clauses()->size() - 1;  _stats.shrinking_benefit = 0;  _shrinking_cls.clear();  _stats.shrinking_cls_length = 0;}void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl) {    assert(value == 0 || value == 1);    CVariable & var = variable(v);    assert(var.value() == UNKNOWN);    assert(dl == dlevel());    var.set_dlevel(dl);    var.set_value(value);    var.antecedent() = ante;    var.assgn_stack_pos() = _assignment_stack[dl]->size();    _assignment_stack[dl]->push_back(v * 2 + !value);    set_var_value_BCP(v, value);    ++_stats.num_implications ;    if (var.is_branchable())        --num_free_variables();}void CSolver::set_var_value_BCP(int v, int value) {  vector<CLitPoolElement *> & watchs = variable(v).watched(value);  for (vector <CLitPoolElement *>::iterator itr = watchs.begin();       itr != watchs.end(); ++itr) {    ClauseIdx cl_idx;    CLitPoolElement * other_watched = *itr;    CLitPoolElement * watched = *itr;    int dir = watched->direction();    CLitPoolElement * ptr = watched;    while (true) {      ptr += dir;      if (ptr->val() <= 0) {  // reached one end of the clause        if (dir == 1)  // reached the right end, i.e. spacing element is cl_id          cl_idx = ptr->get_clause_index();        if (dir == watched->direction()) {  // we haven't go both directions.          ptr = watched;          dir = -dir;                     // change direction, go the other way          continue;        }        // otherwise, we have already go through the whole clause        int the_value = literal_value(*other_watched);        if (the_value == 0)  // a conflict          _conflicts.push_back(cl_idx);        else if (the_value != 1)  // i.e. unknown          queue_implication(other_watched->s_var(), cl_idx);        break;      }      if (ptr->is_watched()) {  // literal is the other watched lit, skip it.        other_watched = ptr;        continue;      }      if (literal_value(*ptr) == 0)  // literal value is 0, keep going        continue;      // now the literal's value is either 1 or unknown, watch it instead      int v1 = ptr->var_index();      int sign = ptr->var_sign();      variable(v1).watched(sign).push_back(ptr);      ptr->set_watch(dir);      // remove the original watched literal from watched list      watched->unwatch();      *itr = watchs.back();  // copy the last element in it's place      watchs.pop_back();     // remove the last element      --itr;                 // do this so with don't skip one during traversal      break;    }  }}void CSolver::unset_var_value(int v) {  if (v == 0)    return;  CVariable & var = variable(v);  var.set_value(UNKNOWN);  var.set_antecedent(NULL_CLAUSE);  var.set_dlevel(-1);  var.assgn_stack_pos() = -1;  if (var.is_branchable()) {    ++num_free_variables();    if (var.var_score_pos() < _max_score_pos)      _max_score_pos = var.var_score_pos();  }}void CSolver::dump_assignment_stack(ostream & os ) {  os << "Assignment Stack:  ";  for (int i = 0; i <= dlevel(); ++i) {    os << "(" <<i << ":";    for (unsigned j = 0; j < (*_assignment_stack[i]).size(); ++j) {      os << ((*_assignment_stack[i])[j]&0x1?"-":"+")         << ((*_assignment_stack[i])[j] >> 1) << " ";    }    os << ") " << endl;  }  os << endl;}void CSolver::dump_implication_queue(ostream & os) {  _implication_queue.dump(os);}void CSolver::delete_clause_group(int gid) {  assert(is_gid_allocated(gid));  if (_stats.been_reset == false)    reset();  // if delete some clause, then implication queue are invalidated  for (vector<CClause>::iterator itr = clauses()->begin();       itr != clauses()->end(); ++itr) {    CClause & cl = *itr;    if (cl.status() != DELETED_CL) {      if (cl.gid(gid) == true) {        mark_clause_deleted(cl);      }    }  }  // delete the index from variables  for (vector<CVariable>::iterator itr = variables()->begin();         itr != variables()->end(); ++itr) {    for (unsigned i = 0; i < 2; ++i) {  // for each phase      // delete the lit index from the vars#ifdef KEEP_LIT_CLAUSES      vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);      for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();           itr1 != lit_clauses.end(); ++itr1) {        if (clause(*itr1).status() == DELETED_CL) {          *itr1 = lit_clauses.back();          lit_clauses.pop_back();          --itr1;        }      }#endif      // delete the watched index from the vars      vector<CLitPoolElement *> & watched = (*itr).watched(i);      for (vector<CLitPoolElement *>::iterator itr1 = watched.begin();           itr1 != watched.end(); ++itr1) {        if ((*itr1)->val() <= 0) {          *itr1 = watched.back();          watched.pop_back();