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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-20 22:02:01 -08:00
parent 90ca594835
commit f977e1a3e2
1 changed files with 0 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
chores.txt
View file

@ -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<rational (unsigned)> m_var2val;
public:
pdd_eval(pdd_manager& m): m(m) {}
void operator=(std::function<rational (unsigned)>& 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<interval (unsigned)> m_var2interval;
public:
pdd_interval(pdd_manager& m, reslimit& lim): m(m) m_intervals(lim) {}
void operator=(std::function<interval (unsigned)>& 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.