mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

prepare the mixed case

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-14 16:49:40 -08:00
parent 8980aff7f3
commit 0e86c567cc
4 changed files with 37 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/math/lp/lar_solver.cpp
View file

@ -1289,44 +1289,53 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
}
}
// (x, y) != (x', y') => (x + delty*y) != (x' + delty*y')
void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
variable_values.clear();
mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes
unsigned j;
unsigned n = m_mpq_lar_core_solver.m_r_x.size();
std::unordered_set<impq> set_of_different_pairs;
std::unordered_set<mpq> set_of_different_singles;
do {
// different pairs have to produce different singleton values
std::unordered_set<impq> set_of_different_pairs;
std::unordered_set<mpq> set_of_different_singles;
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
set_of_different_pairs.clear();
set_of_different_singles.clear();
for (j = 0; j < n; j++ ) {
const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[j];
set_of_different_pairs.insert(rp);
mpq x = rp.x + delta * rp.y;
set_of_different_singles.insert(x);
if (set_of_different_pairs.size()
!= set_of_different_singles.size()) {
if (set_of_different_pairs.size() != set_of_different_singles.size()) {
delta /= mpq(2);
break;
}
TRACE("get_model", tout << this->get_variable_name(j) << " := " << x << "\n";);
if (!column_corresponds_to_term(j))
variable_values[j] = x;
variable_values[j] = x;
}
} while (j != n);
TRACE("lar_solver_model", tout << "delta = " << delta << "\nmodel:\n";
for (auto p : variable_values ) {
tout << this->get_variable_name(p.first) << " = " << p.second << "\n";
});
}
void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const {
mpq delta = mpq(1);
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1));
for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
const impq & rp = m_mpq_lar_core_solver.m_r_x[i];
variable_values[i] = rp.x + delta * rp.y;
}
}
void lar_solver::get_rid_of_inf_eps() {
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1));
for (unsigned j = 0; j < number_of_vars(); j++) {
auto & r = m_mpq_lar_core_solver.m_r_x[j];
r = impq(r.x + delta * r.y);
}
}
void lar_solver::set_variable_name(var_index vi, std::string name) {
m_var_register.set_name(vi, name);
}

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

@ -45,9 +45,10 @@ Revision History:
namespace lp {
typedef unsigned lpvar;
const lpvar null_lpvar = UINT_MAX;
class lar_solver : public column_namer {
typedef unsigned lpvar;
struct term_hasher {
std::size_t operator()(const lar_term &t) const
{
@ -483,6 +484,8 @@ public:
void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
void get_rid_of_inf_eps();
void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
std::string get_variable_name(var_index vi) const;

8
src/math/lp/nla_core.cpp
View file

@ -164,7 +164,8 @@ rational core::product_value(const unsigned_vector & m) const {
// return true iff the monic value is equal to the product of the values of the factors
bool core::check_monic(const monic& m) const {
SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int());
SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int());
TRACE("nla_solver", print_monic_with_vars(m, tout) << '\n';);
return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
}
@ -1122,13 +1123,9 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
return m;
}
bool core::rm_check(const monic& rm) const {
return check_monic(m_emons[rm.var()]);
}
/**
\brief Add |v| ~ |bound|
@ -1330,6 +1327,7 @@ bool core::elists_are_consistent(bool check_in_model) const {
lbool core::check(vector<lemma>& l_vec) {
lp_settings().stats().m_nla_calls++;
TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
m_lar_solver.get_rid_of_inf_eps();
m_lemma_vec = &l_vec;
if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";);

13
src/smt/theory_lra.cpp
View file

@ -752,7 +752,7 @@ class theory_lra::imp {
lpvar register_theory_var_in_lar_solver(theory_var v) {
lpvar lpv = lp().external_to_local(v);
if (lpv + 1)
if (lpv != lp::null_lpvar)
return lpv;
return lp().add_var(v, is_int(v));
}
@ -3717,12 +3717,17 @@ public:
}
void display(std::ostream & out) const {
void display(std::ostream & out) {
if (m_solver) {
lp().print_constraints(out);
lp().print_terms(out);
// auto pp = lp ::core_solver_pretty_printer<lp::mpq, lp::impq>(lp().m_mpq_lar_core_solver.m_r_solver, out);
// pp.print();
// the tableau
auto pp = lp ::core_solver_pretty_printer<lp::mpq, lp::impq>(
lp().m_mpq_lar_core_solver.m_r_solver, out);
pp.print();
for (unsigned j = 0; j < lp().number_of_vars(); j++) {
lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
}
}
unsigned nv = th.get_num_vars();
for (unsigned v = 0; v < nv; ++v) {