mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
initial unit test for pdd_grobner
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
3fca59ac84
commit
58be42d2a9
6 changed files with 104 additions and 34 deletions
|
|
@ -761,7 +761,7 @@ namespace dd {
|
|||
first = false;
|
||||
rational c = abs(m.first);
|
||||
m.second.reverse();
|
||||
if (!c.is_one()) {
|
||||
if (!c.is_one() || m.second.empty()) {
|
||||
out << c;
|
||||
if (!m.second.empty()) out << "*";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -112,16 +112,15 @@ namespace dd {
|
|||
bool grobner::basic_step() {
|
||||
equation* e = pick_next();
|
||||
if (!e) return false;
|
||||
scoped_detach sd(*this, e);
|
||||
equation& eq = *e;
|
||||
TRACE("grobner", display(tout << "eq = ", eq); display(tout););
|
||||
SASSERT(!eq.is_processed());
|
||||
if (!simplify_using(eq, m_processed)) return false;
|
||||
if (eliminate(eq)) return true;
|
||||
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
|
||||
if (check_conflict(eq)) return false;
|
||||
if (!simplify_using(m_processed, eq)) return false;
|
||||
TRACE("grobner", tout << "eq = "; display_equation(tout, eq););
|
||||
superpose(eq);
|
||||
eq.set_processed(true);
|
||||
m_processed.push_back(e);
|
||||
return simplify_using(m_to_simplify, eq);
|
||||
}
|
||||
|
||||
|
|
@ -156,7 +155,7 @@ namespace dd {
|
|||
*/
|
||||
bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
|
||||
bool simplified, changed_leading_term;
|
||||
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of size " << eqs.size() << "\n";);
|
||||
TRACE("grobner", display(tout << "simplifying: ", eq); tout << "using equalities of size " << eqs.size() << "\n";);
|
||||
do {
|
||||
simplified = false;
|
||||
for (equation* p : eqs) {
|
||||
|
|
@ -170,7 +169,7 @@ namespace dd {
|
|||
}
|
||||
while (simplified && !eq.poly().is_val());
|
||||
|
||||
TRACE("grobner", tout << "simplification result: "; display_equation(tout, eq););
|
||||
TRACE("grobner", display(tout << "simplification result: ", eq););
|
||||
|
||||
check_conflict(eq);
|
||||
return !done();
|
||||
|
|
@ -209,12 +208,12 @@ namespace dd {
|
|||
bool grobner::simplify_source_target(equation const& source, equation& target, bool& changed_leading_term) {
|
||||
TRACE("grobner", tout << "simplifying: " << target.poly() << "\nusing: " << source.poly() << "\n";);
|
||||
m_stats.m_simplified++;
|
||||
pdd t = target.poly();
|
||||
pdd r = source.poly().reduce(t);
|
||||
if (r == source.poly() || is_too_complex(r)) {
|
||||
pdd t = source.poly();
|
||||
pdd r = target.poly().reduce(t);
|
||||
if (r == target.poly() || is_too_complex(r)) {
|
||||
return false;
|
||||
}
|
||||
changed_leading_term = target.is_processed() && m.different_leading_term(r, source.poly());
|
||||
changed_leading_term = target.is_processed() && m.different_leading_term(r, target.poly());
|
||||
target = r;
|
||||
target = m_dep_manager.mk_join(target.dep(), source.dep());
|
||||
update_stats_max_degree_and_size(target);
|
||||
|
|
@ -230,7 +229,7 @@ namespace dd {
|
|||
let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
|
||||
*/
|
||||
bool grobner::superpose(equation const& eq1, equation const& eq2) {
|
||||
TRACE("grobner_d", tout << "eq1="; display_equation(tout, eq1) << "eq2="; display_equation(tout, eq2););
|
||||
TRACE("grobner_d", tout << "eq1="; display(tout, eq1) << "eq2="; display(tout, eq2););
|
||||
pdd r(m);
|
||||
if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return false;
|
||||
m_stats.m_superposed++;
|
||||
|
|
@ -242,29 +241,28 @@ namespace dd {
|
|||
bool grobner::tuned_step() {
|
||||
equation* e = tuned_pick_next();
|
||||
if (!e) return false;
|
||||
scoped_detach sd(*this, e);
|
||||
equation& eq = *e;
|
||||
SASSERT(!m_watch[eq.poly().var()].contains(e));
|
||||
SASSERT(!eq.is_processed());
|
||||
if (!simplify_using(eq, m_processed)) return false;
|
||||
if (eliminate(eq)) return true;
|
||||
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
|
||||
if (check_conflict(eq)) return false;
|
||||
if (!simplify_using(m_processed, eq)) return false;
|
||||
TRACE("grobner", tout << "eq = "; display_equation(tout, eq););
|
||||
TRACE("grobner", tout << "eq = "; display(tout, eq););
|
||||
superpose(eq);
|
||||
eq.set_processed(true);
|
||||
m_processed.push_back(e);
|
||||
return simplify_to_simplify(eq);
|
||||
}
|
||||
|
||||
void grobner::tuned_init() {
|
||||
// TBD: extract free variables, order them, set pointer into variable list.
|
||||
NOT_IMPLEMENTED_YET();
|
||||
m_watch.reserve(m_vars.size());
|
||||
m_watch.reserve(m_level2var.size());
|
||||
m_levelp1 = m_level2var.size();
|
||||
for (equation* eq : m_to_simplify) add_to_watch(*eq);
|
||||
SASSERT(m_processed.empty());
|
||||
}
|
||||
|
||||
// watch top variable
|
||||
void grobner::add_to_watch(equation& eq) {
|
||||
SASSERT(!eq.is_processed());
|
||||
pdd const& p = eq.poly();
|
||||
|
|
@ -274,12 +272,12 @@ namespace dd {
|
|||
}
|
||||
|
||||
bool grobner::simplify_to_simplify(equation const& eq) {
|
||||
unsigned v = m_vars[m_var];
|
||||
unsigned v = eq.poly().var();
|
||||
auto& watch = m_watch[v];
|
||||
unsigned j = 0;
|
||||
for (equation* _target : watch) {
|
||||
equation& target = *_target;
|
||||
if (target.is_processed()) continue;
|
||||
SASSERT(!target.is_processed());
|
||||
bool changed_leading_term = false;
|
||||
bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
|
||||
if (simplified && is_trivial(target)) {
|
||||
|
|
@ -299,8 +297,8 @@ namespace dd {
|
|||
}
|
||||
|
||||
grobner::equation* grobner::tuned_pick_next() {
|
||||
while (m_var < m_vars.size()) {
|
||||
unsigned v = m_vars[m_var];
|
||||
while (m_levelp1 > 0) {
|
||||
unsigned v = m_level2var[m_levelp1-1];
|
||||
equation_vector const& watch = m_watch[v];
|
||||
equation* eq = nullptr;
|
||||
for (equation* curr : watch) {
|
||||
|
|
@ -315,7 +313,7 @@ namespace dd {
|
|||
m_watch[eq->poly().var()].erase(eq);
|
||||
return eq;
|
||||
}
|
||||
++m_var;
|
||||
--m_levelp1;
|
||||
}
|
||||
return nullptr;
|
||||
}
|
||||
|
|
@ -340,7 +338,9 @@ namespace dd {
|
|||
if (p.is_zero()) return;
|
||||
equation * eq = alloc(equation, p, dep, m_to_simplify.size());
|
||||
m_to_simplify.push_back(eq);
|
||||
check_conflict(*eq);
|
||||
if (!check_conflict(*eq) && is_tuned()) {
|
||||
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
|
||||
}
|
||||
update_stats_max_degree_and_size(*eq);
|
||||
}
|
||||
|
||||
|
|
@ -384,15 +384,15 @@ namespace dd {
|
|||
st.update("size", m_stats.m_max_expr_size);
|
||||
}
|
||||
|
||||
std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const {
|
||||
out << "expr = " << eq.poly() << "\n";
|
||||
m_print_dep(eq.dep(), out);
|
||||
std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
|
||||
out << eq.poly() << "\n";
|
||||
if (m_print_dep) m_print_dep(eq.dep(), out);
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& grobner::display(std::ostream& out) const {
|
||||
out << "processed\n"; for (auto e : m_processed) display_equation(out, *e);
|
||||
out << "to_simplify\n"; for (auto e : m_to_simplify) display_equation(out, *e);
|
||||
out << "processed\n"; for (auto e : m_processed) display(out, *e);
|
||||
out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
|
||||
statistics st;
|
||||
collect_statistics(st);
|
||||
st.display(out);
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ public:
|
|||
unsigned m_superposed;
|
||||
unsigned m_compute_steps;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
stats() { reset(); }
|
||||
};
|
||||
|
||||
struct config {
|
||||
|
|
@ -50,7 +51,6 @@ public:
|
|||
{}
|
||||
};
|
||||
|
||||
private:
|
||||
class equation {
|
||||
bool m_processed; //!< state
|
||||
unsigned m_idx; //!< unique index
|
||||
|
|
@ -73,6 +73,7 @@ private:
|
|||
void set_processed(bool p) { m_processed = p; }
|
||||
void set_index(unsigned idx) { m_idx = idx; }
|
||||
};
|
||||
private:
|
||||
|
||||
typedef ptr_vector<equation> equation_vector;
|
||||
typedef std::function<void (u_dependency* d, std::ostream& out)> print_dep_t;
|
||||
|
|
@ -95,7 +96,8 @@ public:
|
|||
void operator=(config const& c) { m_config = c; }
|
||||
|
||||
void reset();
|
||||
void add(pdd const&, u_dependency * dep);
|
||||
void add(pdd const& p) { add(p, nullptr); }
|
||||
void add(pdd const& p, u_dependency * dep);
|
||||
|
||||
void saturate();
|
||||
|
||||
|
|
@ -103,7 +105,7 @@ public:
|
|||
u_dependency_manager& dep() const { return m_dep_manager; }
|
||||
|
||||
void collect_statistics(statistics & st) const;
|
||||
std::ostream& display_equation(std::ostream& out, const equation& eq) const;
|
||||
std::ostream& display(std::ostream& out, const equation& eq) const;
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
private:
|
||||
|
|
@ -129,8 +131,9 @@ private:
|
|||
|
||||
// tuned implementation
|
||||
vector<equation_vector> m_watch; // watch list mapping variables to vector of equations where they occur (generally a subset)
|
||||
unsigned m_var; // index into vars with current variable
|
||||
unsigned_vector m_vars; // variables sorted by priority, higher priority first.
|
||||
unsigned m_levelp1; // index into level+1
|
||||
unsigned_vector m_level2var; // level -> var
|
||||
unsigned_vector m_var2level; // var -> level
|
||||
|
||||
bool tuned_step();
|
||||
void tuned_init();
|
||||
|
|
@ -146,6 +149,18 @@ private:
|
|||
void push_equation(equation& eq, equation_vector& v);
|
||||
|
||||
void invariant() const;
|
||||
struct scoped_detach {
|
||||
grobner& g;
|
||||
equation* e;
|
||||
scoped_detach(grobner& g, equation* e): g(g), e(e) {}
|
||||
~scoped_detach() {
|
||||
if (e) {
|
||||
e->set_processed(true);
|
||||
e->set_index(g.m_processed.size());
|
||||
g.m_processed.push_back(e);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void update_stats_max_degree_and_size(const equation& e);
|
||||
bool is_tuned() const { return m_config.m_algorithm == config::tuned; }
|
||||
|
|
|
|||
|
|
@ -83,6 +83,7 @@ add_executable(test-z3
|
|||
parray.cpp
|
||||
pb2bv.cpp
|
||||
pdd.cpp
|
||||
pdd_grobner.cpp
|
||||
permutation.cpp
|
||||
polynomial.cpp
|
||||
polynorm.cpp
|
||||
|
|
|
|||
|
|
@ -254,6 +254,7 @@ int main(int argc, char ** argv) {
|
|||
TST_ARGV(cnf_backbones);
|
||||
TST(bdd);
|
||||
TST(pdd);
|
||||
TST(pdd_grobner);
|
||||
TST(solver_pool);
|
||||
//TST_ARGV(hs);
|
||||
}
|
||||
|
|
|
|||
53
src/test/pdd_grobner.cpp
Normal file
53
src/test/pdd_grobner.cpp
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
#include "util/rlimit.h"
|
||||
#include "math/grobner/pdd_grobner.h"
|
||||
|
||||
namespace dd {
|
||||
void print_eqs(ptr_vector<grobner::equation> const& eqs) {
|
||||
std::cout << "eqs\n";
|
||||
for (grobner::equation* e : eqs) {
|
||||
std::cout << e->poly() << "\n";
|
||||
}
|
||||
}
|
||||
void test1() {
|
||||
pdd_manager m(4);
|
||||
reslimit lim;
|
||||
pdd v0 = m.mk_var(0);
|
||||
pdd v1 = m.mk_var(1);
|
||||
pdd v2 = m.mk_var(2);
|
||||
pdd v3 = m.mk_var(3);
|
||||
|
||||
grobner gb(lim, m);
|
||||
gb.add(v1*v2 + v1*v3);
|
||||
gb.add(v1 - 1);
|
||||
print_eqs(gb.equations());
|
||||
gb.saturate();
|
||||
print_eqs(gb.equations());
|
||||
gb.reset();
|
||||
|
||||
gb.add(v1*v1*v2 + v2*v3);
|
||||
gb.add(v1*v1*v2 + v2*v1);
|
||||
gb.saturate();
|
||||
print_eqs(gb.equations());
|
||||
gb.reset();
|
||||
|
||||
gb.add(v1*v1*v2 + v2*v1);
|
||||
gb.add(v1*v1*v2 + v2*v1);
|
||||
gb.saturate();
|
||||
print_eqs(gb.equations());
|
||||
gb.reset();
|
||||
|
||||
gb.add(v1*v3*v3 + v3*v1 + 2);
|
||||
gb.add(v1*v3*v3 + v3*v1);
|
||||
gb.add(v3*v1 + v1*v2 + v2*v3);
|
||||
gb.add(v3*v1 + v1*v2 + v2*v3 + v1);
|
||||
gb.add(v3*v1 + v1*v2 + v2*v3 + v2);
|
||||
gb.saturate();
|
||||
print_eqs(gb.equations());
|
||||
gb.reset();
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
void tst_pdd_grobner() {
|
||||
dd::test1();
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue