mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove unused functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-31 16:25:25 -08:00
parent 6b4ddf352d
commit 09dbacdf50
3 changed files with 13 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/math/grobner/pdd_solver.cpp
View file

@ -127,7 +127,7 @@ namespace dd {
void solver::saturate() { void solver::saturate() {
simplify(); simplify();
tuned_init(); init_saturate();
TRACE("dd.solver", display(tout);); TRACE("dd.solver", display(tout););
try { try {
while (!done() && step()) { while (!done() && step()) {
@ -144,11 +144,6 @@ namespace dd {
} }
} }
bool solver::step() {
m_stats.m_compute_steps++;
return tuned_step();
}
void solver::scoped_process::done() { void solver::scoped_process::done() {
pdd p = e->poly(); pdd p = e->poly();
SASSERT(!p.is_val()); SASSERT(!p.is_val());
@ -167,19 +162,7 @@ namespace dd {
SASSERT(!p.is_val()); SASSERT(!p.is_val());
g.push_equation(processed, e); g.push_equation(processed, e);
} }
} }
solver::equation* solver::pick_next() {
equation* eq = nullptr;
for (auto* curr : m_to_simplify) {
if (!eq || is_simpler(*curr, *eq)) {
eq = curr;
}
}
if (eq) pop_equation(eq);
return eq;
}
void solver::simplify() { void solver::simplify() {
try { try {
@ -639,8 +622,9 @@ namespace dd {
} }
} }
bool solver::tuned_step() { bool solver::step() {
equation* e = tuned_pick_next(); m_stats.m_compute_steps++;
equation* e = pick_next();
if (!e) return false; if (!e) return false;
scoped_process sd(*this, e); scoped_process sd(*this, e);
equation& eq = *e; equation& eq = *e;
@ -660,7 +644,7 @@ namespace dd {
return true; return true;
} }
void solver::tuned_init() { void solver::init_saturate() {
unsigned_vector const& l2v = m.get_level2var(); unsigned_vector const& l2v = m.get_level2var();
m_level2var.resize(l2v.size()); m_level2var.resize(l2v.size());
m_var2level.resize(l2v.size()); m_var2level.resize(l2v.size());
@ -714,7 +698,7 @@ namespace dd {
watch.shrink(j); watch.shrink(j);
} }
solver::equation* solver::tuned_pick_next() { solver::equation* solver::pick_next() {
while (m_levelp1 > 0) { while (m_levelp1 > 0) {
unsigned v = m_level2var[m_levelp1-1]; unsigned v = m_level2var[m_levelp1-1];
equation_vector const& watch = m_watch[v]; equation_vector const& watch = m_watch[v];

5
src/math/grobner/pdd_solver.h
View file

@ -142,15 +142,12 @@ private:
bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); } bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; } bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; }
// tuned implementation
vector<equation_vector> m_watch; // watch list mapping variables to vector of equations where they occur (generally a subset) vector<equation_vector> m_watch; // watch list mapping variables to vector of equations where they occur (generally a subset)
unsigned m_levelp1; // index into level+1 unsigned m_levelp1; // index into level+1
unsigned_vector m_level2var; // level -> var unsigned_vector m_level2var; // level -> var
unsigned_vector m_var2level; // var -> level unsigned_vector m_var2level; // var -> level
bool tuned_step(); void init_saturate();
void tuned_init();
equation* tuned_pick_next();
void simplify_watch(equation const& eq); void simplify_watch(equation const& eq);
void add_to_watch(equation& eq); void add_to_watch(equation& eq);

10
src/test/pdd_solver.cpp
View file

@ -11,9 +11,9 @@
#include "tactic/bv/bit_blaster_tactic.h" #include "tactic/bv/bit_blaster_tactic.h"
namespace dd { namespace dd {
void print_eqs(ptr_vector<grobner::equation> const& eqs) { void print_eqs(ptr_vector<solver::equation> const& eqs) {
std::cout << "eqs\n"; std::cout << "eqs\n";
for (grobner::equation* e : eqs) { for (solver::equation* e : eqs) {
std::cout << e->poly() << "\n"; std::cout << e->poly() << "\n";
} }
} }
@ -25,7 +25,7 @@ namespace dd {
pdd v2 = m.mk_var(2); pdd v2 = m.mk_var(2);
pdd v3 = m.mk_var(3); pdd v3 = m.mk_var(3);
grobner gb(lim, m); solver gb(lim, m);
gb.add(v1*v2 + v1*v3); gb.add(v1*v2 + v1*v3);
gb.add(v1 - 1); gb.add(v1 - 1);
gb.display(std::cout); gb.display(std::cout);
@ -142,7 +142,7 @@ namespace dd {
return expr_ref(cache[e], m); return expr_ref(cache[e], m);
} }
void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) { void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, solver& g) {
expr* a, *b; expr* a, *b;
pdd v1 = p.mk_var(id2var[e->get_id()]); pdd v1 = p.mk_var(id2var[e->get_id()]);
pdd q(p); pdd q(p);
@ -200,7 +200,7 @@ namespace dd {
collect_id2var(id2var, fmls); collect_id2var(id2var, fmls);
pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e); pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e);
grobner g(m.limit(), p); solver g(m.limit(), p);
for (expr* e : subterms(fmls)) { for (expr* e : subterms(fmls)) {
add_def(id2var, to_app(e), m, p, g); add_def(id2var, to_app(e), m, p, g);