updated notes, fixes to dual solver

src/ast/euf/euf_egraph.cpp

@@ -19,36 +19,63 @@ Each node has a congruence closure root, cg.
 cg is set to the representative in the cc table 
 (first insertion of congruent node).
 Each node n has a set of parents, denoted n.P.
+The table maintains the invariant
+ - p.cg = find(p)
 
-set r2 to the root of r1:
+Merge sets r2 to the root of r1 
+(r2 and r1 are both considered roots before the merge).
+The operation Unmerge reverses the effect of Merge.
 
-Merge:  Erase:
-            for each p r1.P such that p.cg == p:
-              erase from table
-        Update root:
-            r1.root := r2
-        Insert:
-            for each p in r1.P:
+
+Merge(r1, r2)
+-------------
+
+Erase:        for each p in r1.P such that p.cg == p:
+                 erase from table        
+Update root:  r1.root := r2
+Insert:       for each p in r1.P:
                  p.cg = insert p in table
                  if p.cg == p:
                    append p to r2.P
                  else 
-                   add p.cg, p to worklist
+                   add (p.cg == p) to 'to_merge' 
 
-Unmerge:  Erase:
-             for each p in added nodes:
-                erase p from table 
-          Revert root:
-             r1.root := r1
-          Insert:
-             for each p in r1.P:
-                insert p if n was cc root before merge
+Unmerge(r1, r2)
+---------------
+
+Erase:        for each p in r2.P added from r1.P:
+                 erase p from table 
+Revert root:  r1.root := r1
+Insert:       for each p in r1.P:
+                 insert p if n was cc root before merge
 
 condition for being cc root before merge:
-  p->cg == p
-  congruent(p, p->cg)
+  p.cg == p or !congruent(p, p.cg)
 
