mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

wip - add bit-vector validator plugins and logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-18 14:50:21 -07:00
parent 464d52babe
commit cdfab8cb13
8 changed files with 272 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/CMakeLists.txt
View file

@ -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

85
src/sat/smt/bv_solver.cpp
View file

@ -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);
}
}
}

16
src/sat/smt/bv_solver.h
View file

@ -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.

76
src/sat/smt/bv_theory_checker.cpp Normal file
View file

@ -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; }
}

95
src/sat/smt/bv_theory_checker.h Normal file
View file

@ -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);
}
};
}

10
src/sat/smt/euf_internalize.cpp
View file

@ -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));
}
}
}

8
src/sat/smt/euf_proof_checker.cpp
View file

@ -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

4
src/sat/smt/euf_solver.h
View file

@ -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);