on #4702

Add weighting function to cycle more fairly through nla solvers.
Handles anomaly from https://github.com/Z3Prover/z3/files/5361721/pero.txt

src/math/lp/nla_core.cpp

@@ -10,6 +10,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+#include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
 #include "math/lp/nex.h"
@@ -1452,6 +1453,31 @@ bool core::integrality_holds() {
     return false;
 }
 
+/**
+ * Cycle through different end-game solvers weighted by probability.
+ */
+void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks) {
+    unsigned bound = 0;
+    for (unsigned i = 0; i < sz; ++i) 
+        bound += checks[i].first;
+    uint_set seen;
+    while (bound > 0 && !done() && m_lemma_vec->empty()) {
+        SASSERT(bound > 0);
+        unsigned n = random() % bound;
+        for (unsigned i = 0; i < sz; ++i) {
+            if (seen.contains(i))
+                continue;
+            if (n < checks[i].first) {
+                seen.insert(i);
+                checks[i].second();
+                bound -= n;
+                break;
+            }
+            n -= checks[i].first;
+        }
+    }
+}
+
 
 lbool core::check(vector<lemma>& l_vec) {
     lp_settings().stats().m_nla_calls++;
@@ -1487,14 +1513,16 @@ lbool core::check(vector<lemma>& l_vec) {
     if (l_vec.empty() && !done()) 
         m_basics.basic_lemma(false);
 
-    if (l_vec.empty() && !done()) 
-        m_order.order_lemma();    
-
     if (l_vec.empty() && !done()) {
-        if (!done())
-            m_monotone.monotonicity_lemma();
-        if (!done())
-            m_tangents.tangent_lemma();
+        std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
+        std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma(); };
+        std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma(); };
+        
+        std::pair<unsigned, std::function<void(void)>> checks[] = 
+            { { 6, check1 }, 
+              { 2, check2 }, 
+              { 1, check3 }};
+        check_weighted(3, checks);
     }
 
     if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {

src/math/lp/nla_core.h

@@ -178,6 +178,9 @@ private:
     bool                     m_cautious_patching;
     lpvar                    m_patched_var;
     monic const*             m_patched_monic;      
+
+    void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
+
 public:    
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);