mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-25 20:05:03 -08:00
parent 65d818437a
commit e73ce6e712
2 changed files with 30 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/math/grobner/pdd_grobner.cpp
View file

@ -146,9 +146,22 @@ namespace dd {
return basic_step(pick_next()); return basic_step(pick_next());
} }
grobner::scoped_process::~scoped_process() {
if (e) {
pdd p = e->poly();
SASSERT(!p.is_val());
if (p.hi().is_val()) {
g.push_equation(solved, e);
}
else {
g.push_equation(processed, e);
}
}
}
bool grobner::basic_step(equation* e) { bool grobner::basic_step(equation* e) {
if (!e) return false; if (!e) return false;
scoped_detach sd(*this, e); scoped_process sd(*this, e);
equation& eq = *e; equation& eq = *e;
TRACE("grobner", display(tout << "eq = ", eq); display(tout);); TRACE("grobner", display(tout << "eq = ", eq); display(tout););
SASSERT(eq.state() == to_simplify); SASSERT(eq.state() == to_simplify);
@ -174,7 +187,7 @@ namespace dd {
grobner::equation* grobner::pick_linear() { grobner::equation* grobner::pick_linear() {
equation* eq = nullptr; equation* eq = nullptr;
for (auto* curr : m_to_simplify) { for (auto* curr : m_to_simplify) {
if (!eq || curr->poly().is_linear() && is_simpler(*curr, *eq)) { if (!eq || (curr->poly().is_linear() && is_simpler(*curr, *eq))) {
eq = curr; eq = curr;
} }
} }
@ -184,8 +197,9 @@ namespace dd {
void grobner::simplify() { void grobner::simplify() {
try { try {
while (simplify_linear_step() /*|| simplify_cc_step() */ || simplify_elim_step()) { while (simplify_linear_step(true) || simplify_linear_step(false) /*|| simplify_cc_step() */ || simplify_elim_step()) {
DEBUG_CODE(invariant();); DEBUG_CODE(invariant(););
TRACE("grobner", display(tout););
} }
} }
catch (pdd_manager::mem_out) { catch (pdd_manager::mem_out) {
@ -199,11 +213,14 @@ namespace dd {
} }
}; };
bool grobner::simplify_linear_step() { bool grobner::simplify_linear_step(bool binary) {
equation_vector linear; equation_vector linear;
for (equation* e : m_to_simplify) { for (equation* e : m_to_simplify) {
if (e->poly().is_linear()) { pdd p = e->poly();
linear.push_back(e); if (p.is_linear()) {
if (!binary || p.lo().is_val() || p.lo().lo().is_val()) {
linear.push_back(e);
}
} }
} }
if (linear.empty()) return false; if (linear.empty()) return false;
@ -252,7 +269,7 @@ namespace dd {
pdd p = eq1->poly(); pdd p = eq1->poly();
auto* e = los.insert_if_not_there2(p.lo().index(), eq1); auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
equation* eq2 = e->get_data().m_value; equation* eq2 = e->get_data().m_value;
if (eq2 != eq1 && !p.lo().is_val()) { if (eq2 != eq1 && p.hi().is_val() && !p.lo().is_val()) {
*eq1 = p - eq2->poly(); *eq1 = p - eq2->poly();
*eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep()); *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
reduced = true; reduced = true;
@ -495,7 +512,7 @@ namespace dd {
bool grobner::tuned_step() { bool grobner::tuned_step() {
equation* e = tuned_pick_next(); equation* e = tuned_pick_next();
if (!e) return false; if (!e) return false;
scoped_detach sd(*this, e); scoped_process sd(*this, e);
equation& eq = *e; equation& eq = *e;
SASSERT(!m_watch[eq.poly().var()].contains(e)); SASSERT(!m_watch[eq.poly().var()].contains(e));
SASSERT(eq.state() == to_simplify); SASSERT(eq.state() == to_simplify);

14
src/math/grobner/pdd_grobner.h
View file

@ -73,7 +73,7 @@ public:
const pdd& poly() const { return m_poly; } const pdd& poly() const { return m_poly; }
u_dependency * dep() const { return m_dep; } u_dependency * dep() const { return m_dep; }
unsigned idx() const { return m_idx; } unsigned idx() const { return m_idx; }
void operator=(pdd& p) { m_poly = p; } void operator=(pdd const& p) { m_poly = p; }
void operator=(u_dependency* d) { m_dep = d; } void operator=(u_dependency* d) { m_dep = d; }
eq_state state() const { return m_state; } eq_state state() const { return m_state; }
void set_state(eq_state st) { m_state = st; } void set_state(eq_state st) { m_state = st; }
@ -160,7 +160,7 @@ private:
void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); } void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); }
struct compare_top_var; struct compare_top_var;
bool simplify_linear_step(); bool simplify_linear_step(bool binary);
typedef vector<equation_vector> use_list_t; typedef vector<equation_vector> use_list_t;
use_list_t get_use_list(); use_list_t get_use_list();
void add_to_use(equation* e, use_list_t& use_list); void add_to_use(equation* e, use_list_t& use_list);
@ -170,15 +170,11 @@ private:
bool simplify_elim_step(); bool simplify_elim_step();
void invariant() const; void invariant() const;
struct scoped_detach { struct scoped_process {
grobner& g; grobner& g;
equation* e; equation* e;
scoped_detach(grobner& g, equation* e): g(g), e(e) {} scoped_process(grobner& g, equation* e): g(g), e(e) {}
~scoped_detach() { ~scoped_process();
if (e) {
g.push_equation(processed, *e);
}
}
}; };
void update_stats_max_degree_and_size(const equation& e); void update_stats_max_degree_and_size(const equation& e);