mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix #3194, remove euclidean solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-08 16:05:13 +01:00
parent 9b3c844c2a
commit 611c14844d
12 changed files with 5 additions and 1319 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -34,7 +34,6 @@ def init_project_def():
add_lib('tactic', ['ast', 'model'])
add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
add_lib('parser_util', ['ast'], 'parsers/util')
add_lib('euclid', ['util'], 'math/euclid')
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
add_lib('solver', ['model', 'tactic', 'proofs'])
add_lib('cmd_context', ['solver', 'rewriter'])
@ -52,7 +51,7 @@ def init_project_def():
add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params')
add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
'substitution', 'grobner', 'euclid', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('smt_tactic', ['smt'], 'smt/tactic')

1
src/CMakeLists.txt
View file

@ -54,7 +54,6 @@ add_subdirectory(math/grobner)
add_subdirectory(sat)
add_subdirectory(nlsat)
add_subdirectory(math/lp)
add_subdirectory(math/euclid)
add_subdirectory(tactic/core)
add_subdirectory(math/subpaving/tactic)
add_subdirectory(tactic/aig)

6
src/math/euclid/CMakeLists.txt
View file

@ -1,6 +0,0 @@
z3_add_component(euclid
SOURCES
euclidean_solver.cpp
COMPONENT_DEPENDENCIES
util
)

2
src/math/euclid/README
View file

@ -1,2 +0,0 @@
Basic Euclidean solver for linear integer equations.
This solver generates "explanations".

862
src/math/euclid/euclidean_solver.cpp
View file

