From cdfab8cb132d2a6379d75529950f5b352396c1fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Oct 2022 14:50:21 -0700
Subject: [PATCH] wip - add bit-vector validator plugins and logging

---
 src/sat/smt/CMakeLists.txt        |  1 +
 src/sat/smt/bv_solver.cpp         | 85 ++++++++++++++++++++++-----
 src/sat/smt/bv_solver.h           | 16 +++++-
 src/sat/smt/bv_theory_checker.cpp | 76 +++++++++++++++++++++++++
 src/sat/smt/bv_theory_checker.h   | 95 +++++++++++++++++++++++++++++++
 src/sat/smt/euf_internalize.cpp   | 10 ++--
 src/sat/smt/euf_proof_checker.cpp |  8 ++-
 src/sat/smt/euf_solver.h          |  4 +-
 8 files changed, 272 insertions(+), 23 deletions(-)
 create mode 100644 src/sat/smt/bv_theory_checker.cpp
 create mode 100644 src/sat/smt/bv_theory_checker.h

diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index cef7f96c4..22fc9963c 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -15,6 +15,7 @@ z3_add_component(sat_smt
     bv_internalize.cpp
     bv_invariant.cpp
     bv_solver.cpp
+    bv_theory_checker.cpp
     dt_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 8ef2c5cd5..c50f7c4e6 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -395,68 +395,123 @@ namespace bv {
         sat::literal leq1(s().num_vars() + 1, false);
         sat::literal leq2(s().num_vars() + 2, false);
         expr_ref eq1(m), eq2(m);
+        expr* a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr;
+        
         if (c.m_kind == bv_justification::kind_t::bv2int) {
-            eq1 = m.mk_eq(c.a->get_expr(), c.b->get_expr());
-            eq2 = m.mk_eq(c.a->get_expr(), c.c->get_expr());
-            ctx.set_tmp_bool_var(leq1.var(), eq1);
-            ctx.set_tmp_bool_var(leq2.var(), eq1);
+            a1 = c.a->get_expr();
+            a2 = c.b->get_expr();
+            b1 = c.a->get_expr();
+            b2 = c.c->get_expr();
         }
         else if (c.m_kind != bv_justification::kind_t::bit2ne) {
-            expr* e1 = var2expr(c.m_v1);
-            expr* e2 = var2expr(c.m_v2);
-            eq1 = m.mk_eq(e1, e2);      
+            a1 = var2expr(c.m_v1);
+            a2 = var2expr(c.m_v2);
+        }
+
+        if (a1) {
+            eq1 = m.mk_eq(a1, a2);
             ctx.set_tmp_bool_var(leq1.var(), eq1);
         }
 
+        if (b1) {
+            eq2 = m.mk_eq(b1, b2);
+            ctx.set_tmp_bool_var(leq2.var(), eq2);
+        }
+
+        ctx.push(value_trail(m_lit_tail));
+        ctx.push(restore_size_trail(m_proof_literals));
+
         sat::literal_vector lits;
         switch (c.m_kind) {
         case bv_justification::kind_t::eq2bit:
-            lits.push_back(~leq1);
             lits.push_back(~c.m_antecedent);
             lits.push_back(c.m_consequent);
+            m_proof_literals.append(lits);
+            lits.push_back(~leq1);
             break;
         case bv_justification::kind_t::ne2bit:
             get_antecedents(c.m_consequent, c.to_index(), lits, true);
+            for (auto& lit : lits)
+                lit.neg();
             lits.push_back(c.m_consequent);
+            m_proof_literals.append(lits);
             break;
         case bv_justification::kind_t::bit2eq:      
             get_antecedents(leq1, c.to_index(), lits, true);
             for (auto& lit : lits)
                 lit.neg();
+            m_proof_literals.append(lits);
             lits.push_back(leq1);
             break;
         case bv_justification::kind_t::bit2ne: 
             get_antecedents(c.m_consequent, c.to_index(), lits, true);
+            lits.push_back(~c.m_consequent);            
             for (auto& lit : lits)
                 lit.neg();
-            lits.push_back(c.m_consequent);            
+            m_proof_literals.append(lits);
             break;
         case bv_justification::kind_t::bv2int:
             get_antecedents(leq1, c.to_index(), lits, true);
             get_antecedents(leq2, c.to_index(), lits, true);
             for (auto& lit : lits)
                 lit.neg();
+            m_proof_literals.append(lits);
             lits.push_back(leq1);
             lits.push_back(leq2);
             break;
         }
-        ctx.get_drat().add(lits, status());
+        
+        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);
+        ctx.get_drat().add(lits, st);
+        m_lit_head = m_lit_tail;
         // TBD, a proper way would be to delete the lemma after use.
         ctx.set_tmp_bool_var(leq1.var(), nullptr);
         ctx.set_tmp_bool_var(leq2.var(), nullptr);
-
     }
 
-    void solver::asserted(literal l) {
-        
+    expr* solver::proof_hint::get_hint(euf::solver& s) const {
+        ast_manager& m = s.get_manager();
+        sort* proof = m.mk_proof_sort();
+        expr_ref_vector& args = s.expr_args();
+        ptr_buffer<sort> sorts;
+        for (unsigned i = m_lit_head; i < m_lit_tail; ++i) 
+            args.push_back(s.literal2expr(m_proof_literals[i]));
+        if (m_kind == bv_justification::kind_t::eq2bit)
+            args.push_back(m.mk_not(m.mk_eq(a1, a2)));            
+        else if (a1) 
+            args.push_back(m.mk_eq(a1, a2));
+        if (b1) 
+            args.push_back(m.mk_eq(b1, b2));
+        for (auto * arg : args)
+            sorts.push_back(arg->get_sort());
+        symbol th;
+        switch (m_kind) {
+        case bv_justification::kind_t::eq2bit:
+            th = "eq2bit"; break;
+        case bv_justification::kind_t::ne2bit:
+            th = "ne2bit"; break;
+        case bv_justification::kind_t::bit2eq:      
+            th = "bit2eq"; break;
+        case bv_justification::kind_t::bit2ne: 
+            th = "bit2ne"; break;
+        case bv_justification::kind_t::bv2int:
+            th = "bv2int"; break;
+        }
+        func_decl* f = m.mk_func_decl(th, sorts.size(), sorts.data(), proof);
+        return m.mk_app(f, args);
+    };
+
+    void solver::asserted(literal l) {        
         atom* a = get_bv2a(l.var());
         TRACE("bv", tout << "asserted: " << l << "\n";);
         if (a) {
             force_push();
             m_prop_queue.push_back(propagation_item(a));            
-            for (auto p : a->m_bit2occ) {
+            for (auto p : a->m_bit2occ) 
                 del_eq_occurs(p.first, p.second);
-            }
         }
     }
 
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 2c8fb4ae9..e4a44e769 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -35,6 +35,9 @@ namespace bv {
         }
     };
 
+
+
+
     class solver : public euf::th_euf_solver {
         typedef rational numeral;
         typedef euf::theory_var theory_var;
@@ -94,8 +97,19 @@ namespace bv {
         sat::justification mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a);
         sat::ext_constraint_idx mk_bv2int_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c);
         void log_drat(bv_justification const& c);
+        class proof_hint : public euf::th_proof_hint {
+            bv_justification::kind_t   m_kind;
+            sat::literal_vector& m_proof_literals;
+            unsigned m_lit_head, m_lit_tail;
+            expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr;
+        public:
+            proof_hint(bv_justification::kind_t k, sat::literal_vector& pl, unsigned lh, unsigned lt, expr* a1 = nullptr, expr* a2 = nullptr, expr* b1 = nullptr, expr* b2 = nullptr) :
+                m_kind(k), m_proof_literals(pl), m_lit_head(lh), m_lit_tail(lt), a1(a1), a2(a2), b1(b1), b2(b2) {}
+            expr* get_hint(euf::solver& s) const override;
+        };
+        sat::literal_vector m_proof_literals;
+        unsigned m_lit_head = 0, m_lit_tail = 0;
  
