From 5c7eaec566f3db02026163142ced0b4be9556365 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2022 00:38:31 -0700 Subject: [PATCH] #6364 - remove option of redundant clauses from internalization gc-ing definitions leads to unsoundness when they are not replayed. Instead of attempting to replay definitions theory internalization is irredundant by default. This is also the old solver behavior where TH_LEMMA is essentially never used, but is valid for top-level theory lemmas. --- src/sat/smt/arith_internalize.cpp | 8 +++---- src/sat/smt/arith_solver.cpp | 5 ++--- src/sat/smt/arith_solver.h | 4 ++-- src/sat/smt/array_internalize.cpp | 10 ++++----- src/sat/smt/array_solver.h | 4 ++-- src/sat/smt/bv_internalize.cpp | 28 ++++++++++++------------ src/sat/smt/bv_solver.cpp | 4 ++-- src/sat/smt/bv_solver.h | 4 ++-- src/sat/smt/dt_solver.cpp | 10 ++++----- src/sat/smt/dt_solver.h | 4 ++-- src/sat/smt/euf_ackerman.cpp | 4 +--- src/sat/smt/euf_internalize.cpp | 36 +++++++++++++++---------------- src/sat/smt/euf_proof.cpp | 6 +++--- src/sat/smt/euf_solver.cpp | 30 +++++++++++++------------- src/sat/smt/euf_solver.h | 4 ++-- src/sat/smt/fpa_solver.cpp | 10 ++++----- src/sat/smt/fpa_solver.h | 4 ++-- src/sat/smt/pb_internalize.cpp | 9 ++++---- src/sat/smt/pb_solver.h | 4 ++-- src/sat/smt/q_solver.cpp | 6 +++--- src/sat/smt/q_solver.h | 4 ++-- src/sat/smt/recfun_solver.cpp | 10 ++++----- src/sat/smt/recfun_solver.h | 4 ++-- src/sat/smt/sat_internalizer.h | 2 +- src/sat/smt/sat_th.cpp | 13 ++++------- src/sat/smt/sat_th.h | 15 ++++++------- src/sat/smt/user_solver.cpp | 16 +++++++------- src/sat/smt/user_solver.h | 4 ++-- src/sat/tactic/goal2sat.cpp | 18 +++++++--------- 29 files changed, 133 insertions(+), 147 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 30eab0b5395..04a3ae4ef3a 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -20,9 +20,8 @@ Module Name: namespace arith { - sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { init_internalize(); - flet _is_learned(m_is_redundant, learned); internalize_atom(e); literal lit = ctx.expr2literal(e); if (sign) @@ -30,9 +29,8 @@ namespace arith { return lit; } - void solver::internalize(expr* e, bool redundant) { + void solver::internalize(expr* e) { init_internalize(); - flet _is_learned(m_is_redundant, redundant); if (m.is_bool(e)) internalize_atom(e); else @@ -247,7 +245,7 @@ namespace arith { ctx.push(push_back_vector(m_idiv_terms)); m_idiv_terms.push_back(n); app_ref mod(a.mk_mod(n1, n2), m); - internalize(mod, m_is_redundant); + internalize(mod); st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index eb0af0c690a..a658315e352 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -952,7 +952,6 @@ namespace arith { sat::check_result solver::check() { force_push(); m_model_is_initialized = false; - flet _is_learned(m_is_redundant, true); IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); SASSERT(lp().ax_is_correct()); @@ -1174,7 +1173,7 @@ namespace arith { for (auto const& c : core) m_core2.push_back(~c); m_core2.push_back(lit); - add_clause(m_core2, pma); + add_redundant(m_core2, pma); } else { auto* jst = euf::th_explain::propagate(*this, core, eqs, lit, pma); @@ -1215,7 +1214,7 @@ namespace arith { for (literal& c : m_core) c.neg(); - add_clause(m_core, explain(hint_type::farkas_h)); + add_redundant(m_core, explain(hint_type::farkas_h)); } bool solver::is_infeasible() const { diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 3d3f1ddd776..775fecd704e 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -504,8 +504,8 @@ namespace arith { void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); } void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool add_dep(euf::enode* n, top_sort& dep) override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; void eq_internalized(euf::enode* n) override; void apply_sort_cnstr(euf::enode* n, sort* s) override {} bool is_shared(theory_var v) const override; diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 4df4f3a505a..c7517f5a485 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -20,9 +20,9 @@ Module Name: namespace array { - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { SASSERT(m.is_bool(e)); - if (!visit_rec(m, e, sign, root, redundant)) { + if (!visit_rec(m, e, sign, root)) { TRACE("array", tout << mk_pp(e, m) << "\n";); return sat::null_literal; } @@ -32,8 +32,8 @@ namespace array { return lit; } - void solver::internalize(expr* e, bool redundant) { - visit_rec(m, e, false, false, redundant); + void solver::internalize(expr* e) { + visit_rec(m, e, false, false); } euf::theory_var solver::mk_var(euf::enode* n) { @@ -66,7 +66,7 @@ namespace array { if (visited(e)) return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); euf::enode* n = expr2enode(e); ensure_var(n); return true; diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 5c2708842da..4f100d69406 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -296,8 +296,8 @@ namespace array { bool include_func_interp(func_decl* f) const override { return a.is_ext(f); } void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool add_dep(euf::enode* n, top_sort& dep) override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; euf::theory_var mk_var(euf::enode* n) override; void apply_sort_cnstr(euf::enode* n, sort* s) override; bool is_shared(theory_var v) const override; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index cffd62acdc6..99d2a34ae11 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -99,10 +99,10 @@ namespace bv { get_var(n); } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { force_push(); SASSERT(m.is_bool(e)); - if (!visit_rec(m, e, sign, root, redundant)) + if (!visit_rec(m, e, sign, root)) return sat::null_literal; sat::literal lit = expr2literal(e); if (sign) @@ -110,14 +110,14 @@ namespace bv { return lit; } - void solver::internalize(expr* e, bool redundant) { + void solver::internalize(expr* e) { force_push(); - visit_rec(m, e, false, false, redundant); + visit_rec(m, e, false, false); } bool solver::visit(expr* e) { if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); return true; } m_stack.push_back(sat::eframe(e)); @@ -246,7 +246,7 @@ namespace bv { for (unsigned i = 0; i < bv_size; i++) { expr_ref b2b(bv.mk_bit2bool(e, i), m); m_bits[v].push_back(sat::null_literal); - sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant); + sat::literal lit = ctx.internalize(b2b, false, false); TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); if (m_bits[v].back() == sat::null_literal) m_bits[v].back() = lit; @@ -344,7 +344,7 @@ namespace bv { SASSERT(bits.size() == m_bits[v].size()); unsigned i = 0; for (expr* bit : bits) { - sat::literal lit = ctx.internalize(bit, false, false, m_is_redundant); + sat::literal lit = ctx.internalize(bit, false, false); TRACE("bv", tout << "set " << m_bits[v][i] << " == " << lit << "\n";); add_clause(~lit, m_bits[v][i]); add_clause(lit, ~m_bits[v][i]); @@ -353,7 +353,7 @@ namespace bv { return; } for (expr* bit : bits) - add_bit(v, ctx.internalize(bit, false, false, m_is_redundant)); + add_bit(v, ctx.internalize(bit, false, false)); for (expr* bit : bits) get_var(expr2enode(bit)); SASSERT(get_bv_size(n) == bits.size()); @@ -371,7 +371,7 @@ namespace bv { sat::literal solver::mk_true() { if (m_true == sat::null_literal) { ctx.push(value_trail(m_true)); - m_true = ctx.internalize(m.mk_true(), false, true, false); + m_true = ctx.internalize(m.mk_true(), false, true); s().assign_unit(m_true); } return m_true; @@ -493,7 +493,7 @@ namespace bv { m_bb.mk_sle(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le); else m_bb.mk_ule(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le); - literal def = ctx.internalize(le, false, false, m_is_redundant); + literal def = ctx.internalize(le, false, false); if (Negated) def.neg(); add_def(def, expr2literal(n)); @@ -598,7 +598,7 @@ namespace bv { get_arg_bits(n, 1, arg2_bits); expr_ref out(m); fn(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), out); - sat::literal def = ctx.internalize(out, false, false, m_is_redundant); + sat::literal def = ctx.internalize(out, false, false); add_def(def, expr2literal(n)); } @@ -753,12 +753,11 @@ namespace bv { return; if (v1 > v2) std::swap(v1, v2); - flet _red(m_is_redundant, true); ++m_stats.m_ackerman; expr* o1 = var2expr(v1); expr* o2 = var2expr(v2); expr_ref oe = mk_var_eq(v1, v2); - literal oeq = ctx.internalize(oe, false, false, m_is_redundant); + literal oeq = ctx.internalize(oe, false, false); unsigned sz = m_bits[v1].size(); TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";); literal_vector eqs; @@ -772,6 +771,7 @@ namespace bv { eqs.push_back(~eq); } TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";); - add_clause(eqs); + euf::th_proof_hint* ph = ctx.mk_smt_clause(name(), eqs.size(), eqs.data()); + s().mk_clause(eqs, sat::status::th(true, m.get_basic_family_id(), ph)); } } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index c50f7c4e6cb..f103f876aa7 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -168,7 +168,7 @@ namespace bv { TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2);); m_stats.m_num_diseq_static++; expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m); - add_unit(~ctx.internalize(eq, false, false, m_is_redundant)); + add_unit(~ctx.internalize(eq, false, false)); } std::ostream& solver::display(std::ostream& out, theory_var v) const { @@ -464,7 +464,7 @@ namespace bv { m_lit_head = m_lit_tail; m_lit_tail = m_proof_literals.size(); proof_hint* ph = new (get_region()) proof_hint(c.m_kind, m_proof_literals, m_lit_head, m_lit_tail, a1, a2, b1, b2); - auto st = sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + auto st = sat::status::th(false, m.get_basic_family_id(), ph); ctx.get_drat().add(lits, st); m_lit_head = m_lit_tail; // TBD, a proper way would be to delete the lemma after use. diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index e4a44e7698b..dc9cd1456b8 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -385,8 +385,8 @@ namespace bv { std::function& pb) override { return false; } bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override { return false; } - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; void eq_internalized(euf::enode* n) override; euf::theory_var mk_var(euf::enode* n) override; void apply_sort_cnstr(euf::enode * n, sort * s) override; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index a87f8770bd4..56a224d362f 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -804,8 +804,8 @@ namespace dt { } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { - if (!visit_rec(m, e, sign, root, redundant)) + sat::literal solver::internalize(expr* e, bool sign, bool root) { + if (!visit_rec(m, e, sign, root)) return sat::null_literal; auto lit = ctx.expr2literal(e); if (sign) @@ -813,15 +813,15 @@ namespace dt { return lit; } - void solver::internalize(expr* e, bool redundant) { - visit_rec(m, e, false, false, redundant); + void solver::internalize(expr* e) { + visit_rec(m, e, false, false); } bool solver::visit(expr* e) { if (visited(e)) return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); if (is_datatype(e)) mk_var(expr2enode(e)); return true; diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 4e2524f6bc9..51a7679fdd0 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -154,8 +154,8 @@ namespace dt { void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool add_dep(euf::enode* n, top_sort& dep) override; bool include_func_interp(func_decl* f) const override; - sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; euf::theory_var mk_var(euf::enode* n) override; void apply_sort_cnstr(euf::enode* n, sort* s) override; bool is_shared(theory_var v) const override { return false; } diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 19b1a28de3e..9061203146a 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -189,7 +189,6 @@ namespace euf { } void ackerman::add_cc(expr* _a, expr* _b) { - flet _is_redundant(ctx.m_is_redundant, true); app* a = to_app(_a); app* b = to_app(_b); TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); @@ -213,7 +212,6 @@ namespace euf { void ackerman::add_eq(expr* a, expr* b, expr* c) { if (a == c || b == c) return; - flet _is_redundant(ctx.m_is_redundant, true); sat::literal lits[3]; expr_ref eq1(ctx.mk_eq(a, c), m); expr_ref eq2(ctx.mk_eq(b, c), m); @@ -223,7 +221,7 @@ namespace euf { lits[1] = ~ctx.mk_literal(eq2); lits[2] = ctx.mk_literal(eq3); th_proof_hint* ph = ctx.mk_tc_proof_hint(lits); - ctx.s().mk_clause(3, lits, sat::status::th(true, m.get_basic_family_id(), ph)); + ctx.s().add_clause(3, lits, sat::status::th(true, m.get_basic_family_id(), ph)); } } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index c0b2540eae1..e2b116ea25c 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -34,28 +34,28 @@ Module Name: namespace euf { - void solver::internalize(expr* e, bool redundant) { + void solver::internalize(expr* e) { if (get_enode(e)) return; if (si.is_bool_op(e)) - attach_lit(si.internalize(e, redundant), e); + attach_lit(si.internalize(e), e); else if (auto* ext = expr2solver(e)) - ext->internalize(e, redundant); + ext->internalize(e); else - visit_rec(m, e, false, false, redundant); + visit_rec(m, e, false, false); SASSERT(m_egraph.find(e)); } sat::literal solver::mk_literal(expr* e) { expr_ref _e(e, m); bool is_not = m.is_not(e, e); - sat::literal lit = internalize(e, false, false, m_is_redundant); + sat::literal lit = internalize(e, false, false); if (is_not) lit.neg(); return lit; } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { euf::enode* n = get_enode(e); if (n) { if (m.is_bool(e)) { @@ -67,14 +67,14 @@ namespace euf { return sat::null_literal; } if (si.is_bool_op(e)) { - sat::literal lit = attach_lit(si.internalize(e, redundant), e); + sat::literal lit = attach_lit(si.internalize(e), e); if (sign) lit.neg(); return lit; } if (auto* ext = expr2solver(e)) - return ext->internalize(e, sign, root, redundant); - if (!visit_rec(m, e, sign, root, redundant)) { + return ext->internalize(e, sign, root); + if (!visit_rec(m, e, sign, root)) { TRACE("euf", tout << "visit-rec\n";); return sat::null_literal; } @@ -89,13 +89,13 @@ namespace euf { th_solver* s = nullptr; if (n && !si.is_bool_op(e) && (s = expr2solver(e), s && euf::null_theory_var == n->get_th_var(s->get_id()))) { // ensure that theory variables are attached in shared contexts. See notes (*) - s->internalize(e, false); + s->internalize(e); return true; } if (n) return true; if (si.is_bool_op(e)) { - attach_lit(si.internalize(e, m_is_redundant), e); + attach_lit(si.internalize(e), e); return true; } if (is_app(e) && to_app(e)->get_num_args() > 0) { @@ -103,7 +103,7 @@ namespace euf { return false; } if (auto* s = expr2solver(e)) - s->internalize(e, m_is_redundant); + s->internalize(e); else attach_node(mk_enode(e, 0, nullptr)); return true; @@ -118,7 +118,7 @@ namespace euf { return false; SASSERT(!get_enode(e)); if (auto* s = expr2solver(e)) - s->internalize(e, m_is_redundant); + s->internalize(e); else attach_node(mk_enode(e, num, m_args.data())); return true; @@ -167,8 +167,8 @@ namespace euf { ph1 = mk_smt_hint(symbol("tseitin"), ~lit, lit2); ph2 = mk_smt_hint(symbol("tseitin"), lit, ~lit2); } - s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph1)); - s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph2)); + s().mk_clause(~lit, lit2, sat::status::th(false, m.get_basic_family_id(), ph1)); + s().mk_clause(lit, ~lit2, sat::status::th(false, m.get_basic_family_id(), ph2)); add_aux(~lit, lit2); add_aux(lit, ~lit2); lit = lit2; @@ -258,7 +258,7 @@ namespace euf { } pb_util pb(m); expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m); - sat::literal lit = si.internalize(at_least2, m_is_redundant); + sat::literal lit = si.internalize(at_least2); s().add_clause(lit, mk_distinct_status(lit)); } } @@ -331,7 +331,7 @@ namespace euf { } expr_ref fml = mk_or(eqs); sat::literal dist(si.to_bool_var(e), false); - sat::literal some_eq = si.internalize(fml, m_is_redundant); + sat::literal some_eq = si.internalize(fml); add_root(~dist, ~some_eq); add_root(dist, some_eq); s().add_clause(~dist, ~some_eq, mk_distinct_status(~dist, ~some_eq)); @@ -461,7 +461,7 @@ namespace euf { euf::enode* solver::e_internalize(expr* e) { euf::enode* n = m_egraph.find(e); if (!n) { - internalize(e, m_is_redundant); + internalize(e); n = m_egraph.find(e); } return n; diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 742e00cd7b5..a8a9523fd24 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -238,12 +238,12 @@ namespace euf { sat::status solver::mk_tseitin_status(unsigned n, sat::literal const* lits) { th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("tseitin"), n, lits) : nullptr; - return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + return sat::status::th(false, m.get_basic_family_id(), ph); } sat::status solver::mk_distinct_status(unsigned n, sat::literal const* lits) { th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("alldiff"), n, lits) : nullptr; - return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + return sat::status::th(false, m.get_basic_family_id(), ph); } expr* smt_proof_hint::get_hint(euf::solver& s) const { @@ -294,7 +294,7 @@ namespace euf { lits.push_back(jst.lit_consequent()); if (jst.eq_consequent().first != nullptr) lits.push_back(add_lit(jst.eq_consequent())); - get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id(), jst.get_pragma())); + get_drat().add(lits, sat::status::th(false, jst.ext().get_id(), jst.get_pragma())); for (unsigned i = s().num_vars(); i < nv; ++i) set_tmp_bool_var(i, nullptr); } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 149e3b1a2bb..737148cd76d 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -655,14 +655,14 @@ namespace euf { if (si.is_bool_op(e)) lit = literal(replay.m[e], false); else - lit = si.internalize(e, false); + lit = si.internalize(e); VERIFY(lit.var() == v); if (!m_egraph.find(e) && !m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e) && !m.is_implies(e) && !m.is_xor(e)) { ptr_buffer args; if (is_app(e)) for (expr* arg : *to_app(e)) args.push_back(e_internalize(arg)); - internalize(e, true); + internalize(e); if (!m_egraph.find(e)) mk_enode(e, args.size(), args.data()); } @@ -692,10 +692,10 @@ namespace euf { disable_relevancy(e); return; } - auto lit = si.internalize(e, true); + auto lit = si.internalize(e); switch (to_app(e)->get_decl_kind()) { case OP_NOT: { - auto lit2 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(0)); add_aux(lit, lit2); add_aux(~lit, ~lit2); break; @@ -705,8 +705,8 @@ namespace euf { disable_relevancy(e); return; } - auto lit1 = si.internalize(to_app(e)->get_arg(0), true); - auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + auto lit1 = si.internalize(to_app(e)->get_arg(0)); + auto lit2 = si.internalize(to_app(e)->get_arg(1)); add_aux(~lit, ~lit1, lit2); add_aux(~lit, lit1, ~lit2); add_aux(lit, lit1, lit2); @@ -716,7 +716,7 @@ namespace euf { case OP_OR: { sat::literal_vector lits; for (expr* arg : *to_app(e)) - lits.push_back(si.internalize(arg, true)); + lits.push_back(si.internalize(arg)); for (auto lit2 : lits) add_aux(~lit2, lit); lits.push_back(~lit); @@ -726,7 +726,7 @@ namespace euf { case OP_AND: { sat::literal_vector lits; for (expr* arg : *to_app(e)) - lits.push_back(~si.internalize(arg, true)); + lits.push_back(~si.internalize(arg)); for (auto nlit2 : lits) add_aux(~lit, ~nlit2); lits.push_back(lit); @@ -740,9 +740,9 @@ namespace euf { add_aux(~lit); break; case OP_ITE: { - auto lit1 = si.internalize(to_app(e)->get_arg(0), true); - auto lit2 = si.internalize(to_app(e)->get_arg(1), true); - auto lit3 = si.internalize(to_app(e)->get_arg(2), true); + auto lit1 = si.internalize(to_app(e)->get_arg(0)); + auto lit2 = si.internalize(to_app(e)->get_arg(1)); + auto lit3 = si.internalize(to_app(e)->get_arg(2)); add_aux(~lit, ~lit1, lit2); add_aux(~lit, lit1, lit3); add_aux(lit, ~lit1, ~lit2); @@ -754,8 +754,8 @@ namespace euf { disable_relevancy(e); break; } - auto lit1 = si.internalize(to_app(e)->get_arg(0), true); - auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + auto lit1 = si.internalize(to_app(e)->get_arg(0)); + auto lit2 = si.internalize(to_app(e)->get_arg(1)); add_aux(lit, ~lit1, lit2); add_aux(lit, lit1, ~lit2); add_aux(~lit, lit1, lit2); @@ -767,8 +767,8 @@ namespace euf { disable_relevancy(e); break; } - auto lit1 = si.internalize(to_app(e)->get_arg(0), true); - auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + auto lit1 = si.internalize(to_app(e)->get_arg(0)); + auto lit2 = si.internalize(to_app(e)->get_arg(1)); add_aux(~lit, ~lit1, lit2); add_aux(lit, lit1); add_aux(lit, ~lit2); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 5e12324a430..beb0809fb07 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -439,8 +439,8 @@ namespace euf { bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; // internalize - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool learned) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; sat::literal mk_literal(expr* e); void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); } void attach_node(euf::enode* n); diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 4a57959532e..1de72d80be1 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -95,9 +95,9 @@ namespace fpa { TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_expr(), m) << " := " << v << "\n";); } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { SASSERT(m.is_bool(e)); - if (!visit_rec(m, e, sign, root, redundant)) + if (!visit_rec(m, e, sign, root)) return sat::null_literal; sat::literal lit = expr2literal(e); if (sign) @@ -105,8 +105,8 @@ namespace fpa { return lit; } - void solver::internalize(expr* e, bool redundant) { - visit_rec(m, e, false, false, redundant); + void solver::internalize(expr* e) { + visit_rec(m, e, false, false); } bool solver::visited(expr* e) { @@ -118,7 +118,7 @@ namespace fpa { if (visited(e)) return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); return true; } m_stack.push_back(sat::eframe(e)); diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h index 38abb399d71..1473ec463a7 100644 --- a/src/sat/smt/fpa_solver.h +++ b/src/sat/smt/fpa_solver.h @@ -59,8 +59,8 @@ namespace fpa { bool use_diseqs() const override { return true; } void new_diseq_eh(euf::th_eq const& eq) override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; void apply_sort_cnstr(euf::enode* n, sort* s) override; std::ostream& display(std::ostream& out) const override; diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp index eae1bbe5a2e..af25e7a9252 100644 --- a/src/sat/smt/pb_internalize.cpp +++ b/src/sat/smt/pb_internalize.cpp @@ -22,12 +22,11 @@ Module Name: namespace pb { - void solver::internalize(expr* e, bool redundant) { - internalize(e, false, false, redundant); + void solver::internalize(expr* e) { + internalize(e, false, false); } - literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { - flet _redundant(m_is_redundant, redundant); + literal solver::internalize(expr* e, bool sign, bool root) { if (m_pb.is_pb(e)) { sat::literal lit = internalize_pb(e, sign, root); if (m_ctx && !root && lit != sat::null_literal) @@ -84,7 +83,7 @@ namespace pb { void solver::convert_pb_args(app* t, literal_vector& lits) { for (expr* arg : *t) { - lits.push_back(si.internalize(arg, m_is_redundant)); + lits.push_back(si.internalize(arg)); s().set_external(lits.back().var()); } } diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index 09c0e47e043..f6a0c049e1f 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -402,8 +402,8 @@ namespace pb { bool is_blocked(literal l, sat::ext_constraint_idx idx) override; bool check_model(sat::model const& m) const override; - literal internalize(expr* e, bool sign, bool root, bool redundant) override; - void internalize(expr* e, bool redundant) override; + literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; euf::th_solver* clone(euf::solver& ctx) override; diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index ae37b7f072b..26c99180b19 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -53,7 +53,7 @@ namespace q { if (!m_flat.find(q, q_flat)) { if (expand(q)) { for (expr* e : m_expanded) { - sat::literal lit = ctx.internalize(e, l.sign(), false, false); + sat::literal lit = ctx.internalize(e, l.sign(), false); add_clause(~l, lit); } return; @@ -62,7 +62,7 @@ namespace q { } if (is_ground(q_flat->get_expr())) { - auto lit = ctx.internalize(q_flat->get_expr(), l.sign(), false, false); + auto lit = ctx.internalize(q_flat->get_expr(), l.sign(), false); add_clause(~l, lit); } else { @@ -163,7 +163,7 @@ namespace q { m_mbqi.init_search(); } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { SASSERT(is_forall(e) || is_exists(e)); sat::bool_var v = ctx.get_si().add_bool_var(e); sat::literal lit = ctx.attach_lit(sat::literal(v, false), e); diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 153cdc7743e..d0581f85203 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -95,8 +95,8 @@ namespace q { void collect_statistics(statistics& st) const override; euf::th_solver* clone(euf::solver& ctx) override; bool unit_propagate() override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override { internalize(e, false, false, redundant); } + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override { internalize(e, false, false); } euf::theory_var mk_var(euf::enode* n) override; void init_search() override; void finalize_model(model& mdl) override; diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index c88138d3fc1..aef9570340d 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -232,10 +232,10 @@ namespace recfun { ctx.push(push_back_vector>(m_propagation_queue)); } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { force_push(); SASSERT(m.is_bool(e)); - if (!visit_rec(m, e, sign, root, redundant)) { + if (!visit_rec(m, e, sign, root)) { TRACE("array", tout << mk_pp(e, m) << "\n";); return sat::null_literal; } @@ -245,9 +245,9 @@ namespace recfun { return lit; } - void solver::internalize(expr* e, bool redundant) { + void solver::internalize(expr* e) { force_push(); - visit_rec(m, e, false, false, redundant); + visit_rec(m, e, false, false); } bool solver::visited(expr* e) { @@ -259,7 +259,7 @@ namespace recfun { if (visited(e)) return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); return true; } m_stack.push_back(sat::eframe(e)); diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h index 4e41a35a94f..21d75623f15 100644 --- a/src/sat/smt/recfun_solver.h +++ b/src/sat/smt/recfun_solver.h @@ -101,8 +101,8 @@ namespace recfun { void collect_statistics(statistics& st) const override; euf::th_solver* clone(euf::solver& ctx) override; bool unit_propagate() override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; bool add_dep(euf::enode* n, top_sort& dep) override; void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool is_shared(euf::theory_var v) const override { return true; } diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h index 5fbf879ae1c..5be20c4e0ee 100644 --- a/src/sat/smt/sat_internalizer.h +++ b/src/sat/smt/sat_internalizer.h @@ -23,7 +23,7 @@ namespace sat { public: virtual ~sat_internalizer() = default; virtual bool is_bool_op(expr* e) const = 0; - virtual literal internalize(expr* e, bool learned) = 0; + virtual literal internalize(expr* e) = 0; virtual bool_var to_bool_var(expr* e) = 0; virtual bool_var add_bool_var(expr* e) = 0; virtual bool is_cached(app* t, literal l) const = 0; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 81fd7e3844b..17d167829ce 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -21,9 +21,8 @@ Module Name: namespace euf { - bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) { + bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root) { IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n"); - flet _is_learned(m_is_redundant, redundant); svector::scoped_stack _sc(m_stack); unsigned sz = m_stack.size(); visit(a); @@ -125,15 +124,11 @@ namespace euf { pop_core(n); } - sat::status th_euf_solver::mk_status(th_proof_hint const* ps) { - return sat::status::th(m_is_redundant, get_id(), ps); - } - bool th_euf_solver::add_unit(sat::literal lit, th_proof_hint const* ps) { if (ctx.use_drat() && !ps) ps = ctx.mk_smt_clause(name(), 1, &lit); bool was_true = is_true(lit); - ctx.s().add_clause(1, &lit, mk_status(ps)); + ctx.s().add_clause(1, &lit, sat::status::th(false, get_id(), ps)); ctx.add_root(lit); return !was_true; } @@ -161,7 +156,7 @@ namespace euf { return add_clause(4, lits, ps); } - bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) { + bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps, bool is_redundant) { if (ctx.use_drat() && !ps) ps = ctx.mk_smt_clause(name(), n, lits); @@ -169,7 +164,7 @@ namespace euf { for (unsigned i = 0; i < n; ++i) was_true |= is_true(lits[i]); ctx.add_root(n, lits); - s().add_clause(n, lits, mk_status(ps)); + s().add_clause(n, lits, sat::status::th(is_redundant, get_id(), ps)); return !was_true; } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index d64b656358f..a3b81a08d57 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -30,9 +30,8 @@ namespace euf { protected: euf::enode_vector m_args; svector m_stack; - bool m_is_redundant{ false }; - bool visit_rec(ast_manager& m, expr* e, bool sign, bool root, bool redundant); + bool visit_rec(ast_manager& m, expr* e, bool sign, bool root); virtual bool visit(expr* e) { return false; } virtual bool visited(expr* e) { return false; } @@ -41,9 +40,9 @@ namespace euf { public: virtual ~th_internalizer() = default; - virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0; + virtual sat::literal internalize(expr* e, bool sign, bool root) = 0; - virtual void internalize(expr* e, bool redundant) = 0; + virtual void internalize(expr* e) = 0; /** @@ -135,7 +134,7 @@ namespace euf { virtual bool is_beta_redex(euf::enode* p, euf::enode* n) const { return false; } - sat::status status() const { return sat::status::th(m_is_redundant, get_id()); } + sat::status status() const { return sat::status::th(false, get_id()); } }; @@ -155,8 +154,6 @@ namespace euf { sat::literal expr2literal(expr* e) const; region& get_region(); - - sat::status mk_status(th_proof_hint const* ps = nullptr); bool add_unit(sat::literal lit, th_proof_hint const* ps = nullptr); bool add_units(sat::literal_vector const& lits); bool add_clause(sat::literal lit, th_proof_hint const* ps = nullptr) { return add_unit(lit, ps); } @@ -164,9 +161,11 @@ namespace euf { bool add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps = nullptr); bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps = nullptr); bool add_clause(sat::literal_vector const& lits, th_proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); } - bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps = nullptr); + bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps, bool is_redundant = false); void add_equiv(sat::literal a, sat::literal b); void add_equiv_and(sat::literal a, sat::literal_vector const& bs); + bool add_redundant(sat::literal_vector const& lits, th_proof_hint const* ps) { return add_clause(lits.size(), lits.data(), ps, true); } + bool add_redundant(unsigned n, sat::literal* lits, th_proof_hint const* ps); bool is_true(sat::literal lit); diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 5c98a6face7..99e4eeeb1a7 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -30,7 +30,7 @@ namespace user_solver { void solver::add_expr(expr* e) { force_push(); - ctx.internalize(e, false); + ctx.internalize(e); euf::enode* n = expr2enode(e); if (is_attached_to_var(n)) return; @@ -63,7 +63,7 @@ namespace user_solver { return; } force_push(); - ctx.internalize(e, false); + ctx.internalize(e); m_next_split_expr = e; m_next_split_idx = idx; m_next_split_phase = phase; @@ -162,7 +162,7 @@ namespace user_solver { } void solver::propagate_consequence(prop_info const& prop) { - sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true); + sat::literal lit = ctx.internalize(prop.m_conseq, false, false); if (s().value(lit) != l_true) { s().assign(lit, mk_justification(m_qhead)); ++m_stats.m_num_propagations; @@ -250,8 +250,8 @@ namespace user_solver { return result; } - sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { - if (!visit_rec(m, e, sign, root, redundant)) { + sat::literal solver::internalize(expr* e, bool sign, bool root) { + if (!visit_rec(m, e, sign, root)) { TRACE("array", tout << mk_pp(e, m) << "\n";); return sat::null_literal; } @@ -263,15 +263,15 @@ namespace user_solver { return lit; } - void solver::internalize(expr* e, bool redundant) { - visit_rec(m, e, false, false, redundant); + void solver::internalize(expr* e) { + visit_rec(m, e, false, false); } bool solver::visit(expr* e) { if (visited(e)) return true; if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { - ctx.internalize(e, m_is_redundant); + ctx.internalize(e); return true; } m_stack.push_back(sat::eframe(e)); diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 28528b9a1d8..cb1c6fe94c8 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -154,8 +154,8 @@ namespace user_solver { bool unit_propagate() override; void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; void collect_statistics(statistics& st) const override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; - void internalize(expr* e, bool redundant) override; + sat::literal internalize(expr* e, bool sign, bool root) override; + void internalize(expr* e) override; std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index c819403d78f..403cee684c6 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -75,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer { func_decl_ref_vector m_unhandled_funs; bool m_default_external; bool m_euf = false; - bool m_is_redundant = false; bool m_top_level = false; sat::literal_vector aig_lits; @@ -133,7 +132,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } sat::status mk_status(euf::th_proof_hint* ph = nullptr) const { - return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + return sat::status::th(false, m.get_basic_family_id(), ph); } bool relevancy_enabled() { @@ -179,7 +178,7 @@ struct goal2sat::imp : public sat::sat_internalizer { TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";); if (relevancy_enabled()) ensure_euf()->add_root(n, lits); - m_solver.add_clause(n, lits, m_is_redundant ? mk_status(ph) : sat::status::input()); + m_solver.add_clause(n, lits, ph ? mk_status(ph) : sat::status::input()); } sat::bool_var add_var(bool is_ext, expr* n) { @@ -688,7 +687,7 @@ struct goal2sat::imp : public sat::sat_internalizer { sat::literal lit; { flet _top(m_top_level, false); - lit = euf->internalize(e, sign, root, m_is_redundant); + lit = euf->internalize(e, sign, root); } if (lit == sat::null_literal) return; @@ -711,7 +710,7 @@ struct goal2sat::imp : public sat::sat_internalizer { th = dynamic_cast(ext); SASSERT(th); } - auto lit = th->internalize(t, sign, root, m_is_redundant); + auto lit = th->internalize(t, sign, root); m_result_stack.shrink(m_result_stack.size() - t->get_num_args()); if (lit == sat::null_literal) return; @@ -780,12 +779,11 @@ struct goal2sat::imp : public sat::sat_internalizer { } }; - void process(expr* n, bool is_root, bool redundant) { + void process(expr* n, bool is_root) { TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 2) << " root: " << is_root << " result-stack: " << m_result_stack.size() << " frame-stack: " << m_frame_stack.size() << "\n";); - flet _is_redundant(m_is_redundant, redundant); scoped_stack _sc(*this, is_root); unsigned sz = m_frame_stack.size(); if (visit(n, is_root, false)) @@ -836,14 +834,14 @@ struct goal2sat::imp : public sat::sat_internalizer { << " result-stack: " << m_result_stack.size() << "\n";); } - sat::literal internalize(expr* n, bool redundant) override { + sat::literal internalize(expr* n) override { bool is_not = m.is_not(n, n); flet _top(m_top_level, false); unsigned sz = m_result_stack.size(); (void)sz; SASSERT(n->get_ref_count() > 0); TRACE("goal2sat", tout << "internalize " << mk_bounded_pp(n, m, 2) << "\n";); - process(n, false, redundant); + process(n, false); SASSERT(m_result_stack.size() == sz + 1); sat::literal result = m_result_stack.back(); TRACE("goal2sat", tout << "done internalize " << result << " " << mk_bounded_pp(n, m, 2) << "\n";); @@ -889,7 +887,7 @@ struct goal2sat::imp : public sat::sat_internalizer { flet _top(m_top_level, true); VERIFY(m_result_stack.empty()); TRACE("goal2sat", tout << "assert: " << mk_bounded_pp(n, m, 3) << "\n";); - process(n, true, m_is_redundant); + process(n, true); CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";); SASSERT(m_result_stack.empty()); }