zchaff64/zchaff_base.cpp

   1 // /*********************************************************************
   2 //  Copyright 2000-2004, Princeton University.  All rights reserved.
   3 //  By using this software the USER indicates that he or she has read,
   4 //  understood and will comply with the following:
   5 //
   6 //  --- Princeton University hereby grants USER nonexclusive permission
   7 //  to use, copy and/or modify this software for internal, noncommercial,
   8 //  research purposes only. Any distribution, including commercial sale
   9 //  or license, of this software, copies of the software, its associated
  10 //  documentation and/or modifications of either is strictly prohibited
  11 //  without the prior consent of Princeton University.  Title to copyright
  12 //  to this software and its associated documentation shall at all times
  13 //  remain with Princeton University.  Appropriate copyright notice shall
  14 //  be placed on all software copies, and a complete copy of this notice
  15 //  shall be included in all copies of the associated documentation.
  16 //  No right is  granted to use in advertising, publicity or otherwise
  17 //  any trademark,  service mark, or the name of Princeton University.
  18 //
  19 //
  20 //  --- This software and any associated documentation is provided "as is"
  21 //
  22 //  PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 //  OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 //  PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 //  ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 //  TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 //  Princeton University shall not be liable under any circumstances for
  29 //  any direct, indirect, special, incidental, or consequential damages
  30 //  with respect to any claim by USER or any third party on account of
  31 //  or arising from the use, or inability to use, this software or its
  32 //  associated documentation, even if Princeton University has been advised
  33 //  of the possibility of those damages.
  34 // *********************************************************************/
  35
  36 #include <iostream>
  37 #include <vector>
  38
  39 using namespace std;
  40
  41 #include "zchaff_base.h"
  42
  43 void CLitPoolElement::dump(ostream & os) {
  44   os << (var_sign() ? " -" : " +") << var_index();
  45   if (is_watched())
  46     os << "*";
  47 }
  48
  49 void CClause::dump(ostream & os) {
  50   if (status() == DELETED_CL)
  51     os << "\t\t\t======removed=====";
  52   for (int i = 0, sz = num_lits(); i < sz; ++i)
  53     os << literal(i);
  54   os << endl;
  55 }
  56
  57 bool CClause::self_check(void) {
  58   assert(num_lits() > 0);
  59   int watched = 0;
  60   for (unsigned i = 0; i < num_lits(); ++i) {
  61     assert(literal(i).is_literal());
  62     if (literal(i).is_watched())
  63       ++watched;
  64   }
  65   assert(num_lits() ==1 || watched == 2);  // either unit, or have two watched
  66   assert(!literal(num_lits() + 1).is_literal());
  67   return true;
  68 }
  69
  70 bool CVariable::self_check(void) {
  71   for (unsigned i = 0; i < 2; ++i) {
  72     vector<CLitPoolElement*>& w = watched(i);
  73     for (unsigned j = 0; j < w.size(); ++j) {
  74       assert(w[j]->is_watched());
  75       assert((unsigned)w[j]->var_sign() == i);
  76     }
  77   }
  78   return true;
  79 }
  80
  81 void CVariable::dump(ostream & os) {
  82   if (is_marked())
  83     os << "*" ;
  84   os << "V: " << _value << "  DL: " << _dlevel  << "  POS: "<< _assgn_stack_pos
  85      << "  Ante: " << _antecedent << endl;
  86   for (unsigned j = 0; j < 2; ++j) {
  87     os << (j == 0 ? "WPos " : "WNeg ") <<  "(" ;
  88     for (unsigned i = 0; i < watched(j).size(); ++i)
  89       os << watched(j)[i]->find_clause_index() << "  " ;
  90     os << ")" << endl;
  91   }
  92 #ifdef KEEP_LIT_CLAUSES
  93   for (unsigned j = 0; j < 2; ++j) {
  94     os << (j == 0 ? "Pos " : "Neg ") <<  "(" ;
  95     for (unsigned i = 0; i < lit_clause(j).size(); ++i)
  96       os << lit_clause(j)[i] << "  " ;
  97     os << ")" << endl;
  98   }
  99 #endif
 100   os << endl;
 101 }