40 #ifndef _cvc3__minisat__types_h_
41 #define _cvc3__minisat__types_h_
65 explicit Lit(
Var var,
bool sgn) :
x((var+var) + (int)sgn) {}
68 bool sign ()
const {
return x & 1; };
69 int var ()
const {
return x >> 1; };
80 unsigned int hash()
const {
return (
unsigned int)
x; }
83 std::ostringstream buffer;
152 void toLit (std::vector<Lit>& literals)
const;
164 if (
size() == 0)
return "";
166 std::ostringstream buffer;
168 for (
int j = 1; j <
size(); ++j) {
175 for (
int i = 0; i <
size(); ++i) {
176 if (
d_data[i] == l)
return true;
183 Clause*
Lemma_new(
const std::vector<Lit>& ps,
int id,
int pushID);
std::string toString() const
std::string toString() const
const Lit lit_Undef(var_Undef, false)
bool operator!=(const Lit q) const
void toLit(std::vector< Lit > &literals) const
MiniSat global functions.
#define DebugAssert(cond, str)
Clause * Lemma_new(const vector< Lit > &ps, int id, int pushID)
static Clause * s_theoryImplication
friend Clause * Clause_new(const std::vector< Lit > &ps, CVC3::Theorem theorem, int id)
CVC3::Theorem getTheorem() const
Clause * Clause_new(const vector< Lit > &ps, CVC3::Theorem theorem, int id)
bool operator==(const Lit q) const
static Lit id(Lit p, bool sgn)
const Lit lit_Error(var_Undef, true)
static Clause * TheoryImplication()
static Clause * s_decision
unsigned int hash() const
Clause(bool learnt, const std::vector< Lit > &ps, CVC3::Theorem theorem, int id, int pushID)
static Clause * Decision()
friend Clause * Lemma_new(const std::vector< Lit > &ps, int id, int pushID)
bool operator<(const Lit q) const
Lit operator[](int i) const
void setActivity(float activity)
unsigned int d_size_learnt
static int ClauseIDNull()