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

rebase with z3prover and fix term indices in monomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-12 12:46:59 -07:00
parent 578e24d8c1
commit 9a71ed87d9
3 changed files with 17 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -121,8 +121,16 @@ bool core::canonize_sign(const factorization& f) const {
return r; return r;
} }
void core::add(lpvar v, unsigned sz, lpvar const* vs) { void core::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
m_emons.add(v, sz, vs); m_add_buffer.resize(sz);
for (unsigned i = 0; i < sz; i++) {
lpvar j = vs[i];
if (m_lar_solver.is_term(j))
j = m_lar_solver.adjust_term_index(j);
m_add_buffer[i] = j;
}
m_emons.add(v, m_add_buffer);
} }
void core::push() { void core::push() {

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

@ -86,7 +86,11 @@ public:
order m_order; order m_order;
monotone m_monotone; monotone m_monotone;
emonomials m_emons; emonomials m_emons;
svector<lpvar> m_add_buffer;
public:
emonomials& emons() { return m_emons; }
const emonomials& emons() const { return m_emons; }
// constructor
core(lp::lar_solver& s); core(lp::lar_solver& s);
bool compare_holds(const rational& ls, llc cmp, const rational& rs) const; bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;
@ -133,8 +137,7 @@ public:
void deregister_monomial_from_tables(const monomial & m, unsigned i); void deregister_monomial_from_tables(const monomial & m, unsigned i);
// returns the monomial index void add_monomial(lpvar v, unsigned sz, lpvar const* vs);
void add(lpvar v, unsigned sz, lpvar const* vs);
void push(); void push();
void pop(unsigned n); void pop(unsigned n);

3
src/math/lp/nla_solver.cpp
View file

@ -27,9 +27,8 @@
#include "math/lp/nla_intervals.h" #include "math/lp/nla_intervals.h"
namespace nla { namespace nla {
// returns the monomial index
void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) { void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
m_core->add(v, sz, vs); m_core->add_monomial(v, sz, vs);
} }
bool solver::is_monomial_var(lpvar v) const { bool solver::is_monomial_var(lpvar v) const {