/*****************************************************************************/
/*!
* \file clause.h
*
* Author: Sergey Berezin
*
* Created: Fri Mar 7 16:03:38 2003
*
*
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
*
*
* Class to represent a clause, which is a disjunction of formulas
* which are literals for conflict clauses, and possibly more complex
* formulas for the clauses derived from the user-asserted formulas.
*
* class Clause is implemented as a smart pointer to ClauseValue, so
* it can be freely copied and assigned with low overhead (like
* Theorem or Expr).
*/
/*****************************************************************************/
// Include it before ifndef, since it includes this file recursively
#ifndef DOXYGEN
#include "variable.h"
#endif
#ifndef _cvc3__include__clause_h_
#define _cvc3__include__clause_h_
namespace CVC3 {
class Clause;
class ClauseOwner;
class TheoryCore;
class ClauseValue {
friend class Clause;
private:
//! Ref. counter
int d_refcount;
//! Ref. counter of ClauseOwner classes holding it
int d_refcountOwner;
// The original clause (disjunction of literals)
Theorem d_thm;
// Scope where the clause is valid
int d_scope;
// Theorems l_i <=> l'_i for each literal l_i
// FIXME: more efficient implementation for fixed arrays of CDOs
std::vector d_literals;
// Disallow copy constructor and assignment (make private)
ClauseValue(const ClauseValue& c); // Undefined (since it cannot be used)
ClauseValue& operator=(const ClauseValue& c) { return *this; }
// Pointers to watched literals (Watch Pointers). They are not
// backtrackable.
size_t d_wp[2];
// Direction flags for the watch pointers (1 or -1)
// FIXME: should we use one bit of d_wp{1,2} instead? (efficiency
// vs. space)
int d_dir[2];
// A flag indicating that the clause is shown satisfiable
CDO d_sat;
// Marks the clause as deleted
bool d_deleted;
// Creation file and line number (for debugging)
IF_DEBUG(std::string d_file; int d_line);
// Constructor: takes the main clause theorem which must be a
// disjunction of literals and have no assumptions.
ClauseValue(TheoryCore* core, VariableManager* vm,
const Theorem& clause, int scope);
public:
// Destructor
~ClauseValue();
}; // end of class ClauseValue
//! A class representing a CNF clause (a smart pointer)
class Clause {
private:
friend class ClauseOwner;
//! The only value member
ClauseValue* d_clause;
//! Export owner refcounting to ClauseOwner
int& countOwner() {
DebugAssert(d_clause != NULL, "");
return d_clause->d_refcountOwner;
}
public:
Clause(): d_clause(NULL) { }
// Constructors
Clause(TheoryCore* core, VariableManager* vm, const Theorem& clause,
int scope, const std::string& file = "", int line = 0)
: d_clause(new ClauseValue(core, vm, clause, scope)) {
d_clause->d_refcount++;
IF_DEBUG(d_clause->d_file = file; d_clause->d_line=line);
}
// Copy constructor
Clause(const Clause& c): d_clause(c.d_clause) {
if(d_clause != NULL) d_clause->d_refcount++;
}
// Destructor
~Clause();
// Assignment operator
Clause& operator=(const Clause& c);
bool isNull() const { return d_clause == NULL; }
// Other public methods
size_t size() const {
return (d_clause == NULL)? 0 : d_clause->d_literals.size();
}
// Get the theorem representing the entire clause
const Theorem& getTheorem() const {
DebugAssert(!isNull(), "Clause::getTheorem(): Null Clause");
return d_clause->d_thm;
}
// Get the scope where the clause is valid
int getScope() const {
if(isNull()) return 0;
else return d_clause->d_scope;
}
// Get the current value of the i-th literal
const Literal& getLiteral(size_t i) const {
DebugAssert(!isNull(), "Clause::getLiteral(): Null Clause");
DebugAssert(i < size(),
"Clause::getLiteral(" + int2string(i)
+ "): i >= size = " + int2string(size()));
return d_clause->d_literals[i];
}
// Get the current value of the i-th literal
const Literal& operator[](size_t i) const { return getLiteral(i); }
// Get the reference to the vector of literals, for fast access
const std::vector& getLiterals() const {
DebugAssert(!isNull(), "Clause::getLiterals(): Null Clause");
return d_clause->d_literals;
}
// Get the values of watch pointers
size_t wp(int i) const {
DebugAssert(!isNull(), "Clause::wp(i): Null Clause");
DebugAssert(i==0 || i==1,
"wp(i): Watch pointer index is out of bounds: i = "
+ int2string(i));
return d_clause->d_wp[i];
}
// Get the watched literals
const Literal& watched(int i) const { return getLiteral(wp(i)); }
// Set the watch pointers and return the new value
size_t wp(int i, size_t l) const {
DebugAssert(!isNull(), "Clause::wp(i,l): Null Clause");
DebugAssert(i==0 || i==1,
"wp(i,l): Watch pointer index is out of bounds: i = "
+ int2string(i));
DebugAssert(l < size(), "Clause::wp(i = " + int2string(i)
+ ", l = " + int2string(l)
+ "): l >= size() = " + int2string(size()));
TRACE("clauses", " **clauses** UPDATE wp(idx="
+int2string(i)+", l="+int2string(l),
")\n clause #: ", id());
d_clause->d_wp[i] = l;
return l;
}
// Get the direction of the i-th watch pointer
int dir(int i) const {
DebugAssert(!isNull(), "Clause::dir(i): Null Clause");
DebugAssert(i==0 || i==1,
"dir(i): Watch pointer index is out of bounds: i = "
+ int2string(i));
return d_clause->d_dir[i];
}
// Set the direction of the i-th watch pointer
int dir(int i, int d) const {
DebugAssert(!isNull(), "Clause::dir(i,d): Null Clause");
DebugAssert(i==0 || i==1,
"dir(i="+int2string(i)+",d="+int2string(d)
+"): Watch pointer index is out of bounds");
DebugAssert(d==1 || d==-1, "dir(i="+int2string(i)+",d="+int2string(d)
+"): Direction is out of bounds");
d_clause->d_dir[i] = d;
return d;
}
//! Check if the clause marked as SAT
bool sat() const {
DebugAssert(!isNull(), "Clause::sat()");
return d_clause->d_sat;
}
//! Precise version of sat(): check all the literals and cache the result
bool sat(bool ignored) const {
DebugAssert(!isNull(), "Clause::sat()");
bool flag = false;
if (!d_clause->d_sat) {
for (size_t i = 0; !flag && i < d_clause->d_literals.size(); ++i)
if (d_clause->d_literals[i].getValue() == 1)
flag = true;
}
if (flag) {
//std::cout << "*** Manually marking SAT" << std::endl;
markSat();
}
return d_clause->d_sat;
}
// Mark the clause as SAT
void markSat() const {
DebugAssert(!isNull(), "Clause::markSat()");
d_clause->d_sat = true;
}
// Check / mark the clause as deleted
bool deleted() const {
DebugAssert(!isNull(), "Clause::deleted()");
return d_clause->d_deleted;
}
void markDeleted() const;
// For debugging: return some kind of unique ID
size_t id() const { return (size_t) d_clause; }
// Equality: compare the pointers
bool operator==(const Clause& c) const { return d_clause == c.d_clause; }
//! Tell how many owners this clause has (for debugging)
int owners() const { return d_clause->d_refcountOwner; }
// Printing
std::string toString() const;
friend std::ostream& operator<<(std::ostream& os, const Clause& c);
IF_DEBUG(bool wpCheck() const;)
IF_DEBUG(const std::string& getFile() const { return d_clause->d_file; })
IF_DEBUG(int getLine() const { return d_clause->d_line; })
}; // end of class Clause
//! Same as class Clause, but when destroyed, marks the clause as deleted
/*! Needed for backtraking data structures. When the SAT solver
backtracks, some clauses will be thrown away automatically, and we
need to mark those as deleted. */
class ClauseOwner {
Clause d_clause;
//! Disable default constructor
ClauseOwner() { }
public:
//! Constructor from class Clause
ClauseOwner(const Clause& c): d_clause(c) { d_clause.countOwner()++; }
//! Construct a new Clause
ClauseOwner(TheoryCore* core, VariableManager* vm, const Theorem& clause,
int scope): d_clause(core, vm, clause, scope) {
d_clause.countOwner()++;
}
//! Copy constructor (keep track of refcounts)
ClauseOwner(const ClauseOwner& c): d_clause(c.d_clause) {
d_clause.countOwner()++;
}
//! Assignment (keep track of refcounts)
ClauseOwner& operator=(const ClauseOwner& c) {
if(&c == this) return *this; // Seft-assignment
DebugAssert(d_clause.countOwner() > 0, "in operator=");
if(--(d_clause.countOwner()) == 0)
d_clause.markDeleted();
d_clause = c.d_clause;
d_clause.countOwner()++;
return *this;
}
//! Destructor: mark the clause as deleted
~ClauseOwner() {
FatalAssert(d_clause.countOwner() > 0, "in ~ClauseOwner");
if(--(d_clause.countOwner()) == 0) {
d_clause.markDeleted();
}
}
//! Automatic type conversion to Clause ref
operator Clause& () { return d_clause; }
//! Automatic type conversion to Clause const ref
operator const Clause& () const { return d_clause; }
}; // end of class ClauseOwner
// I/O Manipulators
// Print clause in a compact form: Clause[x=-1@scope, ...], mark
// watched literals by '*'
class CompactClause {
private:
Clause d_clause;
public:
CompactClause(const Clause& c): d_clause(c) { }
friend std::ostream& operator<<(std::ostream& os, const CompactClause& c);
std::string toString() const;
};
} // end of namespace CVC3
#endif