CVC3  2.4.1
clause.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file clause.cpp
4  * \brief Implementation of class Clause
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Mon Apr 28 17:20:23 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #include "clause.h"
23 #include "theory_core.h"
24 
25 using namespace std;
26 
27 namespace CVC3 {
28 
29 ////////////////////////////////////////////////////////////////////////
30 // class ClauseValue methods
31 ////////////////////////////////////////////////////////////////////////
32 
33 // Constructor: takes the main clause theorem which must be a
34 // disjunction of literals and have no assumptions.
35 ClauseValue::ClauseValue(TheoryCore* core, VariableManager* vm,
36  const Theorem& clause, int scope)
37  : d_refcount(0), d_refcountOwner(0), d_thm(clause), d_scope(scope),
38  // This backtrackable member is initialized in the first scope
39  // (which is #0)
40  d_sat(core->getCM()->getCurrentContext(), false, 0),
41  d_deleted(false) {
42  // Check the clause
43  DebugAssert(clause.getExpr().isOr(), "Clause(): bad clause given: "
44  + clause.toString());
45 // DebugAssert(clause.getExpr().arity()>0, "Clause(): empty clause: "
46 // + clause.toString());
47  // Initialize watched literals to the edges with directions
48  // pointing outwards
49  d_wp[0]=0; d_dir[0]=-1;
50  d_wp[1] = clause.getExpr().arity()-1; d_dir[1]=1;
51  // Initialize the literals
52  Expr c(clause.getExpr());
53  d_literals.reserve(c.arity());
54  for(Expr::iterator i=c.begin(), iend=c.end(); i!=iend; ++i) {
55  int val(i->isNot()? -1 : 1);
56  Variable v(vm, (val < 0)? (*i)[0] : (*i));
57  Literal l(v, val > 0);
58  d_literals.push_back(l);
59  // Update the literal's count for splitter heuristics
60  l.count()++;
61  }
62  IF_DEBUG(d_sat.setName("CDO[Clause.d_sat]");)
63 }
64 
66  TRACE_MSG("search literals", "~ClauseValue() {");
67  FatalAssert(d_refcount == 0, "~ClauseValue: non-zero refcount: "
69  if(!d_deleted) { // Update the literal counts for splitter heuristics
70  for(vector<Literal>::iterator i=d_literals.begin(),
71  iend=d_literals.end(); i!=iend; ++i) {
72  i->count()--;
73  IF_DEBUG(if(i->count() == 0)
74  TRACE("search literals", "Null count for ", *i, "");)
75  }
76  }
77  TRACE_MSG("search literals", "~ClauseValue() => }");
78 }
79 
80 ////////////////////////////////////////////////////////////////////////
81 // class Clause methods
82 ////////////////////////////////////////////////////////////////////////
83 
84 // Destructor
86  if(d_clause != NULL) {
87  FatalAssert(d_clause->d_refcount > 0,
88  "~Clause: non-positive refcount: "
89  + int2string(d_clause->d_refcount));
90  if(--(d_clause->d_refcount) == 0) delete d_clause;
91  }
92 }
93 
94 
95 void
97  TRACE("search literals", "Clause::markDeleted(",
98  CompactClause(*this), ") {");
99  DebugAssert(!isNull(), "Clause::markDeleted()");
100  if(!d_clause->d_deleted) {
101  d_clause->d_deleted = true;
102  // Update the literal counts for splitter heuristics
103  for(vector<Literal>::iterator i=d_clause->d_literals.begin(),
104  iend=d_clause->d_literals.end(); i!=iend; ++i) {
105  i->count()--;
106  IF_DEBUG(if(i->count() == 0)
107  TRACE("search literals", "Null count for ", *i, "");)
108  }
109  }
110  TRACE_MSG("search literals", "Clause::markDeleted => }");
111 }
112 
113 
114 // Assignment operator
116  if(&c == this) return *this; // Self-assignment
117  if(d_clause != NULL) {
118  DebugAssert(d_clause->d_refcount > 0,
119  "Clause::operator=: non-positive refcount: "
120  + int2string(d_clause->d_refcount));
121  if(--(d_clause->d_refcount) == 0) delete d_clause;
122  }
123  d_clause = c.d_clause;
124  if(d_clause != NULL) d_clause->d_refcount++;
125  return *this;
126 }
127 
128 // Printing
129 string Clause::toString() const {
130  std::ostringstream ss;
131  ss << *this;
132  return ss.str();
133 }
134 
135 ostream& operator<<(ostream& os, const Clause& c) {
136  if(c.isNull()) return os << "Clause[Null]";
137  os << "Clause[";
138  if(c.deleted()) os << "DELETED ";
139  os << c.id();
140  IF_DEBUG(if(c.getFile() != "")
141  os << ", " << c.getFile() << ":" << c.getLine();)
142  os << "](" << c.getTheorem()
143  << ";\n";
144  if(c.wp(0) == c.wp(1)) os << "WARNING: wp[0] = wp[1]\n";
145  for(unsigned i=0; i<c.size(); ++i) {
146  if(c.wp(0) == i)
147  os << "wp[0]" << ((c.dir(0) > 0)? "=>" : "<=") << " ";
148  else if(c.wp(1) == i)
149  os << "wp[1]" << ((c.dir(1) > 0)? "=>" : "<=") << " ";
150  else
151  os << " ";
152  os << c[i] << ";\n";
153  }
154  return os << ((c.sat())? "Clause is SAT" : "") << ")";
155 }
156 
157  static void printLit(ostream& os, const Literal& l) {
158  if(l.isNegative()) os << "!";
159  os << l.getVar().getExpr();
160  int val(l.getValue());
161  if(val != 0) os << "=" << val << "@" << l.getScope();
162  }
163 
164 ostream& operator<<(std::ostream& os, const CompactClause& c) {
165  const vector<Literal>& lits = c.d_clause.getLiterals();
166  int wp0(c.d_clause.wp(0)), wp1(c.d_clause.wp(1));
167  int i=0, iend=c.d_clause.size();
168  os << "Clause[";
169  if(c.d_clause.deleted()) os << "*DELETED* ";
170  if(c.d_clause.owners() > 0) os << "owned(" << c.d_clause.owners() << ") ";
171  if(i!=iend) {
172  if(i==wp0 || i==wp1) os << "*";
173  printLit(os, lits[i]); ++i;
174  }
175  for(; i!=iend; ++i) {
176  os << ", ";
177  if(i==wp0 || i==wp1) os << "*";
178  printLit(os, lits[i]);
179  }
180  os << "]";
181  return os;
182 }
183 
184 string CompactClause::toString() const {
185  ostringstream ss;
186  ss << (*this);
187  return ss.str();
188 }
189 
190 #ifdef _CVC3_DEBUG_MODE
191 bool CVC3::Clause::wpCheck() const
192 {
193  if (sat(true))
194  return true;
195  return (getLiteral(wp(0)).getValue() == 0 && getLiteral(wp(1)).getValue() == 0);
196 }
197 #endif
198 
199 } // end of namespace CVC3
size_t id() const
Definition: clause.h:219
std::string toString() const
Definition: clause.cpp:184
int arity() const
Definition: expr.h:1201
int d_dir[2]
Definition: clause.h:65
Clause & operator=(const Clause &c)
Definition: clause.cpp:115
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
int getValue() const
Definition: variable.h:144
std::string toString() const
Definition: clause.cpp:129
CDO< bool > d_sat
Definition: clause.h:67
unsigned & count()
Definition: variable.h:166
size_t size() const
Definition: clause.h:113
static void printLit(ostream &os, const Literal &l)
Definition: clause.cpp:157
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
size_t d_wp[2]
Definition: clause.h:61
std::vector< Literal > d_literals
Definition: clause.h:55
int owners() const
Tell how many owners this clause has (for debugging)
Definition: clause.h:225
bool d_deleted
Definition: clause.h:69
int dir(int i) const
Definition: clause.h:168
bool isNull() const
Definition: clause.h:111
Variable & getVar()
Definition: variable.h:134
size_t wp(int i) const
Definition: clause.h:143
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isOr() const
Definition: expr.h:422
int getScope() const
Definition: variable.h:148
const Theorem & getTheorem() const
Definition: clause.h:117
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
bool isNegative() const
Definition: variable.h:137
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
std::string toString() const
Definition: theorem.h:404
bool sat() const
Check if the clause marked as SAT.
Definition: clause.h:187
A class representing a CNF clause (a smart pointer)
Definition: clause.h:83
bool deleted() const
Definition: clause.h:212
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & getExpr() const
Definition: variable.cpp:68
#define IF_DEBUG(code)
Definition: debug.h:406
Expr getExpr() const
Definition: theorem.cpp:230
ClauseValue(const ClauseValue &c)
int d_refcount
Ref. counter.
Definition: clause.h:46
Definition: kinds.h:99
const std::vector< Literal > & getLiterals() const
Definition: clause.h:138
void markDeleted() const
Definition: clause.cpp:96
ClauseValue * d_clause
The only value member.
Definition: clause.h:87