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);