diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index a68367f6b..92ba7b808 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -312,7 +312,6 @@ namespace sat {
}
bool lookahead::is_unsat() const {
-#ifdef NEW_CLAUSE
bool all_false = true;
bool first = true;
// check if there is a clause whose literals are false.
@@ -344,20 +343,7 @@ namespace sat {
return true;
}
}
- }
-
-#else
- for (unsigned i = 0; i < m_clauses.size(); ++i) {
- clause& c = *m_clauses[i];
- unsigned j = 0;
- for (; j < c.size() && is_false(c[j]); ++j) {}
- if (j == c.size()) {
- TRACE("sat", tout << c << "\n";);
- TRACE("sat", display(tout););
- return true;
- }
- }
-#endif
+ }
return false;
}
@@ -380,7 +366,6 @@ namespace sat {
}
}
}
-#ifdef NEW_CLAUSE
bool no_true = true;
bool first = true;
// check if there is a clause whose literals are false.
@@ -412,16 +397,6 @@ namespace sat {
}
}
}
-#else
- for (unsigned i = 0; i < m_clauses.size(); ++i) {
- clause& c = *m_clauses[i];
- unsigned j = 0;
- for (; j < c.size() && !is_true(c[j]); ++j) {}
- if (j == c.size()) {
- return false;
- }
- }
-#endif
return true;
}
@@ -476,7 +451,6 @@ namespace sat {
for (literal lit : m_binary[l.index()]) {
if (is_undef(lit)) sum += literal_occs(lit) / 4.0;
}
-#ifdef NEW_CLAUSE
unsigned sz = m_ternary_count[(~l).index()];
for (binary const& b : m_ternary[(~l).index()]) {
if (sz-- == 0) break;
@@ -496,40 +470,6 @@ namespace sat {
unsigned len = m_nary_literals[idx];
sum += pow(0.5, len) * to_add / len;
}
-#else
- watch_list& wlist = m_watches[l.index()];
- for (auto & w : wlist) {
- switch (w.get_kind()) {
- case watched::BINARY:
- UNREACHABLE();
- break;
- case watched::TERNARY: {
- literal l1 = w.get_literal1();
- literal l2 = w.get_literal2();
- if (is_undef(l1) && is_undef(l2)) {
- sum += (literal_occs(l1) + literal_occs(l2)) / 8.0;
- }
- break;
- }
- case watched::CLAUSE: {
- clause_offset cls_off = w.get_clause_offset();
- clause & c = *(m_cls_allocator.get_clause(cls_off));
- unsigned sz = 0;
- double to_add = 0;
- for (literal lit : c) {
- if (is_undef(lit) && lit != ~l) {
- to_add += literal_occs(lit);
- ++sz;
- }
- }
- sum += pow(0.5, sz) * to_add / sz;
- break;
- }
- default:
- break;
- }
- }
-#endif
return sum;
}
@@ -546,45 +486,12 @@ namespace sat {
for (literal lit : m_binary[l.index()]) {
if (is_undef(lit)) sum += 0.5;
}
-#ifdef NEW_CLAUSE
sum += 0.25 * m_ternary_count[(~l).index()];
unsigned sz = m_nary_count[(~l).index()];
for (unsigned cls_idx : m_nary[(~l).index()]) {
if (sz-- == 0) break;
sum += pow(0.5, m_nary_literals[cls_idx]);
}
-#else
- watch_list& wlist = m_watches[l.index()];
- for (auto & w : wlist) {
- switch (w.get_kind()) {
- case watched::BINARY:
- UNREACHABLE();
- break;
- case watched::TERNARY: {
- literal l1 = w.get_literal1();
- literal l2 = w.get_literal2();
- if (is_undef(l1) && is_undef(l2)) {
- sum += 0.25;
- }
- break;
- }
- case watched::CLAUSE: {
- clause_offset cls_off = w.get_clause_offset();
- clause & c = *(m_cls_allocator.get_clause(cls_off));
- unsigned sz = 0;
- for (literal lit : c) {
- if (is_undef(lit) && lit != ~l) {
- ++sz;
- }
- }
- sum += pow(0.5, sz);
- break;
- }
- default:
- break;
- }
- }
-#endif
return sum;
}
@@ -621,44 +528,11 @@ namespace sat {
if (is_undef(lit)) sum += h[lit.index()];
// if (m_freevars.contains(lit.var())) sum += h[lit.index()];
}
-#ifdef NEW_CLAUSE
unsigned sz = m_ternary_count[(~l).index()];
for (binary const& b : m_ternary[(~l).index()]) {
if (sz-- == 0) break;
tsum += h[b.m_u.index()] * h[b.m_v.index()];
}
-#else
- watch_list& wlist = m_watches[l.index()];
- for (auto & w : wlist) {
- switch (w.get_kind()) {
- case watched::BINARY:
- UNREACHABLE();
- break;
- case watched::TERNARY: {
- literal l1 = w.get_literal1();
- literal l2 = w.get_literal2();
- // if (is_undef(l1) && is_undef(l2))
- tsum += h[l1.index()] * h[l2.index()];
- break;
- }
- case watched::CLAUSE: {
- clause_offset cls_off = w.get_clause_offset();
- clause & c = *(m_cls_allocator.get_clause(cls_off));
- // approximation compared to ternary clause case:
- // we pick two other literals from the clause.
- if (c[0] == ~l) {
- tsum += h[c[1].index()] * h[c[2].index()];
- }
- else {
- SASSERT(c[1] == ~l);
- tsum += h[c[0].index()] * h[c[2].index()];
- }
- break;
- }
- // case watched::EXTERNAL:
- }
- }
-#endif
// std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n";
sum = (double)(0.1 + afactor*sum + sqfactor*tsum);
// std::cout << "sum: " << sum << " max score " << m_config.m_max_score << "\n";
@@ -979,58 +853,6 @@ namespace sat {
}
-#ifndef NEW_CLAUSE
-
- // ------------------------------------
- // clause management
-
- void lookahead::attach_clause(clause& c) {
- if (c.size() == 3) {
- attach_ternary(c[0], c[1], c[2]);
- }
- else {
- literal block_lit = c[c.size() >> 2];
- clause_offset cls_off = m_cls_allocator.get_offset(&c);
- m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
- m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
- SASSERT(is_undef(c[0]));
- SASSERT(is_undef(c[1]));
- }
- }
-
- void lookahead::detach_clause(clause& c) {
- clause_offset cls_off = m_cls_allocator.get_offset(&c);
- m_retired_clauses.push_back(&c);
- erase_clause_watch(get_wlist(~c[0]), cls_off);
- erase_clause_watch(get_wlist(~c[1]), cls_off);
- }
-
- void lookahead::del_clauses() {
- for (clause * c : m_clauses) {
- m_cls_allocator.del_clause(c);
- }
- }
-
- void lookahead::detach_ternary(literal l1, literal l2, literal l3) {
- ++m_stats.m_del_ternary;
- m_retired_ternary.push_back(ternary(l1, l2, l3));
- // implicitly erased: erase_ternary_watch(get_wlist(~l1), l2, l3);
- erase_ternary_watch(get_wlist(~l2), l1, l3);
- erase_ternary_watch(get_wlist(~l3), l1, l2);
- }
-
- void lookahead::attach_ternary(ternary const& t) {
- attach_ternary(t.m_u, t.m_v, t.m_w);
- }
-
- void lookahead::attach_ternary(literal l1, literal l2, literal l3) {
- ++m_stats.m_add_ternary;
- TRACE("sat", tout << l1 << " " << l2 << " " << l3 << "\n";);
- m_watches[(~l1).index()].push_back(watched(l2, l3));
- m_watches[(~l2).index()].push_back(watched(l1, l3));
- m_watches[(~l3).index()].push_back(watched(l1, l2));
- }
-#endif
// ------------------------------------
// initialization
@@ -1040,10 +862,6 @@ namespace sat {
m_binary.push_back(literal_vector());
m_watches.push_back(watch_list());
m_watches.push_back(watch_list());
-#ifndef NEW_CLAUSE
- m_full_watches.push_back(clause_vector());
- m_full_watches.push_back(clause_vector());
-#else
m_ternary.push_back(svector<binary>());
m_ternary.push_back(svector<binary>());
m_ternary_count.push_back(0);
@@ -1052,7 +870,6 @@ namespace sat {
m_nary.push_back(unsigned_vector());
m_nary_count.push_back(0);
m_nary_count.push_back(0);
-#endif
m_bstamp.push_back(0);
m_bstamp.push_back(0);
m_stamp.push_back(0);
@@ -1121,7 +938,6 @@ namespace sat {
void lookahead::copy_clauses(clause_vector const& clauses, bool learned) {
// copy clauses
-#ifdef NEW_CLAUSE
for (clause* cp : clauses) {
clause& c = *cp;
if (c.was_removed()) continue;
@@ -1141,27 +957,6 @@ namespace sat {
}
if (m_s.m_config.m_drat) m_drat.add(c, false);
}
-#else
- for (clause* cp : clauses) {
- clause& c = *cp;
- if (c.was_removed()) continue;
- // enable when there is a non-ternary reward system.
- bool was_eliminated = false;
- for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) {
- was_eliminated = m_s.was_eliminated(c[i].var());
- }
- if (was_eliminated) continue;
-
- clause* c1 = m_cls_allocator.mk_clause(c.size(), c.begin(), false);
- m_clauses.push_back(c1);
- attach_clause(*c1);
- for (unsigned i = 0; i < c.size(); ++i) {
- m_full_watches[(~c[i]).index()].push_back(c1);
- SASSERT(!m_s.was_eliminated(c[i].var()));
- }
- if (m_s.m_config.m_drat) m_drat.add(c, false);
- }
-#endif
}
// ------------------------------------
@@ -1173,10 +968,6 @@ namespace sat {
m_binary_trail_lim.push_back(m_binary_trail.size());
m_trail_lim.push_back(m_trail.size());
m_num_tc1_lim.push_back(m_num_tc1);
-#ifndef NEW_CLAUSE
- m_retired_clause_lim.push_back(m_retired_clauses.size());
- m_retired_ternary_lim.push_back(m_retired_ternary.size());
-#endif
m_qhead_lim.push_back(m_qhead);
scoped_level _sl(*this, level);
m_assumptions.push_back(~lit);
@@ -1204,25 +995,6 @@ namespace sat {
m_num_tc1 = m_num_tc1_lim.back();
m_num_tc1_lim.pop_back();
-#ifndef NEW_CLAUSE
- m_trail.shrink(old_sz); // reset assignment.
- m_trail_lim.pop_back();
-
- // unretire clauses
- old_sz = m_retired_clause_lim.back();
- for (unsigned i = old_sz; i < m_retired_clauses.size(); ++i) {
- attach_clause(*m_retired_clauses[i]);
- }
- m_retired_clauses.resize(old_sz);
- m_retired_clause_lim.pop_back();
-
- old_sz = m_retired_ternary_lim.back();
- for (unsigned i = old_sz; i < m_retired_ternary.size(); ++i) {
- attach_ternary(m_retired_ternary[i]);
- }
- m_retired_ternary.shrink(old_sz);
- m_retired_ternary_lim.pop_back();
-#else
for (unsigned i = m_qhead; i > m_qhead_lim.back(); ) {
--i;
restore_ternary(m_trail[i]);
@@ -1232,8 +1004,6 @@ namespace sat {
m_trail.shrink(old_sz); // reset assignment.
m_trail_lim.pop_back();
-#endif
-
// remove local binary clauses
old_sz = m_binary_trail_lim.back();
@@ -1306,18 +1076,6 @@ namespace sat {
m_wstack.reset();
}
-#ifndef NEW_CLAUSE
- clause const& lookahead::get_clause(watch_list::iterator it) const {
- clause_offset cls_off = it->get_clause_offset();
- return *(m_cls_allocator.get_clause(cls_off));
- }
-
- bool lookahead::is_nary_propagation(clause const& c, literal l) const {
- bool r = c.size() > 2 && ((c[0] == l && is_false(c[1])) || (c[1] == l && is_false(c[0])));
- DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(is_false(c[j])););
- return r;
- }
-#endif
//
// The current version is modeled after CDCL SAT solving data-structures.
@@ -1336,7 +1094,6 @@ namespace sat {
double operator()(literal l) { return lh.literal_occs(l); }
};
-#ifdef NEW_CLAUSE
// Ternary clause managagement:
void lookahead::add_ternary(literal u, literal v, literal w) {
@@ -1510,38 +1267,6 @@ namespace sat {
m_nary_literals.push_back(null_literal.index());
}
-#if 0
- // split large clauses into smaller ones to avoid overhead during propagation.
-
- void lookahead::add_clause(unsigned sz, literal const * lits) {
- if (sz > 6) {
- bool_var v = m_s.mk_var(false);
- ++m_num_vars;
- init_var(v);
- literal lit(v, false);
- unsigned mid = sz / 2;
- literal_vector lits1(mid, lits);
- lits1.push_back(lit);
- add_clause(lits1.size(), lits1.c_ptr());
- lit.neg();
- literal_vector lits2(sz - mid, lits + mid);
- lits2.push_back(lit);
- add_clause(lits2.size(), lits2.c_ptr());
- }
- else {
- unsigned idx = m_nary_literals.size();
- m_nary_literals.push_back(sz);
- for (unsigned i = 0; i < sz; ++i) {
- literal l = lits[i];
- m_nary_literals.push_back(l.index());
- m_nary_count[l.index()]++;
- m_nary[l.index()].push_back(idx);
- SASSERT(m_nary_count[l.index()] == m_nary[l.index()].size());
- }
- m_nary_literals.push_back(null_literal.index());
- }
- }
-#endif
void lookahead::propagate_clauses_searching(literal l) {
// clauses where l is negative
@@ -1747,162 +1472,6 @@ namespace sat {
}
-#else
- void lookahead::propagate_clauses(literal l) {
- SASSERT(is_true(l));
- if (inconsistent()) return;
- watch_list& wlist = m_watches[l.index()];
- watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end();
- for (; it != end && !inconsistent(); ++it) {
- switch (it->get_kind()) {
- case watched::BINARY:
- UNREACHABLE();
- break;
- case watched::TERNARY: {
- literal l1 = it->get_literal1();
- literal l2 = it->get_literal2();
- bool skip = false;
- if (is_fixed(l1)) {
- if (is_false(l1)) {
- if (is_undef(l2)) {
- propagated(l2);
- }
- else if (is_false(l2)) {
- TRACE("sat", tout << l1 << " " << l2 << " " << l << "\n";);
- set_conflict();
- }
- }
- else {
- // retire this clause
- }
- }
- else if (is_fixed(l2)) {
- if (is_false(l2)) {
- propagated(l1);
- }
- else {
- // retire this clause
- }
- }
- else {
- switch (m_search_mode) {
- case lookahead_mode::searching:
- detach_ternary(~l, l1, l2);
- try_add_binary(l1, l2);
- skip = true;
- break;
- case lookahead_mode::lookahead1:
- update_binary_clause_reward(l1, l2);
- break;
- case lookahead2:
- break;
- }
- }
- if (!skip) {
- *it2 = *it;
- it2++;
- }
- break;
- }
- case watched::CLAUSE: {
- if (is_true(it->get_blocked_literal())) {
- *it2 = *it;
- ++it2;
- break;
- }
- clause_offset cls_off = it->get_clause_offset();
- clause & c = *(m_cls_allocator.get_clause(cls_off));
- if (c[0] == ~l)
- std::swap(c[0], c[1]);
- if (is_true(c[0])) {
- it->set_blocked_literal(c[0]);
- *it2 = *it;
- it2++;
- break;
- }
- literal * l_it = c.begin() + 2;
- literal * l_end = c.end();
- bool found = false;
- for (; l_it != l_end && !found; ++l_it) {
- if (!is_false(*l_it)) {
- found = true;
- c[1] = *l_it;
- *l_it = ~l;
- m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
- TRACE("sat_verbose", tout << "move watch from " << l << " to " << c[1] << " for clause " << c << "\n";);
- }
- }
- if (found) {
- found = false;
- for (; l_it != l_end && !found; ++l_it) {
- found = !is_false(*l_it);
- }
- // normal clause was converted to a binary clause.
- if (!found && is_undef(c[1]) && is_undef(c[0])) {
- TRACE("sat", tout << "got binary " << l << ": " << c << "\n";);
- switch (m_search_mode) {
- case lookahead_mode::searching:
- detach_clause(c);
- try_add_binary(c[0], c[1]);
- break;
- case lookahead_mode::lookahead1:
- update_binary_clause_reward(c[0], c[1]);
- break;
- case lookahead_mode::lookahead2:
- break;
- }
- }
- else if (found && m_search_mode == lookahead_mode::lookahead1) {
- update_nary_clause_reward(c);
- }
- break;
- }
- if (is_false(c[0])) {
- TRACE("sat", tout << "conflict " << l << ": " << c << "\n";);
- set_conflict();
- *it2 = *it;
- ++it2;
- }
- else {
- TRACE("sat", tout << "propagating " << l << ": " << c << "\n";);
- SASSERT(is_undef(c[0]));
- DEBUG_CODE(for (unsigned i = 2; i < c.size(); ++i) {
- SASSERT(is_false(c[i]));
- });
- *it2 = *it;
- it2++;
- propagated(c[0]);
- }
- break;
- }
- case watched::EXT_CONSTRAINT: {
- SASSERT(m_s.m_ext);
- bool keep = m_s.m_ext->propagate(l, it->get_ext_constraint_idx());
- if (m_search_mode == lookahead_mode::lookahead1 && !m_inconsistent) {
- lookahead_literal_occs_fun literal_occs_fn(*this);
- m_lookahead_reward += m_s.m_ext->get_reward(l, it->get_ext_constraint_idx(), literal_occs_fn);
- }
- if (m_inconsistent) {
- if (!keep) ++it;
- set_conflict();
- }
- else if (keep) {
- *it2 = *it;
- it2++;
- }
- break;
- }
- default:
- UNREACHABLE();
- break;
- }
- }
- for (; it != end; ++it, ++it2) {
- *it2 = *it;
- }
- wlist.set_end(it2);
- }
-#endif
void lookahead::update_binary_clause_reward(literal l1, literal l2) {
SASSERT(!is_false(l1));
@@ -1958,22 +1527,9 @@ namespace sat {
// Sum_{ clause C that contains ~l } 1
double lookahead::literal_occs(literal l) {
double result = m_binary[l.index()].size();
-#ifdef NEW_CLAUSE
unsigned_vector const& nclauses = m_nary[(~l).index()];
result += m_nary_count[(~l).index()];
result += m_ternary_count[(~l).index()];
-#else
- for (clause const* c : m_full_watches[l.index()]) {
- bool has_true = false;
- for (literal l : *c) {
- has_true = is_true(l);
- if (has_true) break;
- }
- if (!has_true) {
- result += 1.0;
- }
- }
-#endif
return result;
}
@@ -2167,11 +1723,9 @@ namespace sat {
++m_stats.m_autarky_propagations;
IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
-#ifdef NEW_CLAUSE
TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
<< " "
<< (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
-#endif
reset_lookahead_reward();
assign(l);
propagate();
@@ -2457,7 +2011,6 @@ namespace sat {
}
std::ostream& lookahead::display_clauses(std::ostream& out) const {
-#ifdef NEW_CLAUSE
bool first = true;
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
@@ -2487,11 +2040,6 @@ namespace sat {
}
}
-#else
- for (unsigned i = 0; i < m_clauses.size(); ++i) {
- out << *m_clauses[i] << "\n";
- }
-#endif
return out;
}
@@ -2719,11 +2267,7 @@ namespace sat {
void lookahead::collect_statistics(statistics& st) const {
st.update("lh bool var", m_vprefix.size());
-#ifndef NEW_CLAUSE
- st.update("lh clauses", m_clauses.size());
-#else
// TBD: keep count of ternary and >3-ary clauses.
-#endif
st.update("lh add binary", m_stats.m_add_binary);
st.update("lh del binary", m_stats.m_del_binary);
st.update("lh add ternary", m_stats.m_add_ternary);
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 87247611c..9a50dceed 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -20,7 +20,6 @@ Notes:
#ifndef _SAT_LOOKAHEAD_H_
#define _SAT_LOOKAHEAD_H_
-#define NEW_CLAUSE
#include "sat_elim_eqs.h"
@@ -125,19 +124,10 @@ namespace sat {
void reset() { memset(this, 0, sizeof(*this)); }
};
-#ifndef NEW_CLAUSE
- struct ternary {
- ternary(literal u, literal v, literal w): m_u(u), m_v(v), m_w(w) {}
- literal m_u, m_v, m_w;
- };
-#endif
-
-#ifdef NEW_CLAUSE
struct binary {
binary(literal u, literal v): m_u(u), m_v(v) {}
literal m_u, m_v;
};
-#endif
struct cube_state {
bool m_first;
@@ -165,7 +155,6 @@ namespace sat {
unsigned_vector m_binary_trail; // trail of added binary clauses
unsigned_vector m_binary_trail_lim;
-#ifdef NEW_CLAUSE
// specialized clause managemet uses ternary clauses and dedicated clause data-structure.
// this replaces m_clauses below
vector<svector<binary>> m_ternary; // lit |-> vector of ternary clauses
@@ -176,21 +165,10 @@ namespace sat {
unsigned_vector m_nary_literals; // the actual literals, clauses start at offset clause_id,
// the first entry is the current length, clauses are separated by a null_literal
-
-#endif
-
unsigned m_num_tc1;
unsigned_vector m_num_tc1_lim;
unsigned m_qhead; // propagation queue head
unsigned_vector m_qhead_lim;
-#ifndef NEW_CLAUSE
- clause_vector m_clauses; // non-binary clauses
- clause_vector m_retired_clauses; // clauses that were removed during search
- unsigned_vector m_retired_clause_lim;
- svector<ternary> m_retired_ternary; // ternary removed during search
- unsigned_vector m_retired_ternary_lim;
- clause_allocator m_cls_allocator;
-#endif
bool m_inconsistent;
unsigned_vector m_bstamp; // literal: timestamp for binary implication
vector<svector<double> > m_H; // literal: fitness score
@@ -203,9 +181,6 @@ namespace sat {
const unsigned c_fixed_truth = UINT_MAX - 1;
vector<watch_list> m_watches; // literal: watch structure
svector<lit_info> m_lits; // literal: attributes.
-#ifndef NEW_CLAUSE
- vector<clause_vector> m_full_watches; // literal: full watch list, used to ensure that autarky reduction is sound
-#endif
double m_lookahead_reward; // metric associated with current lookahead1 literal.
literal_vector m_wstack; // windofall stack that is populated in lookahead1 mode
unsigned m_last_prefix_length;
@@ -420,18 +395,9 @@ namespace sat {
// ------------------------------------
// clause management
-#ifndef NEW_CLAUSE
- void attach_clause(clause& c);
- void detach_clause(clause& c);
- void del_clauses();
- void detach_ternary(literal l1, literal l2, literal l3);
- void attach_ternary(ternary const& t);
- void attach_ternary(literal l1, literal l2, literal l3);
-#endif
watch_list& get_wlist(literal l) { return m_watches[l.index()]; }
watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; }
-#ifdef NEW_CLAUSE
// new clause managment:
void add_ternary(literal u, literal v, literal w);
void propagate_ternary(literal l);
@@ -446,7 +412,7 @@ namespace sat {
void restore_clauses(literal l);
void remove_clause(literal l, unsigned clause_idx);
void remove_clause_at(literal l, unsigned clause_idx);
-#endif
+
// ------------------------------------
// initialization
@@ -532,9 +498,6 @@ namespace sat {
}
~lookahead() {
-#ifndef NEW_CLAUSE
- del_clauses();
-#endif
m_s.rlimit().pop_child();
}