From 857f25f54a6267763b2f9a23dd82220fa031d583 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 21 Jul 2023 15:54:28 +0200 Subject: [PATCH] add notes --- src/math/polysat/slicing.cpp | 17 +++++++++++++++++ src/math/polysat/slicing.h | 8 +++++--- src/math/polysat/viable.cpp | 24 ++++++++++++++++++++++++ 3 files changed, 46 insertions(+), 3 deletions(-) diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 24fa325ac..cecfb95cc 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -39,6 +39,9 @@ TODO: better conflicts with pvar justification - when explaining a conflict that contains pvars: - single pvar x: the egraph has derived that x must have a different value c, learn literal x = c (instead of x != value(x) as is done now by the naive integration) - two pvars x, y: learn literal x = y + - (this is basically what Algorithm 1 of "Solving Bitvectors with MCSAT" does) + +- then check Algorithm 2 of "Solving Bitvectors with MCSAT"; what is the difference to what we are doing now? */ @@ -548,6 +551,10 @@ namespace polysat { end_explain(); } + clause_ref slicing::conflict_clause() { + NOT_IMPLEMENTED_YET(); // TODO: call explain and build clause as described in notes at the top + } + void slicing::egraph_on_propagate(enode* lit, enode* ante) { // ante may be set when symmetric equality is added by congruence if (ante) @@ -844,6 +851,16 @@ namespace polysat { (void)merge(sv, sval, v); } + void slicing::collect_overlaps(pvar v, var_overlap_vector& out) { + // - start at var2slice(v) + // - go into subslices, always starting at lowest ones + // - when we find multiple overlaps, we want to merge them: keep a map for this. + // (but note that there can be "holes" in the overlap. by starting at lsb, process overlaps in order low->high. so when we encounter a hole that should mean the overlap is "done" and replace it with the new one in the map.) + // - at each slice: iterate over equivalence class, check if it has a variable as parent (usually it would be the root of the parent-pointers. maybe we should cache a pointer to the next variable-enode, instead of keeping all the parents.) + // - use enode->mark1/2/3 to process each node only once + NOT_IMPLEMENTED_YET(); + } + std::ostream& slicing::display(std::ostream& out) const { enode_vector base; for (pvar v = 0; v < m_var2slice.size(); ++v) { diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index cb84e4453..cbd2f90d2 100644 --- a/src/math/polysat/slicing.h +++ b/src/math/polysat/slicing.h @@ -271,6 +271,8 @@ namespace polysat { /** Extract reason for conflict */ void explain(sat::literal_vector& out_lits, unsigned_vector& out_vars); + /** Extract conflict clause */ + clause_ref conflict_clause(); /** Extract reason for x == y */ void explain_equal(pvar x, pvar y, sat::literal_vector& out_lits, unsigned_vector& out_vars); @@ -290,10 +292,10 @@ namespace polysat { using var_overlap_vector = svector; /** For a given variable v, find the set of variables that share at least one slice with v. */ - void query_overlaps(pvar v, var_overlap_vector& out); + void collect_overlaps(pvar v, var_overlap_vector& out); - /** Query fixed portions of the variable v */ - void query_fixed(pvar v, rational& mask, rational& value); + /** Collect fixed portions of the variable v */ + void collect_fixed(pvar v, rational& mask, rational& value); std::ostream& display(std::ostream& out) const; std::ostream& display_tree(std::ostream& out) const; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 3820eac37..c3cfb67d8 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1554,6 +1554,30 @@ namespace { if (!collect_bit_information(v, true, fixed, justifications)) return l_false; // conflict already added + slicing::var_overlap_vector overlaps; + s.m_slicing.collect_overlaps(v, overlaps); + // TODO: (combining intervals across equivalence classes from slicing) + // + // When iterating over intervals: + // - instead of only intervals of v, go over intervals of each entry of overlaps + // - need a function to map interval from overlap into an interval over v + // + // Maybe combine only the "simple" overlaps in this method, and do the more comprehensive queries on demand, during conflict resolution (saturation.cpp). + // Here, we should handle at least: + // - direct equivalences (x = y); could just point one interval set to the other and store them together (may be annoying for bookkeeping) + // - lower bits extractions (x[h:0]) and equivalent slices; + // (this is what Algorithm 3 in "Solving Bitvectors with MCSAT" does, and will also let us better handle even coefficients of inequalities). + // + // Problem: + // - we want to iterate intervals in order. do we then need to perform the mapping in advance? (monotonic mapping -> only first one needs to be mapped in advance) + // - should have some "cursor" class which abstracts the prev/next operation. + // + // (in addition to slices, some intervals may transfer by other operations. e.g. x = -y. but maybe it's better to handle these cases on demand by saturation.cpp) + // + // Refinement: + // - is done when we find a "feasible" point, so not directly affected by changes to the algorithm. + // - we don't know which constraint yields the "best" interval, so keep interleaving constraints + // max number of interval refinements before falling back to the univariate solver unsigned const refinement_budget = 1000; unsigned refinements = refinement_budget;