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

fix the build for gcc

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-14 19:20:47 -07:00
parent cbad61ba2e
commit b3673d491e
6 changed files with 41 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/bound_analyzer_on_row.h
View file

@ -284,8 +284,8 @@ private:
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
unsigned row_index = this->m_row_index; unsigned row_index = this->m_row_index;
auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index](lar_solver& s) { return explain_bound_on_var_on_coeff(s, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); }; auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index](int * s) { return explain_bound_on_var_on_coeff((B*)s, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); };
m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain ); m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain);
} }
void advance_u(unsigned j) { void advance_u(unsigned j) {
@ -318,7 +318,8 @@ private:
break; break;
} }
} }
static u_dependency* explain_bound_on_var_on_coeff(lar_solver& lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
auto& lar = bp->lp();
int bound_sign = (is_lower_bound ? 1 : -1); int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;

9
src/math/lp/implied_bound.h
View file

@ -20,7 +20,6 @@ Revision History:
#pragma once #pragma once
#include "math/lp/lp_settings.h" #include "math/lp/lp_settings.h"
#include "math/lp/lar_constraints.h" #include "math/lp/lar_constraints.h"
#include "math/lp/lar_solver.h"
namespace lp { namespace lp {
class implied_bound { class implied_bound {
public: public:
@ -34,10 +33,10 @@ class implied_bound {
bool m_is_lower_bound; bool m_is_lower_bound;
bool m_strict; bool m_strict;
private: private:
std::function<u_dependency*(lar_solver&)> m_explain_bound = nullptr; std::function<u_dependency*(int *)> m_explain_bound = nullptr;
public: public:
u_dependency* explain(lar_solver& s) const { return m_explain_bound(s); } u_dependency* explain(int * s) const { return m_explain_bound(s); }
void set_explain(std::function<u_dependency*(lar_solver&)> f) { m_explain_bound = f; } void set_explain(std::function<u_dependency*(int *)> f) { m_explain_bound = f; }
lconstraint_kind kind() const { lconstraint_kind kind() const {
lconstraint_kind k = m_is_lower_bound? GE : LE; lconstraint_kind k = m_is_lower_bound? GE : LE;
if (m_strict) if (m_strict)
@ -49,7 +48,7 @@ class implied_bound {
unsigned j, unsigned j,
bool is_lower_bound, bool is_lower_bound,
bool is_strict, bool is_strict,
std::function<u_dependency*(lar_solver&)> get_dep): std::function<u_dependency*(int *)> get_dep):
m_bound(a), m_bound(a),
m_j(j), m_j(j),
m_is_lower_bound(is_lower_bound), m_is_lower_bound(is_lower_bound),

4
src/math/lp/lar_constraints.h
View file

@ -137,8 +137,8 @@ class constraint_set {
public: public:
constraint_set(u_dependency_manager& d, column_namer& cn): constraint_set(u_dependency_manager& d, column_namer& cn):
m_dep_manager(d), m_namer(cn),
m_namer(cn) {} m_dep_manager(d) {}
~constraint_set() { ~constraint_set() {
for (auto* c : m_constraints) for (auto* c : m_constraints)

2
src/math/lp/lar_solver.h
View file

@ -311,7 +311,7 @@ class lar_solver : public column_namer {
template <typename T> template <typename T>
void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) { void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
u_dependency* dep = ib.explain(*this); u_dependency* dep = ib.explain((int*)&bp);
for (auto ci : flatten(dep)) for (auto ci : flatten(dep))
bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients
/* /*

58
src/math/lp/lp_bound_propagator.h
View file

@ -40,6 +40,8 @@ class lp_bound_propagator {
return x != UINT_MAX; return x != UINT_MAX;
} }
public: public:
const lar_solver& lp() const { return m_imp.lp(); }
lar_solver& lp() { return m_imp.lp(); }
bool upper_bound_is_available(unsigned j) const { bool upper_bound_is_available(unsigned j) const {
switch (get_column_type(j)) { switch (get_column_type(j)) {
case column_type::fixed: case column_type::fixed:
@ -138,12 +140,13 @@ private:
return n_of_non_fixed <= 1 && !big_bound; return n_of_non_fixed <= 1 && !big_bound;
} }
void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);});
add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);});
} }
void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function<u_dependency* (lar_solver&)> explain_dep) { void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function<u_dependency* (int*)> explain_dep) {
unsigned k; unsigned k;
if (!try_get_value(m_improved_lower_bounds, monic_var, k)) { if (!try_get_value(m_improved_lower_bounds, monic_var, k)) {
m_improved_lower_bounds[monic_var] = m_ibounds.size(); m_improved_lower_bounds[monic_var] = m_ibounds.size();
@ -152,12 +155,12 @@ private:
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) { if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(v, monic_var, true, is_strict, explain_dep); found_bound = implied_bound(v, monic_var, true, is_strict, explain_dep);
TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} }
} }
void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function <u_dependency* (lar_solver&)> explain_bound) { void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function <u_dependency* (int*)> explain_bound) {
unsigned k; unsigned k;
if (!try_get_value(m_improved_upper_bounds, monic_var, k)) { if (!try_get_value(m_improved_upper_bounds, monic_var, k)) {
m_improved_upper_bounds[monic_var] = m_ibounds.size(); m_improved_upper_bounds[monic_var] = m_ibounds.size();
@ -166,7 +169,7 @@ private:
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) { if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(bound_val, monic_var, false, is_strict, explain_bound); found_bound = implied_bound(bound_val, monic_var, false, is_strict, explain_bound);
TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} }
} }
@ -193,66 +196,63 @@ private:
bound_value = lp().column_lower_bound(non_fixed); bound_value = lp().column_lower_bound(non_fixed);
is_strict = !bound_value.y.is_zero(); is_strict = !bound_value.y.is_zero();
if (k.is_pos()) if (k.is_pos())
add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](lar_solver& s) { return s.get_column_lower_bound_witness(non_fixed); }); add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](int* s) { return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(non_fixed); });
else else
add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_lower_bound_witness(non_fixed);}); add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(non_fixed);});
} }
if (upper_bound_is_available(non_fixed)) { if (upper_bound_is_available(non_fixed)) {
bound_value = lp().column_upper_bound(non_fixed); bound_value = lp().column_upper_bound(non_fixed);
is_strict = !bound_value.y.is_zero(); is_strict = !bound_value.y.is_zero();
if (k.is_neg()) if (k.is_neg())
add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(non_fixed);});
else else
add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(non_fixed);});
} }
if (lower_bound_is_available(monic_var)) { if (lower_bound_is_available(monic_var)) {
bound_value = lp().column_lower_bound(monic_var); bound_value = lp().column_lower_bound(monic_var);
is_strict = !bound_value.y.is_zero(); is_strict = !bound_value.y.is_zero();
if (k.is_pos()) if (k.is_pos())
add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_lower_bound_witness(monic_var);}); add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(monic_var);});
else else
add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_lower_bound_witness(monic_var);}); add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(monic_var);});
} }
if (upper_bound_is_available(monic_var)) { if (upper_bound_is_available(monic_var)) {
bound_value = lp().column_upper_bound(monic_var); bound_value = lp().column_upper_bound(monic_var);
is_strict = !bound_value.y.is_zero(); is_strict = !bound_value.y.is_zero();
if (k.is_neg()) if (k.is_neg())
add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_upper_bound_witness(monic_var);}); add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(monic_var);});
else else
add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_upper_bound_witness(monic_var);}); add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(monic_var);});
} }
} else { // all variables are fixed } else { // all variables are fixed
add_lower_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); add_lower_bound_monic(monic_var, k, false, [vars](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_columns(vars);});
add_upper_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); add_upper_bound_monic(monic_var, k, false, [vars](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_columns(vars);});
} }
} }
} }
const lar_solver& lp() const { return m_imp.lp(); }
lar_solver& lp() { return m_imp.lp(); }
column_type get_column_type(unsigned j) const { column_type get_column_type(unsigned j) const {
return (*m_column_types)[j]; return (*m_column_types)[j];
} }
const impq& get_lower_bound(unsigned j) const { const impq& get_lower_bound(unsigned j) const {
return m_imp.lp().get_lower_bound(j); return lp().get_lower_bound(j);
} }
const mpq& get_lower_bound_rational(unsigned j) const { const mpq& get_lower_bound_rational(unsigned j) const {
return m_imp.lp().get_lower_bound(j).x; return lp().get_lower_bound(j).x;
} }
const impq& get_upper_bound(unsigned j) const { const impq& get_upper_bound(unsigned j) const {
return m_imp.lp().get_upper_bound(j); return lp().get_upper_bound(j);
} }
const mpq& get_upper_bound_rational(unsigned j) const { const mpq& get_upper_bound_rational(unsigned j) const {
return m_imp.lp().get_upper_bound(j).x; return lp().get_upper_bound(j).x;
} }
// require also the zero infinitesemal part // require also the zero infinitesemal part
@ -260,8 +260,8 @@ private:
return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero(); return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
} }
void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* (lar_solver&)> explain_bound) { void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* (int*)> explain_bound) {
j = m_imp.lp().column_to_reported_index(j); j = lp().column_to_reported_index(j);
lconstraint_kind kind = is_low ? GE : LE; lconstraint_kind kind = is_low ? GE : LE;
if (strict) if (strict)
@ -277,12 +277,12 @@ private:
found_bound.m_bound = v; found_bound.m_bound = v;
found_bound.m_strict = strict; found_bound.m_strict = strict;
found_bound.set_explain(explain_bound); found_bound.set_explain(explain_bound);
TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_lower_bounds[j] = m_ibounds.size(); m_improved_lower_bounds[j] = m_ibounds.size();
m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }
} else { // the upper bound case } else { // the upper bound case
if (try_get_value(m_improved_upper_bounds, j, k)) { if (try_get_value(m_improved_upper_bounds, j, k)) {
@ -291,12 +291,12 @@ private:
found_bound.m_bound = v; found_bound.m_bound = v;
found_bound.m_strict = strict; found_bound.m_strict = strict;
found_bound.set_explain(explain_bound); found_bound.set_explain(explain_bound);
TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
} }
} else { } else {
m_improved_upper_bounds[j] = m_ibounds.size(); m_improved_upper_bounds[j] = m_ibounds.size();
m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound));
TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout););
} }
} }
} }

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

@ -253,7 +253,7 @@ namespace arith {
first = false; first = false;
reset_evidence(); reset_evidence();
m_explanation.clear(); m_explanation.clear();
be.explain(lp()); be.explain((int*)&m_bp);
} }
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1); updt_unassigned_bounds(v, -1);