From a0bdb8135d99a6ead3d7c215752d688eaffc68e7 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 17 Sep 2019 14:31:09 -0700
Subject: [PATCH] rename monomial to monic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/emonomials.cpp | 128 ++++++++--------
src/math/lp/emonomials.h | 170 +++++++++++-----------
src/math/lp/factorization.cpp | 12 +-
src/math/lp/factorization.h | 22 +--
src/math/lp/factorization_factory_imp.cpp | 8 +-
src/math/lp/factorization_factory_imp.h | 10 +-
src/math/lp/horner.cpp | 14 +-
src/math/lp/int_solver.cpp | 2 +-
src/math/lp/mon_eq.cpp | 2 +-
src/math/lp/{monomial.h => monic.h} | 8 +-
src/math/lp/nla_basics_lemmas.cpp | 100 ++++++-------
src/math/lp/nla_basics_lemmas.h | 60 ++++----
src/math/lp/nla_common.cpp | 16 +-
src/math/lp/nla_common.h | 12 +-
src/math/lp/nla_core.cpp | 108 +++++++-------
src/math/lp/nla_core.h | 86 +++++------
src/math/lp/nla_defs.h | 4 +-
src/math/lp/nla_grobner.cpp | 8 +-
src/math/lp/nla_grobner.h | 2 +
src/math/lp/nla_monotone_lemmas.cpp | 12 +-
src/math/lp/nla_monotone_lemmas.h | 12 +-
src/math/lp/nla_order_lemmas.cpp | 58 ++++----
src/math/lp/nla_order_lemmas.h | 38 ++---
src/math/lp/nla_solver.cpp | 10 +-
src/math/lp/nla_solver.h | 6 +-
src/math/lp/nla_tangent_lemmas.cpp | 6 +-
src/math/lp/nla_tangent_lemmas.h | 6 +-
src/math/lp/nra_solver.cpp | 30 ++--
src/math/lp/nra_solver.h | 2 +-
src/smt/theory_lra.cpp | 8 +-
30 files changed, 481 insertions(+), 479 deletions(-)
rename src/math/lp/{monomial.h => monic.h} (86%)
diff --git a/src/math/lp/emonomials.cpp b/src/math/lp/emonomials.cpp
index 57c8659f1..81351c9ed 100644
--- a/src/math/lp/emonomials.cpp
+++ b/src/math/lp/emonomials.cpp
@@ -26,29 +26,29 @@
namespace nla {
-void emonomials::inc_visited() const {
+void emonics::inc_visited() const {
++m_visited;
if (m_visited == 0) {
- for (auto& svt : m_monomials) {
+ for (auto& svt : m_monics) {
svt.visited() = 0;
}
++m_visited;
}
}
-void emonomials::push() {
+void emonics::push() {
m_u_f_stack.push_scope();
- m_lim.push_back(m_monomials.size());
+ m_lim.push_back(m_monics.size());
m_region.push_scope();
m_ve.push();
- SASSERT(monomials_are_canonized());
+ SASSERT(monics_are_canonized());
}
-void emonomials::pop(unsigned n) {
+void emonics::pop(unsigned n) {
m_ve.pop(n);
unsigned old_sz = m_lim[m_lim.size() - n];
- for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
- monomial & m = m_monomials[i];
+ for (unsigned i = m_monics.size(); i-- > old_sz; ) {
+ monic & m = m_monics[i];
remove_cg_mon(m);
m_var2index[m.var()] = UINT_MAX;
lpvar last_var = UINT_MAX;
@@ -59,15 +59,15 @@ void emonomials::pop(unsigned n) {
}
}
}
- m_monomials.shrink(old_sz);
- m_monomials.shrink(old_sz);
+ m_monics.shrink(old_sz);
+ m_monics.shrink(old_sz);
m_region.pop_scope(n);
m_lim.shrink(m_lim.size() - n);
- SASSERT(monomials_are_canonized());
+ SASSERT(monics_are_canonized());
m_u_f_stack.pop_scope(n);
}
-void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
+void emonics::remove_cell(head_tail& v, unsigned mIndex) {
cell*& cur_head = v.m_head;
cell*& cur_tail = v.m_tail;
cell* old_head = cur_head->m_next;
@@ -81,7 +81,7 @@ void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
}
}
-void emonomials::insert_cell(head_tail& v, unsigned mIndex) {
+void emonics::insert_cell(head_tail& v, unsigned mIndex) {
cell*& cur_head = v.m_head;
cell*& cur_tail = v.m_tail;
cell* new_head = new (m_region) cell(mIndex, cur_head);
@@ -90,7 +90,7 @@ void emonomials::insert_cell(head_tail& v, unsigned mIndex) {
cur_tail->m_next = new_head;
}
-void emonomials::merge_cells(head_tail& root, head_tail& other) {
+void emonics::merge_cells(head_tail& root, head_tail& other) {
if (&root == &other) return;
cell*& root_head = root.m_head;
cell*& root_tail = root.m_tail;
@@ -111,7 +111,7 @@ void emonomials::merge_cells(head_tail& root, head_tail& other) {
}
}
-void emonomials::unmerge_cells(head_tail& root, head_tail& other) {
+void emonics::unmerge_cells(head_tail& root, head_tail& other) {
if (&root == &other) return;
cell*& root_head = root.m_head;
cell*& root_tail = root.m_tail;
@@ -131,26 +131,26 @@ void emonomials::unmerge_cells(head_tail& root, head_tail& other) {
}
}
-emonomials::cell* emonomials::head(lpvar v) const {
+emonics::cell* emonics::head(lpvar v) const {
v = m_ve.find(v).var();
m_use_lists.reserve(v + 1);
return m_use_lists[v].m_head;
}
-monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
+monic const* emonics::find_canonical(svector<lpvar> const& vars) const {
SASSERT(m_ve.is_root(vars));
m_find_key = vars;
std::sort(m_find_key.begin(), m_find_key.end());
- monomial const* result = nullptr;
+ monic const* result = nullptr;
lpvar w;
if (m_cg_table.find(UINT_MAX, w)) {
- result = &m_monomials[m_var2index[w]];
+ result = &m_monics[m_var2index[w]];
}
return result;
}
-void emonomials::remove_cg(lpvar v) {
+void emonics::remove_cg(lpvar v) {
cell* c = m_use_lists[v].m_head;
if (c == nullptr) {
return;
@@ -160,7 +160,7 @@ void emonomials::remove_cg(lpvar v) {
do {
unsigned idx = c->m_index;
c = c->m_next;
- monomial & m = m_monomials[idx];
+ monic & m = m_monics[idx];
if (!is_visited(m)) {
set_visited(m);
remove_cg_mon(m);
@@ -169,7 +169,7 @@ void emonomials::remove_cg(lpvar v) {
while (c != first);
}
-void emonomials::remove_cg_mon(const monomial& m) {
+void emonics::remove_cg_mon(const monic& m) {
lpvar u = m.var(), w;
// equivalence class of u:
if (m_cg_table.find(u, w)) {
@@ -179,13 +179,13 @@ void emonomials::remove_cg_mon(const monomial& m) {
}
/**
- \brief insert canonized monomials using v into a congruence table.
- Prior to insertion, the monomials are canonized according to the current
- variable equivalences. The canonized monomials (monomial) are considered
+ \brief insert canonized monics using v into a congruence table.
+ Prior to insertion, the monics are canonized according to the current
+ variable equivalences. The canonized monics (monic) are considered
in the same equivalence class if they have the same set of representative
variables. Their signs may differ.
*/
-void emonomials::insert_cg(lpvar v) {
+void emonics::insert_cg(lpvar v) {
cell* c = m_use_lists[v].m_head;
if (c == nullptr) {
@@ -197,7 +197,7 @@ void emonomials::insert_cg(lpvar v) {
do {
unsigned idx = c->m_index;
c = c->m_next;
- monomial & m = m_monomials[idx];
+ monic & m = m_monics[idx];
if (!is_visited(m)) {
set_visited(m);
insert_cg_mon(m);
@@ -206,8 +206,8 @@ void emonomials::insert_cg(lpvar v) {
while (c != first);
}
-bool emonomials::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const {
- for (auto const & m : m_monomials) {
+bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const {
+ for (auto const & m : m_monics) {
auto it = lists.find(m.rvars());
if (it == lists.end()) {
std::unordered_set<lpvar> v;
@@ -217,12 +217,12 @@ bool emonomials::elists_are_consistent(std::unordered_map<unsigned_vector, std::
it->second.insert(m.var());
}
}
- for (auto const & m : m_monomials) {
+ for (auto const & m : m_monics) {
SASSERT(is_canonized(m));
- if (!is_canonical_monomial(m.var()))
+ if (!is_canonical_monic(m.var()))
continue;
std::unordered_set<lpvar> c;
- for (const monomial& e : enum_sign_equiv_monomials(m))
+ for (const monic& e : enum_sign_equiv_monics(m))
c.insert(e.var());
auto it = lists.find(m.rvars());
@@ -244,7 +244,7 @@ bool emonomials::elists_are_consistent(std::unordered_map<unsigned_vector, std::
}
-void emonomials::insert_cg_mon(monomial & m) {
+void emonics::insert_cg_mon(monic & m) {
do_canonize(m);
lpvar v = m.var(), w;
if (m_cg_table.find(v, w)) {
@@ -266,25 +266,25 @@ void emonomials::insert_cg_mon(monomial & m) {
}
}
-void emonomials::set_visited(monomial& m) const {
- m_monomials[m_var2index[m.var()]].visited() = m_visited;
+void emonics::set_visited(monic& m) const {
+ m_monics[m_var2index[m.var()]].visited() = m_visited;
}
-bool emonomials::is_visited(monomial const& m) const {
- return m_visited == m_monomials[m_var2index[m.var()]].visited();
+bool emonics::is_visited(monic const& m) const {
+ return m_visited == m_monics[m_var2index[m.var()]].visited();
}
/**
- \brief insert a new monomial.
+ \brief insert a new monic.
Assume that the variables are canonical, that is, not equal in current
- context to another variable. The monomial is inserted into a congruence
- class of equal up-to var_eqs monomials.
+ context to another variable. The monic is inserted into a congruence
+ class of equal up-to var_eqs monics.
*/
-void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
+void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
TRACE("nla_solver_mons", tout << "v = " << v << "\n";);
- unsigned idx = m_monomials.size();
- m_monomials.push_back(monomial(v, sz, vs, idx));
+ unsigned idx = m_monics.size();
+ m_monics.push_back(monic(v, sz, vs, idx));
lpvar last_var = UINT_MAX;
for (unsigned i = 0; i < sz; ++i) {
lpvar w = vs[i];
@@ -297,10 +297,10 @@ void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
}
SASSERT(m_ve.is_root(v));
m_var2index.setx(v, idx, UINT_MAX);
- insert_cg_mon(m_monomials[idx]);
+ insert_cg_mon(m_monics[idx]);
}
-void emonomials::do_canonize(monomial & m) const {
+void emonics::do_canonize(monic & m) const {
m.reset_rfields();
for (lpvar v : m.vars()) {
m.push_rvar(m_ve.find(v));
@@ -308,14 +308,14 @@ void emonomials::do_canonize(monomial & m) const {
m.sort_rvars();
}
-bool emonomials::is_canonized(const monomial & m) const {
- monomial mm(m);
+bool emonics::is_canonized(const monic & m) const {
+ monic mm(m);
do_canonize(mm);
return mm.rvars() == m.rvars();
}
-bool emonomials:: monomials_are_canonized() const {
- for (auto & m: m_monomials) {
+bool emonics:: monics_are_canonized() const {
+ for (auto & m: m_monics) {
if (! is_canonized(m)) {
return false;
}
@@ -324,7 +324,7 @@ bool emonomials:: monomials_are_canonized() const {
}
-bool emonomials::canonize_divides(monomial& m, monomial & n) const {
+bool emonics::canonize_divides(monic& m, monic & n) const {
if (m.size() > n.size()) return false;
unsigned ms = m.size(), ns = n.size();
unsigned i = 0, j = 0;
@@ -347,18 +347,18 @@ bool emonomials::canonize_divides(monomial& m, monomial & n) const {
}
}
-// yes, assume that monomials are non-empty.
-emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end):
+// yes, assume that monics are non-empty.
+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)) {
fast_forward();
}
-emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end):
+emonics::pf_iterator::pf_iterator(emonics const& m, lpvar v, bool at_end):
m_em(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) {
fast_forward();
}
-void emonomials::pf_iterator::fast_forward() {
+void emonics::pf_iterator::fast_forward() {
for (; m_it != m_end; ++m_it) {
if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) {
m_em.set_visited(*m_it);
@@ -371,11 +371,11 @@ void emonomials::pf_iterator::fast_forward() {
}
}
-void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
+void emonics::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
// no-op
}
-void emonomials::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) {
TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";);
if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged
m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
@@ -385,7 +385,7 @@ void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, sig
}
}
-void emonomials::unmerge_eh(signed_var r2, signed_var r1) {
+void emonics::unmerge_eh(signed_var r2, signed_var r1) {
TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";);
if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged
unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
@@ -393,25 +393,25 @@ void emonomials::unmerge_eh(signed_var r2, signed_var r1) {
}
}
-std::ostream& emonomials::display(const core& cr, std::ostream& out) const {
- out << "monomials\n";
+std::ostream& emonics::display(const core& cr, std::ostream& out) const {
+ out << "monics\n";
unsigned idx = 0;
- for (auto const& m : m_monomials) {
+ for (auto const& m : m_monics) {
out << "m" << (idx++) << ": " << pp_mon_with_vars(cr, m) << "\n";
}
return display_use(out);
}
-std::ostream& emonomials::display(std::ostream& out) const {
- out << "monomials\n";
+std::ostream& emonics::display(std::ostream& out) const {
+ out << "monics\n";
unsigned idx = 0;
- for (auto const& m : m_monomials) {
+ for (auto const& m : m_monics) {
out << "m" << (idx++) << ": " << m << "\n";
}
return display_use(out);
}
- std::ostream& emonomials::display_use(std::ostream& out) const {
+ std::ostream& emonics::display_use(std::ostream& out) const {
out << "use lists\n";
unsigned idx = 0;
for (auto const& ht : m_use_lists) {
diff --git a/src/math/lp/emonomials.h b/src/math/lp/emonomials.h
index bbbbf4e0c..04feab465 100644
--- a/src/math/lp/emonomials.h
+++ b/src/math/lp/emonomials.h
@@ -22,7 +22,7 @@
#pragma once
#include "math/lp/lp_utils.h"
#include "math/lp/var_eqs.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "util/region.h"
namespace nla {
@@ -35,9 +35,9 @@ struct hash_svector {
class core;
-class emonomials {
+class emonics {
/**
- \brief singly-lined cyclic list of monomial indices where variable occurs.
+ \brief singly-lined cyclic list of monic indices where variable occurs.
Each variable points to the head and tail of the cyclic list.
Initially, head and tail are nullptr.
New elements are inserted in the beginning of the list.
@@ -55,11 +55,11 @@ class emonomials {
cell* m_tail;
};
struct hash_canonical {
- emonomials& em;
- hash_canonical(emonomials& em): em(em) {}
+ emonics& em;
+ hash_canonical(emonics& em): em(em) {}
unsigned operator()(lpvar v) const {
- auto const& vec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars() : em.m_find_key;
+ auto const& vec = v != UINT_MAX? em.m_monics[em.m_var2index[v]].rvars() : em.m_find_key;
return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
}
};
@@ -67,29 +67,29 @@ class emonomials {
/**
- \brief private fields used by emonomials for maintaining state of canonized monomials.
+ \brief private fields used by emonics for maintaining state of canonized monics.
*/
struct eq_canonical {
- emonomials& em;
- eq_canonical(emonomials& em): em(em) {}
+ emonics& em;
+ eq_canonical(emonics& em): em(em) {}
bool operator()(lpvar u, lpvar v) const {
- auto const& uvec = u != UINT_MAX? em.m_monomials[em.m_var2index[u]].rvars(): em.m_find_key;
- auto const& vvec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars(): em.m_find_key;
+ auto const& uvec = u != UINT_MAX? em.m_monics[em.m_var2index[u]].rvars(): em.m_find_key;
+ auto const& vvec = v != UINT_MAX? em.m_monics[em.m_var2index[v]].rvars(): em.m_find_key;
return uvec == vvec;
}
};
- union_find<emonomials> m_u_f;
- trail_stack<emonomials> m_u_f_stack;
- mutable svector<lpvar> m_find_key; // the key used when looking for a monomial with the specific variables
- var_eqs<emonomials>& m_ve;
- mutable vector<monomial> m_monomials; // set of monomials
+ union_find<emonics> m_u_f;
+ trail_stack<emonics> m_u_f_stack;
+ mutable svector<lpvar> m_find_key; // the key used when looking for a monic with the specific variables
+ var_eqs<emonics>& m_ve;
+ mutable vector<monic> m_monics; // set of monics
mutable unsigned_vector m_var2index; // var_mIndex -> mIndex
unsigned_vector m_lim; // backtracking point
- mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator
+ mutable unsigned m_visited; // timestamp of visited monics during pf_iterator
region m_region; // region for allocating linked lists
- mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur.
+ mutable svector<head_tail> m_use_lists; // use list of monics where variables occur.
hash_canonical m_cg_hash;
eq_canonical m_cg_eq;
hashtable<lpvar, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
@@ -104,23 +104,23 @@ class emonomials {
void remove_cg(lpvar v);
void insert_cg(lpvar v);
- void insert_cg_mon(monomial & m);
- void remove_cg_mon(const monomial & m);
+ void insert_cg_mon(monic & m);
+ void remove_cg_mon(const monic & m);
void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
- void do_canonize(monomial& m) const;
+ void do_canonize(monic& m) const;
cell* head(lpvar v) const;
- void set_visited(monomial& m) const;
- bool is_visited(monomial const& m) const;
+ void set_visited(monic& m) const;
+ bool is_visited(monic const& m) const;
std::ostream& display_use(std::ostream& out) const;
public:
- unsigned number_of_monomials() const { return m_monomials.size(); }
+ unsigned number_of_monics() const { return m_monics.size(); }
/**
- \brief emonomials builds on top of var_eqs.
- push and pop on emonomials calls push/pop on var_eqs, so no
+ \brief emonics builds on top of var_eqs.
+ push and pop on emonics calls push/pop on var_eqs, so no
other calls to push/pop to the var_eqs should take place.
*/
- emonomials(var_eqs<emonomials>& ve):
+ emonics(var_eqs<emonics>& ve):
m_u_f(*this),
m_u_f_stack(*this),
m_ve(ve),
@@ -139,7 +139,7 @@ public:
void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
// this method is required by union_find
- trail_stack<emonomials> & get_trail_stack() { return m_u_f_stack; }
+ trail_stack<emonics> & get_trail_stack() { return m_u_f_stack; }
/**
\brief push/pop scopes.
@@ -150,7 +150,7 @@ public:
void pop(unsigned n);
/**
- \brief create a monomial from an equality v := vs
+ \brief create a monic from an equality v := vs
*/
void add(lpvar v, unsigned sz, lpvar const* vs);
void add(lpvar v, svector<lpvar> const& vs) { add(v, vs.size(), vs.c_ptr()); }
@@ -158,44 +158,44 @@ public:
void add(lpvar v, lpvar x, lpvar y, lpvar z) { lpvar vs[3] = { x, y, z }; add(v, 3, vs); }
/**
- \brief retrieve monomial corresponding to variable v from definition v := vs
+ \brief retrieve monic corresponding to variable v from definition v := vs
*/
- monomial const& operator[](lpvar v) const { return m_monomials[m_var2index[v]]; }
- monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; }
- bool is_canonized(const monomial&) const;
- bool monomials_are_canonized() const;
+ monic const& operator[](lpvar v) const { return m_monics[m_var2index[v]]; }
+ monic & operator[](lpvar v) { return m_monics[m_var2index[v]]; }
+ bool is_canonized(const monic&) const;
+ bool monics_are_canonized() const;
/**
- \brief obtain the representative canonized monomial
+ \brief obtain the representative canonized monic
*/
- monomial const& rep(monomial const& sv) const {
+ monic const& rep(monic const& sv) const {
unsigned j = -1;
m_cg_table.find(sv.var(), j);
- return m_monomials[m_var2index[j]];
+ return m_monics[m_var2index[j]];
}
/**
\brief determine if m1 divides m2 over the canonization obtained from merged variables.
*/
- bool canonize_divides(monomial & m1, monomial& m2) const;
+ bool canonize_divides(monic & m1, monic& m2) const;
/**
- \brief iterator over monomials that are declared.
+ \brief iterator over monics that are declared.
*/
- vector<monomial>::const_iterator begin() const { return m_monomials.begin(); }
- vector<monomial>::const_iterator end() const { return m_monomials.end(); }
+ vector<monic>::const_iterator begin() const { return m_monics.begin(); }
+ vector<monic>::const_iterator end() const { return m_monics.end(); }
/**
- \brief iterators over monomials where a variable is used
+ \brief iterators over monics where a variable is used
*/
class iterator {
- emonomials const& m;
+ emonics const& m;
cell* m_cell;
bool m_touched;
public:
- iterator(emonomials const& m, cell* c, bool at_end): m(m), m_cell(c), m_touched(at_end || c == nullptr) {}
- monomial & operator*() { return m.m_monomials[m_cell->m_index]; }
+ iterator(emonics const& m, cell* c, bool at_end): m(m), m_cell(c), m_touched(at_end || c == nullptr) {}
+ monic & operator*() { return m.m_monics[m_cell->m_index]; }
iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_cell == other.m_cell && m_touched == other.m_touched; }
@@ -203,11 +203,11 @@ public:
};
class use_list {
- emonomials const& m;
+ emonics const& m;
lpvar m_var;
cell* head() { return m.head(m_var); }
public:
- use_list(emonomials const& m, lpvar v): m(m), m_var(v) {}
+ use_list(emonics const& m, lpvar v): m(m), m_var(v) {}
iterator begin() { return iterator(m, head(), false); }
iterator end() { return iterator(m, head(), true); }
};
@@ -215,19 +215,19 @@ public:
use_list get_use_list(lpvar v) const { return use_list(*this, v); }
/**
- \brief retrieve monomials m' where m is a proper factor of modulo current equalities.
+ \brief retrieve monics m' where m is a proper factor of modulo current equalities.
*/
class pf_iterator {
- emonomials const& m_em;
- monomial * m_mon; // monomial
+ emonics const& m_em;
+ monic * m_mon;
iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that do not have m as a factor
iterator m_end;
void fast_forward();
public:
- pf_iterator(emonomials const& m, monomial& mon, bool at_end);
- pf_iterator(emonomials const& m, lpvar v, bool at_end);
- monomial & operator*() {
+ pf_iterator(emonics const& m, monic& mon, bool at_end);
+ pf_iterator(emonics const& m, lpvar v, bool at_end);
+ monic & operator*() {
return *m_it;
}
pf_iterator& operator++() { ++m_it; fast_forward(); return *this; }
@@ -237,77 +237,77 @@ public:
};
class products_of {
- emonomials const& m;
- monomial * mon;
+ emonics const& m;
+ monic * mon;
lpvar m_var;
public:
- products_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {}
- products_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {}
+ products_of(emonics const& m, monic & mon): m(m), mon(&mon), m_var(UINT_MAX) {}
+ products_of(emonics const& m, lpvar v): m(m), mon(nullptr), m_var(v) {}
pf_iterator begin() { if (mon) return pf_iterator(m, *mon, false); return pf_iterator(m, m_var, false); }
pf_iterator end() { if (mon) return pf_iterator(m, *mon, true); return pf_iterator(m, m_var, true); }
};
- products_of get_products_of(monomial& m) const { inc_visited(); return products_of(*this, m); }
+ products_of get_products_of(monic& m) const { inc_visited(); return products_of(*this, m); }
products_of get_products_of(lpvar v) const { inc_visited(); return products_of(*this, v); }
- monomial const* find_canonical(svector<lpvar> const& vars) const;
- bool is_canonical_monomial(lpvar j) const {
- SASSERT(is_monomial_var(j));
+ monic const* find_canonical(svector<lpvar> const& vars) const;
+ bool is_canonical_monic(lpvar j) const {
+ SASSERT(is_monic_var(j));
unsigned idx = m_var2index[j];
if (idx >= m_u_f.get_num_vars())
return true;
return m_u_f.find(idx) == idx;
}
/**
- \brief iterator over sign equivalent monomials.
- These are monomials that are equivalent modulo m_var_eqs amd modulo signs.
+ \brief iterator over sign equivalent monics.
+ These are monics that are equivalent modulo m_var_eqs amd modulo signs.
*/
- class sign_equiv_monomials_it {
- emonomials const& m;
+ class sign_equiv_monics_it {
+ emonics const& m;
unsigned m_index;
bool m_touched;
public:
- sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end):
+ sign_equiv_monics_it(emonics const& m, unsigned idx, bool at_end):
m(m), m_index(idx), m_touched(at_end) {}
- monomial const& operator*() { return m.m_monomials[m_index]; }
+ monic const& operator*() { return m.m_monics[m_index]; }
- sign_equiv_monomials_it& operator++() {
+ sign_equiv_monics_it& operator++() {
m_touched = true;
if (m_index < m.m_u_f.get_num_vars())
m_index = m.m_u_f.next(m_index);
return *this;
}
- sign_equiv_monomials_it operator++(int) {
- sign_equiv_monomials_it tmp = *this;
+ sign_equiv_monics_it operator++(int) {
+ sign_equiv_monics_it tmp = *this;
++*this;
return tmp;
}
- bool operator==(sign_equiv_monomials_it const& other) const {
+ bool operator==(sign_equiv_monics_it const& other) const {
return m_index == other.m_index && m_touched == other.m_touched;
}
- bool operator!=(sign_equiv_monomials_it const& other) const {
+ bool operator!=(sign_equiv_monics_it const& other) const {
return m_index != other.m_index || m_touched != other.m_touched;
}
};
- class sign_equiv_monomials {
- const emonomials& em;
- monomial const& m;
+ class sign_equiv_monics {
+ const emonics& em;
+ monic const& m;
unsigned index() const { return em.m_var2index[m.var()]; }
public:
- sign_equiv_monomials(const emonomials & em, monomial const& m): em(em), m(m) {}
- sign_equiv_monomials_it begin() { return sign_equiv_monomials_it(em, index(), false); }
- sign_equiv_monomials_it end() { return sign_equiv_monomials_it(em, index(), true); }
+ sign_equiv_monics(const emonics & em, monic const& m): em(em), m(m) {}
+ sign_equiv_monics_it begin() { return sign_equiv_monics_it(em, index(), false); }
+ sign_equiv_monics_it end() { return sign_equiv_monics_it(em, index(), true); }
};
- sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) const { return sign_equiv_monomials(*this, m); }
- sign_equiv_monomials enum_sign_equiv_monomials(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
+ sign_equiv_monics enum_sign_equiv_monics(monic const& m) const { return sign_equiv_monics(*this, m); }
+ sign_equiv_monics enum_sign_equiv_monics(lpvar v) { return enum_sign_equiv_monics((*this)[v]); }
/**
- \brief display state of emonomials
+ \brief display state of emonics
*/
std::ostream& display(const core&, std::ostream& out) const;
std::ostream& display(std::ostream& out) const;
@@ -323,16 +323,16 @@ public:
void unmerge_eh(signed_var r2, signed_var r1);
- bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
+ bool is_monic_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const;
-}; // end of emonomials
+}; // end of emonics
struct pp_emons {
const core& m_c;
- const emonomials& m_em;
- pp_emons(const core& c, const emonomials& e): m_c(c), m_em(e) {}
+ const emonics& m_em;
+ pp_emons(const core& c, const emonics& e): m_c(c), m_em(e) {}
inline std::ostream& display(std::ostream& out) const {
return m_em.display(m_c, out);
}
diff --git a/src/math/lp/factorization.cpp b/src/math/lp/factorization.cpp
index 7f51c2f50..f74663f06 100644
--- a/src/math/lp/factorization.cpp
+++ b/src/math/lp/factorization.cpp
@@ -27,7 +27,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
k.set(k_vars[0], factor_type::VAR);
} else {
unsigned i;
- if (!m_ff->find_canonical_monomial_of_vars(k_vars, i)) {
+ if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) {
return false;
}
k.set(i, factor_type::MON);
@@ -37,7 +37,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
j.set(j_vars[0], factor_type::VAR);
} else {
unsigned i;
- if (!m_ff->find_canonical_monomial_of_vars(j_vars, i)) {
+ if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) {
return false;
}
j.set(i, factor_type::MON);
@@ -47,7 +47,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
factorization const_iterator_mon::operator*() const {
if (m_full_factorization_returned == false) {
- return create_full_factorization(m_ff->m_monomial);
+ return create_full_factorization(m_ff->m_monic);
}
factor j, k; rational sign;
if (!get_factors(j, k, sign))
@@ -93,17 +93,17 @@ factorization const_iterator_mon::create_binary_factorization(factor j, factor k
factorization f(nullptr);
f.push_back(j);
f.push_back(k);
- // Let m by *m_ff->m_monomial, the monomial we factorize
+ // Let m by *m_ff->m_monic, the monic we factorize
// We have canonize_sign(m)*m.vars() = m.rvars()
// Let s = canonize_sign(f). Then we have f[0]*f[1] = s*m.rvars()
// s*canonize_sign(m)*val(m).
// Therefore val(m) = sign*val((f[0])*val(f[1]), where sign = canonize_sign(f)*canonize_sign(m).
// We apply this sign to the first factor.
- f[0].sign() ^= (m_ff->canonize_sign(f)^m_ff->canonize_sign(*m_ff->m_monomial));
+ f[0].sign() ^= (m_ff->canonize_sign(f)^m_ff->canonize_sign(*m_ff->m_monic));
return f;
}
-factorization const_iterator_mon::create_full_factorization(const monomial* m) const {
+factorization const_iterator_mon::create_full_factorization(const monic* m) const {
if (m != nullptr)
return factorization(m);
factorization f(nullptr);
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index 9e3981fe4..f566307b1 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -20,7 +20,7 @@
--*/
#pragma once
#include "util/rational.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/nla_defs.h"
namespace nla {
@@ -55,9 +55,9 @@ public:
class factorization {
svector<factor> m_factors;
- const monomial* m_mon;
+ const monic* m_mon;
public:
- factorization(const monomial* m): m_mon(m) {
+ factorization(const monic* m): m_mon(m) {
if (m != nullptr) {
for (lpvar j : m->vars())
m_factors.push_back(factor(j, factor_type::VAR));
@@ -75,8 +75,8 @@ public:
void push_back(factor const& v) {
m_factors.push_back(v);
}
- const monomial& mon() const { return *m_mon; }
- void set_mon(const monomial* m) { m_mon = m; }
+ const monic& mon() const { return *m_mon; }
+ void set_mon(const monic* m) { m_mon = m; }
};
@@ -109,19 +109,19 @@ struct const_iterator_mon {
factorization create_binary_factorization(factor j, factor k) const;
- factorization create_full_factorization(const monomial*) const;
+ factorization create_full_factorization(const monic*) const;
};
struct factorization_factory {
const svector<lpvar>& m_vars;
- const monomial* m_monomial;
+ const monic* m_monic;
// returns true if found
- virtual bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
- virtual bool canonize_sign(const monomial& m) const = 0;
+ virtual bool find_canonical_monic_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
+ virtual bool canonize_sign(const monic& m) const = 0;
virtual bool canonize_sign(const factorization& m) const = 0;
- factorization_factory(const svector<lpvar>& vars, const monomial* m) :
- m_vars(vars), m_monomial(m) {
+ factorization_factory(const svector<lpvar>& vars, const monic* m) :
+ m_vars(vars), m_monic(m) {
}
svector<bool> get_mask() const {
diff --git a/src/math/lp/factorization_factory_imp.cpp b/src/math/lp/factorization_factory_imp.cpp
index bbfca829c..ace85a050 100644
--- a/src/math/lp/factorization_factory_imp.cpp
+++ b/src/math/lp/factorization_factory_imp.cpp
@@ -21,14 +21,14 @@
#include "math/lp/nla_core.h"
namespace nla {
-factorization_factory_imp::factorization_factory_imp(const monomial& rm, const core& s) :
+factorization_factory_imp::factorization_factory_imp(const monic& rm, const core& s) :
factorization_factory(rm.rvars(), &s.emons()[rm.var()]),
m_core(s), m_mon(s.emons()[rm.var()]), m_rm(rm) { }
-bool factorization_factory_imp::find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
- return m_core.find_canonical_monomial_of_vars(vars, i);
+bool factorization_factory_imp::find_canonical_monic_of_vars(const svector<lpvar>& vars, unsigned & i) const {
+ return m_core.find_canonical_monic_of_vars(vars, i);
}
-bool factorization_factory_imp::canonize_sign(const monomial& m) const {
+bool factorization_factory_imp::canonize_sign(const monic& m) const {
return m_core.canonize_sign(m);
}
bool factorization_factory_imp::canonize_sign(const factorization& f) const {
diff --git a/src/math/lp/factorization_factory_imp.h b/src/math/lp/factorization_factory_imp.h
index b24c2bfe7..b404d5f14 100644
--- a/src/math/lp/factorization_factory_imp.h
+++ b/src/math/lp/factorization_factory_imp.h
@@ -24,12 +24,12 @@ namespace nla {
struct factorization_factory_imp: factorization_factory {
const core& m_core;
- const monomial & m_mon;
- const monomial& m_rm;
+ const monic & m_mon;
+ const monic& m_rm;
- factorization_factory_imp(const monomial& rm, const core& s);
- bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
- virtual bool canonize_sign(const monomial& m) const;
+ factorization_factory_imp(const monic& rm, const core& s);
+ bool find_canonical_monic_of_vars(const svector<lpvar>& vars, unsigned & i) const;
+ virtual bool canonize_sign(const monic& m) const;
virtual bool canonize_sign(const factorization& m) const;
};
}
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 49d1e14b4..7c3c22830 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -48,7 +48,7 @@ bool horner::row_is_interesting(const T& row) const {
c().clear_row_var_set();
for (const auto& p : row) {
lpvar j = p.var();
- if (!c().is_monomial_var(j))
+ if (!c().is_monic_var(j))
continue;
auto & m = c().emons()[j];
@@ -133,26 +133,26 @@ void horner::horner_lemmas() {
nex * horner::nexvar(lpvar j, cross_nested& cn) const {
// todo: consider deepen the recursion
- if (!c().is_monomial_var(j))
+ if (!c().is_monic_var(j))
return cn.mk_var(j);
- const monomial& m = c().emons()[j];
+ const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul();
for (lpvar k : m.vars()) {
e->add_child(cn.mk_var(k));
- CTRACE("nla_horner", c().is_monomial_var(k), c().print_var(k, tout) << "\n";);
+ CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
}
return e;
}
nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const {
// todo: consider deepen the recursion
- if (!c().is_monomial_var(j))
+ if (!c().is_monic_var(j))
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
- const monomial& m = c().emons()[j];
+ const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
for (lpvar k : m.vars()) {
e->add_child(cn.mk_var(k));
- CTRACE("nla_horner", c().is_monomial_var(k), c().print_var(k, tout) << "\n";);
+ CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
}
return e;
}
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 77bb9aae9..e17f84a9c 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -7,7 +7,7 @@
#include "math/lp/lar_solver.h"
#include "math/lp/lp_utils.h"
#include <utility>
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/gomory.h"
namespace lp {
diff --git a/src/math/lp/mon_eq.cpp b/src/math/lp/mon_eq.cpp
index 355a493c0..6163231b0 100644
--- a/src/math/lp/mon_eq.cpp
+++ b/src/math/lp/mon_eq.cpp
@@ -3,7 +3,7 @@
Author: Nikolaj Bjorner
*/
#include "math/lp/lar_solver.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
namespace nla {
template <typename T>
diff --git a/src/math/lp/monomial.h b/src/math/lp/monic.h
similarity index 86%
rename from src/math/lp/monomial.h
rename to src/math/lp/monic.h
index a6ce6b28a..b600a71c9 100644
--- a/src/math/lp/monomial.h
+++ b/src/math/lp/monic.h
@@ -39,16 +39,16 @@ public:
};
// support the congruence
-class monomial: public mon_eq {
+class monic: public mon_eq {
// fields
svector<lpvar> m_rvars;
bool m_rsign;
mutable unsigned m_visited;
public:
// constructors
- monomial(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monomial(v, svector<lpvar>(sz, vs), idx) {
+ monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monic(v, svector<lpvar>(sz, vs), idx) {
}
- monomial(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_visited(0) {
+ monic(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_visited(0) {
std::sort(vars().begin(), vars().end());
}
@@ -63,7 +63,7 @@ public:
}
};
- inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
+ inline std::ostream& operator<<(std::ostream& out, monic const& m) {
return out << m.var() << " := " << m.vars() << " r ( " << sign_to_rat(m.rsign()) << " * " << m.rvars() << ")";
}
diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 64804f3cb..b2dc03616 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -26,7 +26,7 @@ basics::basics(core * c) : common(c) {}
// Monomials m and n vars have the same values, 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_monomials(const monomial& m, const monomial& 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());
if (val(m) == val(n) * sign)
return false;
@@ -35,7 +35,7 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
return true;
}
-void basics::generate_zero_lemmas(const monomial& m) {
+void basics::generate_zero_lemmas(const monic& m) {
SASSERT(!val(m).is_zero() && c().product_value(m.vars()).is_zero());
int sign = nla::rat_sign(val(m));
unsigned_vector fixed_zeros;
@@ -86,7 +86,7 @@ void basics::get_non_strict_sign(lpvar j, int& sign) const {
}
-void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
+void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_sign) {
if (product_sign == 0) {
TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; );
generate_zero_lemmas(m);
@@ -104,7 +104,7 @@ bool basics::basic_sign_lemma_model_based() {
unsigned start = c().random();
unsigned sz = c().m_to_refine.size();
for (unsigned i = sz; i-- > 0; ) {
- monomial 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 product_sign = c().rat_sign(m);
if (mon_sign != product_sign) {
@@ -121,7 +121,7 @@ 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().emons()[v];
+ const monic& 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);
@@ -129,10 +129,10 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
);
SASSERT(c().emons().is_canonized(m_v));
- for (auto const& m : c().emons().enum_sign_equiv_monomials(v)) {
+ for (auto const& m : c().emons().enum_sign_equiv_monics(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())
+ if (m_v.var() != m.var() && basic_sign_lemma_on_two_monics(m_v, m) && done())
return true;
}
@@ -155,9 +155,9 @@ bool basics::basic_sign_lemma(bool derived) {
}
return false;
}
-// the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign
+// the value of the i-th monic has to be equal to the value of the k-th monic modulo sign
// but it is not the case in the model
-void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
+void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) {
add_empty_lemma();
TRACE("nla_solver",
tout << "m = " << pp_mon_with_vars(_(), m);
@@ -172,7 +172,7 @@ void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rat
}
// try to find a variable j such that val(j) = 0
// and the bounds on j contain 0 as an inner point
-lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
+lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) const {
lpvar zero_j = -1;
for (unsigned j : m.vars()){
if (val(j).is_zero()){
@@ -185,13 +185,13 @@ lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) c
}
return zero_j;
}
-void basics::add_trival_zero_lemma(lpvar zero_j, const monomial& m) {
+void basics::add_trival_zero_lemma(lpvar zero_j, const monic& m) {
add_empty_lemma();
c().mk_ineq(zero_j, llc::NE);
c().mk_ineq(m.var(), llc::EQ);
TRACE("nla_solver", c().print_lemma(tout););
}
-void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j, int sign_of_zj) {
+void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) {
TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";);
// we know all the signs
add_empty_lemma();
@@ -204,7 +204,7 @@ void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j,
negate_strict_sign(m.var());
TRACE("nla_solver", c().print_lemma(tout););
}
-void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
+void basics::add_fixed_zero_lemma(const monic& m, lpvar j) {
add_empty_lemma();
c().explain_fixed_var(j);
c().mk_ineq(m.var(), llc::EQ);
@@ -229,11 +229,11 @@ void basics::negate_strict_sign(lpvar j) {
// here we use the fact
// xy = 0 -> x = 0 or y = 0
-bool basics::basic_lemma_for_mon_zero(const monomial& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) {
NOT_IMPLEMENTED_YET();
return true;
#if 0
- TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+ TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
add_empty_lemma();
c().explain_fixed_var(var(rm));
std::unordered_set<lpvar> processed;
@@ -258,23 +258,23 @@ bool basics::basic_lemma(bool derived) {
unsigned sz = mon_inds_to_ref.size();
for (unsigned j = 0; j < sz; ++j) {
lpvar v = mon_inds_to_ref[(j + start) % mon_inds_to_ref.size()];
- const monomial& r = c().emons()[v];
- SASSERT (!c().check_monomial(c().emons()[v]));
+ const monic& r = c().emons()[v];
+ SASSERT (!c().check_monic(c().emons()[v]));
basic_lemma_for_mon(r, derived);
}
return false;
}
// Use basic multiplication properties to create a lemma
-// for the given monomial.
+// for the given monic.
// "derived" means derived from constraints - the alternative is model based
-void basics::basic_lemma_for_mon(const monomial& rm, bool derived) {
+void basics::basic_lemma_for_mon(const monic& rm, bool derived) {
if (derived)
basic_lemma_for_mon_derived(rm);
else
basic_lemma_for_mon_model_based(rm);
}
-bool basics::basic_lemma_for_mon_derived(const monomial& rm) {
+bool basics::basic_lemma_for_mon_derived(const monic& rm) {
if (c().var_is_fixed_to_zero(var(rm))) {
for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty())
@@ -300,8 +300,8 @@ bool basics::basic_lemma_for_mon_derived(const monomial& rm) {
return false;
}
// x = 0 or y = 0 -> xy = 0
-bool basics::basic_lemma_for_mon_non_zero_derived(const monomial& rm, const factorization& f) {
- TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factorization& f) {
+ TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
if (! c().var_is_separated_from_zero(var(rm)))
return false;
int zero_j = -1;
@@ -324,11 +324,11 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monomial& rm, const fact
}
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
-bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& rm, const factorization& f) {
- TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm, const factorization& f) {
+ TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
lpvar mon_var = c().emons()[rm.var()].var();
- TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
+ TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto mv = val(mon_var);
const auto abs_mv = abs(mv);
@@ -383,13 +383,13 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
return true;
}
-bool basics::basic_lemma_for_mon_neutral_derived(const monomial& rm, const factorization& factorization) {
+bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factorization& factorization) {
return
- basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization);
+ basic_lemma_for_mon_neutral_monic_to_factor_derived(rm, factorization);
}
// x != 0 or y = 0 => |xy| >= |y|
-void basics::proportion_lemma_model_based(const monomial& rm, const factorization& factorization) {
+void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
rational rmv = abs(val(rm));
if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization));
@@ -405,7 +405,7 @@ void basics::proportion_lemma_model_based(const monomial& rm, const factorizatio
}
}
// x != 0 or y = 0 => |xy| >= |y|
-bool basics::proportion_lemma_derived(const monomial& rm, const factorization& factorization) {
+bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) {
return false;
rational rmv = abs(val(rm));
if (rmv.is_zero()) {
@@ -423,7 +423,7 @@ bool basics::proportion_lemma_derived(const monomial& rm, const factorization& f
return false;
}
// if there are no zero factors then |m| >= |m[factor_index]|
-void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
+void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) {
add_empty_lemma();
unsigned mon_var = m.var();
rational mv = val(mon_var);
@@ -446,11 +446,11 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
// none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm|
-void basics::generate_pl(const monomial& m, const factorization& fc, int factor_index) {
+void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) {
TRACE("nla_solver", tout << "factor_index = " << factor_index << ", m = "
<< pp_mon(c(), m);
tout << ", fc = "; c().print_factorization(fc, tout);
- tout << "orig mon = "; c().print_monomial(c().emons()[m.var()], tout););
+ tout << "orig mon = "; c().print_monic(c().emons()[m.var()], tout););
if (fc.is_mon()) {
generate_pl_on_mon(m, factor_index);
return;
@@ -492,8 +492,8 @@ bool basics::is_separated_from_zero(const factorization& f) const {
// here we use the fact xy = 0 -> x = 0 or y = 0
-void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const factorization& f) {
- TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
+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););
SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
add_empty_lemma();
if (!is_separated_from_zero(f)) {
@@ -511,7 +511,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
TRACE("nla_solver", c().print_lemma(tout););
}
-void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
+void basics::basic_lemma_for_mon_model_based(const monic& rm) {
TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
if (val(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) {
@@ -533,8 +533,8 @@ void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
-bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m) {
- TRACE("nla_solver_bl", c().print_monomial(m, tout););
+bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const monic& m) {
+ TRACE("nla_solver_bl", c().print_monic(m, tout););
lpvar mon_var = m.var();
const auto mv = val(mon_var);
@@ -586,10 +586,10 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
}
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m) {
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(const monic& m) {
lpvar not_one = -1;
rational sign(1);
- TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
+ TRACE("nla_solver_bl", tout << "m = "; c().print_monic(m, tout););
for (auto j : m.vars()){
auto v = val(j);
if (v == rational(1)) {
@@ -631,11 +631,11 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
-bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& rm, const factorization& f) {
- TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
+bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic& rm, const factorization& f) {
+ TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout););
lpvar mon_var = c().emons()[rm.var()].var();
- TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
+ TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto mv = val(mon_var);
const auto abs_mv = abs(mv);
@@ -689,19 +689,19 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
return true;
}
-void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_neutral_model_based(const monic& rm, const factorization& f) {
if (f.is_mon()) {
- basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(f.mon());
- basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(f.mon());
+ basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(f.mon());
+ basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(f.mon());
}
else {
- basic_lemma_for_mon_neutral_monomial_to_factor_model_based(rm, f);
- basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(rm, f);
+ basic_lemma_for_mon_neutral_monic_to_factor_model_based(rm, f);
+ basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(rm, f);
}
}
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& m, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& m, const factorization& f) {
rational sign = sign_to_rat(m.rsign());
SASSERT(m.rsign() == canonize_sign(f));
TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; );
@@ -784,8 +784,8 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
}
// x = 0 or y = 0 -> xy = 0
-void basics::basic_lemma_for_mon_non_zero_model_based(const monomial& rm, const factorization& f) {
- TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
+void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const factorization& f) {
+ TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout););
if (f.is_mon())
basic_lemma_for_mon_non_zero_model_based_mf(f);
else
diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h
index 1f4acf48c..4272b9a59 100644
--- a/src/math/lp/nla_basics_lemmas.h
+++ b/src/math/lp/nla_basics_lemmas.h
@@ -18,7 +18,7 @@
--*/
#pragma once
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/factorization.h"
#include "math/lp/nla_common.h"
@@ -27,9 +27,9 @@ namespace nla {
class core;
struct basics: common {
basics(core *core);
- bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n);
+ bool basic_sign_lemma_on_two_monics(const monic& m, const monic& n);
- void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign);
+ void basic_sign_lemma_model_based_one_mon(const monic& m, int product_sign);
bool basic_sign_lemma_model_based();
bool basic_sign_lemma_on_mon(unsigned i, std::unordered_set<unsigned> & explore);
@@ -39,69 +39,69 @@ struct basics: common {
-ab = a(-b)
*/
bool basic_sign_lemma(bool derived);
- bool basic_lemma_for_mon_zero(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_zero(const monic& rm, const factorization& f);
- void basic_lemma_for_mon_zero_model_based(const monomial& rm, const factorization& f);
+ void basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f);
- void basic_lemma_for_mon_non_zero_model_based(const monomial& rm, const factorization& f);
+ void basic_lemma_for_mon_non_zero_model_based(const monic& rm, const factorization& f);
// x = 0 or y = 0 -> xy = 0
- void basic_lemma_for_mon_non_zero_model_based_rm(const monomial& rm, const factorization& f);
+ void basic_lemma_for_mon_non_zero_model_based_rm(const monic& rm, const factorization& f);
void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f);
// x = 0 or y = 0 -> xy = 0
- bool basic_lemma_for_mon_non_zero_derived(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_non_zero_derived(const monic& rm, const factorization& f);
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
- bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic& rm, const factorization& f);
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
- bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m);
- bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const monic& m);
+ bool basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm, const factorization& f);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
- bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& rm, const factorization& f);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
- bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m);
+ bool basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(const monic& m);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
- bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const monomial& rm, const factorization& f);
- void basic_lemma_for_mon_neutral_model_based(const monomial& rm, const factorization& f);
+ bool basic_lemma_for_mon_neutral_from_factors_to_monic_derived(const monic& rm, const factorization& f);
+ void basic_lemma_for_mon_neutral_model_based(const monic& rm, const factorization& f);
- bool basic_lemma_for_mon_neutral_derived(const monomial& rm, const factorization& factorization);
+ bool basic_lemma_for_mon_neutral_derived(const monic& rm, const factorization& factorization);
- void basic_lemma_for_mon_model_based(const monomial& rm);
+ void basic_lemma_for_mon_model_based(const monic& rm);
- bool basic_lemma_for_mon_derived(const monomial& rm);
+ bool basic_lemma_for_mon_derived(const monic& rm);
// Use basic multiplication properties to create a lemma
- // for the given monomial.
+ // for the given monic.
// "derived" means derived from constraints - the alternative is model based
- void basic_lemma_for_mon(const monomial& rm, bool derived);
+ void basic_lemma_for_mon(const monic& rm, bool derived);
// use basic multiplication properties to create a lemma
bool basic_lemma(bool derived);
- void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign);
- void generate_zero_lemmas(const monomial& m);
- lpvar find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const;
+ void generate_sign_lemma(const monic& m, const monic& n, const rational& sign);
+ void generate_zero_lemmas(const monic& m);
+ lpvar find_best_zero(const monic& m, unsigned_vector & fixed_zeros) const;
bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const;
void get_non_strict_sign(lpvar j, int& sign) const;
- void add_trival_zero_lemma(lpvar zero_j, const monomial& m);
- void generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j, int sign_of_zj);
+ void add_trival_zero_lemma(lpvar zero_j, const monic& m);
+ void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj);
- void add_fixed_zero_lemma(const monomial& m, lpvar j);
+ void add_fixed_zero_lemma(const monic& m, lpvar j);
void negate_strict_sign(lpvar j);
// x != 0 or y = 0 => |xy| >= |y|
- void proportion_lemma_model_based(const monomial& rm, const factorization& factorization);
+ void proportion_lemma_model_based(const monic& rm, const factorization& factorization);
// x != 0 or y = 0 => |xy| >= |y|
- bool proportion_lemma_derived(const monomial& rm, const factorization& factorization);
+ bool proportion_lemma_derived(const monic& rm, const factorization& factorization);
// if there are no zero factors then |m| >= |m[factor_index]|
- void generate_pl_on_mon(const monomial& m, unsigned factor_index);
+ void generate_pl_on_mon(const monic& m, unsigned factor_index);
// none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm|
- void generate_pl(const monomial& rm, const factorization& fc, int factor_index);
+ void generate_pl(const monic& rm, const factorization& fc, int factor_index);
bool is_separated_from_zero(const factorization&) const;
};
}
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index 700003817..eacb83916 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -26,25 +26,25 @@ bool common::done() const { return c().done(); }
template <typename T> void common::explain(const T& t) {
c().explain(t, c().current_expl());
}
-template void common::explain<monomial>(const monomial& t);
+template void common::explain<monic>(const monic& t);
template void common::explain<factor>(const factor& t);
template void common::explain<factorization>(const factorization& t);
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 rational common::val<monomial>(monomial const& t) const;
+template rational common::val<monic>(monic const& t) const;
template rational common::val<factor>(factor const& t) const;
rational common::val(lpvar t) const { return c().val(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<monomial>(monomial const& t) const;
+template lpvar common::var<monic>(monic const& t) const;
void common::add_empty_lemma() { c().add_empty_lemma(); }
template <typename T> bool common::canonize_sign(const T& t) const {
return c().canonize_sign(t);
}
-template bool common::canonize_sign<monomial>(const monomial&) const;
+template bool common::canonize_sign<monic>(const monic&) const;
template bool common::canonize_sign<factor>(const factor&) const;
template bool common::canonize_sign<lpvar>(const lpvar&) const;
template bool common::canonize_sign<factorization>(const factorization&) const;
@@ -102,8 +102,8 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
template
std::ostream& common::print_product<unsigned_vector>(const unsigned_vector & m, std::ostream& out) const;
-std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
- return c().print_monomial(m, out);
+std::ostream& common::print_monic(const monic & m, std::ostream& out) const {
+ return c().print_monic(m, out);
}
std::ostream& common::print_factor(const factor & f, std::ostream& out) const {
@@ -114,8 +114,8 @@ std::ostream& common::print_var(lpvar j, std::ostream& out) const {
return c().print_var(j, out);
}
-bool common::check_monomial(const monomial& m) const {
- return c().check_monomial(m);
+bool common::check_monic(const monic& m) const {
+ return c().check_monic(m);
}
unsigned common::random() {
diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h
index 140746e4b..6d69ff170 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -21,7 +21,7 @@
#include "util/rational.h"
#include "math/lp/nla_defs.h"
#include "math/lp/lar_term.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/emonomials.h"
#include "math/lp/factorization.h"
namespace nla {
@@ -51,7 +51,7 @@ struct common {
template <typename T> rational val(T const& t) const;
rational val(lpvar) const;
- rational rval(const monomial&) const;
+ rational rval(const monic&) const;
template <typename T> lpvar var(T const& t) const;
bool done() const;
template <typename T> void explain(const T&);
@@ -87,10 +87,10 @@ struct common {
std::ostream& print_factor(const factor &, std::ostream& out) const;
std::ostream& print_var(lpvar, std::ostream& out) const;
- std::ostream& print_monomial(const monomial & m, std::ostream& out) const;
- std::ostream& print_rooted_monomial(const monomial &, std::ostream& out) const;
- std::ostream& print_rooted_monomial_with_vars(const monomial&, std::ostream& out) const;
- bool check_monomial(const monomial&) const;
+ std::ostream& print_monic(const monic & m, std::ostream& out) const;
+ std::ostream& print_rooted_monic(const monic &, std::ostream& out) const;
+ std::ostream& print_rooted_monic_with_vars(const monic&, std::ostream& out) const;
+ bool check_monic(const monic&) const;
unsigned random();
};
}
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index b80d1379c..5356a5a1b 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -104,7 +104,7 @@ bool core::canonize_sign(lpvar j) const {
return m_evars.find(j).sign();
}
-bool core::canonize_sign_is_correct(const monomial& m) const {
+bool core::canonize_sign_is_correct(const monic& m) const {
bool r = false;
for (lpvar j : m.vars()) {
r ^= canonize_sign(j);
@@ -112,7 +112,7 @@ bool core::canonize_sign_is_correct(const monomial& m) const {
return r == m.rsign();
}
-bool core::canonize_sign(const monomial& m) const {
+bool core::canonize_sign(const monic& m) const {
SASSERT(canonize_sign_is_correct(m));
return m.rsign();
}
@@ -125,7 +125,7 @@ bool core::canonize_sign(const factorization& f) const {
return r;
}
-void core::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
+void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
m_add_buffer.resize(sz);
for (unsigned i = 0; i < sz; i++) {
lpvar j = vs[i];
@@ -157,13 +157,13 @@ rational core::product_value(const unsigned_vector & m) const {
return r;
}
-// return true iff the monomial value is equal to the product of the values of the factors
-bool core::check_monomial(const monomial& 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.get_column_value(m.var()).is_int());
return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
}
-void core::explain(const monomial& m, lp::explanation& exp) const {
+void core::explain(const monic& m, lp::explanation& exp) const {
for (lpvar j : m.vars())
explain(j, exp);
}
@@ -231,7 +231,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
return out;
}
-std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const {
+std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
if (lp_settings().m_print_external_var_name)
out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
else
@@ -250,8 +250,8 @@ std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const {
return out;
}
-std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
- return print_monomial_with_vars(m_emons[v], out);
+std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const {
+ return print_monic_with_vars(m_emons[v], out);
}
template <typename T>
std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
@@ -262,7 +262,7 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const
return out;
}
-std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
+std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const {
out << "["; print_var(m.var(), out) << "]\n";
out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
if (m.vars() == m.rvars())
@@ -505,8 +505,8 @@ void core:: mk_ineq(lpvar j, llc cmp) {
mk_ineq(j, cmp, rational::zero());
}
-// the monomials should be equal by modulo sign but this is not so in the model
-void core:: fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) {
+// the monics should be equal by modulo sign but this is not so in the model
+void core:: fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign) {
SASSERT(sign == 1 || sign == -1);
explain(a, current_expl());
explain(b, current_expl());
@@ -523,7 +523,7 @@ void core:: fill_explanation_and_lemma_sign(const monomial& a, const monomial &
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
// Also sorts the result.
//
-svector<lpvar> core::reduce_monomial_to_rooted(const svector<lpvar> & vars, rational & sign) const {
+svector<lpvar> core::reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const {
svector<lpvar> ret;
bool s = false;
for (lpvar v : vars) {
@@ -545,10 +545,10 @@ svector<lpvar> core::reduce_monomial_to_rooted(const svector<lpvar> & vars, rati
// m_v = coeff * w1 * ... * wn, where w1, .., wn are canonical
// representatives, which are the roots of the equivalence tree, under current equations.
//
-monomial_coeff core::canonize_monomial(monomial const& m) const {
+monic_coeff core::canonize_monic(monic const& m) const {
rational sign = rational(1);
- svector<lpvar> vars = reduce_monomial_to_rooted(m.vars(), sign);
- return monomial_coeff(vars, sign);
+ svector<lpvar> vars = reduce_monic_to_rooted(m.vars(), sign);
+ return monic_coeff(vars, sign);
}
lemma& core::current_lemma() { return m_lemma_vec->back(); }
@@ -594,7 +594,7 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
return true;
}
-int core::rat_sign(const monomial& m) const {
+int core::rat_sign(const monic& m) const {
int sign = 1;
for (lpvar j : m.vars()) {
auto v = val(j);
@@ -611,8 +611,8 @@ int core::rat_sign(const monomial& m) const {
return sign;
}
-// Returns true if the monomial sign is incorrect
-bool core::sign_contradiction(const monomial& m) const {
+// Returns true if the monic sign is incorrect
+bool core::sign_contradiction(const monic& m) const {
return nla::rat_sign(val(m)) != rat_sign(m);
}
@@ -654,8 +654,8 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
}
std::ostream & core::print_var(lpvar j, std::ostream & out) const {
- if (m_emons.is_monomial_var(j)) {
- print_monomial(m_emons[j], out);
+ if (m_emons.is_monic_var(j)) {
+ print_monic(m_emons[j], out);
}
m_lar_solver.print_column_info(j, out);
@@ -664,9 +664,9 @@ std::ostream & core::print_var(lpvar j, std::ostream & out) const {
return out;
}
-std::ostream & core::print_monomials(std::ostream & out) const {
+std::ostream & core::print_monics(std::ostream & out) const {
for (auto &m : m_emons) {
- print_monomial_with_vars(m, out);
+ print_monic_with_vars(m, out);
}
return out;
}
@@ -707,13 +707,13 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o
return out;
}
-bool core::find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const {
- monomial const* sv = m_emons.find_canonical(vars);
+bool core::find_canonical_monic_of_vars(const svector<lpvar>& vars, lpvar & i) const {
+ monic const* sv = m_emons.find_canonical(vars);
return sv && (i = sv->var(), true);
}
-bool core::is_canonical_monomial(lpvar j) const {
- return m_emons.is_canonical_monomial(j);
+bool core::is_canonical_monic(lpvar j) const {
+ return m_emons.is_canonical_monic(j);
}
@@ -735,7 +735,7 @@ void core::explain_separation_from_zero(lpvar j) {
explain_existing_upper_bound(j);
}
-void core::trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const {
+void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const {
out << "rooted vars: ";
print_product(rm.rvars(), out);
out << "\n";
@@ -926,14 +926,14 @@ void core::trace_print_rms(const T& p, std::ostream& out) {
out << "}";
}
-void core::print_monomial_stats(const monomial& m, std::ostream& out) {
+void core::print_monic_stats(const monic& m, std::ostream& out) {
if (m.size() == 2) return;
- monomial_coeff mc = canonize_monomial(m);
+ monic_coeff mc = canonize_monic(m);
for(unsigned i = 0; i < mc.vars().size(); i++){
if (abs(val(mc.vars()[i])) == rational(1)) {
auto vv = mc.vars();
vv.erase(vv.begin()+i);
- monomial const* sv = m_emons.find_canonical(vv);
+ monic const* sv = m_emons.find_canonical(vv);
if (!sv) {
out << "nf length" << vv.size() << "\n"; ;
}
@@ -959,10 +959,10 @@ void core::init_to_refine() {
TRACE("nla_solver_details", tout << "emons:" << pp_emons(*this, m_emons););
m_to_refine.clear();
m_to_refine.resize(m_lar_solver.number_of_vars());
- unsigned r = random(), sz = m_emons.number_of_monomials();
+ unsigned r = random(), sz = m_emons.number_of_monics();
for (unsigned k = 0; k < sz; k++) {
auto const & m = *(m_emons.begin() + (k + r)% sz);
- if (!check_monomial(m))
+ if (!check_monic(m))
m_to_refine.insert(m.var());
}
@@ -975,7 +975,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
std::unordered_set<lpvar> vars;
auto insert_j = [&](lpvar j) {
vars.insert(j);
- if (m_emons.is_monomial_var(j)) {
+ if (m_emons.is_monic_var(j)) {
for (lpvar k : m_emons[j].vars())
vars.insert(k);
}
@@ -996,7 +996,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
}
// divides bc by c, so bc = b*c
-bool core::divide(const monomial& bc, const factor& c, factor & b) const {
+bool core::divide(const monic& bc, const factor& c, factor & b) const {
svector<lpvar> c_rvars = sorted_rvars(c);
TRACE("nla_solver_div", tout << "c_rvars = "; print_product(c_rvars, tout); tout << "\nbc_rvars = "; print_product(bc.rvars(), tout););
if (!lp::is_proper_factor(c_rvars, bc.rvars()))
@@ -1008,7 +1008,7 @@ bool core::divide(const monomial& bc, const factor& c, factor & b) const {
if (b_rvars.size() == 1) {
b = factor(b_rvars[0], factor_type::VAR);
} else {
- monomial const* sv = m_emons.find_canonical(b_rvars);
+ monic const* sv = m_emons.find_canonical(b_rvars);
if (sv == nullptr) {
TRACE("nla_solver_div", tout << "not in rooted";);
return false;
@@ -1064,10 +1064,10 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
}
-void core::trace_print_ol(const monomial& ac,
+void core::trace_print_ol(const monic& ac,
const factor& a,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b,
std::ostream& out) {
out << "ac = " << pp_mon(*this, ac) << "\n";
@@ -1086,7 +1086,7 @@ void core::maybe_add_a_factor(lpvar i,
std::unordered_set<unsigned>& found_rm,
vector<factor> & r) const {
SASSERT(abs(val(i)) == abs(val(c)));
- if (!m_emons.is_monomial_var(i)) {
+ if (!m_emons.is_monic_var(i)) {
i = m_evars.find(i).var();
if (try_insert(i, found_vars)) {
r.push_back(factor(i, factor_type::VAR));
@@ -1100,7 +1100,7 @@ void core::maybe_add_a_factor(lpvar i,
}
-// Returns rooted monomials by arity
+// Returns rooted monics by arity
std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
std::unordered_map<unsigned, unsigned_vector> m;
for (auto const& mon : m_emons) {
@@ -1116,8 +1116,8 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
-bool core::rm_check(const monomial& rm) const {
- return check_monomial(m_emons[rm.var()]);
+bool core::rm_check(const monic& rm) const {
+ return check_monic(m_emons[rm.var()]);
}
@@ -1174,7 +1174,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
*/
-bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf) {
+bool core::find_bfc_to_refine_on_monic(const monic& m, factorization & bf) {
for (auto f : factorization_factory_imp(m, *this)) {
if (f.size() == 2) {
auto a = f[0];
@@ -1192,14 +1192,14 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf)
return false;
}
-// finds a monomial to refine with its binary factorization
-bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
+// finds a monic to refine with its binary factorization
+bool core::find_bfc_to_refine(const monic* & m, factorization & bf){
m = nullptr;
unsigned r = random(), sz = m_to_refine.size();
for (unsigned k = 0; k < sz; k++) {
lpvar i = m_to_refine[(k + r) % sz];
m = &m_emons[i];
- SASSERT (!check_monomial(*m));
+ SASSERT (!check_monic(*m));
if (m->size() == 2) {
bf.set_mon(m);
bf.push_back(factor(m->vars()[0], factor_type::VAR));
@@ -1207,7 +1207,7 @@ bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
return true;
}
- if (find_bfc_to_refine_on_monomial(*m, bf)) {
+ if (find_bfc_to_refine_on_monic(*m, bf)) {
TRACE("nla_solver",
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";);
@@ -1292,10 +1292,10 @@ bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
bool p;
for (lpvar j : list) {
if (first) {
- p = check_monomial(m_emons[j]);
+ p = check_monic(m_emons[j]);
first = false;
} else
- if (check_monomial(m_emons[j]) != p)
+ if (check_monic(m_emons[j]) != p)
return false;
}
return true;
@@ -1334,8 +1334,8 @@ lbool core::check(vector<lemma>& l_vec) {
ret = inner_check(false);
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemma_vec->size() << "\n";);
- IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monomials(verbose_stream());});
- CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monomials(tout););
+ IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
+ CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monics(tout););
return ret;
}
@@ -1383,7 +1383,7 @@ lbool core::test_check(
// nla_expr<rational> r(expr_type::SUM);
// for (const auto & p : coeffs) {
// lpvar j = p.second;
-// if (is_monomial_var(j))
+// if (is_monic_var(j))
// r.add_child(mk_expr(p.first, m_emons[j].vars()));
// else
// r.add_child(mk_expr(p.first, j));
@@ -1408,8 +1408,8 @@ std::ostream& core::print_terms(std::ostream& out) const {
}
std::string core::var_str(lpvar j) const {
- return is_monomial_var(j)?
- (product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
+ return is_monic_var(j)?
+ (product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
}
std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 497c9e6ec..2d8c070e7 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -79,7 +79,7 @@ public:
class core {
public:
- var_eqs<emonomials> m_evars;
+ var_eqs<emonics> m_evars;
lp::lar_solver& m_lar_solver;
vector<lemma> * m_lemma_vec;
lp::int_set m_to_refine;
@@ -91,7 +91,7 @@ public:
nla_settings m_nla_settings;
nla_grobner m_grobner;
private:
- emonomials m_emons;
+ emonics m_emons;
svector<lpvar> m_add_buffer;
mutable lp::int_set m_row_var_set;
public:
@@ -113,8 +113,8 @@ public:
}
reslimit & reslim() { return m_reslim; }
- emonomials& emons() { return m_emons; }
- const emonomials& emons() const { return m_emons; }
+ emonics& emons() { return m_emons; }
+ const emonics& emons() const { return m_emons; }
// constructor
core(lp::lar_solver& s, reslimit &);
@@ -125,16 +125,16 @@ public:
lp::lar_term subs_terms_to_columns(const lp::lar_term& t) const;
bool ineq_holds(const ineq& n) const;
bool lemma_holds(const lemma& l) const;
- bool is_monomial_var(lpvar j) const { return m_emons.is_monomial_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(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
+ rational val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
- bool canonize_sign_is_correct(const monomial& m) const;
+ bool canonize_sign_is_correct(const monic& m) const;
- lpvar var(monomial const& sv) const { return sv.var(); }
+ lpvar var(monic const& sv) const { return sv.var(); }
- rational val_rooted(const monomial& 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()])); }
@@ -161,24 +161,24 @@ public:
// the value of the rooted monomias is equal to the value of the m.var() variable multiplied
// by the canonize_sign
- bool canonize_sign(const monomial& m) const;
+ bool canonize_sign(const monic& m) const;
- void deregister_monomial_from_monomialomials (const monomial & m, unsigned i);
+ void deregister_monic_from_monicomials (const monic & m, unsigned i);
- void deregister_monomial_from_tables(const monomial & m, unsigned i);
+ void deregister_monic_from_tables(const monic & m, unsigned i);
- void add_monomial(lpvar v, unsigned sz, lpvar const* vs);
+ void add_monic(lpvar v, unsigned sz, lpvar const* vs);
void push();
void pop(unsigned n);
rational mon_value_by_vars(unsigned i) const;
rational product_value(const unsigned_vector & m) const;
- // return true iff the monomial value is equal to the product of the values of the factors
- bool check_monomial(const monomial& m) const;
+ // return true iff the monic value is equal to the product of the values of the factors
+ bool check_monic(const monic& m) const;
- void explain(const monomial& m, lp::explanation& exp) const;
+ void explain(const monic& m, lp::explanation& exp) const;
void explain(const factor& f, lp::explanation& exp) const;
void explain(lpvar j, lp::explanation& exp) const;
void explain_existing_lower_bound(lpvar j);
@@ -189,7 +189,7 @@ public:
std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
std::ostream & print_var(lpvar j, std::ostream & out) const;
- std::ostream & print_monomials(std::ostream & out) const;
+ std::ostream & print_monics(std::ostream & out) const;
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>
@@ -200,27 +200,27 @@ public:
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;
+ std::ostream& print_monic(const monic& m, std::ostream& out) const;
std::ostream& print_bfc(const factorization& m, std::ostream& out) const;
- std::ostream& print_monomial_with_vars(unsigned i, std::ostream& out) const;
+ std::ostream& print_monic_with_vars(unsigned i, std::ostream& out) const;
template <typename T>
std::ostream& print_product_with_vars(const T& m, std::ostream& out) const;
- std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const;
+ std::ostream& print_monic_with_vars(const monic& m, std::ostream& out) const;
std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
template <typename T>
void trace_print_rms(const T& p, std::ostream& out);
- void trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const;
- void print_monomial_stats(const monomial& m, std::ostream& out);
+ void trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const;
+ void print_monic_stats(const monic& m, std::ostream& out);
void print_stats(std::ostream& out);
std::ostream& print_lemma(std::ostream& out) const;
void print_specific_lemma(const lemma& l, std::ostream& out) const;
- void trace_print_ol(const monomial& ac,
+ void trace_print_ol(const monic& ac,
const factor& a,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b,
std::ostream& out);
@@ -251,11 +251,11 @@ public:
llc apply_minus(llc cmp);
- void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign);
+ void fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign);
- svector<lpvar> reduce_monomial_to_rooted(const svector<lpvar> & vars, rational & sign) const;
+ svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
- monomial_coeff canonize_monomial(monomial const& m) const;
+ monic_coeff canonize_monic(monic const& m) const;
lemma& current_lemma();
const lemma& current_lemma() const;
@@ -274,18 +274,18 @@ public:
bool zero_is_an_inner_point_of_bounds(lpvar j) const;
- int rat_sign(const monomial& m) const;
+ int rat_sign(const monic& m) const;
inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); }
- bool sign_contradiction(const monomial& m) const;
+ bool sign_contradiction(const monic& m) const;
bool var_is_fixed_to_zero(lpvar j) const;
bool var_is_fixed_to_val(lpvar j, const rational& v) const;
bool var_is_fixed(lpvar j) const;
- bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const;
- bool is_canonical_monomial(lpvar) const;
+ bool find_canonical_monic_of_vars(const svector<lpvar>& vars, lpvar & i) const;
+ bool is_canonical_monic(lpvar) const;
bool elists_are_consistent(bool check_in_model) const;
bool elist_is_consistent(const std::unordered_set<lpvar>&) const;
bool var_has_positive_lower_bound(lpvar j) const;
@@ -337,9 +337,9 @@ public:
template <typename T>
bool vars_are_roots(const T& v) const;
- void register_monomial_in_tables(unsigned i_mon);
+ void register_monic_in_tables(unsigned i_mon);
- void register_monomials_in_tables();
+ void register_monics_in_tables();
void clear();
@@ -347,7 +347,7 @@ public:
void init_to_refine();
- bool divide(const monomial& bc, const factor& c, factor & b) const;
+ bool divide(const monic& bc, const factor& c, factor & b) const;
void negate_factor_equality(const factor& c, const factor& d);
@@ -355,15 +355,15 @@ public:
std::unordered_set<lpvar> collect_vars(const lemma& l) const;
- bool rm_check(const monomial&) const;
+ bool rm_check(const monic&) const;
std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
void add_abs_bound(lpvar v, llc cmp);
void add_abs_bound(lpvar v, llc cmp, rational const& bound);
- bool find_bfc_to_refine_on_monomial(const monomial&, factorization & bf);
+ bool find_bfc_to_refine_on_monic(const monic&, factorization & bf);
- bool find_bfc_to_refine(const monomial* & m, factorization& bf);
+ bool find_bfc_to_refine(const monic* & m, factorization& bf);
void negate_relation(unsigned j, const rational& a);
bool conflict_found() const;
@@ -381,18 +381,18 @@ public:
struct pp_mon {
core const& c;
- monomial const& m;
- pp_mon(core const& c, monomial const& m): c(c), m(m) {}
+ monic const& m;
+ pp_mon(core const& c, monic const& m): c(c), m(m) {}
pp_mon(core const& c, lpvar v): c(c), m(c.emons()[v]) {}
};
struct pp_mon_with_vars {
core const& c;
- monomial const& m;
- pp_mon_with_vars(core const& c, monomial const& m): c(c), m(m) {}
+ monic const& m;
+ pp_mon_with_vars(core const& c, monic 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_mon_with_vars const& p) { return p.c.print_monomial_with_vars(p.m, out); }
+inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monic(p.m, out); }
+inline std::ostream& operator<<(std::ostream& out, pp_mon_with_vars const& p) { return p.c.print_monic_with_vars(p.m, out); }
struct pp_fac {
core const& c;
diff --git a/src/math/lp/nla_defs.h b/src/math/lp/nla_defs.h
index 464a42321..111165431 100644
--- a/src/math/lp/nla_defs.h
+++ b/src/math/lp/nla_defs.h
@@ -63,11 +63,11 @@ inline std::ostream& operator<<(std::ostream& out, signed_var const& sv) { retur
* represents definition m_v = coeff* v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn]
*/
-class monomial_coeff {
+class monic_coeff {
svector<lp::var_index> m_vs;
rational m_coeff;
public:
- monomial_coeff(const svector<lp::var_index>& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {}
+ monic_coeff(const svector<lp::var_index>& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {}
rational const& coeff() const { return m_coeff; }
const svector<lp::var_index> & vars() const { return m_vs; }
};
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index e4c7b66ae..72fcc671a 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -38,10 +38,10 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
}
}
- if (!c().is_monomial_var(j))
+ if (!c().is_monic_var(j))
return;
- const monomial& m = c().emons()[j];
+ const monic& m = c().emons()[j];
for (auto fcn : factorization_factory_imp(m, c())) {
for (const factor& fc: fcn) {
lpvar j = var(fc);
@@ -71,7 +71,7 @@ var_weight nla_grobner::get_var_weight(lpvar j) const {
UNREACHABLE();
break;
}
- if (c().is_monomial_var(j)) {
+ if (c().is_monic_var(j)) {
return (var_weight)((int)k + 1);
}
return k;
@@ -88,7 +88,7 @@ void nla_grobner::find_nl_cluster() {
prepare_rows_and_active_vars();
std::queue<lpvar> q;
for (lpvar j : c().m_to_refine) {
- TRACE("nla_grobner", c().print_monomial(c().emons()[j], tout) << "\n";);
+ TRACE("nla_grobner", c().print_monic(c().emons()[j], tout) << "\n";);
q.push(j);
}
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index aa294357a..4453dbba0 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -35,6 +35,8 @@ struct grobner_stats {
grobner_stats() { reset(); }
};
+struct monomial {
+};
class equation {
unsigned m_scope_lvl; //!< scope level when this equation was created.
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index 044ef2e77..058dd7401 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -50,8 +50,8 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
}
void monotone::assert_abs_val_a_le_abs_var_b(
- const monomial& a,
- const monomial& b,
+ const monic& a,
+ const monic& b,
bool strict) {
lpvar aj = var(a);
lpvar bj = var(b);
@@ -77,8 +77,8 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj|
}
-void monotone::monotonicity_lemma(monomial const& m) {
- SASSERT(!check_monomial(m));
+void monotone::monotonicity_lemma(monic const& m) {
+ SASSERT(!check_monic(m));
if (c().mon_has_zero(m.vars()))
return;
const rational prod_val = abs(c().product_value(m.vars()));
@@ -89,7 +89,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
monotonicity_lemma_gt(m, prod_val);
}
-void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val) {
+void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {
TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n";);
add_empty_lemma();
for (lpvar j : m.vars()) {
@@ -106,7 +106,7 @@ void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val
<=>
\/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
*/
-void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
+void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) {
add_empty_lemma();
for (lpvar j : m.vars()) {
c().add_abs_bound(j, llc::LT);
diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h
index 47bdc3be6..7330ed385 100644
--- a/src/math/lp/nla_monotone_lemmas.h
+++ b/src/math/lp/nla_monotone_lemmas.h
@@ -25,13 +25,13 @@ public:
monotone(core *core);
void monotonicity_lemma();
private:
- void monotonicity_lemma(monomial const& m);
- void monotonicity_lemma_gt(const monomial& m, const rational& prod_val);
- void monotonicity_lemma_lt(const monomial& m, const rational& prod_val);
- std::vector<rational> get_sorted_key(const monomial& rm) const;
- vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monomial& a) const;
+ void monotonicity_lemma(monic const& m);
+ void monotonicity_lemma_gt(const monic& m, const rational& prod_val);
+ void monotonicity_lemma_lt(const monic& m, const rational& prod_val);
+ std::vector<rational> get_sorted_key(const monic& rm) const;
+ vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
void negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict);
void negate_abs_a_lt_abs_b(lpvar a, lpvar b);
- void assert_abs_val_a_le_abs_var_b(const monomial& a, const monomial& b, bool strict);
+ void assert_abs_val_a_le_abs_var_b(const monic& a, const monic& b, bool strict);
};
}
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index aaa214979..de919132c 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -38,7 +38,7 @@ void order::order_lemma() {
unsigned sz = to_ref.size();
for (unsigned i = 0; i < sz && !done(); ++i) {
lpvar j = to_ref[(i + r) % sz];
- order_lemma_on_monomial(c().emons()[j]);
+ order_lemma_on_monic(c().emons()[j]);
}
}
@@ -46,7 +46,7 @@ void order::order_lemma() {
// a > b && c > 0 => ac > bc
// Consider here some binary factorizations of m=ac and
// try create order lemmas with either factor playing the role of c.
-void order::order_lemma_on_monomial(const monomial& m) {
+void order::order_lemma_on_monic(const monic& m) {
TRACE("nla_solver_details",
tout << "m = " << pp_mon(c(), m););
@@ -61,13 +61,13 @@ void order::order_lemma_on_monomial(const monomial& m) {
break;
}
}
-// Here ac is a monomial of size 2
+// Here ac is a monic of size 2
// Trying to get an order lemma is
// 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) {
+void order::order_lemma_on_binomial(const monic& ac) {
TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac););
- SASSERT(!check_monomial(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 acv = val(ac);
bool gt = acv > mult_val;
@@ -89,7 +89,7 @@ void order::order_lemma_on_binomial(const monomial& ac) {
y >= 0 or x > a or xy >= ay
*/
-void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
+void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(val(y));
add_empty_lemma();
@@ -99,13 +99,13 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
TRACE("nla_solver", print_lemma(tout););
}
-// 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) {
+// We look for monics 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 monic& ac, bool k) {
TRACE("nla_solver", tout << "ac = " << pp_mon_with_vars(c(), ac););
SASSERT(ac.size() == 2);
lpvar c = ac.vars()[k];
- for (monomial const& bd : _().emons().get_products_of(c)) {
+ for (monic const& bd : _().emons().get_products_of(c)) {
if (bd.var() == ac.var()) continue;
TRACE("nla_solver", tout << "bd = " << pp_mon_with_vars(_(), bd););
order_lemma_on_factor_binomial_rm(ac, k, bd);
@@ -116,8 +116,8 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
}
// ac is a binomial
-// 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) {
+// create order lemma on monics bd where d is equivalent to ac[k]
+void order::order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const monic& bd) {
TRACE("nla_solver",
tout << "ac=" << pp_mon_with_vars(_(), ac) << "\n";
tout << "k=" << k << "\n";
@@ -131,7 +131,7 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const
}
// ac >= bd && |c| = |d| => ac/|c| >= bd/|d|
-void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
+void order::order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& bd, const factor& b, lpvar d) {
lpvar a = ac.vars()[!k];
lpvar c = ac.vars()[k];
TRACE("nla_solver",
@@ -162,11 +162,11 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const mono
// c and d are equivalent |c| == |d|
// ac > bd => ac/|c| > bd/|d| => a*c_sign > b*d_sign
// but the last inequality does not hold
-void order::generate_mon_ol(const monomial& ac,
+void order::generate_mon_ol(const monic& ac,
lpvar a,
const rational& c_sign,
lpvar c,
- const monomial& bd,
+ const monic& bd,
const factor& b,
const rational& d_sign,
lpvar d,
@@ -199,10 +199,10 @@ void order::generate_mon_ol(const monomial& ac,
// a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c
-bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
+bool order::order_lemma_on_ac_and_bc(const monic& rm_ac,
const factorization& ac_f,
bool k,
- const monomial& rm_bd) {
+ const monic& rm_bd) {
TRACE("nla_solver",
tout << "rm_ac = " << pp_mon_with_vars(_(), rm_ac) << "\n";
tout << "rm_bd = " << pp_mon_with_vars(_(), rm_bd) << "\n";
@@ -216,9 +216,9 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
// Here ab is a binary factorization of m.
-// We try to find a monomial n = cd, such that |b| = |d|
+// We try to find a monic n = cd, such that |b| = |d|
// and get a lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation
-void order::order_lemma_on_factorization(const monomial& m, const factorization& ab) {
+void order::order_lemma_on_factorization(const monic& m, const factorization& ab) {
bool sign = m.rsign();
for (factor f: ab)
sign ^= _().canonize_sign(f);
@@ -230,7 +230,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
if (mv == fv)
return;
bool gt = mv > fv;
- TRACE("nla_solver", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
+ TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
order_lemma_on_ab(m, sign_to_rat(sign), var(ab[k]), var(ab[j]), gt);
explain(ab); explain(m);
@@ -239,19 +239,19 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
}
}
-bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool k) {
+bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k) {
const factor c = ac[k];
TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
if (c.is_var()) {
TRACE("nla_solver", tout << "var(c) = " << var(c););
- for (monomial const& bc : _().emons().get_use_list(c.var())) {
+ for (monic const& bc : _().emons().get_use_list(c.var())) {
if (order_lemma_on_ac_and_bc(rm ,ac, k, bc)) {
return true;
}
}
}
else {
- for (monomial const& bc : _().emons().get_products_of(c.var())) {
+ for (monic const& bc : _().emons().get_products_of(c.var())) {
if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) {
return true;
}
@@ -262,11 +262,11 @@ bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& a
// |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
-void order::generate_ol(const monomial& ac,
+void order::generate_ol(const monic& ac,
const factor& a,
int c_sign,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b,
llc ab_cmp) {
add_empty_lemma();
@@ -282,10 +282,10 @@ void order::generate_ol(const monomial& ac,
TRACE("nla_solver", _().print_lemma(tout););
}
-bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
+bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
const factor& a,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b) {
auto cv = val(c);
int c_sign = nla::rat_sign(cv);
@@ -311,7 +311,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& 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 monomial& 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));
add_empty_lemma();
if (val(a).is_pos()) {
@@ -339,7 +339,7 @@ void order::order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar
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_lt(const monomial& 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) {
SASSERT(sign * val(m) < val(a) * val(b));
add_empty_lemma();
if (val(a).is_pos()) {
@@ -360,7 +360,7 @@ void order::order_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar
}
}
-void order::order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt) {
+void order::order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) {
if (gt)
order_lemma_on_ab_gt(m, sign, a, b);
else
diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h
index 1582828f6..341bef43d 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -30,59 +30,59 @@ public:
private:
- bool order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
+ bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,
const factor& a,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b);
// a >< b && c > 0 => ac >< bc
// a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c
- bool order_lemma_on_ac_and_bc(const monomial& rm_ac,
+ bool order_lemma_on_ac_and_bc(const monic& rm_ac,
const factorization& ac_f,
bool k,
- const monomial& rm_bd);
+ const monic& rm_bd);
- bool order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool k);
+ bool order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k);
- void order_lemma_on_factorization(const monomial& rm, const factorization& ab);
+ void order_lemma_on_factorization(const monic& rm, const factorization& ab);
/**
\brief Add lemma:
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_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b);
+ void order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b);
// we need to deduce ab >= val(b)*a
/**
\brief Add lemma:
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_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar a, lpvar b);
- void order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt);
- void order_lemma_on_factor_binomial_explore(const monomial& m, bool k);
- void order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd);
- void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d);
- void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
- void order_lemma_on_binomial(const monomial& ac);
- void order_lemma_on_monomial(const monomial& rm);
+ void order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b);
+ void order_lemma_on_ab(const monic& m, const rational& sign, lpvar a, lpvar b, bool gt);
+ void order_lemma_on_factor_binomial_explore(const monic& m, bool k);
+ void order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const monic& bd);
+ void order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& bd, const factor& b, lpvar d);
+ void order_lemma_on_binomial_sign(const monic& ac, lpvar x, lpvar y, int sign);
+ void order_lemma_on_binomial(const monic& ac);
+ void order_lemma_on_monic(const monic& rm);
// |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
- void generate_ol(const monomial& ac,
+ void generate_ol(const monic& ac,
const factor& a,
int c_sign,
const factor& c,
- const monomial& bc,
+ const monic& bc,
const factor& b,
llc ab_cmp);
- void generate_mon_ol(const monomial& ac,
+ void generate_mon_ol(const monic& ac,
lpvar a,
const rational& c_sign,
lpvar c,
- const monomial& bd,
+ const monic& bd,
const factor& b,
const rational& d_sign,
lpvar d,
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 3a7ab7c51..56a74582b 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -19,19 +19,19 @@
--*/
#include "math/lp/nla_solver.h"
#include <map>
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/lp_utils.h"
#include "math/lp/var_eqs.h"
#include "math/lp/factorization.h"
#include "math/lp/nla_solver.h"
namespace nla {
-void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
- m_core->add_monomial(v, sz, vs);
+void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
+ m_core->add_monic(v, sz, vs);
}
-bool solver::is_monomial_var(lpvar v) const {
- return m_core->is_monomial_var(v);
+bool solver::is_monic_var(lpvar v) const {
+ return m_core->is_monic_var(v);
}
bool solver::need_check() { return true; }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 62d77c7e5..5a0d5cb05 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -24,7 +24,7 @@ Revision History:
#include "util/params.h"
#include "nlsat/nlsat_solver.h"
#include "math/lp/lar_solver.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
#include "math/lp/nla_core.h"
namespace nla {
@@ -34,7 +34,7 @@ class solver {
reslimit m_res_limit;
core* m_core;
public:
- void add_monomial(lpvar v, unsigned sz, lpvar const* vs);
+ void add_monic(lpvar v, unsigned sz, lpvar const* vs);
solver(lp::lar_solver& s);
~solver();
@@ -43,6 +43,6 @@ public:
void pop(unsigned scopes);
bool need_check();
lbool check(vector<lemma>&);
- bool is_monomial_var(lpvar) const;
+ bool is_monic_var(lpvar) const;
};
}
diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp
index 430054f6a..c1f254765 100644
--- a/src/math/lp/nla_tangent_lemmas.cpp
+++ b/src/math/lp/nla_tangent_lemmas.cpp
@@ -35,13 +35,13 @@ void tangents::tangent_lemma() {
return;
}
factorization bf(nullptr);
- const monomial* m;
+ const monic* m;
if (c().find_bfc_to_refine(m, bf)) {
tangent_lemma_bf(*m, bf);
}
}
-void tangents::generate_explanations_of_tang_lemma(const monomial& rm, const factorization& bf, lp::explanation& exp) {
+void tangents::generate_explanations_of_tang_lemma(const monic& rm, const factorization& bf, lp::explanation& exp) {
// here we repeat the same explanation for each lemma
c().explain(rm, exp);
c().explain(bf[0], exp);
@@ -69,7 +69,7 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
c().mk_ineq(t, below? llc::GT : llc::LT, - a*b);
}
-void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){
+void tangents::tangent_lemma_bf(const monic& m, const factorization& bf){
point a, b;
point xy (val(bf[0]), val(bf[1]));
rational correct_mult_val = xy.x * xy.y;
diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h
index d415e608d..24dda0e13 100644
--- a/src/math/lp/nla_tangent_lemmas.h
+++ b/src/math/lp/nla_tangent_lemmas.h
@@ -53,9 +53,9 @@ public:
void tangent_lemma();
private:
lpvar find_binomial_to_refine();
- void generate_explanations_of_tang_lemma(const monomial& m, const factorization& bf, lp::explanation& exp);
- void generate_simple_tangent_lemma(const monomial& m, const factorization&);
- void tangent_lemma_bf(const monomial& m,const factorization& bf);
+ void generate_explanations_of_tang_lemma(const monic& m, const factorization& bf, lp::explanation& exp);
+ void generate_simple_tangent_lemma(const monic& m, const factorization&);
+ void tangent_lemma_bf(const monic& m,const factorization& bf);
void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j);
void generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j);
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 2c59077e7..830dfd12e 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -9,7 +9,7 @@
#include "math/polynomial/polynomial.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/map.h"
-#include "math/lp/monomial.h"
+#include "math/lp/monic.h"
namespace nra {
@@ -23,8 +23,8 @@ typedef nla::variable_map_type variable_map_type;
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum> m_zero;
- vector<mon_eq> m_monomials;
- unsigned_vector m_monomials_lim;
+ vector<mon_eq> m_monics;
+ unsigned_vector m_monics_lim;
mutable variable_map_type m_variable_values; // current model
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p):
@@ -34,21 +34,21 @@ typedef nla::variable_map_type variable_map_type;
}
bool need_check() {
- return !m_monomials.empty() && !check_assignments(m_monomials, s, m_variable_values);
+ return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
}
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
- m_monomials.push_back(mon_eq(v, sz, vs));
+ m_monics.push_back(mon_eq(v, sz, vs));
}
void push() {
- m_monomials_lim.push_back(m_monomials.size());
+ m_monics_lim.push_back(m_monics.size());
}
void pop(unsigned n) {
if (n == 0) return;
- m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]);
- m_monomials_lim.shrink(m_monomials_lim.size() - n);
+ m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
+ m_monics_lim.shrink(m_monics_lim.size() - n);
}
/*
@@ -67,7 +67,7 @@ typedef nla::variable_map_type variable_map_type;
bool check_assignments() const {
s.get_model(m_variable_values);
- for (auto const& m : m_monomials) {
+ for (auto const& m : m_monics) {
if (!check_assignment(m)) return false;
}
return true;
@@ -97,8 +97,8 @@ typedef nla::variable_map_type variable_map_type;
}
// add polynomial definitions.
- for (auto const& m : m_monomials) {
- add_monomial_eq(m);
+ for (auto const& m : m_monics) {
+ add_monic_eq(m);
}
// TBD: add variable bounds?
@@ -134,7 +134,7 @@ typedef nla::variable_map_type variable_map_type;
return r;
}
- void add_monomial_eq(mon_eq const& m) {
+ void add_monic_eq(mon_eq const& m) {
polynomial::manager& pm = m_nlsat->pm();
svector<polynomial::var> vars;
for (auto v : m.vars()) {
@@ -142,7 +142,7 @@ typedef nla::variable_map_type variable_map_type;
}
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.var()), 1), pm);
- polynomial::monomial* mls[2] = { m1, m2 };
+ polynomial::monomial * mls[2] = { m1, m2 };
polynomial::scoped_numeral_vector coeffs(pm.m());
coeffs.push_back(mpz(1));
coeffs.push_back(mpz(-1));
@@ -226,7 +226,7 @@ typedef nla::variable_map_type variable_map_type;
}
std::ostream& display(std::ostream& out) const {
- for (auto m : m_monomials) {
+ for (auto m : m_monics) {
out << "v" << m.var() << " = ";
for (auto v : m.vars()) {
out << "v" << v << " ";
@@ -245,7 +245,7 @@ typedef nla::variable_map_type variable_map_type;
dealloc(m_imp);
}
- void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
+ void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
m_imp->add(v, sz, vs);
}
diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h
index a7b586aee..d8af073ef 100644
--- a/src/math/lp/nra_solver.h
+++ b/src/math/lp/nra_solver.h
@@ -33,7 +33,7 @@ namespace nra {
\brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
The variable v is equal to the product of variables vs.
*/
- void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
+ void add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs);
/*
\brief Check feasiblity of linear constraints augmented by polynomial definitions
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 8e25a46d4..94801b099 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -308,14 +308,14 @@ class theory_lra::imp {
}
- void add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
+ void add_monic(lpvar v, unsigned sz, lpvar const* vs) {
if (m_use_nla) {
m_th_imp.ensure_nla();
- (*m_nla)->add_monomial(v, sz, vs);
+ (*m_nla)->add_monic(v, sz, vs);
}
else {
m_th_imp.ensure_nra();
- (*m_nra)->add_monomial(v, sz, vs);
+ (*m_nra)->add_monic(v, sz, vs);
}
}
@@ -658,7 +658,7 @@ class theory_lra::imp {
m_solver->m_need_register_terms = true;
m_solver->register_existing_terms();
}
- m_switcher.add_monomial(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
+ m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
}
}