@ -1,862 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
euclidean_solver.cpp
Abstract:
Euclidean Solver with support for explanations.
Author:
Leonardo de Moura (leonardo) 2011-07-08.
Revision History:
--*/
#include "math/euclid/euclidean_solver.h"
#include "util/numeral_buffer.h"
#include "util/heap.h"
struct euclidean_solver::imp {
typedef unsigned var;
typedef unsigned justification;
typedef unsynch_mpq_manager numeral_manager;
typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;
typedef numeral_buffer<mpq, numeral_manager> mpq_buffer;
typedef svector<justification> justification_vector;
static const justification null_justification = UINT_MAX;
#define null_var UINT_MAX
#define null_eq_idx UINT_MAX
typedef svector<var> var_vector;
typedef svector<mpz> mpz_vector;
typedef svector<mpq> mpq_vector;
struct elim_order_lt {
unsigned_vector & m_solved;
elim_order_lt(unsigned_vector & s):m_solved(s) {}
bool operator()(var x1, var x2) const { return m_solved[x1] < m_solved[x2]; }
};
typedef heap<elim_order_lt> var_queue; // queue used for scheduling variables for applying substitution.
static unsigned pos(unsigned_vector const & xs, unsigned x_i) {
if (xs.empty())
return UINT_MAX;
int low = 0;
int high = xs.size() - 1;
while (true) {
int mid = low + ((high - low) / 2);
var x_mid = xs[mid];
if (x_i > x_mid) {
low = mid + 1;
if (low > high)
return UINT_MAX;
}
else if (x_i < x_mid) {
high = mid - 1;
if (low > high)
return UINT_MAX;
}
else {
return mid;
}
}
}
/**
Equation as[0]*xs[0] + ... + as[n-1]*xs[n-1] + c = 0 with justification bs[0]*js[0] + ... + bs[m-1]*js[m-1]
*/
struct equation {
mpz_vector m_as;
var_vector m_xs;
mpz m_c;
// justification
mpq_vector m_bs;
justification_vector m_js;
unsigned size() const { return m_xs.size(); }
unsigned js_size() const { return m_js.size(); }
var x(unsigned i) const { return m_xs[i]; }
var & x(unsigned i) { return m_xs[i]; }
mpz const & a(unsigned i) const { return m_as[i]; }
mpz & a(unsigned i) { return m_as[i]; }
mpz const & c() const { return m_c; }
mpz & c() { return m_c; }
var j(unsigned i) const { return m_js[i]; }
var & j(unsigned i) { return m_js[i]; }
mpq const & b(unsigned i) const { return m_bs[i]; }
mpq & b(unsigned i) { return m_bs[i]; }
unsigned pos_x(unsigned x_i) const { return pos(m_xs, x_i); }
};
typedef ptr_vector<equation> equations;
typedef svector<unsigned> occs;
numeral_manager * m_manager;
bool m_owns_m;
equations m_equations;
equations m_solution;
svector<bool> m_parameter;
unsigned_vector m_solved; // null_eq_idx if var is not solved, otherwise the position in m_solution
vector<occs> m_occs; // occurrences of the variable in m_equations.
unsigned m_inconsistent; // null_eq_idx if not inconsistent, otherwise it is the index of an unsatisfiable equality in m_equations.
unsigned m_next_justification;
mpz_buffer m_decompose_buffer;
mpz_buffer m_as_buffer;
mpq_buffer m_bs_buffer;
var_vector m_tmp_xs;
mpz_buffer m_tmp_as;
mpq_buffer m_tmp_bs;
var_vector m_norm_xs_vector;
mpz_vector m_norm_as_vector;
mpq_vector m_norm_bs_vector;
var_queue m_var_queue;
// next candidate
unsigned m_next_eq;
var m_next_x;
mpz m_next_a;
bool m_next_pos_a;
numeral_manager & m() const { return *m_manager; }
bool solved(var x) const { return m_solved[x] != null_eq_idx; }
template<typename Numeral>
void sort_core(svector<Numeral> & as, unsigned_vector & xs, numeral_buffer<Numeral, numeral_manager> & buffer) {
std::sort(xs.begin(), xs.end());
unsigned num = as.size();
for (unsigned i = 0; i < num; i++) {
m().swap(as[i], buffer[xs[i]]);
}
unsigned j = 0;
for (unsigned i = 0; i < num; ++i) {
if (i > 0 && xs[j] == xs[i]) {
m().add(as[j], as[i], as[j]);
continue;
}
if (i != j) {
xs[j] = xs[i];
m().set(as[j], as[i]);
}
++j;
}
xs.shrink(j);
as.shrink(j);
}
template<typename Numeral>
void sort(svector<Numeral> & as, unsigned_vector & xs, numeral_buffer<Numeral, numeral_manager> & buffer) {
unsigned num = as.size();
for (unsigned i = 0; i < num; i++) {
m().set(buffer[xs[i]], as[i]);
}
sort_core(as, xs, buffer);
}
equation * mk_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, unsigned num_js, mpq const * bs, justification const * js,
bool sort = true) {
equation * new_eq = alloc(equation);
for (unsigned i = 0; i < num; i++) {
m().set(m_as_buffer[xs[i]], as[i]);
new_eq->m_as.push_back(mpz());
new_eq->m_xs.push_back(xs[i]);
}
sort_core(new_eq->m_as, new_eq->m_xs, m_as_buffer);
m().set(new_eq->m_c, c);
for (unsigned i = 0; i < num_js; i++) {
m().set(m_bs_buffer[js[i]], bs[i]);
new_eq->m_bs.push_back(mpq());
new_eq->m_js.push_back(js[i]);
}
if (sort)
sort_core(new_eq->m_bs, new_eq->m_js, m_bs_buffer);
return new_eq;
}
template<typename Numeral>
void div(svector<Numeral> & as, mpz const & g) {
unsigned n = as.size();
for (unsigned i = 0; i < n; i++)
m().div(as[i], g, as[i]);
}
void normalize_eq(unsigned eq_idx) {
if (inconsistent())
return;
equation & eq = *(m_equations[eq_idx]);
TRACE("euclidean_solver", tout << "normalizing:\n"; display(tout, eq); tout << "\n";);
unsigned num = eq.size();
if (num == 0) {
// c == 0 inconsistency
if (!m().is_zero(eq.c())) {
TRACE("euclidean_solver", tout << "c = 0 inconsistency detected\n";);
m_inconsistent = eq_idx;
}
else {
del_eq(&eq);
m_equations[eq_idx] = 0;
}
return;
}
mpz g;
mpz a;
m().set(g, eq.a(0));
m().abs(g);
for (unsigned i = 1; i < num; i++) {
if (m().is_one(g))
break;
m().set(a, eq.a(i));
m().abs(a);
m().gcd(g, a, g);
}
if (m().is_one(g))
return;
if (!m().divides(g, eq.c())) {
// g does not divide c
TRACE("euclidean_solver", tout << "gcd inconsistency detected\n";);
m_inconsistent = eq_idx;
return;
}
div(eq.m_as, g);
div(eq.m_bs, g);
m().del(g);
m().del(a);
TRACE("euclidean_solver", tout << "after normalization:\n"; display(tout, eq); tout << "\n";);
}
bool is_better(mpz const & a, var x, unsigned eq_sz) {
SASSERT(m().is_pos(a));
if (m_next_x == null_var)
return true;
if (m().lt(a, m_next_a))
return true;
if (m().lt(m_next_a, a))
return false;
if (m_occs[x].size() < m_occs[m_next_x].size())
return true;
if (m_occs[x].size() > m_occs[m_next_x].size())
return false;
return eq_sz < m_equations[m_next_eq]->size();
}
void updt_next_candidate(unsigned eq_idx) {
if (!m_equations[eq_idx])
return;
mpz abs_a;
equation const & eq = *(m_equations[eq_idx]);
unsigned num = eq.size();
for (unsigned i = 0; i < num; i++) {
mpz const & a = eq.a(i);
m().set(abs_a, a);
m().abs(abs_a);
if (is_better(abs_a, eq.x(i), num)) {
m().set(m_next_a, abs_a);
m_next_x = eq.x(i);
m_next_eq = eq_idx;
m_next_pos_a = m().is_pos(a);
}
}
m().del(abs_a);
}
/**
\brief Select next variable to be eliminated.
Return false if there is not variable to eliminate.
The result is in
m_next_x variable to be eliminated
m_next_eq id of the equation containing x
m_next_a absolute value of the coefficient of x in eq.
m_next_pos_a true if the coefficient of x is positive in eq.
*/
bool select_next_var() {
while (!m_equations.empty() && m_equations.back() == 0)
m_equations.pop_back();
if (m_equations.empty())
return false;
SASSERT(!m_equations.empty() && m_equations.back() != 0);
m_next_x = null_var;
unsigned eq_idx = m_equations.size();
while (eq_idx > 0) {
--eq_idx;
updt_next_candidate(eq_idx);
// stop as soon as possible
// TODO: use heuristics
if (m_next_x != null_var && m().is_one(m_next_a))
return true;
}
CTRACE("euclidean_solver_bug", m_next_x == null_var, display(tout););
SASSERT(m_next_x != null_var);
return true;
}
template<typename Numeral>
void del_nums(svector<Numeral> & as) {
unsigned sz = as.size();
for (unsigned i = 0; i < sz; i++)
m().del(as[i]);
as.reset();
}
void del_eq(equation * eq) {
m().del(eq->c());
del_nums(eq->m_as);
del_nums(eq->m_bs);
dealloc(eq);
}
void del_equations(equations & eqs) {
unsigned sz = eqs.size();
for (unsigned i = 0; i < sz; i++) {
if (eqs[i])
del_eq(eqs[i]);
}
}
/**
\brief Store the "solved" variables in xs into m_var_queue.
*/
void schedule_var_subst(unsigned num, var const * xs) {
for (unsigned i = 0; i < num; i++) {
if (solved(xs[i]))
m_var_queue.insert(xs[i]);
}
}
void schedule_var_subst(var_vector const & xs) {
schedule_var_subst(xs.size(), xs.c_ptr());
}
/**
\brief Store as1*xs1 + k*as2*xs2 into new_as*new_xs
If UpdateOcc == true,
Then,
1) for each variable x occurring in xs2 but not in xs1:
- eq_idx is added to m_occs[x]
2) for each variable that occurs in xs1 and xs2 and the resultant coefficient is zero,
- eq_idx is removed from m_occs[x] IF x != except_var
If UpdateQueue == true
Then,
1) for each variable x occurring in xs2 but not in xs1:
- if x is solved, then x is inserted into m_var_queue
2) for each variable that occurs in xs1 and xs2 and the resultant coefficient is zero,
- if x is solved, then x is removed from m_var_queue
*/
template<typename Numeral, bool UpdateOcc, bool UpdateQueue>
void addmul(svector<Numeral> const & as1, var_vector const & xs1,
mpz const & k, svector<Numeral> const & as2, var_vector const & xs2,
numeral_buffer<Numeral, numeral_manager> & new_as, var_vector & new_xs,
unsigned eq_idx = null_eq_idx, var except_var = null_var) {
Numeral new_a;
SASSERT(as1.size() == xs1.size());
SASSERT(as2.size() == xs2.size());
new_as.reset();
new_xs.reset();
unsigned sz1 = xs1.size();
unsigned sz2 = xs2.size();
unsigned i1 = 0;
unsigned i2 = 0;
while (true) {
if (i1 == sz1) {
// copy remaining entries from as2*xs2
while (i2 < sz2) {
var x2 = xs2[i2];
if (UpdateOcc)
m_occs[x2].push_back(eq_idx);
if (UpdateQueue && solved(x2))
m_var_queue.insert(x2);
new_as.push_back(Numeral());
m().mul(k, as2[i2], new_as.back());
new_xs.push_back(x2);
i2++;
}
break;
}
if (i2 == sz2) {
// copy remaining entries from as1*xs1
while (i1 < sz1) {
new_as.push_back(as1[i1]);
new_xs.push_back(xs1[i1]);
i1++;
}
break;
}
var x1 = xs1[i1];
var x2 = xs2[i2];
if (x1 < x2) {
new_as.push_back(as1[i1]);
new_xs.push_back(xs1[i1]);
i1++;
}
else if (x1 > x2) {
if (UpdateOcc)
m_occs[x2].push_back(eq_idx);
if (UpdateQueue && solved(x2))
m_var_queue.insert(x2);
new_as.push_back(Numeral());
m().mul(k, as2[i2], new_as.back());
new_xs.push_back(x2);
i2++;
}
else {
m().addmul(as1[i1], k, as2[i2], new_a);
TRACE("euclidean_solver_add_mul", tout << "i1: " << i1 << ", i2: " << i2 << " new_a: " << m().to_string(new_a) << "\n";
tout << "as1: " << m().to_string(as1[i1]) << ", k: " << m().to_string(k) << ", as2: " << m().to_string(as2[i2]) << "\n";);
if (m().is_zero(new_a)) {
// variable was canceled
if (UpdateOcc && x1 != except_var)
m_occs[x1].erase(eq_idx);
if (UpdateQueue && solved(x1) && m_var_queue.contains(x1))
m_var_queue.erase(x1);
}
else {
new_as.push_back(new_a);
new_xs.push_back(x1);
}
i1++;
i2++;
}
}
m().del(new_a);
}
template<bool UpdateOcc, bool UpdateQueue>
void apply_solution(var x, mpz_vector & as, var_vector & xs, mpz & c, mpq_vector & bs, justification_vector & js,
unsigned eq_idx = null_eq_idx, var except_var = null_var) {
SASSERT(solved(x));
unsigned idx = pos(xs, x);
if (idx == UINT_MAX)
return;
mpz const & a1 = as[idx];
SASSERT(!m().is_zero(a1));
equation const & eq2 = *(m_solution[m_solved[x]]);
TRACE("euclidean_solver_apply",
tout << "applying: " << m().to_string(a1) << " * "; display(tout, eq2); tout << "\n";
tout << "index: " << idx << "\n";
for (unsigned i = 0; i < xs.size(); i++) tout << m().to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";);
SASSERT(eq2.pos_x(x) != UINT_MAX);
SASSERT(m().is_minus_one(eq2.a(eq2.pos_x(x))));
addmul<mpz, UpdateOcc, UpdateQueue>(as, xs, a1, eq2.m_as, eq2.m_xs, m_tmp_as, m_tmp_xs, eq_idx, except_var);
m().addmul(c, a1, eq2.m_c, c);
m_tmp_as.swap(as);
m_tmp_xs.swap(xs);
SASSERT(as.size() == xs.size());
TRACE("euclidean_solver_apply", for (unsigned i = 0; i < xs.size(); i++) tout << m().to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";);
addmul<mpq, false, false>(bs, js, a1, eq2.m_bs, eq2.m_js, m_tmp_bs, m_tmp_xs);
m_tmp_bs.swap(bs);
m_tmp_xs.swap(js);
SASSERT(pos(xs, x) == UINT_MAX);
}
void apply_solution(mpz_vector & as, var_vector & xs, mpz & c, mpq_vector & bs, justification_vector & js) {
m_var_queue.reset();
schedule_var_subst(xs);
while (!m_var_queue.empty()) {
var x = m_var_queue.erase_min();
apply_solution<false, true>(x, as, xs, c, bs, js);
}
}
void apply_solution(equation & eq) {
apply_solution(eq.m_as, eq.m_xs, eq.m_c, eq.m_bs, eq.m_js);
}
void display(std::ostream & out, equation const & eq) const {
unsigned num = eq.js_size();
for (unsigned i = 0; i < num; i ++) {
if (i > 0) out << " ";
out << m().to_string(eq.b(i)) << "*j" << eq.j(i);
}
if (num > 0) out << " ";
out << "|= ";
num = eq.size();
for (unsigned i = 0; i < num; i++) {
out << m().to_string(eq.a(i)) << "*x" << eq.x(i) << " + ";
}
out << m().to_string(eq.c()) << " = 0";
}
void display(std::ostream & out, equations const & eqs) const {
unsigned num = eqs.size();
for (unsigned i = 0; i < num; i++) {
if (eqs[i]) {
display(out, *(eqs[i]));
out << "\n";
}
}
}
void display(std::ostream & out) const {
if (inconsistent()) {
out << "inconsistent: ";
display(out, *(m_equations[m_inconsistent]));
out << "\n";
}
out << "solution set:\n";
display(out, m_solution);
out << "todo:\n";
display(out, m_equations);
}
void add_occs(unsigned eq_idx) {
equation const & eq = *(m_equations[eq_idx]);
unsigned sz = eq.size();
for (unsigned i = 0; i < sz; i++)
m_occs[eq.x(i)].push_back(eq_idx);
}
imp(numeral_manager * m):
m_manager(m == nullptr ? alloc(numeral_manager) : m),
m_owns_m(m == nullptr),
m_decompose_buffer(*m_manager),
m_as_buffer(*m_manager),
m_bs_buffer(*m_manager),
m_tmp_as(*m_manager),
m_tmp_bs(*m_manager),
m_var_queue(16, elim_order_lt(m_solved)) {
m_inconsistent = null_eq_idx;
m_next_justification = 0;
m_next_x = null_var;
m_next_eq = null_eq_idx;
}
~imp() {
m().del(m_next_a);
del_equations(m_equations);
del_equations(m_solution);
if (m_owns_m)
dealloc(m_manager);
}
var mk_var(bool parameter) {
var x = m_solved.size();
m_parameter.push_back(parameter);
m_solved.push_back(null_eq_idx);
m_occs.push_back(occs());
m_as_buffer.push_back(mpz());
m_var_queue.reserve(x+1);
return x;
}
justification mk_justification() {
justification r = m_next_justification;
m_bs_buffer.push_back(mpq());
m_next_justification++;
return r;
}
void assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j) {
if (inconsistent())
return;
equation * eq;
if (j == null_justification) {
eq = mk_eq(num, as, xs, c, 0, nullptr, nullptr);
}
else {
mpq one(1);
eq = mk_eq(num, as, xs, c, 1, &one, &j);
}
TRACE("euclidean_solver", tout << "new-eq:\n"; display(tout, *eq); tout << "\n";);
unsigned eq_idx = m_equations.size();
m_equations.push_back(eq);
apply_solution(*eq);
normalize_eq(eq_idx);
add_occs(eq_idx);
TRACE("euclidean_solver", tout << "asserted:\n"; display(tout, *eq); tout << "\n";);
}
justification_vector const & get_justification() const {
SASSERT(inconsistent());
return m_equations[m_inconsistent]->m_js;
}
template<typename Numeral>
void neg_coeffs(svector<Numeral> & as) {
unsigned sz = as.size();
for (unsigned i = 0; i < sz; i++) {
m().neg(as[i]);
}
}
void substitute_most_recent_solution(var x) {
SASSERT(!m_solution.empty());
TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n";
display(tout, *(m_solution.back())); tout << "\n";);
occs & use_list = m_occs[x];
occs::iterator it = use_list.begin();
occs::iterator end = use_list.end();
for (; it != end; ++it) {
unsigned eq_idx = *it;
// remark we don't want to update the use_list of x while we are traversing it.
equation & eq2 = *(m_equations[eq_idx]);
TRACE("euclidean_solver", tout << "eq before substituting x" << x << "\n"; display(tout, eq2); tout << "\n";);
apply_solution<true, false>(x, eq2.m_as, eq2.m_xs, eq2.m_c, eq2.m_bs, eq2.m_js, eq_idx, x);
TRACE("euclidean_solver", tout << "eq after substituting x" << x << "\n"; display(tout, eq2); tout << "\n";);
normalize_eq(eq_idx);
if (inconsistent())
break;
}
use_list.reset();
}
void elim_unit() {
SASSERT(m().is_one(m_next_a));
equation & eq = *(m_equations[m_next_eq]);
TRACE("euclidean_solver", tout << "eliminating equation with unit coefficient:\n"; display(tout, eq); tout << "\n";);
if (m_next_pos_a) {
// neg coeffs... to make sure that m_next_x is -1
neg_coeffs(eq.m_as);
neg_coeffs(eq.m_bs);
m().neg(eq.m_c);
}
unsigned sz = eq.size();
for (unsigned i = 0; i < sz; i++) {
m_occs[eq.x(i)].erase(m_next_eq);
}
m_solved[m_next_x] = m_solution.size();
m_solution.push_back(&eq);
m_equations[m_next_eq] = 0;
substitute_most_recent_solution(m_next_x);
}
void decompose(bool pos_a, mpz const & abs_a, mpz const & a_i, mpz & new_a_i, mpz & r_i) {
mpz abs_a_i;
bool pos_a_i = m().is_pos(a_i);
m().set(abs_a_i, a_i);
if (!pos_a_i)
m().neg(abs_a_i);
bool new_pos_a_i = pos_a_i;
if (pos_a)
new_pos_a_i = !new_pos_a_i;
m().div(abs_a_i, abs_a, new_a_i);
if (m().divides(abs_a, a_i)) {
m().reset(r_i);
}
else {
if (pos_a_i)
m().submul(a_i, abs_a, new_a_i, r_i);
else
m().addmul(a_i, abs_a, new_a_i, r_i);
}
if (!new_pos_a_i)
m().neg(new_a_i);
m().del(abs_a_i);
}
void decompose_and_elim() {
m_tmp_xs.reset();
mpz_buffer & buffer = m_decompose_buffer;
buffer.reset();
var p = mk_var(true);
mpz new_a_i;
equation & eq = *(m_equations[m_next_eq]);
TRACE("euclidean_solver", tout << "decomposing equation for x" << m_next_x << "\n"; display(tout, eq); tout << "\n";);
unsigned sz = eq.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
var x_i = eq.x(i);
if (x_i == m_next_x) {
m().set(new_a_i, -1);
buffer.push_back(new_a_i);
m_tmp_xs.push_back(m_next_x);
m_occs[x_i].erase(m_next_eq);
}
else {
decompose(m_next_pos_a, m_next_a, eq.a(i), new_a_i, eq.m_as[j]);
buffer.push_back(new_a_i);
m_tmp_xs.push_back(x_i);
if (m().is_zero(eq.m_as[j])) {
m_occs[x_i].erase(m_next_eq);
}
else {
eq.m_xs[j] = x_i;
j++;
}
}
}
SASSERT(j < sz);
// add parameter: p to new equality, and m_next_pos_a * m_next_a * p to current eq
m().set(new_a_i, 1);
buffer.push_back(new_a_i);
m_tmp_xs.push_back(p);
m().set(eq.m_as[j], m_next_a);
if (!m_next_pos_a)
m().neg(eq.m_as[j]);
eq.m_xs[j] = p;
j++;
unsigned new_sz = j;
// shrink current eq
for (; j < sz; j++)
m().del(eq.m_as[j]);
eq.m_as.shrink(new_sz);
eq.m_xs.shrink(new_sz);
// adjust c
mpz new_c;
decompose(m_next_pos_a, m_next_a, eq.m_c, new_c, eq.m_c);
// create auxiliary equation
equation * new_eq = mk_eq(m_tmp_xs.size(), buffer.c_ptr(), m_tmp_xs.c_ptr(), new_c, 0, nullptr, nullptr, false);
// new_eq doesn't need to normalized, since it has unit coefficients
TRACE("euclidean_solver", tout << "decomposition: new parameter x" << p << " aux eq:\n";
display(tout, *new_eq); tout << "\n";
display(tout, eq); tout << "\n";
tout << "next_x " << m_next_x << "\n";);
m_solved[m_next_x] = m_solution.size();
m_solution.push_back(new_eq);
substitute_most_recent_solution(m_next_x);
m().del(new_a_i);
m().del(new_c);
}
bool solve() {
if (inconsistent()) return false;
TRACE("euclidean_solver", tout << "solving...\n"; display(tout););
while (select_next_var()) {
CTRACE("euclidean_solver_bug", m_next_x == null_var, display(tout););
TRACE("euclidean_solver", tout << "eliminating x" << m_next_x << "\n";);
if (m().is_one(m_next_a) || m().is_minus_one(m_next_a))
elim_unit();
else
decompose_and_elim();
TRACE("euclidean_solver", display(tout););
if (inconsistent()) return false;
}
return true;
}
bool inconsistent() const {
return m_inconsistent != null_eq_idx;
}
bool is_parameter(var x) const {
return m_parameter[x];
}
void normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime, justification_vector & js) {
TRACE("euclidean_solver", tout << "before applying solution set\n";
for (unsigned i = 0; i < num; i++) {
tout << m().to_string(as[i]) << "*x" << xs[i] << " ";
}
tout << "\n";);
m_norm_xs_vector.reset();
m_norm_as_vector.reset();
for (unsigned i = 0; i < num; i++) {
m_norm_xs_vector.push_back(xs[i]);
m_norm_as_vector.push_back(mpz());
m().set(m_norm_as_vector.back(), as[i]);
}
sort(m_norm_as_vector, m_norm_xs_vector, m_as_buffer);
DEBUG_CODE(for (unsigned i = 1; i < m_norm_xs_vector.size(); ++i) SASSERT(m_norm_xs_vector[i - 1] != m_norm_xs_vector[i]););
m_norm_bs_vector.reset();
js.reset();
m().set(c_prime, c);
apply_solution(m_norm_as_vector, m_norm_xs_vector, c_prime, m_norm_bs_vector, js);
TRACE("euclidean_solver", tout << "after applying solution set\n";
for (unsigned i = 0; i < m_norm_as_vector.size(); i++) {
tout << m().to_string(m_norm_as_vector[i]) << "*x" << m_norm_xs_vector[i] << " ";
}
tout << "\n";);
// compute gcd of the result m_norm_as_vector
if (m_norm_as_vector.empty()) {
m().set(a_prime, 0);
}
else {
mpz a;
m().set(a_prime, m_norm_as_vector[0]);
m().abs(a_prime);
unsigned sz = m_norm_as_vector.size();
for (unsigned i = 1; i < sz; i++) {
if (m().is_one(a_prime))
break;
m().set(a, m_norm_as_vector[i]);
m().abs(a);
m().gcd(a_prime, a, a_prime);
}
m().del(a);
}
// REMARK: m_norm_bs_vector contains the linear combination of the justifications. It may be useful if we
// decided (one day) to generate detailed proofs for this step.
del_nums(m_norm_as_vector);
del_nums(m_norm_bs_vector);
}
};
euclidean_solver::euclidean_solver(numeral_manager * m):
m_imp(alloc(imp, m)) {
}
euclidean_solver::~euclidean_solver() {
dealloc(m_imp);
}
euclidean_solver::numeral_manager & euclidean_solver::m() const {
return m_imp->m();
}
void euclidean_solver::reset() {
numeral_manager * m = m_imp->m_manager;
bool owns_m = m_imp->m_owns_m;
m_imp->m_owns_m = false;
dealloc(m_imp);
m_imp = alloc(imp, m);
m_imp->m_owns_m = owns_m;
}
euclidean_solver::var euclidean_solver::mk_var() {
return m_imp->mk_var(false);
}
euclidean_solver::justification euclidean_solver::mk_justification() {
return m_imp->mk_justification();
}
void euclidean_solver::assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j) {
m_imp->assert_eq(num, as, xs, c, j);
}
bool euclidean_solver::solve() {
return m_imp->solve();
}
euclidean_solver::justification_vector const & euclidean_solver::get_justification() const {
return m_imp->get_justification();
}
bool euclidean_solver::inconsistent() const {
return m_imp->inconsistent();
}
bool euclidean_solver::is_parameter(var x) const {
return m_imp->is_parameter(x);
}
void euclidean_solver::normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime,
justification_vector & js) {
return m_imp->normalize(num, as, xs, c, a_prime, c_prime, js);
}
void euclidean_solver::display(std::ostream & out) const {
m_imp->display(out);
}

