feat(library/unifier): divide constraints in clear groups

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/unifier.cpp

@@ -197,8 +197,36 @@ std::pair<unify_status, substitution> unify_simple(substitution const & s, const
 }
 
 static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
-static unsigned g_first_delayed      = 1u << 28;
+
-static unsigned g_first_very_delayed = 1u << 30;
+/**
+    The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, Reduction, FlexFlex, DelayedChoice
+
+    1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
+       The are not even inserted in the constraint priority queue.
+
+    2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints
+       that cannot be solved, and the unification plugin must be invoked.
+
+    3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application
+
+    4) Reduction: contraints such (elim ... (?m ...)) and (?m ... (intro ...)), where elim is an eliminator/recursor and
+       intro is an introduction/constructor. This constraints are delayed because after ?m is assigned we may be able
+       to reduce them.
+
+    5) FlexFlex:  (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
+       ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
+       we simply discard it.
+
+    6) DelayedChoice: delayed choice constraints, they are used to model features such as class-instance
+       They are really term synthesizers. We use the unifier just to exploit the non-chronological backtracking
+       infrastructure
+*/
+enum class cnstr_group { Basic = 0, FlexRigid, Reduction, FlexFlex, DelayedChoice };
+static unsigned g_group_size = 1u << 28;
+static unsigned g_cnstr_group_first_index[5] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size};
+static unsigned get_group_first_index(cnstr_group g) {
+    return g_cnstr_group_first_index[static_cast<unsigned>(g)];
+}
 
 /** \brief Auxiliary functional object for implementing simultaneous higher-order unification */
 struct unifier_fn {
@@ -448,29 +476,13 @@ struct unifier_fn {
     }
 
     /** \brief Add constraint to the constraint queue */
-    void add_cnstr(constraint const & c, name_set const * mlvl_occs, name_set const * mvar_occs, unsigned start_cidx = 0) {
+    void add_cnstr(constraint const & c, name_set const * mlvl_occs, name_set const * mvar_occs, cnstr_group g) {
-        unsigned cidx = m_next_cidx + start_cidx;
+        unsigned cidx = m_next_cidx + get_group_first_index(g);
         m_cnstrs.insert(cnstr(c, cidx));
         add_occs(cidx, mlvl_occs, mvar_occs);
         m_next_cidx++;
     }
 
-    /**
-        \brief Add (delayed) constraint to the constraint queue. Delayed constraints are processed after regular constraints
-        added with \c add_cnstr
-    */
-    void add_delayed_cnstr(constraint const & c, name_set const * mlvl_occs, name_set const * mvar_occs) {
-        add_cnstr(c, mlvl_occs, mvar_occs, g_first_delayed);
-    }
-
-    /**
-       \brief Add (very delayed) constraint to the constraint queue. Very delayed constraints are processed after
-       regular and delayed constraints added with \c add_cnstr and \c add_delayed_cnstr.
-    */
-    void add_very_delayed_cnstr(constraint const & c, name_set const * mlvl_occs, name_set const * mvar_occs) {
-        add_cnstr(c, mlvl_occs, mvar_occs, g_first_very_delayed);
-    }
-
     bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
         if (m_tc.is_def_eq(t1, t2, j)) {
             return true;
@@ -595,16 +607,16 @@ struct unifier_fn {
 
         // We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
         if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs) || is_meta_intro_app(lhs) || is_meta_intro_app(rhs)) {
-            add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
+            add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::Reduction);
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
-            add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
+            add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::FlexFlex);
         } else if (is_meta(lhs) || is_meta(rhs)) {
             // flex-rigid constraints are delayed.
-            add_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
+            add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::FlexRigid);
         } else {
             // this constraints require the unifier plugin to be solved
-            add_cnstr(c, &unassigned_lvls, &unassigned_exprs);
+            add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::Basic);
         }
         return true;
     }
@@ -668,9 +680,9 @@ struct unifier_fn {
 
         if (lhs != cnstr_lhs_level(c) || rhs != cnstr_rhs_level(c)) {
             constraint new_c = mk_level_eq_cnstr(lhs, rhs, new_jst);
-            add_delayed_cnstr(new_c, &unassigned_lvls, nullptr);
+            add_cnstr(new_c, &unassigned_lvls, nullptr, cnstr_group::FlexRigid);
         } else {
-            add_delayed_cnstr(c, &unassigned_lvls, nullptr);
+            add_cnstr(c, &unassigned_lvls, nullptr, cnstr_group::FlexRigid);
         }
 
         return true;
@@ -689,9 +701,9 @@ struct unifier_fn {
         case constraint_kind::Choice:
             // Choice constraints are never considered easy.
             if (cnstr_delayed(c))
-                add_very_delayed_cnstr(c, nullptr, nullptr);
+                add_cnstr(c, nullptr, nullptr, cnstr_group::DelayedChoice);
             else
-                add_cnstr(c, nullptr, nullptr);
+                add_cnstr(c, nullptr, nullptr, cnstr_group::Basic);
             return true;
         case constraint_kind::Eq:
             return process_eq_constraint(c);