mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

add proof checker plugin

Browse source 
fixes to monomials
This commit is contained in:
Nikolaj Bjorner 2023-12-31 05:30:21 -08:00
parent 32825a26cb
commit 7bd7faa722
8 changed files with 113 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,7 @@ Author:
#include "sat/smt/arith_theory_checker.h"
#include "sat/smt/q_theory_checker.h"
#include "sat/smt/bv_theory_checker.h"
#include "sat/smt/polysat_theory_checker.h"
#include "sat/smt/distinct_theory_checker.h"
#include "sat/smt/tseitin_theory_checker.h"
#include "params/solver_params.hpp"
@ -294,6 +295,7 @@ namespace euf {
add_plugin(alloc(smt_theory_checker_plugin, m));
add_plugin(alloc(tseitin::theory_checker, m));
add_plugin(alloc(bv::theory_checker, m));
add_plugin(alloc(polysat::theory_checker, m));
}
theory_checker::~theory_checker() {

12
src/sat/smt/polysat/core.cpp
View file

@ -491,16 +491,16 @@ namespace polysat {
return s.trail();
}
void core::add_axiom(char const* name, constraint_or_dependency_list const& cs, bool is_redundant) {
s.add_axiom(name, cs.begin(), cs.end(), is_redundant);
bool core::add_axiom(char const* name, constraint_or_dependency_list const& cs, bool is_redundant) {
return s.add_axiom(name, cs.begin(), cs.end(), is_redundant);
}
void core::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
s.add_axiom(name, begin, end, is_redundant);
bool core::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
return s.add_axiom(name, begin, end, is_redundant);
}
void core::add_axiom(char const* name, constraint_or_dependency_vector const& cs, bool is_redundant) {
s.add_axiom(name, cs.begin(), cs.end(), is_redundant);
bool core::add_axiom(char const* name, constraint_or_dependency_vector const& cs, bool is_redundant) {
return s.add_axiom(name, cs.begin(), cs.end(), is_redundant);
}
std::ostream& core::display(std::ostream& out) const {

6
src/sat/smt/polysat/core.h
View file

@ -139,9 +139,9 @@ namespace polysat {
* In other words, the clause represents the formula /\ d_i -> \/ sc_j
* Where d_i are logical interpretations of dependencies and sc_j are signed constraints.
*/
void add_axiom(char const* name, constraint_or_dependency_list const& cs, bool is_redundant);
void add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant);
void add_axiom(char const* name, constraint_or_dependency_vector const& cs, bool is_redundant);
bool add_axiom(char const* name, constraint_or_dependency_list const& cs, bool is_redundant);
bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant);
bool add_axiom(char const* name, constraint_or_dependency_vector const& cs, bool is_redundant);
pvar add_var(unsigned sz);
pdd var(pvar p) { return m_vars[p]; }

45
src/sat/smt/polysat/monomials.cpp
View file

@ -102,14 +102,15 @@ namespace polysat {
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return mulp2(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
return l_false;
return l_undef;
}
@ -132,7 +133,7 @@ namespace polysat {
}
bool monomials::eval_to_false(unsigned i) {
rational rhs, lhs, p_val;
rational rhs, lhs;
auto& mon = m_monomials[i];
if (!c.try_eval(mon.var, mon.val))
return false;
@ -140,11 +141,9 @@ namespace polysat {
return false;
if (rhs == mon.val)
return false;
for (unsigned j = mon.size(); j-- > 0; ) {
if (!c.try_eval(mon.args[j], p_val))
return false;
mon.arg_vals[j] = p_val;
}
for (unsigned j = mon.size(); j-- > 0; )
if (!c.try_eval(mon.args[j], mon.arg_vals[j]))
return false;
return true;
}
@ -227,7 +226,8 @@ namespace polysat {
if (i != big_index)
clause.push_back(~C.eq(mon.args[i]));
clause.push_back(C.ule(mon.args[big_index], mon.var));
return false;
c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
return true;
}
// ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1
@ -254,24 +254,18 @@ namespace polysat {
return true;
}
// p * q = 0 => p = 0 or even(q)
// p * q = 0 => p = 0 or q = 0 or even(q)
// parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0
bool monomials::parity0(monomial const& mon) {
if (mon.val != 0)
if (mon.val.is_odd())
return false;
if (!all_of(mon.arg_vals, [&](auto const& v) { return v.is_odd(); }))
return false;
constraint_or_dependency_vector clause;
clause.push_back(~C.eq(mon.var, 0));
for (auto const& val : mon.arg_vals)
if (!val.is_odd() || val == 0)
return false;
clause.push_back(~C.parity_at_least(mon.var, 1));
for (auto const& p : mon.args)
clause.push_back(C.eq(p));
for (auto const& p : mon.args) {
clause.push_back(C.parity_at_least(p, 1));
c.add_axiom("p * q = 0 => p = 0 or q = 0 or even(q)", clause, true);
clause.pop_back();
}
return false;
clause.push_back(C.parity_at_least(p, 1));
c.add_axiom("parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0", clause, true);
return true;
}
// 0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k
@ -305,14 +299,15 @@ namespace polysat {
continue;
if (!c.try_eval(c.var(yslice.v), y_val) || y_val != mon.arg_vals[1])
continue;
c.add_axiom("0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k",
bool added = c.add_axiom("0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k",
{ dependency({x, xslice}), dependency({y, yslice}),
~C.ule(mon.args[0], xmax_value),
~C.ule(mon.args[1], xmax_value),
~C.ugt(mon.var, xmax_value),
C.umul_ovfl(c.var(xslice.v), c.var(yslice.v)) },
true);
return true;
if (added)
return true;
}
}
return false;

11
src/sat/smt/polysat_internalize.cpp
View file

@ -81,7 +81,7 @@ namespace polysat {
#define if_unary(F) if (a->get_num_args() == 1) { internalize_unary(a, [&](pdd const& p) { return F(p); }); break; }
switch (a->get_decl_kind()) {
case OP_BMUL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
case OP_BMUL: internalize_mul(a); break;
case OP_BADD: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
case OP_BLSHR: internalize_lshr(a); break;
@ -110,7 +110,7 @@ namespace polysat {
case OP_BSMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_udfl(p, q); }); break;
case OP_BUMUL_OVFL:
case OP_BUMUL_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break;
case OP_BSMUL_OVFL:
case OP_BSDIV_OVFL:
case OP_BNEG_OVFL:
@ -604,6 +604,13 @@ namespace polysat {
internalize_set(a, p);
}
void solver::internalize_mul(app* a) {
vector<dd::pdd> args;
for (expr* arg : *to_app(a))
args.push_back(expr2pdd(arg));
internalize_set(a, m_core.mul(args.size(), args.data()));
}
// TODO - test that internalize works with recursive call on bit2bool
void solver::internalize_mkbv(app* a) {
unsigned i = 0;

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

@ -397,12 +397,14 @@ namespace polysat {
result = m.mk_not(result);
return result;
}
case ckind_t::smul_fl_t:
case ckind_t::op_t:
UNREACHABLE();
break;
case ckind_t::smul_fl_t:
NOT_IMPLEMENTED_YET();
break;
}
throw default_exception("constraint2expr nyi");
return result;
}
expr_ref solver::pdd2expr(pdd const& p) {
@ -424,12 +426,12 @@ namespace polysat {
family_id fid = m.get_family_id("bv");
solver& p = dynamic_cast<solver&>(*s.fid2solver(fid));
expr_ref_vector args(m);
args.push_back(m.mk_const(name, m.mk_proof_sort()));
for (unsigned i = m_lit_head; i < m_lit_tail; ++i)
args.push_back(s.literal2expr(p.m_mk_hint.lit(i)));
for (unsigned i = m_eq_head; i < m_eq_tail; ++i)
args.push_back(s.mk_eq(p.m_mk_hint.eq(i).first, p.m_mk_hint.eq(i).second));
expr* pr = m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
return m.mk_app(symbol("bv"), 1, &pr, m.mk_proof_sort());
return m.mk_app(symbol("polysat"), args.size(), args.data(), m.mk_proof_sort());
}
void solver::proof_hint_builder::init(euf::solver& ctx, char const* name) {

7
src/sat/smt/polysat_solver.h
View file

@ -28,9 +28,6 @@ namespace euf {
namespace polysat {
class solver : public euf::th_euf_solver, public solver_interface {
typedef euf::theory_var theory_var;
typedef euf::theory_id theory_id;
@ -137,6 +134,7 @@ namespace polysat {
void init_bits(expr* e, expr_ref_vector const & bits);
void mk_bits(theory_var v);
void add_def(sat::literal def, sat::literal l);
void internalize_unary(app* e, std::function<pdd(pdd)> const& fn);
void internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn);
void internalize_binary(app* e, std::function<expr*(expr*, expr*)> const& fn);
@ -144,7 +142,8 @@ namespace polysat {
void internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn);
void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
void internalize_num(app * n);
void internalize_num(app * n);
void internalize_mul(app* e);
void internalize_concat(app * n);
void internalize_bv2int(app* n);
void internalize_int2bv(app* n);

64
src/sat/smt/polysat_theory_checker.h Normal file
View file

@ -0,0 +1,64 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
polysat_proof_checker.h
Abstract:
Plugin for checking polysat bit-vector lemmas
Author:
Nikolaj Bjorner (nbjorner) 2022-08-28
--*/
#pragma once
#include "ast/ast_util.h"
#include "sat/smt/euf_proof_checker.h"
#include <iostream>
namespace polysat {
class theory_checker : public euf::theory_checker_plugin {
ast_manager& m;
public:
theory_checker(ast_manager& m):
m(m) {}
expr_ref_vector clause(app* jst) override {
expr_ref_vector result(m);
for (expr* arg : *jst)
if (m.is_bool(arg))
result.push_back(mk_not(m, arg));
return result;
}
bool check(app* jst) override {
params_ref params;
params.set_uint("smt.bv.solver",2); // use int-blast solver to check lemmas
scoped_ptr<solver> s = mk_smt_solver(m, params, symbol());
auto cl = clause(jst);
for (auto arg : cl)
s->assert_expr(mk_not(m, arg));
lbool r = s->check_sat();
if (r == l_true) {
model_ref mdl;
s->get_model(mdl);
IF_VERBOSE(0, verbose_stream() << "checking failed for\n" << mk_pp(jst, m) << "\n" << * mdl << "\n");
}
return r == l_false;
}
void register_plugins(euf::theory_checker& pc) override {
pc.register_plugin(symbol("polysat"), this);
}
};
}