// *********************************************************************// 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 <cstdlib>#include <iostream>#include <vector>#include <set>using namespace std;#include "zchaff_dbase.h"CDatabase::CDatabase(void) {  _stats.mem_used_up                 = false;  _stats.init_num_clauses            = 0;  _stats.init_num_literals           = 0;  _stats.num_added_clauses           = 0;  _stats.num_added_literals          = 0;  _stats.num_deleted_clauses         = 0;  _stats.num_del_orig_cls            = 0;  _stats.num_deleted_literals        = 0;  _stats.num_enlarge                 = 0;  _stats.num_compact                 = 0;  _lit_pool_start = (CLitPoolElement *) malloc(sizeof(CLitPoolElement) *                                               STARTUP_LIT_POOL_SIZE);  _lit_pool_finish = _lit_pool_start;  _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;  lit_pool_push_back(0);  // set the first element as a dummy element  _params.mem_limit = 1024 * 1024 * 1024;  // that's 1 G  variables()->resize(1);                  // var_id == 0 is never used.  _allocated_gid                    = 0;}CDatabase::~CDatabase(void) {  free(_lit_pool_start);}unsigned CDatabase::estimate_mem_usage(void) {  unsigned mem_lit_pool = sizeof(CLitPoolElement) * (lit_pool_size() +                                                     lit_pool_free_space());  unsigned mem_vars = sizeof(CVariable) * variables()->capacity();  unsigned mem_cls = sizeof(CClause) * clauses()->capacity();  unsigned mem_cls_queue = sizeof(int) * _unused_clause_idx.size();  unsigned mem_watched = 2 * num_clauses() * sizeof(CLitPoolElement *);  unsigned mem_lit_clauses = 0;#ifdef KEEP_LIT_CLAUSES  mem_lit_clauses = num_literals() * sizeof(ClauseIdx);#endif  return (mem_lit_pool + mem_vars + mem_cls +          mem_cls_queue + mem_watched + mem_lit_clauses);}unsigned CDatabase::mem_usage(void) {  int mem_lit_pool = (lit_pool_size() + lit_pool_free_space()) *                     sizeof(CLitPoolElement);  int mem_vars = sizeof(CVariable) * variables()->capacity();  int mem_cls = sizeof(CClause) * clauses()->capacity();  int mem_cls_queue = sizeof(int) * _unused_clause_idx.size();  int mem_watched = 0, mem_lit_clauses = 0;  for (unsigned i = 0, sz = variables()->size(); i < sz ;  ++i) {    CVariable & v = variable(i);    mem_watched        += v.watched(0).capacity() + v.watched(1).capacity();#ifdef KEEP_LIT_CLAUSES    mem_lit_clauses += v.lit_clause(0).capacity() + v.lit_clause(1).capacity();#endif  }  mem_watched *= sizeof(CLitPoolElement*);  mem_lit_clauses *= sizeof(ClauseIdx);  return (mem_lit_pool + mem_vars + mem_cls +          mem_cls_queue + mem_watched + mem_lit_clauses);}int CDatabase::alloc_gid(void) {  for (unsigned i = 1; i <= WORD_WIDTH; ++i) {    if (is_gid_allocated(i) == false) {      _allocated_gid |= (1 << (i-1));      return i;    }  }  warning(_POSITION_, "Not enough GID");  return VOLATILE_GID;}void CDatabase::free_gid(int gid) {  assert(gid > 0 && "Can't free volatile or permanent group");  assert(gid <= WORD_WIDTH && "gid > WORD_WIDTH?");  if (!is_gid_allocated(gid)) {    fatal(_POSITION_, "Can't free unallocated GID");  }  _allocated_gid &= (~(1<< (gid-1)));}bool CDatabase::is_gid_allocated(int gid) {  if (gid == VOLATILE_GID || gid == PERMANENT_GID)    return true;  assert(gid <= WORD_WIDTH && gid > 0);  if (_allocated_gid & (1 << (gid -1)))    return true;  return false;}int CDatabase::merge_clause_group(int g2, int g1) {  assert(g1 >0 && g2> 0 && "Can't merge with permanent or volatile group");  assert(g1 != g2);  assert(is_gid_allocated(g1) && is_gid_allocated(g2));  for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) {    if (clause(i).status() != DELETED_CL) {      if (clause(i).gid(g1) == true) {        clause(i).clear_gid(g1);        clause(i).set_gid(g2);      }    }  }  free_gid(g1);  return g2;}void CDatabase::mark_clause_deleted(CClause & cl) {  ++_stats.num_deleted_clauses;  _stats.num_deleted_literals += cl.num_lits();  CLAUSE_STATUS status = cl.status();  if (status == ORIGINAL_CL)     _stats.num_del_orig_cls++;  cl.set_status(DELETED_CL);  for (unsigned i = 0; i < cl.num_lits(); ++i) {    CLitPoolElement & l = cl.literal(i);    --variable(l.var_index()).lits_count(l.var_sign());    l.val() = 0;  }  _unused_clause_idx.insert(&cl - &(*clauses()->begin()));}bool CDatabase::is_conflicting(ClauseIdx cl) {  CLitPoolElement * lits = clause(cl).literals();  for (int i = 0, sz= clause(cl).num_lits(); i < sz;  ++i) {    if (literal_value(lits[i]) != 0)      return false;  }  return true;}bool CDatabase::is_satisfied(ClauseIdx cl) {  CLitPoolElement * lits = clause(cl).literals();  for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {    if (literal_value(lits[i]) == 1)      return true;  }  return false;}bool CDatabase::is_unit(ClauseIdx cl) {  int num_unassigned = 0;  CLitPoolElement * lits = clause(cl).literals();  for (unsigned i = 0, sz= clause(cl).num_lits(); i < sz;  ++i) {    int value = literal_value(lits[i]);    if (value == 1)      return false;    else if (value != 0)      ++num_unassigned;  }  return num_unassigned == 1;}int CDatabase::find_unit_literal(ClauseIdx cl) {  // will return 0 if not unit  int unit_lit = 0;  for (int i = 0, sz = clause(cl).num_lits(); i < sz;  ++i) {    int value = literal_value(clause(cl).literal(i));    if (value == 1)      return 0;    else if (value != 0) {      if (unit_lit == 0)        unit_lit = clause(cl).literals()[i].s_var();      else        return 0;    }  }  return unit_lit;}inline CLitPoolElement * CDatabase::lit_pool_begin(void) {  return _lit_pool_start;}inline CLitPoolElement * CDatabase::lit_pool_end(void) {  return _lit_pool_finish;}inline void CDatabase::lit_pool_incr_size(int size) {  _lit_pool_finish += size;  assert(_lit_pool_finish <= _lit_pool_end_storage);}inline void CDatabase::lit_pool_push_back(int value) {  assert(_lit_pool_finish <= _lit_pool_end_storage);  _lit_pool_finish->val() = value;  ++_lit_pool_finish;}inline int CDatabase::lit_pool_size(void) {  return _lit_pool_finish - _lit_pool_start;}inline int CDatabase::lit_pool_free_space(void) {  return _lit_pool_end_storage - _lit_pool_finish;}