mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-13 08:17:21 -08:00
parent c6a8ae1e8c
commit 5fdfd4f3f4
9 changed files with 128 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -208,6 +208,8 @@ namespace arith {
bool solver::check_band_term(app* n) {
unsigned sz;
expr* x, * y;
if (!ctx.is_relevant(expr2enode(n)))
return true;
VERIFY(a.is_band(n, sz, x, y));
if (use_nra_model()) {
found_unsupported(n);
@ -217,6 +219,11 @@ namespace arith {
theory_var vy = expr2enode(y)->get_th_var(get_id());
theory_var vn = expr2enode(n)->get_th_var(get_id());
rational N = rational::power_of_two(sz);
if (!get_value(vx).is_int() || !get_value(vy).is_int()) {
s().display(verbose_stream());
verbose_stream() << vx << " " << vy << " " << mk_pp(n, m) << "\n";
}
SASSERT(get_value(vx).is_int());
SASSERT(get_value(vy).is_int());
SASSERT(get_value(vn).is_int());

13
src/sat/smt/euf_solver.cpp
View file

@ -22,6 +22,7 @@ Author:
#include "sat/smt/pb_solver.h"
#include "sat/smt/bv_solver.h"
#include "sat/smt/polysat_solver.h"
#include "sat/smt/intblast_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/array_solver.h"
#include "sat/smt/arith_solver.h"
@ -135,8 +136,16 @@ namespace euf {
special_relations_util sp(m);
if (pb.get_family_id() == fid)
ext = alloc(pb::solver, *this, fid);
else if (bvu.get_family_id() == fid)
ext = alloc(polysat::solver, *this, fid);
else if (bvu.get_family_id() == fid) {
if (get_config().m_bv_solver == 0)
ext = alloc(bv::solver, *this, fid);
else if (get_config().m_bv_solver == 1)
ext = alloc(polysat::solver, *this, fid);
else if (get_config().m_bv_solver == 2)
ext = alloc(intblast::solver, *this);
else
throw default_exception("unknown bit-vector solver. Accepted values 0 (bit blast), 1 (polysat), 2 (int blast)");
}
else if (au.get_family_id() == fid)
ext = alloc(array::solver, *this, fid);
else if (fpa.get_family_id() == fid)

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

@ -88,22 +88,25 @@ namespace intblast {
expr* e = n->get_expr();
expr* x, * y;
VERIFY(m.is_eq(n->get_expr(), x, y));
SASSERT(bv.is_bv(x));
ensure_translated(x);
ensure_translated(y);
m_args.reset();
m_args.push_back(translated(x));
m_args.push_back(translated(y));
add_equiv(expr2literal(e), eq_internalize(umod(x, 0), umod(x, 1)));
m_args.push_back(a.mk_sub(translated(x), translated(y)));
expr_ref lhs(umod(x, 0), m);
ctx.get_rewriter()(lhs);
add_equiv(expr2literal(e), eq_internalize(lhs, a.mk_int(0)));
}
void solver::internalize_bv(app* e) {
ensure_args(e);
m_args.reset();
for (auto arg : *e)
m_args.push_back(translated(arg));
translate_bv(e);
ensure_translated(e);
// possibly wait until propagation?
if (m.is_bool(e))
add_equiv(expr2literal(e), mk_literal(translated(e)));
if (m.is_bool(e)) {
expr_ref r(translated(e), m);
ctx.get_rewriter()(r);
add_equiv(expr2literal(e), mk_literal(r));
}
add_bound_axioms();
}
@ -120,32 +123,28 @@ namespace intblast {
}
}
void solver::ensure_args(app* e) {
void solver::ensure_translated(expr* e) {
if (m_translate.get(e->get_id(), nullptr))
return;
ptr_vector<expr> todo;
ast_fast_mark1 visited;
for (auto arg : *e) {
if (!m_translate.get(arg->get_id(), nullptr))
todo.push_back(arg);
}
if (todo.empty())
return;
todo.push_back(e);
visited.mark(e);
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (m.is_bool(e))
if (!is_app(e))
continue;
else if (is_app(e)) {
for (auto arg : *to_app(e))
if (!visited.is_marked(arg)) {
visited.mark(arg);
todo.push_back(arg);
}
}
else if (is_lambda(e))
throw default_exception("lambdas are not supported in intblaster");
app* a = to_app(e);
if (m.is_bool(e) && a->get_family_id() != bv.get_family_id())
continue;
for (auto arg : *a)
if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) {
visited.mark(arg);
todo.push_back(arg);
}
}
std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
for (expr* e : todo)
for (expr* e : todo)
translate_expr(e);
}
@ -369,7 +368,7 @@ namespace intblast {
}
if (any_of(m_vars, [&](expr* v) { return translated(v) == x; }))
return x;
return to_expr(a.mk_mod(x, a.mk_int(N)));
return a.mk_mod(x, a.mk_int(N));
}
expr* solver::smod(expr* bv_expr, unsigned i) {
@ -393,6 +392,10 @@ namespace intblast {
translate_var(to_var(e));
else {
app* ap = to_app(e);
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
set_translated(e, e);
return;
}
m_args.reset();
for (auto arg : *ap)
m_args.push_back(translated(arg));
@ -543,7 +546,6 @@ namespace intblast {
r = a.mk_uminus(arg(0));
break;
case OP_CONCAT: {
r = a.mk_int(0);
unsigned sz = 0;
for (unsigned i = 0; i < args.size(); ++i) {
expr* old_arg = e->get_arg(i);
@ -595,7 +597,7 @@ namespace intblast {
expr* x = arg(0), * y = arg(1);
r = a.mk_int(0);
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = m.mk_ite(a.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r);
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r);
break;
}
case OP_BNOT:
@ -605,7 +607,7 @@ namespace intblast {
expr* x = arg(0), * y = arg(1);
r = a.mk_int(0);
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = m.mk_ite(a.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
break;
}
// Or use (p + q) - band(p, q)?
@ -649,7 +651,7 @@ namespace intblast {
r = m.mk_ite(signbit, a.mk_int(N - 1), a.mk_int(0));
for (unsigned i = 0; i < bv.get_bv_size(e); ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = m.mk_ite(a.mk_eq(y, a.mk_int(i)),
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
m.mk_ite(signbit, a.mk_uminus(d), d),
r);
}
@ -686,6 +688,7 @@ namespace intblast {
bv_expr = e->get_arg(0);
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
break;
case OP_BSMOD_I:
case OP_BSMOD: {
bv_expr = e;
expr* x = umod(bv_expr, 0), *y = umod(bv_expr, 0);
@ -693,12 +696,12 @@ namespace intblast {
expr* signx = a.mk_ge(x, a.mk_int(N/2));
expr* signy = a.mk_ge(y, a.mk_int(N/2));
expr* u = a.mk_mod(x, y);
// x < 0, y < 0 -> r = -u
// x < 0, y >= 0 -> r = y - u
// x >= 0, y < 0 -> r = y + u
// x >= 0, y >= 0 -> r = u
// u = 0 -> r = 0
// y = 0 -> r = x
// u = 0 -> 0
// y = 0 -> x
// x < 0, y < 0 -> -u
// x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u
r = a.mk_uminus(u);
r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r);
r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
@ -707,15 +710,41 @@ namespace intblast {
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break;
}
case OP_BSDIV_I:
case OP_BSDIV: {
// d = udiv(x mod N, y mod N)
// y = 0, x > 0 -> 1
// y = 0, x <= 0 -> -1
// y != 0 -> machine_div(x, y)
#if 0
#endif
// x = 0, y != 0 -> 0
// x < 0, y < 0 -> -d
// x < 0, y > 0 -> -d
// x > 0, y > 0 -> d
// x < 0, y < 0 -> d
bv_expr = e;
expr* x = umod(bv_expr, 0), * y = umod(bv_expr, 0);
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* d = a.mk_idiv(x, y);
r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), m.mk_ite(signx, a.mk_int(-1), a.mk_int(1)), r);
break;
}
case OP_BSREM_I:
case OP_BSREM: {
// y = 0 -> x
// else x - sdiv(x, y) * y
bv_expr = e;
expr* x = umod(bv_expr, 0), * y = umod(bv_expr, 0);
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* d = a.mk_idiv(x, y);
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = a.mk_sub(x, a.mk_mul(d, y));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break;
}
case OP_ROTATE_LEFT:
case OP_ROTATE_RIGHT:
case OP_EXT_ROTATE_LEFT:
@ -723,7 +752,7 @@ namespace intblast {
case OP_REPEAT:
case OP_BREDOR:
case OP_BREDAND:
case OP_BSREM:
verbose_stream() << mk_pp(e, m) << "\n";
NOT_IMPLEMENTED_YET();
break;
@ -739,11 +768,16 @@ namespace intblast {
bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
if (has_bv_arg) {
expr* bv_expr = e->get_arg(0);
set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
m_args[0] = a.mk_sub(arg(0), arg(1));
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
}
else
set_translated(e, m.mk_eq(arg(0), arg(1)));
}
else if (m.is_ite(e))
set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
else if (m_is_plugin)
set_translated(e, e);
else
set_translated(e, m.mk_app(e->get_decl(), m_args));
}

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

@ -57,7 +57,7 @@ namespace intblast {
sat::literal_vector m_core;
ptr_vector<app> m_bv2int, m_int2bv;
statistics m_stats;
bool m_is_plugin = true; // when the solver is used as a plugin, then do not translate below quantifiers.
bool m_is_plugin = true; // when the solver is used as a plugin, then do not translate below quantifiers.
bool is_bv(sat::literal lit);
void translate(expr_ref_vector& es);
@ -80,7 +80,7 @@ namespace intblast {
void translate_quantifier(quantifier* q);
void translate_var(var* v);
void ensure_args(app* e);
void ensure_translated(expr* e);
void internalize_bv(app* e);
unsigned m_vars_qhead = 0;

5
src/sat/smt/polysat/constraints.h
View file

@ -31,12 +31,15 @@ namespace polysat {
class constraint {
unsigned_vector m_vars;
unsigned m_num_watch = 0;
public:
virtual ~constraint() {}
unsigned_vector& vars() { return m_vars; }
unsigned_vector const& vars() const { return m_vars; }
unsigned var(unsigned idx) const { return m_vars[idx]; }
bool contains_var(pvar v) const { return m_vars.contains(v); }
unsigned num_watch() const { return m_num_watch; }
void set_num_watch(unsigned n) { SASSERT(n <= 2); m_num_watch = n; }
virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
virtual lbool eval() const = 0;
@ -63,6 +66,8 @@ namespace polysat {
unsigned_vector const& vars() const { return m_constraint->vars(); }
unsigned var(unsigned idx) const { return m_constraint->var(idx); }
bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
unsigned num_watch() const { return m_constraint->num_watch(); }
void set_num_watch(unsigned n) { m_constraint->set_num_watch(n); }
void activate(core& c, dependency const& d) { m_constraint->activate(c, m_sign, d); }
void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); }
bool is_always_true() const { return eval() == l_true; }

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

@ -74,11 +74,13 @@ namespace polysat {
if (vars.size() > 0) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[0]] << ") ";
if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") ";
verbose_stream() << "\n");
SASSERT(vars.size() <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
if (vars.size() > 0)
unsigned n = sc.num_watch();
SASSERT(n <= vars.size());
SASSERT(n <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
SASSERT(n <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
if (n > 0)
c.m_watch[vars[0]].pop_back();
if (vars.size() > 1)
if (n > 1)
c.m_watch[vars[1]].pop_back();
c.m_constraint_index.pop_back();
}
@ -138,9 +140,10 @@ namespace polysat {
for (; i < sz && j < 2; ++i)
if (!is_assigned(vars[i]))
std::swap(vars[i], vars[j++]);
if (vars.size() > 0)
sc.set_num_watch(i);
if (i > 0)
add_watch(idx, vars[0]);
if (vars.size() > 1)
if (i > 1)
add_watch(idx, vars[1]);
IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << " ";
if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
@ -225,19 +228,12 @@ namespace polysat {
s.trail().push(mk_assign_var(v, *this));
return;
// to debug:
unsigned sz = m_watch[v].size();
for (unsigned i = 0; i < sz; ++i) {
auto idx = m_watch[v][i];
auto [sc, dep, value] = m_constraint_index[idx];
sc.propagate(*this, value, dep);
}
// update the watch lists for pvars
// remove constraints from m_watch[v] that have more than 2 free variables.
// for entries where there is only one free variable left add to viable set
unsigned j = 0;
for (auto idx : m_watch[v]) {
unsigned j = 0, sz = m_watch[v].size();
for (unsigned k = 0; k < sz; ++k) {
auto idx = m_watch[v][k];
auto [sc, dep, value] = m_constraint_index[idx];
auto& vars = sc.vars();
if (vars[0] != v)
@ -253,6 +249,11 @@ namespace polysat {
break;
}
}
// this can create fresh literals and update m_watch, but
// will not update m_watch[v] (other than copy constructor for m_watch)
// because v has been assigned a value.
sc.propagate(*this, value, dep);
SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
if (swapped)
@ -267,6 +268,7 @@ namespace polysat {
// detect unitary, add to viable, detect conflict?
m_viable.add_unitary(v1, idx);
}
SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
m_watch[v].shrink(j);
verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n";
}

1
src/smt/params/smt_params_helper.pyg
View file

@ -54,6 +54,7 @@ def_module_params(module_name='smt',
('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
('bv.solver', UINT, 1, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),

2
src/smt/params/theory_bv_params.cpp
View file

@ -28,6 +28,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
m_bv_delay = p.bv_delay();
m_bv_size_reduce = p.bv_size_reduce();
m_bv_solver = p.bv_solver();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
@ -42,4 +43,5 @@ void theory_bv_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_bv_enable_int2bv2int);
DISPLAY_PARAM(m_bv_delay);
DISPLAY_PARAM(m_bv_size_reduce);
DISPLAY_PARAM(m_bv_solver);
}

1
src/smt/params/theory_bv_params.h
View file

@ -36,6 +36,7 @@ struct theory_bv_params {
bool m_bv_watch_diseq = false;
bool m_bv_delay = true;
bool m_bv_size_reduce = false;
unsigned m_bv_solver = 0;
theory_bv_params(params_ref const & p = params_ref()) {
updt_params(p);
}