mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

remove windowsArm64 from nightly

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-17 10:04:49 -08:00
parent d0a59f3740
commit 4867073290
6 changed files with 47 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/sat/smt/arith_axioms.cpp
View file

@ -260,6 +260,9 @@ namespace arith {
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
rational r = mod(valx * rational::power_of_two(k), N);
if (r == valn)
return true;
sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)));
if (s().value(eq) == l_true)
return true;
@ -272,6 +275,9 @@ namespace arith {
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
rational r = mod(div(valx, rational::power_of_two(k)), N);
if (r == valn)
return true;
sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))));
if (s().value(eq) == l_true)
return true;
@ -284,6 +290,12 @@ namespace arith {
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
bool signvalx = x >= N/2;
rational valxdiv2k = div(valx, rational::power_of_two(k));
if (signvalx)
valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N);
if (valn == valxdiv2k)
return true;
sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
sat::literal eq;
expr* xdiv2k;
@ -335,9 +347,10 @@ namespace arith {
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
if (a.is_band(n)) {
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
add_clause(mk_literal(a.mk_le(n, x)));
add_clause(mk_literal(a.mk_le(n, y)));
}

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

@ -282,7 +282,7 @@ namespace euf {
}
void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
out << "Failed to validate b" << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
s().display(out);
euf::enode_vector nodes;
nodes.push_back(n);

53
src/sat/smt/intblast_solver.cpp
View file

@ -148,7 +148,7 @@ namespace intblast {
auto a = expr2literal(e);
auto b = mk_literal(r);
ctx.mark_relevant(b);
// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
add_equiv(a, b);
}
return true;
@ -305,28 +305,6 @@ namespace intblast {
sorted.push_back(arg);
}
}
//
// Add ground equalities to ensure the model is valid with respect to the current case splits.
// This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal
// assignment from complete level.
// E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment.
// If intblast is SAT, then force the model and literal assignment on the rest of the literals.
//
if (!is_ground(e))
continue;
euf::enode* n = ctx.get_enode(e);
if (!n)
continue;
if (n == n->get_root())
continue;
expr* r = n->get_root()->get_expr();
es.push_back(m.mk_eq(e, r));
r = es.back();
if (!visited.is_marked(r) && !is_translated(r)) {
visited.mark(r);
sorted.push_back(r);
}
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
@ -646,7 +624,7 @@ namespace intblast {
}
case OP_BUDIV:
case OP_BUDIV_I: {
expr* x = arg(0), * y = umod(e, 1);
expr* x = umod(e, 0), * y = umod(e, 1);
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y));
break;
}
@ -978,13 +956,38 @@ namespace intblast {
arith::arith_value av(ctx);
rational r;
VERIFY(av.get_value(b2i->get_expr(), r));
verbose_stream() << ctx.bpp(n) << " := " << r << "\n";
value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
}
values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
}
void solver::finalize_model(model& mdl) {
for (auto n : ctx.get_egraph().nodes()) {
expr* e = n->get_expr();
if (!bv.is_bv(e))
continue;
if (!is_translated(e))
continue;
expr* f = translated(e);
rational r1, r2;
expr_ref val1 = mdl(e);
expr_ref val2 = mdl(f);
if (bv.is_numeral(val1, r1) && a.is_numeral(val2, r2) && r1 != r2) {
rational N = rational::power_of_two(bv.get_bv_size(e));
r2 = mod(r2, N);
if (r1 == r2)
continue;
verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n";
verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n";
for (expr* arg : *to_app(e)) {
verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n";
}
}
}
}
sat::literal_vector const& solver::unsat_core() {
return m_core;
}

2
src/sat/smt/intblast_solver.h
View file

@ -108,6 +108,8 @@ namespace intblast {
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
void finalize_model(model& mdl) override;
std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override;