102
src/math/euclid/euclidean_solver.h
View file

@ -1,102 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
euclidean_solver.h
Abstract:
Euclidean Solver with support for explanations.
Author:
Leonardo de Moura (leonardo) 2011-07-08.
Revision History:
--*/
#ifndef EUCLIDEAN_SOLVER_H_
#define EUCLIDEAN_SOLVER_H_
#include "util/mpq.h"
#include "util/vector.h"
class euclidean_solver {
struct imp;
imp * m_imp;
public:
typedef unsigned var;
typedef unsigned justification;
typedef unsynch_mpq_manager numeral_manager;
typedef svector<justification> justification_vector;
static const justification null_justification = UINT_MAX;
/**
\brief If m == 0, then the solver will create its own numeral manager.
*/
euclidean_solver(numeral_manager * m);
~euclidean_solver();
numeral_manager & m() const;
/**
\brief Reset the state of the euclidean solver.
*/
void reset();
/**
\brief Creates a integer variable.
*/
var mk_var();
/**
\brief Creates a fresh justification id.
*/
justification mk_justification();
/**
\brief Asserts an equation of the form as[0]*xs[0] + ... + as[num-1]*xs[num-1] + c = 0 with justification j.
The numerals must be created using the numeral_manager m().
*/
void assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j = null_justification);
/**
\brief Solve the current set of equations. Return false if it is inconsistent.
*/
bool solve();
/**
\brief Return a set of justifications (proof) for the inconsitency.
\pre inconsistent()
*/
justification_vector const & get_justification() const;
bool inconsistent() const;
/**
\brief Return true if the variable is a "parameter" created by the Euclidean solver.
*/
bool is_parameter(var x) const;
/**
Given a linear polynomial as[0]*xs[0] + ... + as[num-1]*xs[num-1] + c and the current solution set,
It applies the solution set to produce a polynomial of the for a_prime * p + c_prime, where
a_prime * p represents a linear polynomial where the coefficient of every monomial is a multiple of
a_prime.
The justification is stored in js.
Note that, this function does not return the actual p.
The numerals must be created using the numeral_manager m().
*/
void normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime, justification_vector & js);
void display(std::ostream & out) const;
};
#endif