-congruent(p,q) := roots of p.children = roots of q.children
+congruent(p,q) := roots of p.args = roots of q.args
+
+The algorithm orients r1, r2 such that class_size(r1) <= class_size(r2).
+With N nodes, there can be at most N calls to Merge.
+Each of the calls traverse r1.P from the smaller class size.
+Label a merge tree with nodes from the larger class size.
+In other words, if Merge(r2,r1); Merge(r3,r1) is a sequence
+of calls where r1 is selected root, then the merge tree is
+
+    r1 
+  /   \
+ r1    r3  
+   \
+   r2
+
+Note that parent lists are re-examined only for nodes that join
+from right subtrees (with lesser class sizes).
+Claim: a node participates in a path along right adjoining sub-trees at most O(log(N)) times.
+Justification (very roughly): the size of a right adjoining subtree can at most 
+be equal to the left adjoining sub-tree. This entails a logarithmic number of 
+re-examinations from the right adjoining tree.
+(TBD check how Hopcroft's main argument is phrased)
+
+The parent lists are bounded by the maximal arity of functions.
 
 Example:
 
@@ -491,14 +518,9 @@ namespace euf {
     bool egraph::propagate() {
         SASSERT(m_new_lits_qhead <= m_new_lits.size());
         SASSERT(m_num_scopes == 0 || m_to_merge.empty());
-        unsigned head = 0, tail = m_to_merge.size();
-        while (head < tail && m.limit().inc() && !inconsistent()) {
-            for (unsigned i = head; i < tail && !inconsistent(); ++i) {
-                auto const& w = m_to_merge[i];
-                merge(w.a, w.b, justification::congruence(w.commutativity));                
-            }
-            head = tail;
-            tail = m_to_merge.size();
+        for (unsigned i = 0; i < m_to_merge.size() && m_limit().inc() && !inconsistent(); ++i) {
+            auto const& w = m_to_merge[i];
+            merge(w.a, w.b, justification::congruence(w.commutativity));                
         }
         m_to_merge.reset();
         force_push();

src/math/lp/int_gcd_test.cpp

@@ -13,7 +13,35 @@ Author:
     Nikolaj Bjorner (nbjorner)
     Lev Nachmanson (levnach)
 
-Revision History:
+Notes:
+
+Basic:
+    For each row a*x + b = 0, where fixed variables are replaced by b, 
+    check if gcd(a) divides b 
+
+Extended:
+    For each row a*x + b*y + c = 0, where 
+    - the coefficients in a are all the same and smaller than the coefficients in b
+    - the variables x are bounded
+    Let l := a*lb(x), u := a*ub(x)
+    - that is the lower and upper bounds for a*x based on the bounds for x.
+    let ll := ceil  (l / gcd(b,c))
+        uu := floor (u / gcd(b,c))
+    If uu > ll, there is no space to find solutions for x within the bounds
+
+Accumulative:
+    For each row a*x + b*y - c = 0, where |a| = 1 < |b|, and x is a single variable,
+    (it could also be a group of variables) accumulate constraint x = c mod b
+
+    If there are row gcd constraints, such that 
+    - x = c1 mod b1, from rows R1
+    - x = c2 mod b2, from rows R2
+    
+    - If c1 mod gcd(b1,b2) != c2 mod gcd(b1,b2) report conflict for the rows involved.
+   
+    - Otherwise accumulate x = (c1 * lcm(b1,b2) / b2) + (c2 * lcm(b1,b2) / b1) mod lcm(b,b2)
+      and accumulate the rows from R1, R2
+
 --*/
 
 #include "math/lp/int_solver.h"
@@ -28,15 +56,7 @@ namespace lp {
 
         if (!lia.settings().int_run_gcd_test())
             return false;
-#if 1
         return true;
-#else
-        if (m_delay == 0) {
-            return true;
-        }
-        --m_delay;
-        return false;
-#endif
     }
 
     lia_move int_gcd_test::operator()() {              

src/sat/smt/sat_dual_solver.cpp

@@ -24,22 +24,19 @@ namespace sat {
 
     void dual_solver::push() {
         m_solver.user_push(); 
-        m_roots_lim.push_back(m_roots.size());     
-        m_tracked_lim.push_back(m_tracked_stack.size());
-        m_units_lim.push_back(m_units.size());
+        m_roots.push_scope();
+        m_tracked_vars.push_scope();
+        m_units.push_scope();
     }
 
     void dual_solver::pop(unsigned num_scopes) {
         m_solver.user_pop(num_scopes);
-        unsigned old_sz = m_roots_lim.size() - num_scopes;
-        for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; ) 
-            m_is_tracked[v] = false; 
-        m_roots.shrink(m_roots_lim[old_sz]);
-        m_tracked_stack.shrink(m_tracked_lim[old_sz]);
-        m_units.shrink(m_units_lim[old_sz]);
-        m_roots_lim.shrink(old_sz);
-        m_tracked_lim.shrink(old_sz);
-        m_units_lim.shrink(old_sz);
+        unsigned old_sz = m_tracked_vars.old_size(num_scopes);
+        for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
+            m_is_tracked[m_tracked_vars[i]] = false; 
+        m_units.pop_scope(num_scopes);
+        m_roots.pop_scope(num_scopes);
+        m_tracked_vars.pop_scope(num_scopes);
     }
 
     bool_var dual_solver::ext2var(bool_var v) {
@@ -56,7 +53,7 @@ namespace sat {
         v = ext2var(v);
         if (!m_is_tracked.get(v, false)) {
             m_is_tracked.setx(v, true, false);
-            m_tracked_stack.push_back(v);
+            m_tracked_vars.push_back(v);
         }
     }
 
@@ -69,6 +66,10 @@ namespace sat {
     }
 
     void dual_solver::add_root(unsigned sz, literal const* clause) {
+        if (sz == 1) {
+            m_units.push_back(clause[0]);
+            return;
+        }
         literal root(m_solver.mk_var(), false);
         for (unsigned i = 0; i < sz; ++i)
             m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
@@ -86,7 +87,7 @@ namespace sat {
         m_solver.user_push();
         m_solver.add_clause(m_roots.size(), m_roots.c_ptr(), status::input());
         m_lits.reset();
-        for (bool_var v : m_tracked_stack)
+        for (bool_var v : m_tracked_vars)
             m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
         lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
         m_core.reset();

src/sat/smt/sat_dual_solver.h

@@ -8,6 +8,8 @@ Module Name:
 Abstract:
 
     Solver for obtaining implicant.
+    Based on an idea by Armin Biere to use dual propagation 
+    for representation of negated goal.
 
 Author:
 
@@ -15,18 +17,19 @@ Author:
 
 --*/
 #pragma once
+#include "util/lim_vector.h"
 #include "sat/sat_solver.h"
 
 namespace sat {
 
     class dual_solver {
         solver          m_solver;
-        literal_vector  m_roots, m_lits, m_core, m_units;
+        lim_svector<literal> m_units, m_roots;
+        lim_svector<bool_var> m_tracked_vars;
+        literal_vector  m_lits, m_core;
         bool_var_vector m_is_tracked;
-        unsigned_vector m_tracked_stack;
         unsigned_vector m_ext2var;
         unsigned_vector m_var2ext;
-        unsigned_vector m_roots_lim, m_tracked_lim, m_units_lim;
         void add_literal(literal lit);
 
         bool_var ext2var(bool_var v);

src/util/lim_vector.h

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    lim_vector.h
+
+Abstract:
+
+    Vector that restores during backtracking.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-29-09
+
+--*/
+#pragma once
+
+#include "util/vector.h"
+
+template<typename T>
+class lim_svector : public svector<T> {
+    unsigned_vector  m_lim;
+public:
+    lim_svector() {}
+
+    void push_scope() {
+        m_lim.push_back(size());
+    }
+
+    void pop_scope(unsigned num_scopes) {
+        SASSERT(num_scopes > 0);
+        unsigned old_sz = m_lim.size() - num_scopes;
+        shrink(m_lim[old_sz]);
+        m_lim.shrink(old_sz);
+    }
+
+    unsigned num_scopes() const { return m_lim.size(); }
+
+    unsigned old_size(unsigned n) const { return m_lim[m_lim.size() - n]; }
+};
+