record simplified input clauses as lemmas

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_cleaner.cpp

@@ -78,7 +78,6 @@ namespace sat {
     }
 
     void cleaner::cleanup_clauses(clause_vector & cs) {
-        tmp_clause tmp;
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = cs.end();
@@ -134,10 +133,6 @@ namespace sat {
                     s.del_clause(c);
                     break;
                 default:
-                    SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
-                    if (s.m_config.m_drat && new_sz < sz) {
-                        tmp.set(c.size(), c.begin(), c.is_learned());
-                    }
                     c.shrink(new_sz);
                     *it2 = *it;
                     it2++;
@@ -145,11 +140,12 @@ namespace sat {
                         s.attach_clause(c);
                     }
                     if (s.m_config.m_drat && new_sz < sz) {
-                        // for optimization, could also report deletion 
-                        // of previous version of clause.
                         s.m_drat.add(c, true);
-                        s.m_drat.del(*tmp.get());
+                        c.restore(sz);
+                        s.m_drat.del(c);
+                        c.shrink(new_sz);
                     }
+                    break;
                 }
             }
         }

src/sat/sat_solver.cpp

@@ -320,11 +320,18 @@ namespace sat {
     clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
         TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << (learned?" learned":" aux") << "\n";);
         if (!learned) {
+            unsigned old_sz = num_lits;
             bool keep = simplify_clause(num_lits, lits);
             TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";);
             if (!keep) {
                 return nullptr; // clause is equivalent to true.
             }
+            // if an input clause is simplified, then log the simplified version as learned
+            if (!learned && old_sz > num_lits && m_config.m_drat) {
+                m_lemma.reset();
+                m_lemma.append(num_lits, lits);
+                m_drat.add(m_lemma);
+            }
             ++m_stats.m_non_learned_generation;
         }
         
@@ -706,7 +713,7 @@ namespace sat {
                 if (curr != prev) {
                     prev = curr;
                     if (i != j)
-                        lits[j] = lits[i];
+                        std::swap(lits[j], lits[i]);
                     j++;
                 }
                 break;

src/smt/mam.cpp

@@ -3915,7 +3915,7 @@ namespace smt {
                 SASSERT(bindings[i]->get_generation() <= max_generation);
             }
 #endif
-            unsigned min_gen, max_gen;
+            unsigned min_gen = 0, max_gen = 0;
             m_interpreter.get_min_max_top_generation(min_gen, max_gen);
             m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes);
         }

src/smt/smt_clause.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include "smt/smt_clause.h"
 #include "smt/smt_justification.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
 
 namespace smt {
     /**
@@ -96,22 +97,33 @@ namespace smt {
         }
     }
 
-    void clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
+    std::ostream& clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
         out << "(clause";
         for (unsigned i = 0; i < m_num_literals; i++) {
             out << " ";
             m_lits[i].display(out, m, bool_var2expr_map);
         }
-        out << ")";
+        return out << ")";
     }
 
-    void clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
+    std::ostream& clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
         out << "(clause";
         for (unsigned i = 0; i < m_num_literals; i++) {
             out << " ";
             m_lits[i].display_compact(out, bool_var2expr_map);
         }
-        out << ")";
+        return out << ")";
+    }
+
+    std::ostream& clause::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < m_num_literals; i++) {
+            literal lit = m_lits[i];
+            args.push_back(bool_var2expr_map[lit.var()]);
+            if (lit.sign()) args[args.size()-1] = m.mk_not(args.back());
+        }
+        expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m);
+        return out << disj;
     }
 
 };

src/smt/smt_clause.h

@@ -239,9 +239,11 @@ namespace smt {
             set_activity(get_activity() + 1);
         }
 
-        void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
+        std::ostream& display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
+        
+        std::ostream& display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
 
-        void display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
+        std::ostream& display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
 
         unsigned hash() const {
             return get_ptr_hash(this); 

src/smt/smt_context_pp.cpp

@@ -160,7 +160,7 @@ namespace smt {
     }
 
     void context::display_clause(std::ostream & out, clause const * cls) const {
-        cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
+        cls->display_smt2(out, m_manager, m_bool_var2expr.c_ptr());
     }
 
     void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
@@ -185,11 +185,18 @@ namespace smt {
                         out << "binary clauses:\n";
                         first = false;
                     }
+                    expr_ref t1(m_manager), t2(m_manager);
+                    literal2expr(neg_l1, t1);
+                    literal2expr(l2, t2);
+                    expr_ref disj(m_manager.mk_or(t1, t2), m_manager);
+                    out << disj << "\n";
+#if 0
                     out << "(clause ";
                     display_literal(out, neg_l1);
                     out << " ";
                     display_literal(out, l2);
                     out << ")\n";
+#endif
                 }
             }
         }

src/smt/smt_quantifier.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 #include "ast/ast_pp.h"
-#include "ast/ast_smt2_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "smt/smt_quantifier.h"
 #include "smt/smt_context.h"
 #include "smt/smt_quantifier_stat.h"
@@ -260,13 +260,20 @@ namespace smt {
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
                 m_num_instances++;
             }
-            TRACE("quantifier",
+            static unsigned count = 0;
-                  tout << mk_pp(q, m()) << " ";
+            CTRACE("quantifier", f != nullptr, 
+                   tout << (count++) << " " << q->get_id() << "\n";
+                   if (q->get_id() == 28 || true) {
+                       tout << mk_ll_pp(q, m()) << "\n";
+                   }
+                   );
+
+            CTRACE("quantifier_", f != nullptr, 
+                  tout << expr_ref(q, m()) << " ";
                   for (unsigned i = 0; i < num_bindings; ++i) {
-                      tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
+                      tout << expr_ref(bindings[i]->get_owner(), m()) << " ";
                   }
                   tout << "\n";
-                  tout << "inserted: " << (f != nullptr) << "\n";
                   );
 
             return f != nullptr;
@@ -646,7 +653,7 @@ namespace smt {
                     m_lazy_mam->add_pattern(q, mp);
                 }
                 else {
-                    TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m) << "\n";);
+                    TRACE("quantifier", tout << "adding:\n" << expr_ref(mp, m) << "\n";);
                     m_mam->add_pattern(q, mp);
                 }
                 if (!unary)