mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 20:05:51 +00:00
merge LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
085d31dca2
commit
911b24784a
120 changed files with 23069 additions and 15 deletions
260
src/util/lp/test_bound_analyzer.h
Normal file
260
src/util/lp/test_bound_analyzer.h
Normal file
|
|
@ -0,0 +1,260 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/linear_combination_iterator.h"
|
||||
#include "util/lp/implied_bound.h"
|
||||
#include "util/lp/lp_settings.h"
|
||||
#include <functional>
|
||||
// this class is for testing only
|
||||
|
||||
// We have an equality : sum by j of row[j]*x[j] = rs
|
||||
// We try to pin a var by pushing the total by using the variable bounds
|
||||
// In a loop we drive the partial sum down, denoting the variables of this process by _u.
|
||||
// In the same loop trying to pin variables by pushing the partial sum up, denoting the variable related to it by _l
|
||||
|
||||
// here in addition we assume that all coefficient in the row are positive
|
||||
namespace lean {
|
||||
|
||||
class test_bound_analyzer {
|
||||
linear_combination_iterator<mpq> & m_it;
|
||||
std::function<impq (unsigned)>& m_low_bounds;
|
||||
std::function<impq (unsigned)>& m_upper_bounds;
|
||||
std::function<column_type (unsigned)> m_column_types;
|
||||
vector<implied_bound> & m_implied_bounds;
|
||||
vector<mpq> m_coeffs;
|
||||
int m_coeff_sign;
|
||||
vector<unsigned> m_index;
|
||||
unsigned m_row_or_term_index;
|
||||
std::function<bool (unsigned, bool, mpq &, bool & strict)> & m_try_get_found_bound;
|
||||
public :
|
||||
// constructor
|
||||
test_bound_analyzer(linear_combination_iterator<mpq> &it,
|
||||
std::function<impq (unsigned) > & low_bounds,
|
||||
std::function<impq (unsigned)> & upper_bounds,
|
||||
std::function<column_type (unsigned)> column_types,
|
||||
vector<implied_bound> & evidence_vector,
|
||||
unsigned row_or_term_index,
|
||||
std::function<bool (unsigned, bool, mpq &, bool & strict)> & try_get_found_bound) :
|
||||
m_it(it),
|
||||
m_low_bounds(low_bounds),
|
||||
m_upper_bounds(upper_bounds),
|
||||
m_column_types(column_types),
|
||||
m_implied_bounds(evidence_vector),
|
||||
m_row_or_term_index(row_or_term_index),
|
||||
m_try_get_found_bound(try_get_found_bound)
|
||||
{
|
||||
m_it.reset();
|
||||
unsigned i;
|
||||
mpq a;
|
||||
while (m_it.next(a, i) ) {
|
||||
m_coeffs.push_back(a);
|
||||
m_index.push_back(i);
|
||||
}
|
||||
}
|
||||
|
||||
static int sign (const mpq & t) { return is_pos(t) ? 1: -1;}
|
||||
|
||||
void analyze() {
|
||||
// We have the equality sum by j of row[j]*x[j] = m_rs
|
||||
// We try to pin a var by pushing the total of the partial sum down, denoting the variable of this process by _u.
|
||||
for (unsigned i = 0; i < m_index.size(); i++) {
|
||||
analyze_i(i);
|
||||
}
|
||||
}
|
||||
void analyze_i(unsigned i) {
|
||||
// set the m_coeff_is_pos
|
||||
m_coeff_sign = sign(m_coeffs[i]);
|
||||
analyze_i_for_lower(i);
|
||||
analyze_i_for_upper(i);
|
||||
}
|
||||
|
||||
void analyze_i_for_upper(unsigned i) {
|
||||
mpq l;
|
||||
bool strict = false;
|
||||
lean_assert(is_zero(l));
|
||||
for (unsigned k = 0; k < m_index.size(); k++) {
|
||||
if (k == i)
|
||||
continue;
|
||||
mpq lb;
|
||||
bool str;
|
||||
if (!upper_bound_of_monoid(k, lb, str)) {
|
||||
return;
|
||||
}
|
||||
l += lb;
|
||||
if (str)
|
||||
strict = true;
|
||||
}
|
||||
l /= m_coeffs[i];
|
||||
unsigned j = m_index[i];
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
{
|
||||
const auto & lb = m_upper_bounds(j);
|
||||
if (l > lb.x || (l == lb.x && !(is_zero(lb.y) && strict))) {
|
||||
break; // no improvement on the existing upper bound
|
||||
}
|
||||
}
|
||||
default:
|
||||
// std::cout << " got an upper bound with " << T_to_string(l) << "\n";
|
||||
m_implied_bounds.push_back(implied_bound(l, j, false, is_pos(m_coeffs[i]), m_row_or_term_index, strict));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool low_bound_of_monoid(unsigned k, mpq & lb, bool &strict) const {
|
||||
int s = - m_coeff_sign * sign(m_coeffs[k]);
|
||||
unsigned j = m_index[k];
|
||||
if (s > 0) {
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::low_bound:
|
||||
lb = -m_coeffs[k] * m_low_bounds(j).x;
|
||||
strict = !is_zero(m_low_bounds(j).y);
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
lb = -m_coeffs[k] * m_upper_bounds(j).x;
|
||||
strict = !is_zero(m_upper_bounds(j).y);
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool upper_bound_of_monoid(unsigned k, mpq & lb, bool & strict) const {
|
||||
int s = - m_coeff_sign * sign(m_coeffs[k]);
|
||||
unsigned j = m_index[k];
|
||||
if (s > 0) {
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
lb = -m_coeffs[k] * m_upper_bounds(j).x;
|
||||
strict = !is_zero(m_upper_bounds(j).y);
|
||||
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::low_bound:
|
||||
lb = -m_coeffs[k] * m_low_bounds(j).x;
|
||||
strict = !is_zero(m_low_bounds(j).y);
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void analyze_i_for_lower(unsigned i) {
|
||||
mpq l;
|
||||
lean_assert(is_zero(l));
|
||||
bool strict = false;
|
||||
for (unsigned k = 0; k < m_index.size(); k++) {
|
||||
if (k == i)
|
||||
continue;
|
||||
mpq lb;
|
||||
bool str;
|
||||
if (!low_bound_of_monoid(k, lb, str)) {
|
||||
return;
|
||||
}
|
||||
if (str)
|
||||
strict = true;
|
||||
l += lb;
|
||||
}
|
||||
l /= m_coeffs[i];
|
||||
unsigned j = m_index[i];
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::low_bound:
|
||||
{
|
||||
const auto & lb = m_low_bounds(j);
|
||||
if (l < lb.x || (l == lb.x && !(is_zero(lb.y) && strict))) {
|
||||
break; // no improvement on the existing upper bound
|
||||
}
|
||||
}
|
||||
default:
|
||||
// std::cout << " got a lower bound with " << T_to_string(l) << "\n";
|
||||
m_implied_bounds.push_back(implied_bound(l, j, true, is_pos(m_coeffs[i]), m_row_or_term_index, strict));
|
||||
}
|
||||
}
|
||||
|
||||
bool low_bound_is_available(unsigned j) const {
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::low_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool upper_bound_is_available(unsigned j) const {
|
||||
switch(m_column_types(j)) {
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool try_get_best_avail_bound(unsigned j, bool is_lower_bound, mpq & best_bound, bool & strict_of_best_bound) const {
|
||||
if (m_try_get_found_bound(j, is_lower_bound, best_bound, strict_of_best_bound)) {
|
||||
return true;
|
||||
}
|
||||
if (is_lower_bound) {
|
||||
if (low_bound_is_available(j)) {
|
||||
best_bound = m_low_bounds(j).x;
|
||||
strict_of_best_bound = !is_zero(m_low_bounds(j).y);
|
||||
return true;
|
||||
}
|
||||
} else {
|
||||
if (upper_bound_is_available(j)) {
|
||||
best_bound = m_upper_bounds(j).x;
|
||||
strict_of_best_bound = !is_zero(m_low_bounds(j).y);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool bound_is_new(unsigned j, const mpq& b, bool is_lower_bound, bool strict) const {
|
||||
mpq best_bound;
|
||||
bool strict_of_best_bound;
|
||||
if (try_get_best_avail_bound(j, is_lower_bound, best_bound, strict_of_best_bound)) {
|
||||
if (is_lower_bound) {
|
||||
if (b > best_bound || ( b != best_bound && (strict && !strict_of_best_bound))) // the second clouse stands for strong inequality
|
||||
return true;
|
||||
} else {
|
||||
if (b < best_bound || ( b == best_bound && (strict && !strict_of_best_bound)))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue