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)
98 : d_clause(new
ClauseValue(core, vm, clause, scope)) {
100 IF_DEBUG(d_clause->d_file = file; d_clause->d_line=line;)
111 bool isNull()
const {
return d_clause == NULL; }
114 return (d_clause == NULL)? 0 : d_clause->
d_literals.size();
119 return d_clause->
d_thm;
143 size_t wp(
int i)
const {
146 "wp(i): Watch pointer index is out of bounds: i = "
148 return d_clause->
d_wp[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());
164 d_clause->
d_wp[i] = l;
171 "dir(i): Watch pointer index is out of bounds: i = "
173 return d_clause->
d_dir[i];
176 int dir(
int i,
int d)
const {
180 +
"): Watch pointer index is out of bounds");
182 +
"): Direction is out of bounds");
183 d_clause->
d_dir[i] = d;
189 return d_clause->
d_sat;
192 bool sat(
bool ignored)
const {
195 if (!d_clause->
d_sat) {
196 for (
size_t i = 0; !flag && i < d_clause->
d_literals.size(); ++i)
204 return d_clause->
d_sat;
209 d_clause->
d_sat =
true;
233 IF_DEBUG(
const std::string& getFile()
const {
return d_clause->d_file; })
234 IF_DEBUG(
int getLine()
const {
return d_clause->d_line; })
251 int scope): d_clause(core, vm, clause, scope) {
260 if(&c ==
this)
return *
this;
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.