CVC3  2.4.1
clause.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file clause.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Fri Mar 7 16:03:38 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * Class to represent a clause, which is a disjunction of formulas
19  * which are literals for conflict clauses, and possibly more complex
20  * formulas for the clauses derived from the user-asserted formulas.
21  *
22  * class Clause is implemented as a smart pointer to ClauseValue, so
23  * it can be freely copied and assigned with low overhead (like
24  * Theorem or Expr).
25  */
26 /*****************************************************************************/
27 
28 // Include it before ifndef, since it includes this file recursively
29 #ifndef DOXYGEN
30 #include "variable.h"
31 #endif
32 
33 #ifndef _cvc3__include__clause_h_
34 #define _cvc3__include__clause_h_
35 
36 namespace CVC3 {
37 
38  class Clause;
39  class ClauseOwner;
40  class TheoryCore;
41 
42  class ClauseValue {
43  friend class Clause;
44  private:
45  //! Ref. counter
47  //! Ref. counter of ClauseOwner classes holding it
49  // The original clause (disjunction of literals)
51  // Scope where the clause is valid
52  int d_scope;
53  // Theorems l_i <=> l'_i for each literal l_i
54  // FIXME: more efficient implementation for fixed arrays of CDOs
55  std::vector<Literal> d_literals;
56  // Disallow copy constructor and assignment (make private)
57  ClauseValue(const ClauseValue& c); // Undefined (since it cannot be used)
58  ClauseValue& operator=(const ClauseValue& c) { return *this; }
59  // Pointers to watched literals (Watch Pointers). They are not
60  // backtrackable.
61  size_t d_wp[2];
62  // Direction flags for the watch pointers (1 or -1)
63  // FIXME: should we use one bit of d_wp{1,2} instead? (efficiency
64  // vs. space)
65  int d_dir[2];
66  // A flag indicating that the clause is shown satisfiable
68  // Marks the clause as deleted
69  bool d_deleted;
70  // Creation file and line number (for debugging)
71  IF_DEBUG(std::string d_file; int d_line;)
72  // Constructor: takes the main clause theorem which must be a
73  // disjunction of literals and have no assumptions.
75  const Theorem& clause, int scope);
76  public:
77  // Destructor
78  ~ClauseValue();
79 
80  }; // end of class ClauseValue
81 
82  //! A class representing a CNF clause (a smart pointer)
83  class Clause {
84  private:
85  friend class ClauseOwner;
86  //! The only value member
88  //! Export owner refcounting to ClauseOwner
89  int& countOwner() {
90  DebugAssert(d_clause != NULL, "");
91  return d_clause->d_refcountOwner;
92  }
93  public:
94  Clause(): d_clause(NULL) { }
95  // Constructors
96  Clause(TheoryCore* core, VariableManager* vm, const Theorem& clause,
97  int scope, const std::string& file = "", int line = 0)
98  : d_clause(new ClauseValue(core, vm, clause, scope)) {
100  IF_DEBUG(d_clause->d_file = file; d_clause->d_line=line;)
101  }
102  // Copy constructor
103  Clause(const Clause& c): d_clause(c.d_clause) {
104  if(d_clause != NULL) d_clause->d_refcount++;
105  }
106  // Destructor
107  ~Clause();
108  // Assignment operator
109  Clause& operator=(const Clause& c);
110 
111  bool isNull() const { return d_clause == NULL; }
112  // Other public methods
113  size_t size() const {
114  return (d_clause == NULL)? 0 : d_clause->d_literals.size();
115  }
116  // Get the theorem representing the entire clause
117  const Theorem& getTheorem() const {
118  DebugAssert(!isNull(), "Clause::getTheorem(): Null Clause");
119  return d_clause->d_thm;
120  }
121  // Get the scope where the clause is valid
122  int getScope() const {
123  if(isNull()) return 0;
124  else return d_clause->d_scope;
125  }
126  // Get the current value of the i-th literal
127  const Literal& getLiteral(size_t i) const {
128  DebugAssert(!isNull(), "Clause::getLiteral(): Null Clause");
129  DebugAssert(i < size(),
130  "Clause::getLiteral(" + int2string(i)
131  + "): i >= size = " + int2string(size()));
132  return d_clause->d_literals[i];
133  }
134  // Get the current value of the i-th literal
135  const Literal& operator[](size_t i) const { return getLiteral(i); }
136 
137  // Get the reference to the vector of literals, for fast access
138  const std::vector<Literal>& getLiterals() const {
139  DebugAssert(!isNull(), "Clause::getLiterals(): Null Clause");
140  return d_clause->d_literals;
141  }
142  // Get the values of watch pointers
143  size_t wp(int i) const {
144  DebugAssert(!isNull(), "Clause::wp(i): Null Clause");
145  DebugAssert(i==0 || i==1,
146  "wp(i): Watch pointer index is out of bounds: i = "
147  + int2string(i));
148  return d_clause->d_wp[i];
149  }
150  // Get the watched literals
151  const Literal& watched(int i) const { return getLiteral(wp(i)); }
152  // Set the watch pointers and return the new value
153  size_t wp(int i, size_t l) const {
154  DebugAssert(!isNull(), "Clause::wp(i,l): Null Clause");
155  DebugAssert(i==0 || i==1,
156  "wp(i,l): Watch pointer index is out of bounds: i = "
157  + int2string(i));
158  DebugAssert(l < size(), "Clause::wp(i = " + int2string(i)
159  + ", l = " + int2string(l)
160  + "): l >= size() = " + int2string(size()));
161  TRACE("clauses", " **clauses** UPDATE wp(idx="
162  +int2string(i)+", l="+int2string(l),
163  ")\n clause #: ", id());
164  d_clause->d_wp[i] = l;
165  return l;
166  }
167  // Get the direction of the i-th watch pointer
168  int dir(int i) const {
169  DebugAssert(!isNull(), "Clause::dir(i): Null Clause");
170  DebugAssert(i==0 || i==1,
171  "dir(i): Watch pointer index is out of bounds: i = "
172  + int2string(i));
173  return d_clause->d_dir[i];
174  }
175  // Set the direction of the i-th watch pointer
176  int dir(int i, int d) const {
177  DebugAssert(!isNull(), "Clause::dir(i,d): Null Clause");
178  DebugAssert(i==0 || i==1,
179  "dir(i="+int2string(i)+",d="+int2string(d)
180  +"): Watch pointer index is out of bounds");
181  DebugAssert(d==1 || d==-1, "dir(i="+int2string(i)+",d="+int2string(d)
182  +"): Direction is out of bounds");
183  d_clause->d_dir[i] = d;
184  return d;
185  }
186  //! Check if the clause marked as SAT
187  bool sat() const {
188  DebugAssert(!isNull(), "Clause::sat()");
189  return d_clause->d_sat;
190  }
191  //! Precise version of sat(): check all the literals and cache the result
192  bool sat(bool ignored) const {
193  DebugAssert(!isNull(), "Clause::sat()");
194  bool flag = false;
195  if (!d_clause->d_sat) {
196  for (size_t i = 0; !flag && i < d_clause->d_literals.size(); ++i)
197  if (d_clause->d_literals[i].getValue() == 1)
198  flag = true;
199  }
200  if (flag) {
201  //std::cout << "*** Manually marking SAT" << std::endl;
202  markSat();
203  }
204  return d_clause->d_sat;
205  }
206  // Mark the clause as SAT
207  void markSat() const {
208  DebugAssert(!isNull(), "Clause::markSat()");
209  d_clause->d_sat = true;
210  }
211  // Check / mark the clause as deleted
212  bool deleted() const {
213  DebugAssert(!isNull(), "Clause::deleted()");
214  return d_clause->d_deleted;
215  }
216  void markDeleted() const;
217 
218  // For debugging: return some kind of unique ID
219  size_t id() const { return (size_t) d_clause; }
220 
221  // Equality: compare the pointers
222  bool operator==(const Clause& c) const { return d_clause == c.d_clause; }
223 
224  //! Tell how many owners this clause has (for debugging)
225  int owners() const { return d_clause->d_refcountOwner; }
226 
227  // Printing
228  std::string toString() const;
229 
230  friend std::ostream& operator<<(std::ostream& os, const Clause& c);
231 
232  IF_DEBUG(bool wpCheck() const;)
233  IF_DEBUG(const std::string& getFile() const { return d_clause->d_file; })
234  IF_DEBUG(int getLine() const { return d_clause->d_line; })
235 
236  }; // end of class Clause
237 
238  //! Same as class Clause, but when destroyed, marks the clause as deleted
239  /*! Needed for backtraking data structures. When the SAT solver
240  backtracks, some clauses will be thrown away automatically, and we
241  need to mark those as deleted. */
242  class ClauseOwner {
244  //! Disable default constructor
246  public:
247  //! Constructor from class Clause
248  ClauseOwner(const Clause& c): d_clause(c) { d_clause.countOwner()++; }
249  //! Construct a new Clause
250  ClauseOwner(TheoryCore* core, VariableManager* vm, const Theorem& clause,
251  int scope): d_clause(core, vm, clause, scope) {
252  d_clause.countOwner()++;
253  }
254  //! Copy constructor (keep track of refcounts)
256  d_clause.countOwner()++;
257  }
258  //! Assignment (keep track of refcounts)
260  if(&c == this) return *this; // Seft-assignment
261  DebugAssert(d_clause.countOwner() > 0, "in operator=");
262  if(--(d_clause.countOwner()) == 0)
263  d_clause.markDeleted();
264  d_clause = c.d_clause;
265  d_clause.countOwner()++;
266  return *this;
267  }
268  //! Destructor: mark the clause as deleted
270  FatalAssert(d_clause.countOwner() > 0, "in ~ClauseOwner");
271  if(--(d_clause.countOwner()) == 0) {
272  d_clause.markDeleted();
273  }
274  }
275  //! Automatic type conversion to Clause ref
276  operator Clause& () { return d_clause; }
277  //! Automatic type conversion to Clause const ref
278  operator const Clause& () const { return d_clause; }
279  }; // end of class ClauseOwner
280 
281 
282  // I/O Manipulators
283 
284  // Print clause in a compact form: Clause[x=-1@scope, ...], mark
285  // watched literals by '*'
287  private:
289  public:
290  CompactClause(const Clause& c): d_clause(c) { }
291  friend std::ostream& operator<<(std::ostream& os, const CompactClause& c);
292  std::string toString() const;
293  };
294 
295 } // end of namespace CVC3
296 
297 #endif
size_t id() const
Definition: clause.h:219
int d_dir[2]
Definition: clause.h:65
ClauseOwner()
Disable default constructor.
Definition: clause.h:245
Clause & operator=(const Clause &c)
Definition: clause.cpp:115
Clause(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope, const std::string &file="", int line=0)
Definition: clause.h:96
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
std::string toString() const
Definition: clause.cpp:129
~ClauseOwner()
Destructor: mark the clause as deleted.
Definition: clause.h:269
CDO< bool > d_sat
Definition: clause.h:67
ClauseOwner & operator=(const ClauseOwner &c)
Assignment (keep track of refcounts)
Definition: clause.h:259
size_t size() const
Definition: clause.h:113
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
Clause d_clause
Definition: clause.h:243
Theorem d_thm
Definition: clause.h:50
size_t wp(int i) const
Definition: clause.h:143
#define DebugAssert(cond, str)
Definition: debug.h:408
int getScope() const
Definition: clause.h:122
Clause(const Clause &c)
Definition: clause.h:103
int & countOwner()
Export owner refcounting to ClauseOwner.
Definition: clause.h:89
ClauseValue & operator=(const ClauseValue &c)
Definition: clause.h:58
const Theorem & getTheorem() const
Definition: clause.h:117
ClauseOwner(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope)
Construct a new Clause.
Definition: clause.h:250
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
bool sat() const
Check if the clause marked as SAT.
Definition: clause.h:187
bool operator==(const Clause &c) const
Definition: clause.h:222
A class representing a CNF clause (a smart pointer)
Definition: clause.h:83
bool deleted() const
Definition: clause.h:212
const Literal & operator[](size_t i) const
Definition: clause.h:135
std::string int2string(int n)
Definition: cvc_util.h:46
CompactClause(const Clause &c)
Definition: clause.h:290
#define IF_DEBUG(code)
Definition: debug.h:406
int d_refcountOwner
Ref. counter of ClauseOwner classes holding it.
Definition: clause.h:48
bool sat(bool ignored) const
Precise version of sat(): check all the literals and cache the result.
Definition: clause.h:192
const Literal & watched(int i) const
Definition: clause.h:151
int dir(int i, int d) const
Definition: clause.h:176
void markSat() const
Definition: clause.h:207
ClauseOwner(const Clause &c)
Constructor from class Clause.
Definition: clause.h:248
ClauseValue(const ClauseValue &c)
int d_refcount
Ref. counter.
Definition: clause.h:46
Same as class Clause, but when destroyed, marks the clause as deleted.
Definition: clause.h:242
Definition: kinds.h:99
size_t wp(int i, size_t l) const
Definition: clause.h:153
const Literal & getLiteral(size_t i) const
Definition: clause.h:127
const std::vector< Literal > & getLiterals() const
Definition: clause.h:138
ClauseOwner(const ClauseOwner &c)
Copy constructor (keep track of refcounts)
Definition: clause.h:255
friend std::ostream & operator<<(std::ostream &os, const Clause &c)
Definition: clause.cpp:135
void markDeleted() const
Definition: clause.cpp:96
ClauseValue * d_clause
The only value member.
Definition: clause.h:87