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:
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.
20 // --- This software and any associated documentation is provided "as is"
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.
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 // *********************************************************************/
41 #include "zchaff_base.h"
43 void CLitPoolElement::dump(ostream & os) {
44 os << (var_sign() ? " -" : " +") << var_index();
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)
57 bool CClause::self_check(void) {
58 assert(num_lits() > 0);
60 for (unsigned i = 0; i < num_lits(); ++i) {
61 assert(literal(i).is_literal());
62 if (literal(i).is_watched())
65 assert(num_lits() ==1 || watched == 2); // either unit, or have two watched
66 assert(!literal(num_lits() + 1).is_literal());
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);
81 void CVariable::dump(ostream & 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() << " " ;
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] << " " ;