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

reverting signed mon_eq, try to rely on canonization state during add/pop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-19 17:14:59 -07:00 committed by Lev Nachmanson
parent 6877840342
commit 8a665e25ed
12 changed files with 110 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/math/lp/emonics.cpp
View file

@ -53,12 +53,15 @@ void emonics::pop(unsigned n) {
for (unsigned j = 0; j < n; ++j) { for (unsigned j = 0; j < n; ++j) {
unsigned old_sz = m_lim[m_lim.size() - 1]; unsigned old_sz = m_lim[m_lim.size() - 1];
for (unsigned i = m_monics.size(); i-- > old_sz; ) { for (unsigned i = m_monics.size(); i-- > old_sz; ) {
m_ve.pop(1);
monic & m = m_monics[i]; monic & m = m_monics[i];
TRACE("nla_solver_mons", display(tout << m << "\n");); TRACE("nla_solver_mons", display(tout << m << "\n"););
remove_cg_mon(m); remove_cg_mon(m);
m_var2index[m.var()] = UINT_MAX; m_var2index[m.var()] = UINT_MAX;
do_canonize(m);
// variables in vs are in the same state as they were when add was called
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
for (lpvar v : m.vars()) { for (lpvar v : m.rvars()) {
if (v != last_var) { if (v != last_var) {
remove_cell(m_use_lists[v]); remove_cell(m_use_lists[v]);
last_var = v; last_var = v;
@ -168,7 +171,7 @@ monic const* emonics::find_canonical(svector<lpvar> const& vars) const {
void emonics::remove_cg(lpvar v) { void emonics::remove_cg(lpvar v) {
TRACE("nla_solver_mons", tout << "remove: " << v << "\n";); TRACE("nla_solver_mons", tout << "remove: " << v << "\n";);
TRACE("nla_solver_mons", display(tout);); // TRACE("nla_solver_mons", display(tout););
cell* c = m_use_lists[v].m_head; cell* c = m_use_lists[v].m_head;
if (c == nullptr) { if (c == nullptr) {
return; return;
@ -233,7 +236,7 @@ void emonics::insert_cg(lpvar v) {
} }
} }
while (c != first); while (c != first);
TRACE("nla_solver_mons", display(tout << "insert: " << v << "\n");); TRACE("nla_solver_mons", tout << "insert: " << v << "\n";);
} }
bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const { bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const {
@ -248,6 +251,7 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
} }
} }
for (auto const & m : m_monics) { for (auto const & m : m_monics) {
// bail out of invariant check
SASSERT(is_canonized(m)); SASSERT(is_canonized(m));
if (!is_canonical_monic(m.var())) if (!is_canonical_monic(m.var()))
continue; continue;
@ -279,7 +283,7 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
void emonics::insert_cg_mon(monic & m) { void emonics::insert_cg_mon(monic & m) {
do_canonize(m); do_canonize(m);
lpvar v = m.var(), w; lpvar v = m.var(), w;
TRACE("nla_solver_mons", tout << m << " hash: " << m_cg_hash(v) << "\n";); TRACE("nla_solver_mons", tout << m << "\n";); // hash: " << m_cg_hash(v) << "\n";);
auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector()); auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector());
auto& vec = entry->get_data().m_value; auto& vec = entry->get_data().m_value;
if (vec.empty()) { if (vec.empty()) {
@ -323,21 +327,14 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
SASSERT(!is_monic_var(v)); SASSERT(!is_monic_var(v));
m_ve.push(); m_ve.push();
unsigned idx = m_monics.size(); unsigned idx = m_monics.size();
bool sign = false; m_monics.push_back(monic(v, sz, vs, idx));
m_vs.reset(); do_canonize(m_monics.back());
for (unsigned i = 0; i < sz; ++i) {
signed_var sv = m_ve.find(vs[i]);
m_vs.push_back(sv.var());
sign ^= sv.sign();
}
m_monics.push_back(monic(sign, v, sz, m_vs.c_ptr(), idx));
// variables in the new monic are sorted, // variables in m_vs are canonical and sorted,
// so use last_var to skip duplicates, // so use last_var to skip duplicates,
// while updating use-lists // while updating use-lists
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
for (lpvar w : m_monics[idx].vars()) { for (lpvar w : m_monics.back().rvars()) {
SASSERT(w == m_ve.find(w).var());
if (w != last_var) { if (w != last_var) {
m_use_lists.reserve(w + 1); m_use_lists.reserve(w + 1);
insert_cell(m_use_lists[w], idx); insert_cell(m_use_lists[w], idx);
@ -347,6 +344,7 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
m_var2index.setx(v, idx, UINT_MAX); m_var2index.setx(v, idx, UINT_MAX);
insert_cg_mon(m_monics[idx]); insert_cg_mon(m_monics[idx]);
SASSERT(invariant()); SASSERT(invariant());
m_ve.push();
} }
void emonics::do_canonize(monic & m) const { void emonics::do_canonize(monic & m) const {
@ -363,6 +361,12 @@ bool emonics::is_canonized(const monic & m) const {
return mm.rvars() == m.rvars(); return mm.rvars() == m.rvars();
} }
void emonics::ensure_canonized() {
for (auto & m : m_monics) {
do_canonize(m);
}
}
bool emonics::monics_are_canonized() const { bool emonics::monics_are_canonized() const {
for (auto & m: m_monics) { for (auto & m: m_monics) {
if (!is_canonized(m)) { if (!is_canonized(m)) {
@ -372,7 +376,6 @@ bool emonics::monics_are_canonized() const {
return true; return true;
} }
bool emonics::canonize_divides(monic& m, monic & n) const { bool emonics::canonize_divides(monic& m, monic & n) const {
if (m.size() > n.size()) return false; if (m.size() > n.size()) return false;
unsigned ms = m.size(), ns = n.size(); unsigned ms = m.size(), ns = n.size();
@ -398,7 +401,9 @@ bool emonics::canonize_divides(monic& m, monic & n) const {
// yes, assume that monics are non-empty. // yes, assume that monics are non-empty.
emonics::pf_iterator::pf_iterator(emonics const& m, monic & mon, bool at_end): emonics::pf_iterator::pf_iterator(emonics const& m, monic & mon, bool at_end):
m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) { m_em(m), m_mon(&mon),
m_it(iterator(m, m.head(mon.vars()[0]), at_end)),
m_end(iterator(m, m.head(mon.vars()[0]), true)) {
fast_forward(); fast_forward();
} }
@ -425,7 +430,7 @@ void emonics::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v
} }
void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged if (m_ve.find(~r1) == m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been merged
TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";); TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";);
m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
TRACE("nla_solver_mons", tout << "rehashing " << r1.var() << "\n";); TRACE("nla_solver_mons", tout << "rehashing " << r1.var() << "\n";);
@ -435,7 +440,7 @@ void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed
} }
void emonics::unmerge_eh(signed_var r2, signed_var r1) { void emonics::unmerge_eh(signed_var r2, signed_var r1) {
if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged if (m_ve.find(~r1) != m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been unmerged
TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";); TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";);
unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
rehash_cg(r1.var()); rehash_cg(r1.var());

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

@ -93,7 +93,6 @@ class emonics {
mutable svector<head_tail> m_use_lists; // use list of monics where variables occur. mutable svector<head_tail> m_use_lists; // use list of monics where variables occur.
hash_canonical m_cg_hash; hash_canonical m_cg_hash;
eq_canonical m_cg_eq; eq_canonical m_cg_eq;
unsigned_vector m_vs; // temporary buffer of canonized variables
map<lpvar, unsigned_vector, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table. map<lpvar, unsigned_vector, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
@ -167,7 +166,8 @@ public:
monic & operator[](lpvar v) { return m_monics[m_var2index[v]]; } monic & operator[](lpvar v) { return m_monics[m_var2index[v]]; }
bool is_canonized(const monic&) const; bool is_canonized(const monic&) const;
bool monics_are_canonized() const; bool monics_are_canonized() const;
void ensure_canonized();
/** /**
\brief obtain the representative canonized monic \brief obtain the representative canonized monic
*/ */

1
src/math/lp/factorization.h
View file

@ -73,7 +73,6 @@ public:
void push_back(factor const& v) { m_factors.push_back(v); } void push_back(factor const& v) { m_factors.push_back(v); }
const monic& mon() const { return *m_mon; } const monic& mon() const { return *m_mon; }
void set_mon(const monic* m) { m_mon = m; } void set_mon(const monic* m) { m_mon = m; }
}; };
struct const_iterator_mon { struct const_iterator_mon {

42
src/math/lp/monic.h
View file

@ -2,45 +2,45 @@
Copyright (c) 2017 Microsoft Corporation Copyright (c) 2017 Microsoft Corporation
Author: Nikolaj Bjorner Author: Nikolaj Bjorner
Lev Nachmanson Lev Nachmanson
A mon_eq represents a definition m_v = v1*v2*...*vn,
where m_vs = [v1, v2, .., vn]
A monic contains a mon_eq and variables in canonized form.
*/ */
#pragma once #pragma once
#include "math/lp/lp_settings.h" #include "math/lp/lp_settings.h"
#include "util/vector.h" #include "util/vector.h"
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
#include "math/lp/nla_defs.h" #include "math/lp/nla_defs.h"
namespace nla { namespace nla {
/*
* represents definition m_v = v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn]
*/
class mon_eq { class mon_eq {
// fields // fields
bool m_sign;
lp::var_index m_v; lp::var_index m_v;
svector<lp::var_index> m_vs; svector<lp::var_index> m_vs;
public: public:
// constructors // constructors
mon_eq(bool sign, lp::var_index v, unsigned sz, lp::var_index const* vs): mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_sign(sign), m_v(v), m_vs(sz, vs) { m_v(v), m_vs(sz, vs) {
std::sort(m_vs.begin(), m_vs.end()); std::sort(m_vs.begin(), m_vs.end());
} }
mon_eq(bool sign, lp::var_index v, const svector<lp::var_index> &vs): mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
m_sign(sign), m_v(v), m_vs(vs) { m_v(v), m_vs(vs) {
std::sort(m_vs.begin(), m_vs.end()); std::sort(m_vs.begin(), m_vs.end());
} }
mon_eq():m_sign(false), m_v(UINT_MAX) {} mon_eq(): m_v(UINT_MAX) {}
unsigned var() const { return m_v; } unsigned var() const { return m_v; }
unsigned size() const { return m_vs.size(); } unsigned size() const { return m_vs.size(); }
bool sign() const { return m_sign; }
const svector<lp::var_index>& vars() const { return m_vs; } const svector<lp::var_index>& vars() const { return m_vs; }
bool empty() const { return m_vs.empty(); } bool empty() const { return m_vs.empty(); }
protected: protected:
svector<lp::var_index>& vars1() { return m_vs; } svector<lp::var_index>& vars1() { return m_vs; }
}; };
// support the congruence // support the congruence
@ -51,11 +51,10 @@ class monic: public mon_eq {
mutable unsigned m_visited; mutable unsigned m_visited;
public: public:
// constructors // constructors
monic(bool sign, lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):
monic(sign, v, svector<lpvar>(sz, vs), idx) { monic(v, svector<lpvar>(sz, vs), idx) {}
} monic(lpvar v, const svector<lpvar> &vs, unsigned idx):
monic(bool sign, lpvar v, const svector<lpvar> &vs, unsigned idx): mon_eq(v, vs), m_rsign(false), m_visited(0) {
mon_eq(sign, v, vs), m_rsign(false), m_visited(0) {
std::sort(vars1().begin(), vars1().end()); std::sort(vars1().begin(), vars1().end());
} }
@ -63,14 +62,15 @@ public:
void set_visited(unsigned v) { m_visited = v; } void set_visited(unsigned v) { m_visited = v; }
svector<lpvar> const& rvars() const { return m_rvars; } svector<lpvar> const& rvars() const { return m_rvars; }
bool rsign() const { return m_rsign; } bool rsign() const { return m_rsign; }
void reset_rfields() { m_rsign = sign(); m_rvars.reset(); SASSERT(m_rvars.size() == 0); } void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); } void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
}; };
inline std::ostream& operator<<(std::ostream& out, monic const& m) { inline std::ostream& operator<<(std::ostream& out, monic const& m) {
return out << m.var() << " := " << (m.sign()?"- ":"") << m.vars() << " r ( " << (m.rsign()?"- ":"") << m.rvars() << ")"; return out << m.var() << " := " << m.vars()
} << " r ( " << (m.rsign()?"- ":"") << m.rvars() << ")";
}
typedef std::unordered_map<lpvar, rational> variable_map_type; typedef std::unordered_map<lpvar, rational> variable_map_type;

26
src/math/lp/nla_basics_lemmas.cpp
View file

@ -28,7 +28,7 @@ basics::basics(core * c) : common(c) {}
// Generate a lemma if values of m.var() and n.var() are not the same up to sign // Generate a lemma if values of m.var() and n.var() are not the same up to sign
bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) { bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) {
const rational sign = sign_to_rat(m.rsign() ^ n.rsign()); const rational sign = sign_to_rat(m.rsign() ^ n.rsign());
if (val(m) == val(n) * sign) if (var_val(m) == var_val(n) * sign)
return false; return false;
TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";); TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";);
generate_sign_lemma(m, n, sign); generate_sign_lemma(m, n, sign);
@ -36,8 +36,8 @@ bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) {
} }
void basics::generate_zero_lemmas(const monic& m) { void basics::generate_zero_lemmas(const monic& m) {
SASSERT(!val(m).is_zero() && c().product_value(m).is_zero()); SASSERT(!var_val(m).is_zero() && c().product_value(m).is_zero());
int sign = nla::rat_sign(val(m)); int sign = nla::rat_sign(var_val(m));
unsigned_vector fixed_zeros; unsigned_vector fixed_zeros;
lpvar zero_j = find_best_zero(m, fixed_zeros); lpvar zero_j = find_best_zero(m, fixed_zeros);
SASSERT(is_set(zero_j)); SASSERT(is_set(zero_j));
@ -105,7 +105,7 @@ bool basics::basic_sign_lemma_model_based() {
unsigned sz = c().m_to_refine.size(); unsigned sz = c().m_to_refine.size();
for (unsigned i = sz; i-- > 0; ) { for (unsigned i = sz; i-- > 0; ) {
monic const& m = c().emons()[c().m_to_refine[(start + i) % sz]]; monic const& m = c().emons()[c().m_to_refine[(start + i) % sz]];
int mon_sign = nla::rat_sign(val(m)); int mon_sign = nla::rat_sign(var_val(m));
int product_sign = c().rat_sign(m); int product_sign = c().rat_sign(m);
if (mon_sign != product_sign) { if (mon_sign != product_sign) {
basic_sign_lemma_model_based_one_mon(m, product_sign); basic_sign_lemma_model_based_one_mon(m, product_sign);
@ -392,7 +392,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) { void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,
return; // or smaller than 1 return; // or smaller than 1
rational rmv = abs(val(rm)); rational rmv = abs(var_val(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization)); SASSERT(c().has_zero_factor(factorization));
return; return;
@ -409,7 +409,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization&
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) { bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) {
return false; return false;
rational rmv = abs(val(rm)); rational rmv = abs(var_val(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization)); SASSERT(c().has_zero_factor(factorization));
return false; return false;
@ -459,7 +459,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
} }
add_empty_lemma(); add_empty_lemma();
int fi = 0; int fi = 0;
rational mv = val(m); rational mv = var_val(m);
rational sm = rational(nla::rat_sign(mv)); rational sm = rational(nla::rat_sign(mv));
unsigned mon_var = var(m); unsigned mon_var = var(m);
c().mk_ineq(sm, mon_var, llc::LT); c().mk_ineq(sm, mon_var, llc::LT);
@ -505,7 +505,7 @@ bool basics::factorization_has_real(const factorization& f) const {
// here we use the fact xy = 0 -> x = 0 or y = 0 // here we use the fact xy = 0 -> x = 0 or y = 0
void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
SASSERT(val(rm).is_zero()&& ! c().rm_check(rm)); SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm));
add_empty_lemma(); add_empty_lemma();
if (!is_separated_from_zero(f)) { if (!is_separated_from_zero(f)) {
c().mk_ineq(var(rm), llc::NE); c().mk_ineq(var(rm), llc::NE);
@ -524,7 +524,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori
void basics::basic_lemma_for_mon_model_based(const monic& rm) { void basics::basic_lemma_for_mon_model_based(const monic& rm) {
TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";); TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
if (val(rm).is_zero()) { if (var_val(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) { for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty()) if (factorization.is_empty())
continue; continue;
@ -548,7 +548,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
TRACE("nla_solver_bl", c().print_monic(m, tout);); TRACE("nla_solver_bl", c().print_monic(m, tout););
lpvar mon_var = m.var(); lpvar mon_var = m.var();
const auto mv = val(mon_var); const auto mv = var_val(m);
const auto abs_mv = abs(mv); const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) { if (abs_mv == rational::zero()) {
return false; return false;
@ -619,7 +619,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
} }
if (not_one + 1) { // we found the only not_one if (not_one + 1) { // we found the only not_one
if (val(m) == val(not_one) * sign) { if (var_val(m) == val(not_one) * sign) {
TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;); TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
return false; return false;
} }
@ -740,13 +740,13 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
if (not_one + 1) { if (not_one + 1) {
// we found the only not_one // we found the only not_one
if (val(m) == val(not_one) * sign) { if (var_val(m) == val(not_one) * sign) {
TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;); TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;);
return false; return false;
} }
} else { } else {
// we have +-ones only in the factorization // we have +-ones only in the factorization
if (val(m) == sign) { if (var_val(m) == sign) {
return false; return false;
} }
} }

4
src/math/lp/nla_common.cpp
View file

@ -33,9 +33,11 @@ template void common::explain<factorization>(const factorization& t);
void common::explain(lpvar j) { c().explain(j, c().current_expl()); } void common::explain(lpvar j) { c().explain(j, c().current_expl()); }
template <typename T> rational common::val(T const& t) const { return c().val(t); } template <typename T> rational common::val(T const& t) const { return c().val(t); }
template rational common::val<monic>(monic const& t) const;
template rational common::val<factor>(factor const& t) const; template rational common::val<factor>(factor const& t) const;
rational common::val(lpvar t) const { return c().val(t); } rational common::val(lpvar t) const { return c().val(t); }
rational common::var_val(monic const& m) const { return c().var_val(m); }
rational common::mul_val(monic const& m) const { return c().mul_val(m); }
template <typename T> lpvar common::var(T const& t) const { return c().var(t); } template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
template lpvar common::var<factor>(factor const& t) const; template lpvar common::var<factor>(factor const& t) const;
template lpvar common::var<monic>(monic const& t) const; template lpvar common::var<monic>(monic const& t) const;

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

@ -57,6 +57,8 @@ struct common {
template <typename T> rational val(T const& t) const; template <typename T> rational val(T const& t) const;
rational val(lpvar) const; rational val(lpvar) const;
rational var_val(monic const& m) const; // value obtained from variable representing monomial
rational mul_val(monic const& m) const; // value obtained from multiplying variables of monomial
template <typename T> lpvar var(T const& t) const; template <typename T> lpvar var(T const& t) const;
bool done() const; bool done() const;
template <typename T> void explain(const T&); template <typename T> void explain(const T&);

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

@ -101,7 +101,7 @@ bool core::canonize_sign(lpvar j) const {
} }
bool core::canonize_sign_is_correct(const monic& m) const { bool core::canonize_sign_is_correct(const monic& m) const {
bool r = m.sign(); bool r = false;
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
r ^= canonize_sign(j); r ^= canonize_sign(j);
} }
@ -145,7 +145,7 @@ void core::pop(unsigned n) {
} }
rational core::product_value(const monic& m) const { rational core::product_value(const monic& m) const {
rational r(m.sign() ? -1 : 1); rational r(1);
for (auto j : m.vars()) { for (auto j : m.vars()) {
r *= m_lar_solver.get_column_value_rational(j); r *= m_lar_solver.get_column_value_rational(j);
} }
@ -609,7 +609,7 @@ int core::rat_sign(const monic& m) const {
// Returns true if the monic sign is incorrect // Returns true if the monic sign is incorrect
bool core::sign_contradiction(const monic& m) const { bool core::sign_contradiction(const monic& m) const {
return nla::rat_sign(val(m)) != rat_sign(m); return nla::rat_sign(var_val(m)) != rat_sign(m);
} }
/* /*
@ -741,7 +741,7 @@ void core::trace_print_monic_and_factorization(const monic& rm, const factorizat
out << "\n"; out << "\n";
out << "mon: " << pp_mon(*this, rm.var()) << "\n"; out << "mon: " << pp_mon(*this, rm.var()) << "\n";
out << "value: " << val(rm) << "\n"; out << "value: " << var_val(rm) << "\n";
print_factorization(f, out << "fact: ") << "\n"; print_factorization(f, out << "fact: ") << "\n";
} }
@ -842,6 +842,7 @@ void core::collect_equivs() {
add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
} }
} }
m_emons.ensure_canonized();
} }
@ -1177,7 +1178,7 @@ bool core::find_bfc_to_refine_on_monic(const monic& m, factorization & bf) {
if (f.size() == 2) { if (f.size() == 2) {
auto a = f[0]; auto a = f[0];
auto b = f[1]; auto b = f[1];
if (val(m) != val(a) * val(b)) { if (var_val(m) != val(a) * val(b)) {
bf = f; bf = f;
TRACE("nla_solver", tout << "found bf"; TRACE("nla_solver", tout << "found bf";
tout << ":m:" << pp_mon_with_vars(*this, m) << "\n"; tout << ":m:" << pp_mon_with_vars(*this, m) << "\n";
@ -1208,7 +1209,7 @@ bool core::find_bfc_to_refine(const monic* & m, factorization & bf){
if (find_bfc_to_refine_on_monic(*m, bf)) { if (find_bfc_to_refine_on_monic(*m, bf)) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "bf = "; print_factorization(bf, tout); tout << "bf = "; print_factorization(bf, tout);
tout << "\nval(*m) = " << val(*m) << ", should be = (val(bf[0])=" << val(bf[0]) << ")*(val(bf[1]) = " << val(bf[1]) << ") = " << val(bf[0])*val(bf[1]) << "\n";); tout << "\nval(*m) = " << var_val(*m) << ", should be = (val(bf[0])=" << val(bf[0]) << ")*(val(bf[1]) = " << val(bf[1]) << ") = " << val(bf[0])*val(bf[1]) << "\n";);
return true; return true;
} }
} }

10
src/math/lp/nla_core.h
View file

@ -128,7 +128,13 @@ public:
bool is_monic_var(lpvar j) const { return m_emons.is_monic_var(j); } bool is_monic_var(lpvar j) const { return m_emons.is_monic_var(j); }
rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); } rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
rational val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); } rational var_val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
rational mul_val(const monic& m) const {
rational r(1);
for (lpvar v : m.vars()) r *= m_lar_solver.get_column_value_rational(v);
return r;
}
bool canonize_sign_is_correct(const monic& m) const; bool canonize_sign_is_correct(const monic& m) const;
@ -136,7 +142,7 @@ public:
rational val_rooted(const monic& m) const { return m.rsign()*val(m.var()); } rational val_rooted(const monic& m) const { return m.rsign()*val(m.var()); }
rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); } rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : var_val(m_emons[f.var()])); }
rational val(const factorization&) const; rational val(const factorization&) const;

2
src/math/lp/nla_monotone_lemmas.cpp
View file

@ -82,7 +82,7 @@ void monotone::monotonicity_lemma(monic const& m) {
if (c().mon_has_zero(m.vars())) if (c().mon_has_zero(m.vars()))
return; return;
const rational prod_val = abs(c().product_value(m)); const rational prod_val = abs(c().product_value(m));
const rational m_val = abs(val(m)); const rational m_val = abs(var_val(m));
if (m_val < prod_val) if (m_val < prod_val)
monotonicity_lemma_lt(m, prod_val); monotonicity_lemma_lt(m, prod_val);
else if (m_val > prod_val) else if (m_val > prod_val)

52
src/math/lp/nla_order_lemmas.cpp
View file

@ -68,8 +68,8 @@ void order::order_lemma_on_monic(const monic& m) {
void order::order_lemma_on_binomial(const monic& ac) { void order::order_lemma_on_binomial(const monic& ac) {
TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac);); TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac););
SASSERT(!check_monic(ac) && ac.size() == 2); SASSERT(!check_monic(ac) && ac.size() == 2);
const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]); const rational mult_val = mul_val(ac);
const rational acv = val(ac); const rational acv = var_val(ac);
bool gt = acv > mult_val; bool gt = acv > mult_val;
bool k = false; bool k = false;
do { do {
@ -138,11 +138,11 @@ void order::order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic&
tout << "ac = " << pp_mon(_(), ac) << "a = " << pp_var(_(), a) << "c = " << pp_var(_(), c) << "\nbd = " << pp_mon(_(), bd) << "b = " << pp_fac(_(), b) << "d = " << pp_var(_(), d) << "\n"; tout << "ac = " << pp_mon(_(), ac) << "a = " << pp_var(_(), a) << "c = " << pp_var(_(), c) << "\nbd = " << pp_mon(_(), bd) << "b = " << pp_fac(_(), b) << "d = " << pp_var(_(), d) << "\n";
); );
SASSERT(_().m_evars.find(c).var() == d); SASSERT(_().m_evars.find(c).var() == d);
rational acv = val(ac); rational acv = var_val(ac);
rational av = val(a); rational av = val(a);
rational c_sign = rrat_sign(val(c)); rational c_sign = rrat_sign(val(c));
rational d_sign = rrat_sign(val(d)); rational d_sign = rrat_sign(val(d));
rational bdv = val(bd); rational bdv = var_val(bd);
rational bv = val(b); rational bv = val(b);
// Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign // Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign; auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
@ -171,16 +171,9 @@ void order::generate_mon_ol(const monic& ac,
const rational& d_sign, const rational& d_sign,
lpvar d, lpvar d,
llc ab_cmp) { llc ab_cmp) {
SASSERT( SASSERT(ab_cmp == llc::LT || ab_cmp == llc::GT);
(ab_cmp == llc::LT || ab_cmp == llc::GT) && SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
( SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
(ab_cmp != llc::LT ||
(val(ac) >= val(bd) && val(a)*c_sign < val(b)*d_sign))
||
(ab_cmp != llc::GT ||
(val(ac) <= val(bd) && val(a)*c_sign > val(b)*d_sign))
)
);
add_empty_lemma(); add_empty_lemma();
mk_ineq(c_sign, c, llc::LE); mk_ineq(c_sign, c, llc::LE);
@ -224,10 +217,10 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
sign ^= _().canonize_sign(f); sign ^= _().canonize_sign(f);
const rational rsign = sign_to_rat(sign); const rational rsign = sign_to_rat(sign);
const rational fv = val(var(ab[0])) * val(var(ab[1])); const rational fv = val(var(ab[0])) * val(var(ab[1]));
const rational mv = rsign * val(m); const rational mv = rsign * var_val(m);
TRACE("nla_solver", TRACE("nla_solver",
tout << "ab.size()=" << ab.size() << "\n"; tout << "ab.size()=" << ab.size() << "\n";
tout << "we should have sign*val(m):" << mv << "=(" << rsign << ")*(" << val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";); tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";);
if (mv == fv) if (mv == fv)
return; return;
bool gt = mv > fv; bool gt = mv > fv;
@ -263,7 +256,7 @@ bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac,
} }
// |c_sign| = 1, and c*c_sign > 0 // |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign // ac > bc && ac/|c| > bc/|c| => a*c_sign > b*c_sign
void order::generate_ol(const monic& ac, void order::generate_ol(const monic& ac,
const factor& a, const factor& a,
int c_sign, int c_sign,
@ -271,11 +264,22 @@ void order::generate_ol(const monic& ac,
const monic& bc, const monic& bc,
const factor& b, const factor& b,
llc ab_cmp) { llc ab_cmp) {
add_empty_lemma();
rational rc_sign = rational(c_sign); rational rc_sign = rational(c_sign);
mk_ineq(rc_sign * sign_to_rat(canonize_sign(c)), var(c), llc::LE); rational sign_a = rc_sign * sign_to_rat(canonize_sign(a));
rational sign_b = rc_sign * sign_to_rat(canonize_sign(b));
rational sign_c = rc_sign * sign_to_rat(canonize_sign(c));
add_empty_lemma();
#if 0
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
<< " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n"
<< " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n"
<< " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n");
#endif
mk_ineq(sign_c, var(c), llc::LE);
mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp); mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
mk_ineq(sign_to_rat(canonize_sign(a))*rc_sign, var(a), - sign_to_rat(canonize_sign(b))*rc_sign, var(b), negate(ab_cmp)); mk_ineq(sign_a, var(a), - sign_b, var(b), negate(ab_cmp));
explain(ac); explain(ac);
explain(a); explain(a);
explain(bc); explain(bc);
@ -294,8 +298,8 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
SASSERT(c_sign != 0); SASSERT(c_sign != 0);
auto av_c_s = val(a)*rational(c_sign); auto av_c_s = val(a)*rational(c_sign);
auto bv_c_s = val(b)*rational(c_sign); auto bv_c_s = val(b)*rational(c_sign);
auto acv = val(ac); auto acv = var_val(ac);
auto bcv = val(bc); auto bcv = var_val(bc);
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout);); TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
// Suppose ac >= bc, then ac/|c| >= bc/|c|. // Suppose ac >= bc, then ac/|c| >= bc/|c|.
// Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s // Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s
@ -314,7 +318,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0 a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0
*/ */
void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) { void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * val(m) > val(a) * val(b)); SASSERT(sign * var_val(m) > val(a) * val(b));
add_empty_lemma(); add_empty_lemma();
if (val(a).is_pos()) { if (val(a).is_pos()) {
TRACE("nla_solver", tout << "a is pos\n";); TRACE("nla_solver", tout << "a is pos\n";);
@ -344,7 +348,7 @@ void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a,
void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b) { void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b) {
TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) << TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) <<
", b = "; c().print_var(b, tout) << "\n";); ", b = "; c().print_var(b, tout) << "\n";);
SASSERT(sign * val(m) < val(a) * val(b)); SASSERT(sign * var_val(m) < val(a) * val(b));
add_empty_lemma(); add_empty_lemma();
if (val(a).is_pos()) { if (val(a).is_pos()) {
//negate a > 0 //negate a > 0

2
src/math/lp/nra_solver.cpp
View file

@ -38,7 +38,7 @@ typedef nla::variable_map_type variable_map_type;
} }
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) { void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
m_monics.push_back(mon_eq(false, v, sz, vs)); m_monics.push_back(mon_eq(v, sz, vs));
} }
void push() { void push() {