-
         /**
            \brief Structure used to store the position of a bitvector variable that
            contains the true_literal/false_literal.
diff --git a/src/sat/smt/bv_theory_checker.cpp b/src/sat/smt/bv_theory_checker.cpp
new file mode 100644
index 000000000..9e4418a96
--- /dev/null
+++ b/src/sat/smt/bv_theory_checker.cpp
@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_theory_checker.cpp
+
+Abstract:
+
+    Plugin for bitvector lemmas
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-08-28
+
+Notes:
+
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/bv_theory_checker.h"
+
+
+namespace bv {
+
+
+    /**
+       bv is a generic rule used for internalizing bit-vectors. 
+       It corresponds to the Tseitin of bit-vectors.
+       
+       To bypass theory checking we pretend it is trusted.
+     */
+    bool theory_checker::check_bv(app* jst) { return true; }
+
+    /**
+       Let x, y be bit-vector terms and k be an assignment to constants bit2eq encodes the rule:
+
+       x = k, y = k
+       ------------
+          x = y
+     */
+    bool theory_checker::check_bit2eq(app* jst) { return true; }
+
+    /**
+       x[i] = false, y[i] = true
+       -------------------------
+           x != y
+     */
+    bool theory_checker::check_bit2ne(app* jst) { return true; }
+
+    /**
+          x = y
+       -----------
+       x[i] = y[i]
+     */
+    bool theory_checker::check_eq2bit(app* jst) { return true; }
+
+    /**
+         x != y, x is assigned on all but position i, x[j] = y[j] on other positions.
+         ----------------------------------------------------------------------------
+              x[i] != y[i]         
+     */
+    bool theory_checker::check_ne2bit(app* jst) { return true; }
+
+    /**
+        int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
+
+        n = bv2int(x), n = z
+        --------------------
+           int2bv(z) = x              
+     */
+    bool theory_checker::check_bv2int(app* jst) { return true; }
+
+}
diff --git a/src/sat/smt/bv_theory_checker.h b/src/sat/smt/bv_theory_checker.h
new file mode 100644
index 000000000..4dda5e7c7
--- /dev/null
+++ b/src/sat/smt/bv_theory_checker.h
@@ -0,0 +1,95 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_theory_checker.h
+
+Abstract:
+
+    Plugin for bitvector lemmas
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-08-28
+
+Notes:
+
+
+--*/
+#pragma once
+
+#include "util/obj_pair_set.h"
+#include "ast/ast_trail.h"
+#include "ast/ast_util.h"
+#include "ast/bv_decl_plugin.h"
+#include "sat/smt/euf_proof_checker.h"
+#include <iostream>
+
+
+namespace bv {
+
+    class theory_checker : public euf::theory_checker_plugin {
+        ast_manager& m;
+        bv_util      bv;
+
+        symbol m_eq2bit = symbol("eq2bit");
+        symbol m_ne2bit = symbol("ne2bit");
+        symbol m_bit2eq = symbol("bit2eq");
+        symbol m_bit2ne = symbol("bit2ne");
+        symbol m_bv2int = symbol("bv2int");
+        symbol m_bv     = symbol("bv");
+
+        bool check_bv(app* jst);
+        bool check_bit2eq(app* jst);
+        bool check_bit2ne(app* jst);
+        bool check_eq2bit(app* jst);
+        bool check_ne2bit(app* jst);
+        bool check_bv2int(app* jst);
+
+    public:
+        theory_checker(ast_manager& m): 
+            m(m),
+            bv(m) {}
+
+        bool check(app* jst) override {
+            if (jst->get_name() == m_bv)
+                return check_bv(jst);
+            if (jst->get_name() == m_eq2bit)
+                return check_eq2bit(jst);
+            if (jst->get_name() == m_ne2bit)
+                return check_ne2bit(jst);
+            if (jst->get_name() == m_bit2eq)
+                return check_bit2eq(jst);
+            if (jst->get_name() == m_bit2ne)
+                return check_bit2ne(jst);
+            if (jst->get_name() == m_bv2int)
+                return check_bv2int(jst);            
+            return false;
+        }
+
+        expr_ref_vector clause(app* jst) override {
+            expr_ref_vector result(m);
+            if (jst->get_name() == m_bv) {
+                for (expr* arg : *jst) 
+                    result.push_back(mk_not(m, arg));
+            }
+            else {
+                for (expr* arg : *jst) 
+                    result.push_back(arg);
+            }
+            return result;
+        }
+
+        void register_plugins(euf::theory_checker& pc) override {
+            pc.register_plugin(m_bv, this);
+            pc.register_plugin(m_bit2eq, this);
+            pc.register_plugin(m_bit2ne, this);
+            pc.register_plugin(m_eq2bit, this);
+            pc.register_plugin(m_ne2bit, this);
+            pc.register_plugin(m_bv2int, this);
+        }
+        
+    };
+
+}
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 865f58fde..73d059942 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -330,13 +330,13 @@ namespace euf {
                     eqs.push_back(eq);
                 }
             }
