21 #ifndef _cvc3__include__cnf_h_
22 #define _cvc3__include__cnf_h_
56 explicit Lit(
Var v,
bool positive=
true) {
58 else d_index = positive ? v+1 : -v-1;
125 virtual bool empty()
const = 0;
129 virtual unsigned numVars()
const = 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
friend Lit operator!(const Lit &lit)
const_iterator end() const
std::vector< Lit >::const_iterator const_iterator
static Val invertValue(Val)
Lit(Var v, bool positive=true)