fixes in new solver

fix logging and lemma signs in arith_solver, move logging of drat equalities to euf

src/sat/smt/arith_solver.cpp

@@ -1120,9 +1120,12 @@ namespace arith {
     void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
         reset_evidence();
         m_core.append(core);
+        TRACE("arith", 
+              tout << "Core - " << is_conflict << "\n";
+              for (literal c : m_core) tout << literal2expr(c) << "\n";);
+
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
-        TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto const& ev : m_explanation)
             set_evidence(ev.ci(), m_core, m_eqs);
         DEBUG_CODE(
@@ -1134,6 +1137,11 @@ namespace arith {
             m_core.push_back(eq_internalize(eq.first, eq.second));
         for (literal& c : m_core)
             c.neg();
+        TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n");
+              tout << "Clause\n";
+              for (literal c : m_core) tout << literal2expr(c) << "\n";              
+              );
+
         add_clause(m_core);
     }
 
@@ -1322,25 +1330,23 @@ namespace arith {
         for (auto const& ineq : m_lemma.ineqs()) {
             bool is_lower = true, pos = true, is_eq = false;
             switch (ineq.cmp()) {
-            case lp::LE: is_lower = false; pos = false;  break;
+            case lp::LE: is_lower = false; pos = false; break;
-            case lp::LT: is_lower = true;  pos = true; break;
+            case lp::LT: is_lower = true;  pos = true;  break;
-            case lp::GE: is_lower = true;  pos = false;  break;
+            case lp::GE: is_lower = true;  pos = false; break;
-            case lp::GT: is_lower = false; pos = true; break;
+            case lp::GT: is_lower = false; pos = true;  break;
-            case lp::EQ: is_eq = true; pos = false; break;
+            case lp::EQ: is_eq = true;     pos = false; break;
-            case lp::NE: is_eq = true; pos = true; break;
+            case lp::NE: is_eq = true;     pos = true;  break;
             default: UNREACHABLE();
             }
             TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
-            app_ref atom(m);
             // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
             // then term is used instead of ineq.m_term
-            if (is_eq) {
+            sat::literal lit;
-                core.push_back(~mk_eq(ineq.term(), ineq.rs()));
+            if (is_eq) 
-            }
+                lit = mk_eq(ineq.term(), ineq.rs());
-            else {
+            else 
-                // create term >= 0 (or term <= 0)
+                lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
-                core.push_back(~ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower)));
+            core.push_back(pos ? lit : ~lit);
-            }
         }
         set_conflict_or_lemma(core, false);
     }

src/sat/smt/bv_solver.cpp

@@ -345,12 +345,8 @@ namespace bv {
         if (c.m_kind != bv_justification::kind_t::bit2ne) {
             expr* e1 = var2expr(c.m_v1);
             expr* e2 = var2expr(c.m_v2);
-            eq = m.mk_eq(e1, e2);                                           
+            eq = m.mk_eq(e1, e2);       
-            ctx.get_drat().def_begin('e', eq->get_id(), std::string("="));
+            ctx.drat_eq_def(leq, eq);
-            ctx.get_drat().def_add_arg(e1->get_id());
-            ctx.get_drat().def_add_arg(e2->get_id());
-            ctx.get_drat().def_end();
-            ctx.get_drat().bool_def(leq.var(), eq->get_id());
         }
 
         static unsigned s_count = 0;

src/sat/smt/euf_proof.cpp

@@ -126,5 +126,32 @@ namespace euf {
         }
     }
 
+    void solver::log_justification(literal l, th_propagation const& jst) {
+        literal_vector lits;
+        for (auto lit : euf::th_propagation::lits(jst))
+            lits.push_back(~lit);
+        lits.push_back(l);
+        unsigned nv = s().num_vars();
+        expr_ref_vector eqs(m);
+        for (auto eq : euf::th_propagation::eqs(jst)) {
+            ++nv;
+            literal lit(nv, false);
+            eqs.push_back(m.mk_eq(eq.first->get_expr(), eq.second->get_expr()));
+            drat_eq_def(lit, eqs.back());            
+            lits.push_back(lit);
+        }
+        
+        get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id()));
+    }
+
+    void solver::drat_eq_def(literal lit, expr* eq) {
+        expr *a = nullptr, *b = nullptr;
+        VERIFY(m.is_eq(eq, a, b));
+        get_drat().def_begin('e', eq->get_id(), std::string("="));
+        get_drat().def_add_arg(a->get_id());
+        get_drat().def_add_arg(b->get_id());
+        get_drat().def_end();
+        get_drat().bool_def(lit.var(), eq->get_id());
+    }
 
 }

src/sat/smt/euf_solver.cpp

@@ -211,15 +211,8 @@ namespace euf {
         for (auto eq : euf::th_propagation::eqs(jst))
             add_antecedent(eq.first, eq.second);
 
-        if (!probing && use_drat()) {
+        if (!probing && use_drat()) 
-            literal_vector lits;
+            log_justification(l, jst);
-            for (auto lit : euf::th_propagation::lits(jst))
-                lits.push_back(~lit);
-            lits.push_back(l);
-            get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id()));
-            for (auto eq : euf::th_propagation::eqs(jst))
-                IF_VERBOSE(0, verbose_stream() << "drat-log with equalities is TBD " << eq.first->get_expr_id() << "\n");
-        }
     }
 
     void solver::add_antecedent(enode* a, enode* b) {

src/sat/smt/euf_solver.h

@@ -156,6 +156,7 @@ namespace euf {
         // proofs
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
         void log_antecedents(literal l, literal_vector const& r);
+        void log_justification(literal l, th_propagation const& jst);
         void drat_log_decl(func_decl* f);
         void drat_log_expr(expr* n);
         void drat_log_expr1(expr* n);
@@ -293,6 +294,7 @@ namespace euf {
         bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
         sat::drat& get_drat() { return s().get_drat(); }
         void drat_bool_def(sat::bool_var v, expr* n);
+        void drat_eq_def(sat::literal lit, expr* eq);
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,

src/shell/drat_frontend.cpp

@@ -203,12 +203,12 @@ public:
                 }
                 if (name == "Real" && sz == 4) {
                     arith_util au(m);
-                    rational num = sexpr->get_child(2)->get_numeral();
+                    rational r = sexpr->get_child(2)->get_numeral();
-                    rational den = sexpr->get_child(3)->get_numeral();
+                    // rational den = sexpr->get_child(3)->get_numeral();
-                    result = au.mk_numeral(num/den, false);
+                    result = au.mk_numeral(r, false);
                     return;
                 }
-                if (name == "Int" && sz == 3) {
+                if (name == "Int" && sz == 4) {
                     arith_util au(m);
                     rational num = sexpr->get_child(2)->get_numeral();
                     result = au.mk_numeral(num, true);