From dc5e4ca1c5267e78b74951092b7e1de14333eff1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Jan 2019 13:19:09 -0800
Subject: [PATCH] fix drat generation in asymmetric branch simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_asymm_branch.cpp | 20 ++++++++++++++------
 src/sat/sat_drat.cpp         | 15 ++++++++++++++-
 src/tactic/goal.cpp          |  8 ++++----
 3 files changed, 32 insertions(+), 11 deletions(-)

diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 941426321..e25a79d5b 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -342,7 +342,10 @@ namespace sat {
                     break;
                 default:
                     if (!m_to_delete.contains(lit)) {
-                        c[j++] = lit;
+                        if (i != j) {
+                            std::swap(c[i], c[j]);
+                        }
+                        j++;
                     }
                     break;
                 }
@@ -406,12 +409,13 @@ namespace sat {
 
     bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
         VERIFY(s.m_trail.size() == s.m_qhead);
-        m_elim_literals += c.size() - new_sz;
+        unsigned old_sz = c.size();
+        m_elim_literals += old_sz - new_sz;
         if (c.is_learned()) {
-            m_elim_learned_literals += c.size() - new_sz; 
+            m_elim_learned_literals += old_sz - new_sz; 
         }
 
-        switch(new_sz) {
+        switch (new_sz) {
         case 0:
             s.set_conflict(justification());
             return false;
@@ -430,8 +434,12 @@ namespace sat {
             return false;
         default:
             c.shrink(new_sz);
-            if (s.m_config.m_drat) s.m_drat.add(c, true);
-            // if (s.m_config.m_drat) s.m_drat.del(c0); // TBD
+            if (s.m_config.m_drat && new_sz < old_sz) {
+                s.m_drat.add(c, true);
+                c.restore(old_sz);
+                s.m_drat.del(c);
+                c.shrink(new_sz);
+            }
             return true;
         }
     }
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index eea88bde7..110ad3b8a 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -585,8 +585,21 @@ namespace sat {
 
     void drat::del(clause& c) {
 
+#if 0
+        // check_duplicates:
+        for (literal lit : c) {
+            VERIFY(!m_seen[lit.index()]);
+            m_seen[lit.index()] = true;
+        }
+        for (literal lit : c) {
+            m_seen[lit.index()] = false;
+        }
+#endif
+
         TRACE("sat", tout << "del: " << c << "\n";);
-        if (m_out) dump(c.size(), c.begin(), status::deleted);
+        if (m_out) {
+            dump(c.size(), c.begin(), status::deleted);
+        }
         if (m_check) {
             clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); 
             append(*c1, status::deleted);
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 6444cbc05..8f8b86a65 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -480,15 +480,15 @@ void goal::display_dimacs(std::ostream & out) const {
                 out << "-";
                 l = to_app(l)->get_arg(0);
             }
-            unsigned id = expr2var[l->get_id()];
-            SASSERT(id != UINT_MAX);
-            out << id << " ";
+            SASSERT(exprs[l->get_id()]);
+            out << expr2var[l->get_id()] << " ";
         }
         out << "0\n";
     }
     for (expr* e : exprs) {
         if (e && is_app(e)) {
-            out << "c " << expr2var[e->get_id()] << " " << to_app(e)->get_decl()->get_name() << "\n";
+            symbol const& n = to_app(e)->get_decl()->get_name();
+            out << "c " << expr2var[e->get_id()] << " " << n << "\n";            
         }
     }
 }