-            expr_ref fml(m.mk_or(eqs), m);
+            expr_ref fml = mk_or(eqs);
             sat::literal dist(si.to_bool_var(e), false);
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
             add_root(~dist, ~some_eq);
             add_root(dist, some_eq);
-            s().add_clause(~dist, ~some_eq, mk_tseitin_status(~dist, ~some_eq));
-            s().add_clause(dist, some_eq, mk_tseitin_status(dist, some_eq));
+            s().add_clause(~dist, ~some_eq, mk_distinct_status(~dist, ~some_eq));
+            s().add_clause(dist, some_eq, mk_distinct_status(dist, some_eq));
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -347,8 +347,8 @@ namespace euf {
                 sat::literal lit2 = expr2literal(e2);
                 add_root(~lit1, lit2);
                 add_root(lit1, ~lit2);
-                s().add_clause(~lit1, lit2, mk_tseitin_status(~lit1, lit2));
-                s().add_clause(lit1, ~lit2, mk_tseitin_status(lit1, ~lit2));
+                s().add_clause(~lit1, lit2, mk_distinct_status(~lit1, lit2));
+                s().add_clause(lit1, ~lit2, mk_distinct_status(lit1, ~lit2));
             }
         }
     }
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 9bb2cfbaa..79f7e6880 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -25,6 +25,7 @@ Author:
 #include "sat/smt/euf_proof_checker.h"
 #include "sat/smt/arith_theory_checker.h"
 #include "sat/smt/q_theory_checker.h"
+#include "sat/smt/bv_theory_checker.h"
 #include "sat/smt/distinct_theory_checker.h"
 #include "sat/smt/tseitin_theory_checker.h"
 
@@ -292,6 +293,7 @@ namespace euf {
         add_plugin(alloc(distinct::theory_checker, m));
         add_plugin(alloc(smt_theory_checker_plugin, m)); 
         add_plugin(alloc(tseitin::theory_checker, m));
+        add_plugin(alloc(bv::theory_checker, m));
     }
 
     theory_checker::~theory_checker() {
@@ -341,8 +343,12 @@ namespace euf {
         for (expr* arg : clause2)
             literals.mark(arg, true);
         for (expr* arg : clause1)
-            if (!literals.is_marked(arg))
+            if (!literals.is_marked(arg)) {
+                if (m.is_not(arg, arg) && m.is_not(arg, arg) && literals.is_marked(arg)) // kludge
+                    continue;
+                IF_VERBOSE(0, verbose_stream() << mk_bounded_pp(arg, m) << " not in " << clause2 << "\n");
                 return false;
+            }
 
         // extract negated units for literals in clause2 but not in clause1
         // the literals should be rup
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 720053d7d..9983a48dd 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -19,6 +19,7 @@ Author:
 #include "util/scoped_ptr_vector.h"
 #include "util/trail.h"
 #include "ast/ast_translation.h"
+#include "ast/ast_util.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "tactic/model_converter.h"
@@ -391,6 +392,7 @@ namespace euf {
         void visit_expr(std::ostream& out, expr* e);
         std::ostream& display_expr(std::ostream& out, expr* e);        
         void on_instantiation(unsigned n, sat::literal const* lits, unsigned k, euf::enode* const* bindings);
+        expr_ref_vector& expr_args() { m_expr_args.reset(); return m_expr_args; }
         smt_proof_hint* mk_smt_hint(symbol const& n, literal_vector const& lits, enode_pair_vector const& eqs) {
             return mk_smt_hint(n, lits.size(), lits.data(), eqs.size(), eqs.data());
         }
@@ -441,7 +443,7 @@ namespace euf {
         euf::enode* mk_enode(expr* e, unsigned n, enode* const* args);
         void set_bool_var2expr(sat::bool_var v, expr* e) { m_bool_var2expr.setx(v, e, nullptr); }
         expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
-        expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return (e && lit.sign()) ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
+        expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return (e && lit.sign()) ? expr_ref(mk_not(m, e), m) : expr_ref(e, m); }
         unsigned generation() const { return m_generation; }
 
         sat::literal attach_lit(sat::literal lit, expr* e);