mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

add cut

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-04 11:59:00 -07:00
parent da9382956c
commit ea365de820
2 changed files with 33 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/sat/smt/arith_proof_checker.h
View file

@ -96,6 +96,31 @@ namespace arith {
mul(dst, x);
add(dst, src, y);
}
void cut(row& r) {
if (r.m_coeffs.empty())
return;
auto const& [v, coeff] = *r.m_coeffs.begin();
if (!a.is_int(v))
return;
rational lc = denominator(r.m_coeff);
for (auto const& [v, coeff] : r.m_coeffs)
lc = lcm(lc, denominator(coeff));
if (lc != 1) {
r.m_coeff *= lc;
for (auto & [v, coeff] : r.m_coeffs)
coeff *= lc;
}
rational g(0);
for (auto const& [v, coeff] : r.m_coeffs)
g = gcd(coeff, g);
if (g == 1)
return;
rational m = mod(r.m_coeff, g);
if (m == 0)
return;
r.m_coeff += g - m;
}
/**
* \brief populate m_coeffs, m_coeff based on mul*e
@ -205,6 +230,7 @@ namespace arith {
if (m_ineq.m_coeffs.empty() ||
m_conseq.m_coeffs.empty())
return false;
cut(m_ineq);
auto const& [v, coeff1] = *m_ineq.m_coeffs.begin();
rational coeff2;
if (!m_conseq.m_coeffs.find(v, coeff2))

13
src/shell/drat_frontend.cpp
View file

@ -151,13 +151,13 @@ public:
m_input_solver = mk_smt_solver(m, m_params, symbol());
}
void add(sat::literal_vector const& lits, sat::status const& st) {
void add(sat::literal_vector const& lits, sat::status const& st, bool validated) {
for (sat::literal lit : lits)
while (lit.var() >= m_drat.get_solver().num_vars())
m_drat.get_solver().mk_var(true);
if (st.is_input() && m_check_inputs)
check_assertion_redundant(lits);
else if (!st.is_sat() && !st.is_deleted())
else if (!st.is_sat() && !st.is_deleted() && !validated)
check_clause(lits);
// m_drat.add(lits, st);
}
@ -184,7 +184,7 @@ public:
for (unsigned i = 0; i < sz; ++i) {
auto const& [coeff, lit] = hint.m_literals[i];
app_ref e(to_app(m_b2e[lit.var()]), m);
if (i + 1 == sz && sat::hint_type::bound_h == hint.m_ty) {
if (i + 1 == sz && (sat::hint_type::bound_h == hint.m_ty || sat::hint_type::cut_h == hint.m_ty)) {
if (!achecker.add_conseq(coeff, e, lit.sign())) {
std::cout << "p failed checking hint " << e << "\n";
return false;
@ -432,14 +432,15 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
std::cout << dimacs::drat_pp(r, write_theory);
std::cout.flush();
switch (r.m_tag) {
case dimacs::drat_record::tag_t::is_clause:
checker.add(r.m_lits, r.m_status);
checker.validate_hint(exprs, r.m_lits, r.m_hint);
case dimacs::drat_record::tag_t::is_clause: {
bool validated = checker.validate_hint(exprs, r.m_lits, r.m_hint);
checker.add(r.m_lits, r.m_status, validated);
if (drat_checker.inconsistent()) {
std::cout << "inconsistent\n";
return;
}
break;
}
case dimacs::drat_record::tag_t::is_node: {
expr_ref e(m);
args.reset();