21 #ifndef _cvc3__include__cnf_h_
22 #define _cvc3__include__cnf_h_
39 Var() : d_index(-1) {}
40 Var(
int index) :d_index(index) {}
42 bool isNull()
const {
return d_index == -1; }
45 bool isVar()
const {
return d_index > 0; }
56 explicit Lit(
Var v,
bool positive=
true) {
57 if (v.
isNull()) d_index = 0;
58 else d_index = positive ? v+1 : -v-1;
63 bool isNull()
const {
return d_index == 0; }
66 bool isFalse()
const {
return d_index == -1; }
67 bool isTrue()
const {
return d_index == 1; }
68 bool isVar()
const {
return abs(d_index) > 1; }
72 return abs(d_index)-1;
90 d_lits(clause.d_lits), d_reason(clause.d_reason) { };
93 const_iterator
begin()
const {
return d_lits.begin(); }
94 const_iterator
end()
const {
return d_lits.end(); }
97 unsigned size()
const {
return d_lits.size(); }
102 bool isNull()
const {
return d_lits.size() == 0; }
125 virtual bool empty()
const = 0;
127 virtual const_iterator
begin()
const = 0;
128 virtual const_iterator
end()
const = 0;
129 virtual unsigned numVars()
const = 0;
156 bool empty()
const {
return d_formula.empty(); }
178 :
CNF_Formula(), d_formula(context), d_numVars(context, 0, 0) {}
const_iterator begin() const
unsigned getMaxVar() const
bool operator==(const Var &var) const
Clause(const Clause &clause)
std::vector< Lit > d_lits
void setClauseTheorem(CVC3::Theorem thm)
#define DebugAssert(cond, str)
static Lit mkLit(int index)
CVC3::Theorem getClauseTheorem() const
const_iterator end() const
friend Lit operator!(const Lit &lit)
const_iterator end() const
std::vector< Lit >::const_iterator const_iterator
const_iterator begin() const
static Val invertValue(Val)
Lit(Var v, bool positive=true)