From 0c2e3c0894b8bf3b59fb97c42c71dd1f90a0f5f1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 29 May 2018 15:40:39 -0700
Subject: [PATCH] fixes to clause proof tracking

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/spacer_antiunify.cpp |  4 +--
 src/smt/smt_conflict_resolution.cpp |  1 +
 src/smt/smt_conflict_resolution.h   |  2 +-
 src/smt/smt_context.cpp             | 46 ++++++++---------------------
 src/smt/smt_setup.cpp               |  3 +-
 5 files changed, 19 insertions(+), 37 deletions(-)

diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp
index 8b5e9e75b..0edfb6598 100644
--- a/src/muz/spacer/spacer_antiunify.cpp
+++ b/src/muz/spacer/spacer_antiunify.cpp
@@ -57,8 +57,8 @@ struct var_abs_rewriter : public default_rewriter_cfg {
         {
             bool contains_const_child = false;
             app* a = to_app(t);
-            for (unsigned i=0, sz = a->get_num_args(); i < sz; ++i) {
-                if (m_util.is_numeral(a->get_arg(i))) {
+            for (expr * arg : *a) {
+                if (m_util.is_numeral(arg)) {
                     contains_const_child = true;
                 }
             }
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 7984fd5f0..f7bc60051 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1033,6 +1033,7 @@ namespace smt {
             return pr;
         }
         SASSERT(js != 0);
+        TRACE("proof_gen_bug", tout << js << "\n";);
         m_todo_pr.push_back(tp_elem(js));
         return nullptr;
     }
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index b5b857184..90390ae7e 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -96,7 +96,7 @@ namespace smt {
             };
             tp_elem(literal l):m_kind(LITERAL), m_lidx(l.index()) {}
             tp_elem(enode * lhs, enode * rhs):m_kind(EQUALITY), m_lhs(lhs), m_rhs(rhs) {}
-            tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) {}
+        tp_elem(justification * js):m_kind(JUSTIFICATION), m_js(js) { SASSERT(js);}
         };
 
         svector<tp_elem>               m_todo_pr;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ab7e4fa35..c6f77cf1f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3144,8 +3144,14 @@ namespace smt {
             mark_as_relevant(lit);
             m_clause_lits.push_back(get_literal(lit));
         }
-        if (m_clause_lits.size() > 2) 
-            m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX);
+        if (m_clause_lits.size() >= 2) {
+            justification* js = nullptr;
+            if (m_manager.proofs_enabled()) {
+                proof * pr = mk_clause_def_axiom(m_clause_lits.size(), m_clause_lits.c_ptr(), nullptr);
+                js = mk_justification(justification_proof_wrapper(*this, pr));
+            }
+            m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX, js);
+        }
     }
 
     lbool context::decide_clause() {
@@ -3163,38 +3169,12 @@ namespace smt {
                 return l_undef;
             }            
         }
-        for (unsigned i = m_assigned_literals.size(); i-- > 0; ) {
-            literal nlit = ~m_assigned_literals[i];
-            if (m_clause_lits.contains(nlit)) {
-                switch (m_clause_lits.size()) {
-                case 1: {
-                    b_justification js;
-                    set_conflict(js, ~nlit);
-                    break;
-                } 
-                case 2: {
-                    if (nlit == m_clause_lits[1]) {
-                        std::swap(m_clause_lits[0], m_clause_lits[1]);
-                    }
-                    b_justification js(~m_clause_lits[1]);
-                    set_conflict(js, ~nlit);
-                    break;
-                }
-                default: {
-                    for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) {
-                        if (m_clause->get_literal(j) == nlit) {
-                            if (j > 0) m_clause->swap_lits(j, 0);
-                            break;
-                        }
-                    }
-                    b_justification js(m_clause);
-                    set_conflict(js, ~nlit);
-                    break;
-                }
-                }
-                break;
-            }
+        if (m_clause_lits.size() == 1) {
+            set_conflict(b_justification(), ~m_clause_lits[0]);
         }
+        else {
+            set_conflict(b_justification(m_clause), null_literal);
+        }		
         VERIFY(!resolve_conflict());
         return l_false;
     }
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 3ab40cdc3..97f5c433c 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -730,7 +730,8 @@ namespace smt {
     }
 
     void setup::setup_i_arith() {
-        m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));        
+        m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
+        // m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));        
     }
 
     void setup::setup_r_arith() {