diff --git a/chores.txt b/chores.txt deleted file mode 100644 index b699447e7..000000000 --- a/chores.txt +++ /dev/null @@ -1,52 +0,0 @@ - -1. expand unit test for pdd to test the exposed functionality -2. develop nla bridge to pdd_grobner, similar to how grobner wraps - around grobner_core in nla_grobner -3. self-contained unit test for pdd_grobner -4. examine perf / memory for latest rebase. - Possibly nla2bv is used more, but could take resources in the sat solver. - We can put some limits on sat solver by configuring sat.max_conflicts. - -Details: - -1.1 test tree_size, dag_size, degree -1.2 test out of memory scenarios (already tested for - dd_bdd and code is similar) -1.3 tests for reduce (expose bugs with small examples) -1.4 tests for spoly - -2.1 add an eval module for pdd. Sample signature: - class pdd_eval { - pdd_manager& m; - std::function m_var2val; - public: - pdd_eval(pdd_manager& m): m(m) {} - void operator=(std::function& v2v) { m_var2val = v2i; } - rational operator()(pdd const& p); - }; -2.2 disentangle nla_intervals into dep_intervals + nla_intervals - (which uses dep_intervals and provides services for nex/lar_solver). -2.3 add interval module for pdd. Sample signature: - - typedef dep_intervals::interval interval; - - class pdd_interval { - pdd_manager& m; - dep_intervals m_intervals; - std::function m_var2interval; - public: - pdd_interval(pdd_manager& m, reslimit& lim): m(m) m_intervals(lim) {} - void operator=(std::function& v2i) { m_var2interval = v2i; } - interval operator()(pdd const& p); - bool separated_from_zero(pdd const& p, u_dependency*& dep) { return m_intervals.separated_from_zero((*this)(p), dep); } - }; - -2.4 port other code from nla::grobner class to wrap around grobner -2.5 review pdd_grobner for feature compatibility with grobner_core - There are two modes for pdd_grobner: basic and tuned. basic is similar to nla_grobner. - tuned is going to be full of implementation and some conceptual bugs. It is somewhat mild extension over base - so debugging it should be doable. - - -3.1 unit tests for pdd_grobner. Maybe I take a stab at this as a starting point. -