1
src/smt/CMakeLists.txt
View file

@ -77,7 +77,6 @@ z3_add_component(smt
COMPONENT_DEPENDENCIES
bit_blaster
cmd_context
euclid
fpa
grobner
nlsat

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

@ -59,7 +59,6 @@ def_module_params(module_name='smt',
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),

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

@ -29,7 +29,6 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_nl_arith_gb = p.arith_nl_gb();
m_nl_arith_branching = p.arith_nl_branching();
m_nl_arith_rounds = p.arith_nl_rounds();
m_arith_euclidean_solver = p.arith_euclidean_solver();
m_arith_propagate_eqs = p.arith_propagate_eqs();
m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
m_arith_int_eq_branching = p.arith_int_eq_branch();
@ -93,5 +92,4 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_max_degree);
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_arith_euclidean_solver);
}

5
src/smt/params/theory_arith_params.h
View file

@ -106,8 +106,6 @@ struct theory_arith_params {
bool m_nl_arith_branching;
unsigned m_nl_arith_rounds;
// euclidean solver for tighting bounds
bool m_arith_euclidean_solver;
theory_arith_params(params_ref const & p = params_ref()):
@ -155,8 +153,7 @@ struct theory_arith_params {
m_nl_arith_gb_perturbate(true),
m_nl_arith_max_degree(6),
m_nl_arith_branching(true),
m_nl_arith_rounds(1024),
m_arith_euclidean_solver(false) {
m_nl_arith_rounds(1024) {
updt_params(p);
}

6
src/smt/theory_arith.h
View file

@ -853,9 +853,9 @@ namespace smt {
bool max_min_infeasible_int_vars();
void patch_int_infeasible_vars();
void fix_non_base_vars();
unsynch_mpq_manager m_es_num_manager; // manager for euclidean solver.
struct euclidean_solver_bridge;
bool apply_euclidean_solver();
// unsynch_mpq_manager m_es_num_manager; // manager for euclidean solver.
// struct euclidean_solver_bridge;
// bool apply_euclidean_solver();
final_check_status check_int_feasibility();
// -----------------------------------

333
src/smt/theory_arith_int.h
View file

@ -23,7 +23,6 @@ Revision History:
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "ast/ast_smt2_pp.h"
#include "math/euclid/euclidean_solver.h"
namespace smt {
@ -964,335 +963,6 @@ namespace smt {
failed();
}
template<typename Ext>
struct theory_arith<Ext>::euclidean_solver_bridge {
typedef numeral_buffer<mpz, euclidean_solver::numeral_manager> mpz_buffer;
theory_arith & t;
euclidean_solver m_solver;
unsigned_vector m_tv2v; // theory var to euclidean solver var
svector<theory_var> m_j2v; // justification to theory var
// aux fields
unsigned_vector m_xs;
mpz_buffer m_as;
unsigned_vector m_js;
typedef euclidean_solver::var evar;
typedef euclidean_solver::justification ejustification;
euclidean_solver_bridge(theory_arith & _t):t(_t), m_solver(&t.m_es_num_manager), m_as(m_solver.m()) {}
evar mk_var(theory_var v) {
m_tv2v.reserve(v+1, UINT_MAX);
if (m_tv2v[v] == UINT_MAX)
m_tv2v[v] = m_solver.mk_var();
return m_tv2v[v];
}
/**
\brief Given a monomial, retrieve its coefficient and the power product
That is, mon = a * pp
*/
void get_monomial(expr * mon, rational & a, expr * & pp) {
expr * a_expr;
if (t.m_util.is_mul(mon, a_expr, pp) && t.m_util.is_numeral(a_expr, a))
return;
a = rational(1);
pp = mon;
}
/**
\brief Return the theory var associated with the given power product.
*/
theory_var get_theory_var(expr * pp) {
context & ctx = t.get_context();
if (ctx.e_internalized(pp)) {
enode * e = ctx.get_enode(pp);
if (t.is_attached_to_var(e))
return e->get_th_var(t.get_id());
}
return null_theory_var;
}
/**
\brief Create an euclidean_solver variable for the given
power product, if it has a theory variable associated with
it.
*/
evar mk_var(expr * pp) {
theory_var v = get_theory_var(pp);
if (v == null_theory_var)
return UINT_MAX;
return mk_var(v);
}
/**
\brief Return the euclidean_solver variable associated with the given
power product. Return UINT_MAX, if it doesn't have one.
*/
evar get_var(expr * pp) {
theory_var v = get_theory_var(pp);
if (v == null_theory_var || v >= static_cast<int>(m_tv2v.size()))
return UINT_MAX;
return m_tv2v[v];
}
void assert_eqs() {
// traverse definitions looking for equalities
mpz c, a;
mpz one;
euclidean_solver::numeral_manager & m = m_solver.m();
m.set(one, 1);
mpz_buffer & as = m_as;
unsigned_vector & xs = m_xs;
int num = t.get_num_vars();
for (theory_var v = 0; v < num; v++) {
if (!t.is_fixed(v))
continue;
if (!t.is_int(v))
continue; // only integer variables
expr * n = t.get_enode(v)->get_owner();
if (t.m_util.is_numeral(n))
continue; // skip stupid equality c - c = 0
inf_numeral const & val = t.get_value(v);
rational num = val.get_rational().to_rational();
SASSERT(num.is_int());
num.neg();
m.set(c, num.to_mpq().numerator());
ejustification j = m_solver.mk_justification();
m_j2v.reserve(j+1, null_theory_var);
m_j2v[j] = v;
as.reset();
xs.reset();
bool failed = false;
unsigned num_args;
expr * const * args;
if (t.m_util.is_add(n)) {
num_args = to_app(n)->get_num_args();
args = to_app(n)->get_args();
}
else {
num_args = 1;
args = &n;
}
for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i];
expr * pp;
rational a_val;
get_monomial(arg, a_val, pp);
if (!a_val.is_int()) {
failed = true;
break;
}
evar x = mk_var(pp);
if (x == UINT_MAX) {
failed = true;
break;
}
m.set(a, a_val.to_mpq().numerator());
as.push_back(a);
xs.push_back(x);
}
if (!failed) {
m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j);
TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";);
}
else {
TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";);
}
}
m.del(a);
m.del(c);
m.del(one);
}
void mk_bound(theory_var v, rational k, bool lower, bound * old_bound, unsigned_vector const & js) {
derived_bound * new_bound = alloc(derived_bound, v, inf_numeral(k), lower ? B_LOWER : B_UPPER);
t.m_tmp_lit_set.reset();
t.m_tmp_eq_set.reset();
if (old_bound != nullptr) {
t.accumulate_justification(*old_bound, *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set);
}
unsigned_vector::const_iterator it = js.begin();
unsigned_vector::const_iterator end = js.end();
for (; it != end; ++it) {
ejustification j = *it;
theory_var fixed_v = m_j2v[j];
SASSERT(fixed_v != null_theory_var);
t.accumulate_justification(*(t.lower(fixed_v)), *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set);
t.accumulate_justification(*(t.upper(fixed_v)), *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set);
}
t.m_bounds_to_delete.push_back(new_bound);
t.m_asserted_bounds.push_back(new_bound);
}
void mk_lower(theory_var v, rational k, bound * old_bound, unsigned_vector const & js) {
mk_bound(v, k, true, old_bound, js);
}
void mk_upper(theory_var v, rational k, bound * old_bound, unsigned_vector const & js) {
mk_bound(v, k, false, old_bound, js);
}
bool tight_bounds(theory_var v) {
SASSERT(!t.is_fixed(v));
euclidean_solver::numeral_manager & m = m_solver.m();
expr * n = t.get_enode(v)->get_owner();
SASSERT(!t.m_util.is_numeral(n)); // should not be a numeral since v is not fixed.
bool propagated = false;
mpz a;
mpz c;
rational g; // gcd of the coefficients of the variables that are not in m_solver
rational c2;
bool init_g = false;
mpz_buffer & as = m_as;
unsigned_vector & xs = m_xs;
as.reset();
xs.reset();
unsigned num_args;
expr * const * args;
if (t.m_util.is_add(n)) {
num_args = to_app(n)->get_num_args();
args = to_app(n)->get_args();
}
else {
num_args = 1;
args = &n;
}
for (unsigned j = 0; j < num_args; j++) {
expr * arg = args[j];
expr * pp;
rational a_val;
get_monomial(arg, a_val, pp);
if (!a_val.is_int())
goto cleanup;
evar x = get_var(pp);
if (x == UINT_MAX) {
a_val = abs(a_val);
if (init_g)
g = gcd(g, a_val);
else
g = a_val;
init_g = true;
if (g.is_one())
goto cleanup; // gcd of the coeffs is one.
}
else {
m.set(a, a_val.to_mpq().numerator());
as.push_back(a);
xs.push_back(x);
}
}
m_js.reset();
m_solver.normalize(as.size(), as.c_ptr(), xs.c_ptr(), c, a, c, m_js);
if (init_g) {
if (!m.is_zero(a))
g = gcd(g, rational(a));
}
else {
g = rational(a);
}
TRACE("euclidean_solver", tout << "tightening " << mk_ismt2_pp(t.get_enode(v)->get_owner(), t.get_manager()) << "\n";
tout << "g: " << g << ", a: " << m.to_string(a) << ", c: " << m.to_string(c) << "\n";
t.display_var(tout, v););
if (g.is_one())
goto cleanup;
CTRACE("euclidean_solver_zero", g.is_zero(), tout << "tightening " << mk_ismt2_pp(t.get_enode(v)->get_owner(), t.get_manager()) << "\n";
tout << "g: " << g << ", a: " << m.to_string(a) << ", c: " << m.to_string(c) << "\n";
t.display(tout);
tout << "------------\nSolver state:\n";
m_solver.display(tout););
if (g.is_zero()) {
// The definition of v is equal to (0 + c).
// That is, v is fixed at c.
// The justification is just m_js, the existing bounds of v are not needed for justifying the new bounds for v.
c2 = rational(c);
TRACE("euclidean_solver_new", tout << "new fixed: " << c2 << "\n";);
propagated = true;
mk_lower(v, c2, nullptr, m_js);
mk_upper(v, c2, nullptr, m_js);
}
else {
TRACE("euclidean_solver", tout << "inequality can be tightned, since all coefficients are multiple of: " << g << "\n";);
// Let l and u be the current lower and upper bounds.
// Then, the following new bounds can be generated:
//
// l' := g*ceil((l - c)/g) + c
// u' := g*floor((l - c)/g) + c
bound * l = t.lower(v);
bound * u = t.upper(v);
c2 = rational(c);
if (l != nullptr) {
rational l_old = l->get_value().get_rational().to_rational();
rational l_new = g*ceil((l_old - c2)/g) + c2;
TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";
tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";);
if (l_new > l_old) {
propagated = true;
mk_lower(v, l_new, l, m_js);
}
}
if (u != nullptr) {
rational u_old = u->get_value().get_rational().to_rational();
rational u_new = g*floor((u_old - c2)/g) + c2;
TRACE("euclidean_solver_new", tout << "new upper: " << u_new << " old: " << u_old << "\n";);
if (u_new < u_old) {
propagated = true;
mk_upper(v, u_new, u, m_js);
}
}
}
cleanup:
m.del(a);
m.del(c);
return propagated;
}
bool tight_bounds() {
bool propagated = false;
context & ctx = t.get_context();
// try to apply solution set to every definition
int num = t.get_num_vars();
for (theory_var v = 0; v < num; v++) {
if (t.is_fixed(v))
continue; // skip equations...
if (!t.is_int(v))
continue; // skip non integer definitions...
if (t.lower(v) == nullptr && t.upper(v) == nullptr)
continue; // there is nothing to be tightned
if (tight_bounds(v))
propagated = true;
if (ctx.inconsistent())
break;
}
return propagated;
}
bool operator()() {
TRACE("euclidean_solver", t.display(tout););
assert_eqs();
m_solver.solve();
if (m_solver.inconsistent()) {
// TODO: set conflict
TRACE("euclidean_solver_conflict", tout << "conflict detected...\n"; m_solver.display(tout););
return false;
}
return tight_bounds();
}
};
template<typename Ext>
bool theory_arith<Ext>::apply_euclidean_solver() {
TRACE("euclidean_solver", tout << "executing euclidean solver...\n";);
euclidean_solver_bridge esb(*this);
if (esb()) {
propagate_core();
return true;
}
return false;
}
/**
\brief Return FC_DONE if the assignment is int feasible. Otherwise, apply GCD test,
branch and bound and Gomory Cuts.
@ -1341,9 +1011,6 @@ namespace smt {
if (!gcd_test())
return FC_CONTINUE;
if (m_params.m_arith_euclidean_solver)
apply_euclidean_solver();
if (get_context().inconsistent())
return FC_CONTINUE;