mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

convert def into expression tree

Browse source 
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
This commit is contained in:
Nikolaj Bjorner 2025-02-17 18:47:00 -08:00
parent f977b48161
commit f8f26788ad
3 changed files with 1849 additions and 1787 deletions
Download patch file Download diff file Expand all files Collapse all files

3464
src/math/simplex/model_based_opt.cpp
View file

File diff suppressed because it is too large Load diff

114
src/math/simplex/model_based_opt.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/util.h"
#include "util/rational.h"
#include "util/inf_eps_rational.h"
#include <variant>
namespace opt {
@ -58,6 +59,7 @@ namespace opt {
bool operator!=(var const& other) const {
return !(*this == other);
}
var operator*(rational const& c) const { return var(m_id, m_coeff * c); }
};
struct row {
vector<var> m_vars; // variables with coefficients
@ -74,20 +76,94 @@ namespace opt {
rational get_coefficient(unsigned x) const;
};
// A definition is a linear term of the form (vars + coeff) / div
// A definition is a linear term of the form (vars + coeff) / div
struct add_def;
struct mul_def;
struct div_def;
struct const_def;
struct var_def;
struct const_def;
enum def_t { add_t, mul_t, div_t, const_t, var_t};
struct def {
def() = default;
def(row const& r, unsigned x);
vector<var> m_vars;
rational m_coeff;
rational m_div{1};
def operator+(def const& other) const;
def operator/(unsigned n) const { return *this / rational(n); }
def operator/(rational const& n) const;
def operator*(rational const& n) const;
def operator+(rational const& n) const;
void substitute(unsigned v, def const& other);
void normalize();
static def* from_row(row const& r, unsigned x);
def_t m_type;
unsigned m_ref_count = 0;
bool is_add() const { return m_type == add_t; }
bool is_mul() const { return m_type == mul_t; }
bool is_div() const { return m_type == div_t; }
bool is_const() const { return m_type == const_t; }
bool is_var() const { return m_type == var_t; }
void inc_ref() { ++m_ref_count; }
void dec_ref();
add_def& to_add();
mul_def& to_mul();
div_def& to_div();
const_def& to_const();
var_def& to_var();
add_def const& to_add() const;
mul_def const& to_mul() const;
div_def const& to_div() const;
const_def const& to_const() const;
var_def const& to_var() const;
def* operator+(def& other);
def* operator*(def& other);
def* operator/(unsigned n) { return *this / rational(n); }
def* operator/(rational const& n);
def* operator*(rational const& n);
def* operator+(rational const& n);
def* substitute(unsigned v, def& other);
};
class def_ref {
def* m_def = nullptr;
public:
def_ref(def* d) {
if (d) d->inc_ref();
m_def = d;
}
def_ref& operator=(def* d) {
if (d) d->inc_ref();
if (m_def) m_def->dec_ref();
m_def = d;
return *this;
}
def_ref& operator=(def_ref const& d) {
if (&d == this)
return *this;
if (d.m_def) d.m_def->inc_ref();
if (m_def) m_def->dec_ref();
m_def = d.m_def;
return *this;
}
def& operator*() { return *m_def; }
def* operator->() { return m_def; }
def const& operator*() const { return *m_def; }
operator bool() const { return !!m_def; }
~def_ref() { if (m_def) m_def->dec_ref(); };
};
struct add_def : public def {
def* x, *y;
add_def(def* x, def* y) : x(x), y(y) { m_type = add_t; x->inc_ref(); y->inc_ref(); }
};
struct mul_def : public def {
def* x, *y;
mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t; x->inc_ref(); y->inc_ref(); }
};
struct div_def : public def {
def* x;
rational m_div{ 1 };
div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); }
};
struct var_def : public def {
var v;
var_def(var const& v) : v(v) { m_type = var_t; }
};
struct const_def : public def {
rational c;
const_def(rational const& c) : c(c) { m_type = const_t; }
};
private:
@ -101,9 +177,9 @@ namespace opt {
unsigned_vector m_lub, m_glb, m_divides, m_mod, m_div;
unsigned_vector m_above, m_below;
unsigned_vector m_retired_rows;
vector<model_based_opt::def> m_result;
vector<model_based_opt::def_ref> m_result;
void eliminate(unsigned v, def const& d);
void eliminate(unsigned v, def& d);
bool invariant();
bool invariant(unsigned index, row const& r);
@ -164,13 +240,13 @@ namespace opt {
void update_value(unsigned x, rational const& val);
def project(unsigned var, bool compute_def);
def_ref project(unsigned var, bool compute_def);
def solve_for(unsigned row_id, unsigned x, bool compute_def);
def_ref solve_for(unsigned row_id, unsigned x, bool compute_def);
def solve_divides(unsigned x, unsigned_vector const& divide_rows, bool compute_def);
def_ref solve_divides(unsigned x, unsigned_vector const& divide_rows, bool compute_def);
def solve_mod_div(unsigned x, unsigned_vector const& mod_rows, unsigned_vector const& divide_rows, bool compute_def);
def_ref solve_mod_div(unsigned x, unsigned_vector const& mod_rows, unsigned_vector const& divide_rows, bool compute_def);
bool is_int(unsigned x) const { return m_var2is_int[x]; }
@ -219,7 +295,7 @@ namespace opt {
//
// Project set of variables from inequalities.
//
vector<def> project(unsigned num_vars, unsigned const* vars, bool compute_def);
vector<def_ref> project(unsigned num_vars, unsigned const* vars, bool compute_def);
//
// Extract current rows (after projection).

58
src/qe/mbp/mbp_arith.cpp
View file

@ -258,7 +258,7 @@ namespace mbp {
rational c0 = add_def(t1, mul1, coeffs);
tids.insert(t, mbo.add_div(coeffs, c0, mul1));
}
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
rational r;
val = eval(t);
if (!a.is_numeral(val, r)) {
@ -417,7 +417,7 @@ namespace mbp {
TRACE("qe", tout << "remaining vars: " << vars << "\n";
for (unsigned v : real_vars) tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
mbo.display(tout););
vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
vector<opt::model_based_opt::def_ref> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
vector<row> rows;
@ -431,7 +431,7 @@ namespace mbp {
}
rows2fmls(def_vars, rows, index2expr, fmls);
TRACE("qe", mbo.display(tout << "mbo result\n");
for (auto const& d : defs) tout << "def: " << d << "\n";
for (auto const& d : defs) if (d) tout << "def: " << *d << "\n";
tout << fmls << "\n";);
if (compute_def)
@ -448,29 +448,45 @@ namespace mbp {
return true;
}
void optdefs2mbpdef(u_map<row> const& def_vars, vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
expr_ref from_def(u_map<row> const& def_vars, opt::model_based_opt::def const& d, bool is_int, ptr_vector<expr> const& index2expr) {
if (d.is_add()) {
return expr_ref(
a.mk_add(from_def(def_vars, *d.to_add().x, is_int, index2expr),
from_def(def_vars, *d.to_add().y, is_int, index2expr)), m);
}
if (d.is_mul()) {
return expr_ref(
a.mk_mul(from_def(def_vars, *d.to_mul().x, is_int, index2expr),
from_def(def_vars, *d.to_mul().y, is_int, index2expr)), m);
}
if (d.is_const())
return expr_ref(a.mk_numeral(d.to_const().c, is_int), m);
if (d.is_var()) {
auto t = id2expr(def_vars, index2expr, d.to_var().v.m_id);
if (d.to_var().v.m_coeff != 1)
t = a.mk_mul(a.mk_numeral(d.to_var().v.m_coeff, is_int), t);
return expr_ref(t, m);
}
if (d.is_div()) {
auto t = from_def(def_vars, *d.to_div().x, is_int, index2expr);
if (is_int)
t = a.mk_idiv(t, a.mk_numeral(d.to_div().m_div, is_int));
else
t = a.mk_div(t, a.mk_numeral(d.to_div().m_div, is_int));
return expr_ref(t, m);
}
UNREACHABLE();
return expr_ref(nullptr, m);
}
void optdefs2mbpdef(u_map<row> const& def_vars, vector<opt::model_based_opt::def_ref> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
SASSERT(defs.size() == real_vars.size());
for (unsigned i = 0; i < defs.size(); ++i) {
auto const& d = defs[i];
expr* x = index2expr[real_vars[i]];
bool is_int = a.is_int(x);
expr_ref_vector ts(m);
expr_ref t(m);
for (var const& v : d.m_vars) {
t = id2expr(def_vars, index2expr, v.m_id);
if (v.m_coeff != 1)
t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
ts.push_back(t);
}
if (!d.m_coeff.is_zero())
ts.push_back(a.mk_numeral(d.m_coeff, is_int));
if (ts.empty())
ts.push_back(a.mk_numeral(rational(0), is_int));
t = mk_add(ts);
if (!d.m_div.is_one() && is_int)
t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));
else if (!d.m_div.is_one() && !is_int)
t = a.mk_div(t, a.mk_numeral(d.m_div, is_int));
auto t = from_def(def_vars, *d, is_int, index2expr);
result.push_back({ expr_ref(x, m), t });
}
}