mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
print terms as monomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
8955509023
commit
130995a3db
10 changed files with 99 additions and 82 deletions
|
|
@ -397,7 +397,7 @@ std::ostream& emonomials::display(const core& cr, std::ostream& out) const {
|
|||
out << "monomials\n";
|
||||
unsigned idx = 0;
|
||||
for (auto const& m : m_monomials) {
|
||||
out << "m" << (idx++) << ": " << pp_rmon(cr, m) << "\n";
|
||||
out << "m" << (idx++) << ": " << pp_mon_with_vars(cr, m) << "\n";
|
||||
}
|
||||
return display_use(out);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -310,7 +310,7 @@ public:
|
|||
lp_assert(m_int_solver.current_solution_is_inf_on_cut());
|
||||
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
|
||||
m_int_solver.m_lar_solver->subs_term_columns(m_t);
|
||||
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
|
||||
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
|
||||
return lia_move::cut;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1418,7 +1418,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c
|
|||
}
|
||||
|
||||
std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const {
|
||||
print_linear_combination_of_column_indices_only(term, out);
|
||||
print_linear_combination_of_column_indices_only(term.coeffs_as_vector(), out);
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -77,52 +77,51 @@ bool is_non_decreasing(const K& v) {
|
|||
return true;
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
std::ostream& print_linear_combination_customized(const vector<std::pair<T, unsigned>> & coeffs, std::function<std::string (unsigned)> var_str, std::ostream & out) {
|
||||
bool first = true;
|
||||
for (const auto & it : coeffs) {
|
||||
T val = it.first;
|
||||
if (first) {
|
||||
first = false;
|
||||
if (val.is_neg()) {
|
||||
out << "- ";
|
||||
val = -val;
|
||||
}
|
||||
} else {
|
||||
if (val.is_pos()) {
|
||||
out << " + ";
|
||||
} else {
|
||||
out << " - ";
|
||||
val = -val;
|
||||
}
|
||||
}
|
||||
if (val == 1)
|
||||
out << " ";
|
||||
else {
|
||||
out << T_to_string(val);
|
||||
}
|
||||
out << var_str(it.second);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostream & out) {
|
||||
bool first = true;
|
||||
for (const auto & it : coeffs) {
|
||||
auto val = it.coeff();
|
||||
if (first) {
|
||||
first = false;
|
||||
} else {
|
||||
if (val.is_pos()) {
|
||||
out << " + ";
|
||||
} else {
|
||||
out << " - ";
|
||||
val = -val;
|
||||
}
|
||||
}
|
||||
if (val == 1)
|
||||
out << " ";
|
||||
else
|
||||
out << T_to_string(val);
|
||||
|
||||
out << "v" << it.var();
|
||||
}
|
||||
std::ostream& print_linear_combination_of_column_indices_only(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) {
|
||||
return print_linear_combination_customized(
|
||||
coeffs,
|
||||
[](unsigned j) {std::stringstream ss; ss << "v" << j; return ss.str();},
|
||||
out);
|
||||
}
|
||||
template <typename T>
|
||||
void print_linear_combination_of_column_indices_only(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) {
|
||||
bool first = true;
|
||||
template <typename T, typename K>
|
||||
std::ostream& print_linear_combination_indices_only(const T & coeffs, std::ostream & out) {
|
||||
vector<std::pair<K, unsigned>> cfs;
|
||||
|
||||
for (const auto & it : coeffs) {
|
||||
auto val = it.first;
|
||||
if (first) {
|
||||
first = false;
|
||||
} else {
|
||||
if (val.is_pos()) {
|
||||
out << " + ";
|
||||
} else {
|
||||
out << " - ";
|
||||
val = -val;
|
||||
}
|
||||
}
|
||||
if (val == 1)
|
||||
out << " ";
|
||||
else
|
||||
out << T_to_string(val);
|
||||
|
||||
out << "v" << it.second;
|
||||
cfs.push_back(std::make_pair(it.coeff(), it.var()));
|
||||
}
|
||||
return print_linear_combination_of_column_indices_only<K>(cfs, out);
|
||||
}
|
||||
|
||||
inline void throw_exception(std::string && str) {
|
||||
|
|
|
|||
|
|
@ -121,16 +121,16 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
|
|||
if (!try_insert(v, explored)) {
|
||||
return false;
|
||||
}
|
||||
const monomial& m_v = c().m_emons[v];
|
||||
TRACE("nla_solver", tout << "m_v = " << pp_rmon(c(), m_v););
|
||||
CTRACE("nla_solver", !c().m_emons.is_canonized(m_v),
|
||||
c().m_emons.display(c(), tout);
|
||||
const monomial& m_v = c().emons()[v];
|
||||
TRACE("nla_solver", tout << "m_v = " << pp_mon_with_vars(c(), m_v););
|
||||
CTRACE("nla_solver", !c().emons().is_canonized(m_v),
|
||||
c().emons().display(c(), tout);
|
||||
c().m_evars.display(tout);
|
||||
);
|
||||
SASSERT(c().m_emons.is_canonized(m_v));
|
||||
SASSERT(c().emons().is_canonized(m_v));
|
||||
|
||||
for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) {
|
||||
TRACE("nla_solver_details", tout << "m = " << pp_rmon(c(), m););
|
||||
for (auto const& m : c().emons().enum_sign_equiv_monomials(v)) {
|
||||
TRACE("nla_solver_details", tout << "m = " << pp_mon_with_vars(c(), m););
|
||||
SASSERT(m.rvars() == m_v.rvars());
|
||||
if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done())
|
||||
return true;
|
||||
|
|
@ -160,8 +160,8 @@ bool basics::basic_sign_lemma(bool derived) {
|
|||
void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
|
||||
add_empty_lemma();
|
||||
TRACE("nla_solver",
|
||||
tout << "m = " << pp_rmon(_(), m);
|
||||
tout << "n = " << pp_rmon(_(), n);
|
||||
tout << "m = " << pp_mon_with_vars(_(), m);
|
||||
tout << "n = " << pp_mon_with_vars(_(), n);
|
||||
);
|
||||
c().mk_ineq(m.var(), -sign, n.var(), llc::EQ);
|
||||
explain(m);
|
||||
|
|
@ -704,7 +704,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const f
|
|||
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& m, const factorization& f) {
|
||||
rational sign = sign_to_rat(m.rsign());
|
||||
SASSERT(m.rsign() == canonize_sign(f));
|
||||
TRACE("nla_solver_bl", tout << pp_rmon(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; );
|
||||
TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; );
|
||||
lpvar not_one = -1;
|
||||
for (auto j : f){
|
||||
TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
|
||||
|
|
@ -760,7 +760,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
|
|||
explain(f);
|
||||
TRACE("nla_solver",
|
||||
c().print_lemma(tout);
|
||||
tout << "m = " << pp_rmon(c(), m);
|
||||
tout << "m = " << pp_mon_with_vars(c(), m);
|
||||
);
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -189,6 +189,19 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
|
|||
}
|
||||
return out;
|
||||
}
|
||||
template <typename T>
|
||||
std::string core::product_indices_str(const T & m) const {
|
||||
std::stringstream out;
|
||||
bool first = true;
|
||||
for (lpvar v : m) {
|
||||
if (!first)
|
||||
out << "*";
|
||||
else
|
||||
first = false;
|
||||
out << "v" << v;;
|
||||
}
|
||||
return out.str();
|
||||
}
|
||||
|
||||
std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
|
||||
if (f.sign())
|
||||
|
|
@ -209,7 +222,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
|
|||
print_var(f.var(), out);
|
||||
}
|
||||
else {
|
||||
out << " MON = " << pp_rmon(*this, m_emons[f.var()]);
|
||||
out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
|
@ -1184,7 +1197,7 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf)
|
|||
if (val(m) != val(a) * val(b)) {
|
||||
bf = f;
|
||||
TRACE("nla_solver", tout << "found bf";
|
||||
tout << ":m:" << pp_rmon(*this, m) << "\n";
|
||||
tout << ":m:" << pp_mon_with_vars(*this, m) << "\n";
|
||||
tout << "bf:"; print_bfc(bf, tout););
|
||||
|
||||
return true;
|
||||
|
|
@ -1254,6 +1267,7 @@ bool core:: done() const {
|
|||
}
|
||||
|
||||
lbool core:: inner_check(bool derived) {
|
||||
TRACE("nla_cn", print_terms(tout););
|
||||
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
|
||||
TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
|
||||
if (search_level == 0) {
|
||||
|
|
@ -1342,11 +1356,17 @@ lbool core::test_check(
|
|||
return check(l);
|
||||
}
|
||||
|
||||
} // end of nla
|
||||
|
||||
|
||||
#if 0
|
||||
rational core::mon_value_by_vars(unsigned i) const {
|
||||
return product_value(m_monomials[i]);
|
||||
std::ostream& core::print_terms(std::ostream& out) const {
|
||||
for (auto t: m_lar_solver.m_terms)
|
||||
print_term(*t, out) << "\n";
|
||||
return out;
|
||||
}
|
||||
#endif
|
||||
std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
|
||||
return lp::print_linear_combination_customized(
|
||||
t.coeffs_as_vector(),
|
||||
[this](lpvar j) {
|
||||
return is_monomial_var(j)? product_indices_str(m_emons[j].vars()) : (std::string("v") + lp::T_to_string(j));
|
||||
},
|
||||
out);
|
||||
}
|
||||
} // end of nla
|
||||
|
|
|
|||
|
|
@ -162,7 +162,9 @@ public:
|
|||
std::ostream & print_ineqs(const lemma& l, std::ostream & out) const;
|
||||
std::ostream & print_factorization(const factorization& f, std::ostream& out) const;
|
||||
template <typename T>
|
||||
std::ostream& print_product(const T & m, std::ostream& out) const;
|
||||
std::ostream& print_product(const T & m, std::ostream& out) const;
|
||||
template <typename T>
|
||||
std::string product_indices_str(const T & m) const;
|
||||
std::ostream & print_factor(const factor& f, std::ostream& out) const;
|
||||
std::ostream & print_factor_with_vars(const factor& f, std::ostream& out) const;
|
||||
std::ostream& print_monomial(const monomial& m, std::ostream& out) const;
|
||||
|
|
@ -341,6 +343,8 @@ public:
|
|||
|
||||
lbool test_check(vector<lemma>& l);
|
||||
lpvar map_to_root(lpvar) const;
|
||||
std::ostream& print_terms(std::ostream&) const;
|
||||
std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
|
||||
}; // end of core
|
||||
|
||||
struct pp_mon {
|
||||
|
|
@ -349,14 +353,14 @@ struct pp_mon {
|
|||
pp_mon(core const& c, monomial const& m): c(c), m(m) {}
|
||||
pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
|
||||
};
|
||||
struct pp_rmon {
|
||||
struct pp_mon_with_vars {
|
||||
core const& c;
|
||||
monomial const& m;
|
||||
pp_rmon(core const& c, monomial const& m): c(c), m(m) {}
|
||||
pp_rmon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
|
||||
pp_mon_with_vars(core const& c, monomial const& m): c(c), m(m) {}
|
||||
pp_mon_with_vars(core const& c, lpvar v): c(c), m(c.emons()[v]) {}
|
||||
};
|
||||
inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); }
|
||||
inline std::ostream& operator<<(std::ostream& out, pp_rmon const& p) { return p.c.print_monomial_with_vars(p.m, out); }
|
||||
inline std::ostream& operator<<(std::ostream& out, pp_mon_with_vars const& p) { return p.c.print_monomial_with_vars(p.m, out); }
|
||||
|
||||
struct pp_fac {
|
||||
core const& c;
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ void order::order_lemma_on_monomial(const monomial& m) {
|
|||
// a > b && c > 0 => ac > bc,
|
||||
// with either variable of ac playing the role of c
|
||||
void order::order_lemma_on_binomial(const monomial& ac) {
|
||||
TRACE("nla_solver", tout << pp_rmon(c(), ac););
|
||||
TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac););
|
||||
SASSERT(!check_monomial(ac) && ac.size() == 2);
|
||||
const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]);
|
||||
const rational acv = val(ac);
|
||||
|
|
@ -101,13 +101,13 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
|
|||
|
||||
// We look for monomials e = m.rvars()[k]*d and see if we can create an order lemma for m and e
|
||||
void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
|
||||
TRACE("nla_solver", tout << "ac = " << pp_rmon(c(), ac););
|
||||
TRACE("nla_solver", tout << "ac = " << pp_mon_with_vars(c(), ac););
|
||||
SASSERT(ac.size() == 2);
|
||||
lpvar c = ac.vars()[k];
|
||||
|
||||
for (monomial const& bd : _().m_emons.get_products_of(c)) {
|
||||
if (bd.var() == ac.var()) continue;
|
||||
TRACE("nla_solver", tout << "bd = " << pp_rmon(_(), bd););
|
||||
TRACE("nla_solver", tout << "bd = " << pp_mon_with_vars(_(), bd););
|
||||
order_lemma_on_factor_binomial_rm(ac, k, bd);
|
||||
if (done()) {
|
||||
break;
|
||||
|
|
@ -119,9 +119,9 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
|
|||
// create order lemma on monomials bd where d is equivalent to ac[k]
|
||||
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
|
||||
TRACE("nla_solver",
|
||||
tout << "ac=" << pp_rmon(_(), ac) << "\n";
|
||||
tout << "ac=" << pp_mon_with_vars(_(), ac) << "\n";
|
||||
tout << "k=" << k << "\n";
|
||||
tout << "bd=" << pp_rmon(_(), bd) << "\n";
|
||||
tout << "bd=" << pp_mon_with_vars(_(), bd) << "\n";
|
||||
);
|
||||
factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
|
||||
factor b(false);
|
||||
|
|
@ -204,8 +204,8 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
|
|||
bool k,
|
||||
const monomial& rm_bd) {
|
||||
TRACE("nla_solver",
|
||||
tout << "rm_ac = " << pp_rmon(_(), rm_ac) << "\n";
|
||||
tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n";
|
||||
tout << "rm_ac = " << pp_mon_with_vars(_(), rm_ac) << "\n";
|
||||
tout << "rm_bd = " << pp_mon_with_vars(_(), rm_bd) << "\n";
|
||||
tout << "ac_f[k] = ";
|
||||
c().print_factor_with_vars(ac_f[k], tout););
|
||||
factor b(false);
|
||||
|
|
|
|||
|
|
@ -47,11 +47,6 @@ void solver::push(){
|
|||
void solver::pop(unsigned n) {
|
||||
m_core->pop(n);
|
||||
}
|
||||
|
||||
std::ostream& solver::display(std::ostream& out) {
|
||||
return m_core->print_monomials(out);
|
||||
}
|
||||
|
||||
|
||||
solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)) {
|
||||
}
|
||||
|
|
|
|||
|
|
@ -43,7 +43,6 @@ public:
|
|||
void pop(unsigned scopes);
|
||||
bool need_check();
|
||||
lbool check(vector<lemma>&);
|
||||
std::ostream& display(std::ostream& out);
|
||||
bool is_monomial_var(lpvar) const;
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue