add notes

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<pvar, var_overlap> 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) {

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<var_overlap>;
 
         /** 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;

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;