33 #ifndef _cvc3__include__clause_h_
34 #define _cvc3__include__clause_h_
71 IF_DEBUG(std::string d_file;
int d_line;)
75 const Theorem& clause,
int scope);
97 int scope,
const std::string& file =
"",
int line = 0)
143 size_t wp(
int i)
const {
146 "wp(i): Watch pointer index is out of bounds: i = "
153 size_t wp(
int i,
size_t l)
const {
156 "wp(i,l): Watch pointer index is out of bounds: i = "
161 TRACE(
"clauses",
" **clauses** UPDATE wp(idx="
163 ")\n clause #: ",
id());
171 "dir(i): Watch pointer index is out of bounds: i = "
176 int dir(
int i,
int d)
const {
180 +
"): Watch pointer index is out of bounds");
182 +
"): Direction is out of bounds");
192 bool sat(
bool ignored)
const {
251 int scope):
d_clause(core, vm, clause, scope) {
260 if(&c ==
this)
return *
this;
271 if(--(
d_clause.countOwner()) == 0) {
ClauseOwner()
Disable default constructor.
Clause & operator=(const Clause &c)
Clause(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope, const std::string &file="", int line=0)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::string toString() const
~ClauseOwner()
Destructor: mark the clause as deleted.
ClauseOwner & operator=(const ClauseOwner &c)
Assignment (keep track of refcounts)
std::vector< Literal > d_literals
int owners() const
Tell how many owners this clause has (for debugging)
#define DebugAssert(cond, str)
int & countOwner()
Export owner refcounting to ClauseOwner.
ClauseValue & operator=(const ClauseValue &c)
const Theorem & getTheorem() const
ClauseOwner(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope)
Construct a new Clause.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
bool sat() const
Check if the clause marked as SAT.
bool operator==(const Clause &c) const
A class representing a CNF clause (a smart pointer)
const Literal & operator[](size_t i) const
std::string int2string(int n)
CompactClause(const Clause &c)
int d_refcountOwner
Ref. counter of ClauseOwner classes holding it.
bool sat(bool ignored) const
Precise version of sat(): check all the literals and cache the result.
const Literal & watched(int i) const
int dir(int i, int d) const
ClauseOwner(const Clause &c)
Constructor from class Clause.
ClauseValue(const ClauseValue &c)
int d_refcount
Ref. counter.
Same as class Clause, but when destroyed, marks the clause as deleted.
size_t wp(int i, size_t l) const
const Literal & getLiteral(size_t i) const
const std::vector< Literal > & getLiterals() const
ClauseOwner(const ClauseOwner &c)
Copy constructor (keep track of refcounts)
friend std::ostream & operator<<(std::ostream &os, const Clause &c)
ClauseValue * d_clause
The only value member.