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

port grobner basis functionality, prepare create nex objects to the grobner basis calculation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-19 15:51:01 -07:00
parent e8b6b870ac
commit a085edceff
12 changed files with 424 additions and 274 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

257
src/math/lp/cross_nested.h
View file

@ -20,19 +20,10 @@
#pragma once
#include <functional>
#include "math/lp/nex.h"
#include "math/lp/nex_creator.h"
namespace nla {
class cross_nested {
struct occ {
unsigned m_occs;
unsigned m_power;
occ() : m_occs(0), m_power(0) {}
occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {}
// use the "name injection rule here"
friend std::ostream& operator<<(std::ostream& out, const occ& c) {
out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")";
return out;
}
};
// fields
nex * m_e;
@ -40,20 +31,17 @@ class cross_nested {
std::function<bool (unsigned)> m_var_is_fixed;
std::function<unsigned ()> m_random;
bool m_done;
std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers;
ptr_vector<nex> m_allocated;
ptr_vector<nex> m_b_split_vec;
int m_reported;
bool m_random_bit;
nex_creator m_nex_creator;
#ifdef Z3DEBUG
nex* m_e_clone;
#endif
void add_to_allocated(nex* r) {
m_allocated.push_back(r);
}
public:
nex_creator& get_nex_creator() { return m_nex_creator; }
cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed,
std::function<unsigned ()> random):
@ -84,172 +72,25 @@ public:
return c;
}
nex_sum* mk_sum() {
auto r = new nex_sum();
add_to_allocated(r);
return r;
}
template <typename T>
void add_children(T) { }
template <typename T, typename K, typename ...Args>
void add_children(T r, K e, Args ... es) {
r->add_child(e);
add_children(r, es ...);
}
nex_sum* mk_sum(const ptr_vector<nex>& v) {
auto r = new nex_sum();
add_to_allocated(r);
r->children() = v;
return r;
}
nex_mul* mk_mul(const ptr_vector<nex>& v) {
auto r = new nex_mul();
add_to_allocated(r);
r->children() = v;
return r;
}
template <typename K, typename...Args>
nex_sum* mk_sum(K e, Args... es) {
auto r = new nex_sum();
add_to_allocated(r);
r->add_child(e);
add_children(r, es...);
return r;
}
nex_var* mk_var(lpvar j) {
auto r = new nex_var(j);
add_to_allocated(r);
return r;
}
nex_mul* mk_mul() {
auto r = new nex_mul();
add_to_allocated(r);
return r;
}
template <typename K, typename...Args>
nex_mul* mk_mul(K e, Args... es) {
auto r = new nex_mul();
add_to_allocated(r);
add_children(r, e, es...);
return r;
}
nex_scalar* mk_scalar(const rational& v) {
auto r = new nex_scalar(v);
add_to_allocated(r);
return r;
}
nex * mk_div(const nex* a, lpvar j) {
TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";);
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
if (a->is_var())
return mk_scalar(rational(1));
ptr_vector<nex> bv;
bool seenj = false;
for (nex* c : to_mul(a)->children()) {
if (!seenj) {
if (c->contains(j)) {
if (!c->is_var())
bv.push_back(mk_div(c, j));
seenj = true;
continue;
}
}
bv.push_back(c);
}
if (bv.size() > 1) {
return mk_mul(bv);
}
if (bv.size() == 1) {
return bv[0];
}
SASSERT(bv.size() == 0);
return mk_scalar(rational(1));
}
nex * mk_div(const nex* a, const nex* b) {
TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
if (b->is_var()) {
return mk_div(a, to_var(b)->var());
}
SASSERT(b->is_mul());
const nex_mul *bm = to_mul(b);
if (a->is_sum()) {
nex_sum * r = mk_sum();
const nex_sum * m = to_sum(a);
for (auto e : m->children()) {
r->add_child(mk_div(e, bm));
}
TRACE("nla_cn_details", tout << *r << "\n";);
return r;
}
if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) {
return mk_scalar(rational(1));
}
SASSERT(a->is_mul());
const nex_mul* am = to_mul(a);
bm->get_powers_from_mul(m_powers);
nex_mul* ret = new nex_mul();
for (auto e : am->children()) {
TRACE("nla_cn_details", tout << "e=" << *e << "\n";);
if (!e->is_var()) {
SASSERT(e->is_scalar());
ret->add_child(e);
TRACE("nla_cn_details", tout << "continue\n";);
continue;
}
SASSERT(e->is_var());
lpvar j = to_var(e)->var();
auto it = m_powers.find(j);
if (it == m_powers.end()) {
ret->add_child(e);
} else {
it->second --;
if (it->second == 0)
m_powers.erase(it);
}
TRACE("nla_cn_details", tout << *ret << "\n";);
}
SASSERT(m_powers.size() == 0);
if (ret->children().size() == 0) {
delete ret;
TRACE("nla_cn_details", tout << "return 1\n";);
return mk_scalar(rational(1));
}
add_to_allocated(ret);
TRACE("nla_cn_details", tout << *ret << "\n";);
return ret;
}
nex* extract_common_factor(nex* e) {
nex_sum* c = to_sum(e);
TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_occurences_map) << "\n";);
TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
unsigned size = c->children().size();
bool have_factor = false;
for(const auto & p : m_occurences_map) {
for(const auto & p : m_nex_creator.occurences_map()) {
if (p.second.m_occs == size) {
have_factor = true;
break;
}
}
if (have_factor == false) return nullptr;
nex_mul* f = mk_mul();
for(const auto & p : m_occurences_map) { // randomize here: todo
nex_mul* f = m_nex_creator.mk_mul();
for(const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo
if (p.second.m_occs == size) {
unsigned pow = p.second.m_power;
while (pow --) {
f->add_child(mk_var(p.first));
f->add_child(m_nex_creator.mk_var(p.first));
}
}
}
@ -282,9 +123,9 @@ public:
return false;
}
nex* c_over_f = mk_div(*c, f);
nex* c_over_f = m_nex_creator.mk_div(*c, f);
to_sum(c_over_f)->simplify(&c_over_f);
*c = mk_mul(f, c_over_f);
*c = m_nex_creator.mk_mul(f, c_over_f);
TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";);
explore_expr_on_front_elem(&(*((*c)->children_ptr()))[1], front);
@ -310,16 +151,14 @@ public:
}
void pop_allocated(unsigned sz) {
for (unsigned j = sz; j < m_allocated.size(); j ++)
delete m_allocated[j];
m_allocated.resize(sz);
m_nex_creator.pop(sz);
}
void explore_expr_on_front_elem_vars(nex** c, vector<nex**>& front, const svector<lpvar> & vars) {
TRACE("nla_cn", tout << "save c=" << **c << "; front:"; print_front(front, tout) << "\n";);
nex* copy_of_c = *c;
auto copy_of_front = copy_front(front);
int alloc_size = m_allocated.size();
int alloc_size = m_nex_creator.size();
for(lpvar j : vars) {
if (m_var_is_fixed(j)) {
// it does not make sense to explore fixed multupliers
@ -353,26 +192,26 @@ public:
clear_maps();
for (const auto * ce : e->children()) {
if (ce->is_mul()) {
to_mul(ce)->get_powers_from_mul(m_powers);
to_mul(ce)->get_powers_from_mul(m_nex_creator.powers());
update_occurences_with_powers();
} else if (ce->is_var()) {
add_var_occs(to_var(ce)->var());
}
}
remove_singular_occurences();
TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_occurences_map) << "\n";);
TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
}
void fill_vars_from_occurences_map(svector<lpvar>& vars) {
for (auto & p : m_occurences_map)
for (auto & p : m_nex_creator.occurences_map())
vars.push_back(p.first);
m_random_bit = m_random() % 2;
TRACE("nla_cn", tout << "m_random_bit = " << m_random_bit << "\n";);
std::sort(vars.begin(), vars.end(), [this](lpvar j, lpvar k)
{
auto it_j = m_occurences_map.find(j);
auto it_k = m_occurences_map.find(k);
auto it_j = m_nex_creator.occurences_map().find(j);
auto it_k = m_nex_creator.occurences_map().find(k);
const occ& a = it_j->second;
@ -456,46 +295,46 @@ public:
}
void add_var_occs(lpvar j) {
auto it = m_occurences_map.find(j);
if (it != m_occurences_map.end()) {
auto it = m_nex_creator.occurences_map().find(j);
if (it != m_nex_creator.occurences_map().end()) {
it->second.m_occs++;
it->second.m_power = 1;
} else {
m_occurences_map.insert(std::make_pair(j, occ(1, 1)));
m_nex_creator.occurences_map().insert(std::make_pair(j, occ(1, 1)));
}
}
void update_occurences_with_powers() {
for (auto & p : m_powers) {
for (auto & p : m_nex_creator.powers()) {
lpvar j = p.first;
unsigned jp = p.second;
auto it = m_occurences_map.find(j);
if (it == m_occurences_map.end()) {
m_occurences_map[j] = occ(1, jp);
auto it = m_nex_creator.occurences_map().find(j);
if (it == m_nex_creator.occurences_map().end()) {
m_nex_creator.occurences_map()[j] = occ(1, jp);
} else {
it->second.m_occs++;
it->second.m_power = std::min(it->second.m_power, jp);
}
}
TRACE("nla_cn_details", tout << "occs="; dump_occurences(tout, m_occurences_map) << "\n";);
TRACE("nla_cn_details", tout << "occs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
}
void remove_singular_occurences() {
svector<lpvar> r;
for (const auto & p : m_occurences_map) {
for (const auto & p : m_nex_creator.occurences_map()) {
if (p.second.m_occs <= 1) {
r.push_back(p.first);
}
}
for (lpvar j : r)
m_occurences_map.erase(j);
m_nex_creator.occurences_map().erase(j);
}
void clear_maps() {
m_occurences_map.clear();
m_powers.clear();
m_nex_creator.occurences_map().clear();
m_nex_creator.powers().clear();
}
// j -> the number of expressions j appears in as a multiplier
@ -504,16 +343,16 @@ public:
clear_maps();
for (const auto * ce : e->children()) {
if (ce->is_mul()) {
to_mul(ce)->get_powers_from_mul(m_powers);
to_mul(ce)->get_powers_from_mul(m_nex_creator.powers());
update_occurences_with_powers();
} else if (ce->is_var()) {
add_var_occs(to_var(ce)->var());
}
}
remove_singular_occurences();
TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_occurences_map) << "\n";);
TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
vector<std::pair<lpvar, occ>> ret;
for (auto & p : m_occurences_map)
for (auto & p : m_nex_creator.occurences_map())
ret.push_back(p);
std::sort(ret.begin(), ret.end(), [](const std::pair<lpvar, occ>& a, const std::pair<lpvar, occ>& b) {
if (a.second.m_occs > b.second.m_occs)
@ -536,11 +375,11 @@ public:
}
// all factors of j go to a, the rest to b
void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
a = mk_sum();
a = m_nex_creator.mk_sum();
m_b_split_vec.clear();
for (nex * ce: e->children()) {
if (is_divisible_by_var(ce, j)) {
a->add_child(mk_div(ce , j));
a->add_child(m_nex_creator.mk_div(ce , j));
} else {
m_b_split_vec.push_back(ce);
TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";);
@ -557,14 +396,14 @@ public:
TRACE("nla_cn_details", tout << "b = " << *b << "\n";);
} else {
SASSERT(m_b_split_vec.size() > 1);
b = mk_sum(m_b_split_vec);
b = m_nex_creator.mk_sum(m_b_split_vec);
TRACE("nla_cn_details", tout << "b = " << *b << "\n";);
}
}
void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector<nex**> & front, nex_sum* a, nex* b) {
TRACE("nla_cn_details", tout << "b = " << *b << "\n";);
e = mk_sum(mk_mul(mk_var(j), a), b); // e = j*a + b
e = m_nex_creator.mk_sum(m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a), b); // e = j*a + b
if (!a->is_linear()) {
nex **ptr_to_a = &(to_mul(to_sum(e)->children()[0]))->children()[1];
push_to_front(front, ptr_to_a);
@ -578,7 +417,7 @@ public:
void update_front_with_split(nex* & e, lpvar j, vector<nex**> & front, nex_sum* a, nex* b) {
if (b == nullptr) {
e = mk_mul(mk_var(j), a);
e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a);
if (!to_sum(a)->is_linear())
push_to_front(front, &(to_mul(e)->children()[1]));
} else {
@ -635,9 +474,7 @@ public:
}
~cross_nested() {
for (auto e: m_allocated)
delete e;
m_allocated.clear();
m_nex_creator.clear();
}
bool done() const { return m_done; }
@ -646,16 +483,16 @@ public:
switch (a->type()) {
case expr_type::VAR: {
auto v = to_var(a);
return mk_var(v->var());
return m_nex_creator.mk_var(v->var());
}
case expr_type::SCALAR: {
auto v = to_scalar(a);
return mk_scalar(v->value());
return m_nex_creator.mk_scalar(v->value());
}
case expr_type::MUL: {
auto m = to_mul(a);
auto r = mk_mul();
auto r = m_nex_creator.mk_mul();
for (nex * e : m->children()) {
r->add_child(clone(e));
}
@ -663,7 +500,7 @@ public:
}
case expr_type::SUM: {
auto m = to_sum(a);
auto r = mk_sum();
auto r = m_nex_creator.mk_sum();
for (nex * e : m->children()) {
r->add_child(clone(e));
}
@ -701,10 +538,10 @@ public:
return r;
}
nex_sum *r = mk_sum();
nex_sum *r = m_nex_creator.mk_sum();
nex_sum *as = to_sum(a->children()[sum_j]);
for (unsigned k = 0; k < as->size(); k++) {
nex_mul *b = mk_mul(as->children()[k]);
nex_mul *b = m_nex_creator.mk_mul(as->children()[k]);
for (unsigned j = 0; j < a->size(); j ++) {
if ((int)j != sum_j)
b->add_child(a->children()[j]);

14
src/math/lp/horner.cpp
View file

@ -96,7 +96,7 @@ bool horner::lemmas_on_row(const T& row) {
);
SASSERT (row_is_interesting(row));
create_sum_from_row(row, cn);
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum);
return lemmas_on_expr(cn);
}
@ -131,7 +131,7 @@ void horner::horner_lemmas() {
}
}
nex * horner::nexvar(lpvar j, cross_nested& cn) const {
nex * horner::nexvar(lpvar j, nex_creator& cn) const {
// todo: consider deepen the recursion
if (!c().is_monic_var(j))
return cn.mk_var(j);
@ -144,7 +144,7 @@ nex * horner::nexvar(lpvar j, cross_nested& cn) const {
return e;
}
nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const {
nex * horner::nexvar(const rational & coeff, lpvar j, nex_creator& cn) const {
// todo: consider deepen the recursion
if (!c().is_monic_var(j))
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
@ -158,15 +158,15 @@ nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const {
}
template <typename T> void horner::create_sum_from_row(const T& row, cross_nested& cn) {
template <typename T> void horner::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
SASSERT(row.size() > 1);
m_row_sum.children().clear();
sum.children().clear();
for (const auto &p : row) {
if (p.coeff().is_one())
m_row_sum.add_child(nexvar(p.var(), cn));
sum.add_child(nexvar(p.var(), cn));
else {
m_row_sum.add_child(nexvar(p.coeff(), p.var(), cn));
sum.add_child(nexvar(p.coeff(), p.var(), cn));
}
}
}

6
src/math/lp/horner.h
View file

@ -40,7 +40,7 @@ public:
bool lemmas_on_row(const T&);
template <typename T> bool row_is_interesting(const T&) const;
template <typename T>
void create_sum_from_row(const T&, cross_nested&);
void create_sum_from_row(const T&, nex_creator&, nex_sum&);
intervals::interval interval_of_expr_with_deps(const nex* e);
intervals::interval interval_of_expr(const nex* e);
intervals::interval interval_of_sum(const nex_sum*);
@ -51,8 +51,8 @@ public:
bool interval_from_term(const nex* e, interv&) const;
nex* nexvar(lpvar j, cross_nested& cn) const;
nex* nexvar(const rational& coeff, lpvar j, cross_nested& cn) const;
nex* nexvar(lpvar j, nex_creator& ) const;
nex* nexvar(const rational& coeff, lpvar j, nex_creator&) const;
intervals::interval interval_of_sum_with_deps(const nex_sum*);
intervals::interval interval_of_sum_no_term_with_deps(const nex_sum*);
intervals::interval interval_of_mul_with_deps(const nex_mul*);

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

@ -610,8 +610,11 @@ public:
return out;
}
bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }
bool column_is_free(unsigned j) const { return this->m_column_type[j] == column_type::free_column; }
bool column_is_fixed(unsigned j) const { return this->m_column_type[j] == column_type::fixed; }
bool column_has_upper_bound(unsigned j) const {
switch(m_column_types[j]) {
case column_type::free_column:

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

@ -63,6 +63,7 @@ public:
bool is_mul() const { return type() == expr_type::MUL; }
bool is_var() const { return type() == expr_type::VAR; }
bool is_scalar() const { return type() == expr_type::SCALAR; }
virtual bool is_pure_monomial() const { return false; }
std::string str() const { std::stringstream ss; print(ss); return ss.str(); }
virtual ~nex() {}
virtual bool contains(lpvar j) const { return false; }
@ -182,7 +183,8 @@ public:
const ptr_vector<nex>& children() const { return m_children;}
const ptr_vector<nex>* children_ptr() const { return &m_children;}
ptr_vector<nex>* children_ptr() { return &m_children;}
// A monomial is 'pure' if does not have a numeric coefficient.
bool is_pure_monomial() { return size() == 0 || (!m_children[0]->is_scalar()); }
std::ostream & print(std::ostream& out) const {
bool first = true;
for (const nex* v : m_children) {

215
src/math/lp/nex_creator.h Normal file
View file

@ -0,0 +1,215 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
namespace nla {
struct occ {
unsigned m_occs; // number of occurences
unsigned m_power; // min power in occurences
occ() : m_occs(0), m_power(0) {}
occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {}
// use the "name injection rule here"
friend std::ostream& operator<<(std::ostream& out, const occ& c) {
out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")";
return out;
}
};
// the purpose of this class is to create nex objects, keep them, and delete them
class nex_creator {
ptr_vector<nex> m_allocated;
std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers;
public:
const std::unordered_map<lpvar, occ>& occurences_map() const { return m_occurences_map; }
std::unordered_map<lpvar, occ>& occurences_map() { return m_occurences_map; }
const std::unordered_map<lpvar, unsigned> & powers() const { return m_powers; }
std::unordered_map<lpvar, unsigned> & powers() { return m_powers; }
void add_to_allocated(nex* r) { m_allocated.push_back(r); }
void pop(unsigned sz) {
for (unsigned j = sz; j < m_allocated.size(); j ++)
delete m_allocated[j];
m_allocated.resize(sz);
}
void clear() {
for (auto e: m_allocated)
delete e;
m_allocated.clear();
}
unsigned size() const { return m_allocated.size(); }
nex_sum* mk_sum() {
auto r = new nex_sum();
add_to_allocated(r);
return r;
}
template <typename T>
void add_children(T) { }
template <typename T, typename K, typename ...Args>
void add_children(T r, K e, Args ... es) {
r->add_child(e);
add_children(r, es ...);
}
nex_sum* mk_sum(const ptr_vector<nex>& v) {
auto r = new nex_sum();
add_to_allocated(r);
r->children() = v;
return r;
}
nex_mul* mk_mul(const ptr_vector<nex>& v) {
auto r = new nex_mul();
add_to_allocated(r);
r->children() = v;
return r;
}
template <typename K, typename...Args>
nex_sum* mk_sum(K e, Args... es) {
auto r = new nex_sum();
add_to_allocated(r);
r->add_child(e);
add_children(r, es...);
return r;
}
nex_var* mk_var(lpvar j) {
auto r = new nex_var(j);
add_to_allocated(r);
return r;
}
nex_mul* mk_mul() {
auto r = new nex_mul();
add_to_allocated(r);
return r;
}
template <typename K, typename...Args>
nex_mul* mk_mul(K e, Args... es) {
auto r = new nex_mul();
add_to_allocated(r);
add_children(r, e, es...);
return r;
}
nex_scalar* mk_scalar(const rational& v) {
auto r = new nex_scalar(v);
add_to_allocated(r);
return r;
}
nex * mk_div(const nex* a, lpvar j) {
TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";);
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
if (a->is_var())
return mk_scalar(rational(1));
ptr_vector<nex> bv;
bool seenj = false;
for (nex* c : to_mul(a)->children()) {
if (!seenj) {
if (c->contains(j)) {
if (!c->is_var())
bv.push_back(mk_div(c, j));
seenj = true;
continue;
}
}
bv.push_back(c);
}
if (bv.size() > 1) {
return mk_mul(bv);
}
if (bv.size() == 1) {
return bv[0];
}
SASSERT(bv.size() == 0);
return mk_scalar(rational(1));
}
nex * mk_div(const nex* a, const nex* b) {
TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
if (b->is_var()) {
return mk_div(a, to_var(b)->var());
}
SASSERT(b->is_mul());
const nex_mul *bm = to_mul(b);
if (a->is_sum()) {
nex_sum * r = mk_sum();
const nex_sum * m = to_sum(a);
for (auto e : m->children()) {
r->add_child(mk_div(e, bm));
}
TRACE("nla_cn_details", tout << *r << "\n";);
return r;
}
if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) {
return mk_scalar(rational(1));
}
SASSERT(a->is_mul());
const nex_mul* am = to_mul(a);
bm->get_powers_from_mul(m_powers);
nex_mul* ret = new nex_mul();
for (auto e : am->children()) {
TRACE("nla_cn_details", tout << "e=" << *e << "\n";);
if (!e->is_var()) {
SASSERT(e->is_scalar());
ret->add_child(e);
TRACE("nla_cn_details", tout << "continue\n";);
continue;
}
SASSERT(e->is_var());
lpvar j = to_var(e)->var();
auto it = m_powers.find(j);
if (it == m_powers.end()) {
ret->add_child(e);
} else {
it->second --;
if (it->second == 0)
m_powers.erase(it);
}
TRACE("nla_cn_details", tout << *ret << "\n";);
}
SASSERT(m_powers.size() == 0);
if (ret->children().size() == 0) {
delete ret;
TRACE("nla_cn_details", tout << "return 1\n";);
return mk_scalar(rational(1));
}
add_to_allocated(ret);
TRACE("nla_cn_details", tout << *ret << "\n";);
return ret;
}
};
}

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

@ -24,6 +24,8 @@
#include "math/lp/monic.h"
#include "math/lp/emonics.h"
#include "math/lp/factorization.h"
#include "util/dependency.h"
#include "util/region.h"
namespace nla {
@ -92,5 +94,26 @@ struct common {
std::ostream& print_rooted_monic_with_vars(const monic&, std::ostream& out) const;
bool check_monic(const monic&) const;
unsigned random();
class ci_value_manager {
public:
void inc_ref(lp::constraint_index const & v) {
}
void dec_ref(lp::constraint_index const & v) {
}
};
struct ci_dependency_config {
typedef ci_value_manager value_manager;
typedef region allocator;
static const bool ref_count = false;
typedef lp::constraint_index value;
};
typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
};
}

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

@ -628,23 +628,17 @@ bool core::sign_contradiction(const monic& m) const {
bool core:: var_is_fixed_to_zero(lpvar j) const {
return
m_lar_solver.column_has_upper_bound(j) &&
m_lar_solver.column_has_lower_bound(j) &&
m_lar_solver.get_upper_bound(j) == lp::zero_of_type<lp::impq>() &&
m_lar_solver.column_is_fixed(j) &&
m_lar_solver.get_lower_bound(j) == lp::zero_of_type<lp::impq>();
}
bool core:: var_is_fixed_to_val(lpvar j, const rational& v) const {
return
m_lar_solver.column_has_upper_bound(j) &&
m_lar_solver.column_has_lower_bound(j) &&
m_lar_solver.get_upper_bound(j) == lp::impq(v) && m_lar_solver.get_lower_bound(j) == lp::impq(v);
m_lar_solver.column_is_fixed(j) &&
m_lar_solver.get_lower_bound(j) == lp::impq(v);
}
bool core:: var_is_fixed(lpvar j) const {
return
m_lar_solver.column_has_upper_bound(j) &&
m_lar_solver.column_has_lower_bound(j) &&
m_lar_solver.get_upper_bound(j) == m_lar_solver.get_lower_bound(j);
return m_lar_solver.column_is_fixed(j);
}
std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {

86
src/math/lp/nla_grobner.cpp
View file

@ -21,7 +21,7 @@
#include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h"
namespace nla {
nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false) {}
nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc) {}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue
@ -142,8 +142,81 @@ void nla_grobner::display(std::ostream & out) {
c().print_term(r, out) << std::endl;
}
}
void nla_grobner::add_row_to_gb(unsigned) {
void nla_grobner::process_var(nex_mul* m, lpvar j, ci_dependency* & dep, rational & coeff) {
if (c().var_is_fixed(j)) {
if (!m_tmp_var_set.contains(j)) {
m_tmp_var_set.insert(j);
lp::constraint_index lc,uc;
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lc), m_dep_manager.mk_leaf(uc)));
}
coeff *= c().m_lar_solver.column_upper_bound(j).x;
}
else {
m->add_child(m_nex_creator.mk_var(j));
}
}
/**
\brief Create a new monomial using the given coeff and m. Fixed
variables in m are substituted by their values. The arg dep is
updated to store these dependencies. The set already_found is
updated with the fixed variables in m. A variable is only
added to dep if it is not already in already_found.
Return null if the monomial was simplified to 0.
*/
nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * & dep) {
NOT_IMPLEMENTED_YET();
return nullptr;
/*
ptr_buffer<expr> vars;
rational r;
if (c().is_monic_var(j)) {
coeff *= get_monomial_coeff(m);
m = get_monomial_body(m);
if (m_util.is_mul(m)) {
SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
process_var(arg);
}
}
else {
process_var(m);
}
}
else {
process_var(m);
}
if (!coeff.is_zero())
return gb.mk_monomial(coeff, vars.size(), vars.c_ptr());
else
return nullptr;
*/
}
void nla_grobner::add_row(unsigned i) {
NOT_IMPLEMENTED_YET();
/*
const auto& row = c().m_lar_solver.A_r().m_rows[i];
TRACE("non_linear", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout););
nex * row_nex;
v_dependency * dep = nullptr;
m_tmp_var_set.reset();
for (const auto & p : row) {
rational coeff = p.coeff();
lpvar j = p.var();
// TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";);
nex * new_m = mk_monomial(coeff, j, dep, m_tmp_var_set);
TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
if (new_m)
monomials.push_back(new_m);
}
assert_eq_0(monomials, dep);*/
}
void nla_grobner::add_monomial_def(lpvar) {
NOT_IMPLEMENTED_YET();
@ -151,7 +224,7 @@ void nla_grobner::add_monomial_def(lpvar) {
void nla_grobner::init() {
find_nl_cluster();
for (unsigned i : m_rows) {
add_row_to_gb(i);
add_row(i);
}
for (lpvar j : m_active_vars) {
add_monomial_def(j);
@ -178,7 +251,7 @@ bool nla_grobner:: is_better_choice(equation * eq1, equation * eq2) {
}
void nla_grobner::del_equation(equation * eq) {
SASSERT(false);
NOT_IMPLEMENTED_YET();
/*
m_processed.erase(eq);
m_to_process.erase(eq);
@ -377,4 +450,9 @@ void nla_grobner::display(std::ostream & out) const {
NOT_IMPLEMENTED_YET();
}
void nla_grobner::assert_eq_0(ptr_buffer<monomial> &, v_dependency * dep) {
NOT_IMPLEMENTED_YET();
}
} // end of nla namespace

49
src/math/lp/nla_grobner.h
View file

@ -21,6 +21,7 @@
#include "math/lp/nla_common.h"
#include "math/lp/nex.h"
#include "math/lp/nex_creator.h"
#include "util/dependency.h"
namespace nla {
@ -35,21 +36,6 @@ struct grobner_stats {
grobner_stats() { reset(); }
};
struct monomial {
rational m_coeff;
svector<lpvar> m_vars; //!< sorted variables
friend class grobner;
friend struct monomial_lt;
monomial() {}
public:
rational const & get_coeff() const { return m_coeff; }
unsigned get_degree() const { return m_vars.size(); }
unsigned get_size() const { return get_degree(); }
lpvar get_var(unsigned idx) const { return m_vars[idx]; }
};
enum class var_weight {
FIXED = 0,
QUOTED_FIXED = 1,
@ -64,6 +50,21 @@ enum class var_weight {
class nla_grobner : common {
struct monomial {
rational m_coeff;
svector<lpvar> m_vars; //!< sorted variables
friend class grobner;
friend struct monomial_lt;
monomial() {}
public:
rational const & get_coeff() const { return m_coeff; }
unsigned get_degree() const { return m_vars.size(); }
unsigned get_size() const { return get_degree(); }
lpvar get_var(unsigned idx) const { return m_vars[idx]; }
};
class equation {
unsigned m_scope_lvl; //!< scope level when this equation was created.
unsigned m_bidx:31; //!< position at m_equations_to_delete
@ -95,6 +96,12 @@ class nla_grobner : common {
equation_set m_processed;
equation_set m_to_process;
bool m_nl_gb_exhausted;
ptr_vector<nex> m_allocated;
lp::int_set m_tmp_var_set;
region m_alloc;
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_creator m_nex_creator;
public:
nla_grobner(core *core);
void grobner_lemmas();
@ -137,7 +144,17 @@ private:
void get_equations(ptr_vector<equation>& eqs);
bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
bool internalize_gb_eq(equation*);
void add_row_to_gb(unsigned);
void add_row(unsigned);
void add_monomial_def(lpvar);
void assert_eq_0(ptr_buffer<monomial> &, v_dependency * dep);
void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&);
nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&);
rational get_monomial_coeff(const nex_mul* m) {
const nex* a = m->children()[0];
if (a->is_scalar())
return static_cast<const nex_scalar*>(a)->value();
return rational(1);
}
}; // end of grobner
}

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

@ -130,11 +130,11 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) {
return true;
}
intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {
common::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {
return m_dep_manager.mk_leaf(ci);
}
intervals::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const {
common::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const {
intervals::ci_dependency * r = nullptr;
for (auto p : expl) {
if (r == nullptr) {

21
src/math/lp/nla_intervals.h
View file

@ -29,25 +29,6 @@ namespace nla {
class core;
class intervals : common {
class ci_value_manager {
public:
void inc_ref(lp::constraint_index const & v) {
}
void dec_ref(lp::constraint_index const & v) {
}
};
struct ci_dependency_config {
typedef ci_value_manager value_manager;
typedef region allocator;
static const bool ref_count = false;
typedef lp::constraint_index value;
};
typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
class im_config {
unsynch_mpq_manager& m_manager;
@ -139,7 +120,7 @@ class intervals : common {
ci_value_manager m_val_manager;
mutable unsynch_mpq_manager m_num_manager;
mutable ci_dependency_manager m_dep_manager;
im_config m_config;
im_config m_config;
mutable interval_manager<im_config> m_imanager;
public: