36 const Theorem& clause,
int scope)
37 : d_refcount(0), d_refcountOwner(0), d_thm(clause), d_scope(scope),
40 d_sat(core->getCM()->getCurrentContext(), false, 0),
55 int val(i->isNot()? -1 : 1);
56 Variable v(vm, (val < 0)? (*i)[0] : (*i));
66 TRACE_MSG(
"search literals",
"~ClauseValue() {");
70 for(vector<Literal>::iterator i=
d_literals.begin(),
74 TRACE(
"search literals",
"Null count for ", *i,
"");)
77 TRACE_MSG(
"search literals",
"~ClauseValue() => }");
86 if(d_clause != NULL) {
88 "~Clause: non-positive refcount: "
90 if(--(d_clause->d_refcount) == 0)
delete d_clause;
97 TRACE(
"search literals",
"Clause::markDeleted(",
100 if(!d_clause->d_deleted) {
101 d_clause->d_deleted =
true;
103 for(vector<Literal>::iterator i=d_clause->d_literals.begin(),
104 iend=d_clause->d_literals.end(); i!=iend; ++i) {
107 TRACE(
"search literals",
"Null count for ", *i,
"");)
110 TRACE_MSG(
"search literals",
"Clause::markDeleted => }");
116 if(&c ==
this)
return *
this;
117 if(d_clause != NULL) {
119 "Clause::operator=: non-positive refcount: "
121 if(--(d_clause->d_refcount) == 0)
delete d_clause;
130 std::ostringstream ss;
136 if(c.
isNull())
return os <<
"Clause[Null]";
138 if(c.
deleted()) os <<
"DELETED ";
141 os <<
", " << c.getFile() <<
":" << c.getLine();)
144 if(c.
wp(0) == c.
wp(1)) os <<
"WARNING: wp[0] = wp[1]\n";
145 for(
unsigned i=0; i<c.
size(); ++i) {
147 os <<
"wp[0]" << ((c.
dir(0) > 0)?
"=>" :
"<=") <<
" ";
148 else if(c.
wp(1) == i)
149 os <<
"wp[1]" << ((c.
dir(1) > 0)?
"=>" :
"<=") <<
" ";
154 return os << ((c.
sat())?
"Clause is SAT" :
"") <<
")";
161 if(val != 0) os <<
"=" << val <<
"@" << l.
getScope();
172 if(i==wp0 || i==wp1) os <<
"*";
175 for(; i!=iend; ++i) {
177 if(i==wp0 || i==wp1) os <<
"*";
190 #ifdef _CVC3_DEBUG_MODE
191 bool CVC3::Clause::wpCheck()
const
195 return (getLiteral(wp(0)).getValue() == 0 && getLiteral(wp(1)).getValue() == 0);
std::string toString() const
Clause & operator=(const Clause &c)
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::string toString() const
static void printLit(ostream &os, const Literal &l)
ostream & operator<<(ostream &os, const Expr &e)
std::vector< Literal > d_literals
int owners() const
Tell how many owners this clause has (for debugging)
#define DebugAssert(cond, str)
const Theorem & getTheorem() const
#define TRACE_MSG(flag, msg)
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::string toString() const
bool sat() const
Check if the clause marked as SAT.
A class representing a CNF clause (a smart pointer)
std::string int2string(int n)
const Expr & getExpr() const
ClauseValue(const ClauseValue &c)
int d_refcount
Ref. counter.
const std::vector< Literal > & getLiterals() const
ClauseValue * d_clause
The only value member.