#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

@@ -20,19 +20,17 @@ 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<bool> _is_learned(m_is_redundant, learned);
         internalize_atom(e);
         literal lit = ctx.expr2literal(e);
         if (sign)
             lit.neg();
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
+    void solver::internalize(expr* e) {
         init_internalize();
-        flet<bool> _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);
                 }

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<bool> _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 {

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<euf::enode>& 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;

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;

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<euf::enode>& 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;

src/sat/smt/bv_internalize.cpp

@@ -99,25 +99,25 @@ 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)
             lit.neg();
         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<sat::literal>(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<bool> _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));
     }
 }

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.

src/sat/smt/bv_solver.h

@@ -385,8 +385,8 @@ namespace bv {
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& 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;

src/sat/smt/dt_solver.cpp

@@ -804,24 +804,24 @@ 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)
             lit.neg();
         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;

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<euf::enode>& 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; }

src/sat/smt/euf_ackerman.cpp

@@ -189,7 +189,6 @@ namespace euf {
     }
 
     void ackerman::add_cc(expr* _a, expr* _b) {     
-        flet<bool> _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<bool> _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));        
     }
 
 }