30 Clause* Clause::s_decision = NULL;
31 Clause* Clause::s_theoryImplication = NULL;
46 return new (mem)
Clause(
false, ps, theorem,
id,
id);
55 if (s_decision == NULL) {
63 Clause* Clause::TheoryImplication() {
64 if (s_theoryImplication == NULL) {
69 return s_theoryImplication;
72 void Clause::toLit(vector<Lit>& literals)
const {
73 for (
int i = 0; i < size(); ++i) {
74 literals.push_back(d_data[i]);
Clause * Lemma_new(const vector< Lit > &ps, int id, int pushID)
Clause * Clause_new(const vector< Lit > &ps, CVC3::Theorem theorem, int id)
void * malloc_clause(const vector< Lit > &ps)
const int clause_mem_base