source: vis_dev/zchaff/zchaff_base.cpp @ 69

Last change on this file since 69 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 3.7 KB
Line 
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
39using namespace std;
40
41#include "zchaff_base.h"
42
43void CLitPoolElement::dump(ostream & os) {
44  os << (var_sign() ? " -" : " +") << var_index();
45  if (is_watched())
46    os << "*";
47}
48
49void 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
57bool 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
70bool 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
81void 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}
Note: See TracBrowser for help on using the repository browser.