fixup scoring function for sle and ule

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/sls/sls_bv_lookahead.cpp

@@ -81,7 +81,7 @@ namespace sls {
                 continue;
 
             // bail out if no progress, and try random update
-            if (apply_random_update(get_candidate_uninterp()))
+            if (apply_random_update(m_config.walksat_repick?get_candidate_uninterp():vars))
                 recalibrate_weights();
         }
         m_config.max_moves_base += 100;
@@ -379,18 +379,24 @@ namespace sls {
             auto const& vx = wval(x);
             auto const& vy = wval(y);
 
-            if (is_true)
+            if (is_true) {
+                if (vx.bits() <= vy.bits())
+                    return 1.0;
                 // x > y as unsigned.
                 // x - y > 0
                 // score = (x - y) / 2^bw
                 vx.set_sub(m_ev.m_tmp, vx.bits(), vy.bits());
+            }
             else {
+                if (!(vx.bits() <= vy.bits()))
+                    return 1.0;
                 // x <= y as unsigned.
                 // y - x >= 0
                 // score = (y - x + 1) / 2^bw
                 vx.set_sub(m_ev.m_tmp, vy.bits(), vx.bits());
                 vx.add1(m_ev.m_tmp);
             }
+
             rational n = m_ev.m_tmp.get_value(vx.nw);
             n /= rational(rational::power_of_two(vx.bw));
             double dbl = n.get_double();
@@ -407,13 +413,15 @@ namespace sls {
             m_ev.m_tmp2.set(vx.bw - 1, !m_ev.m_tmp2.get(vx.bw - 1));
 
             if (is_true) {
-                // x >s y
-                // x' - y' > 0
+                if (m_ev.m_tmp2 <= m_ev.m_tmp)
+                    return 1.0;
+                // otherwise x' > y'                
                 vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp2, m_ev.m_tmp);
             }
             else {
-                // x <=s y
-                // y' - x' >= 0
+                if (!(m_ev.m_tmp2 <= m_ev.m_tmp))
+                    return 1.0;
+                // x' <= y'
                 vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp, m_ev.m_tmp2);
                 vx.add1(m_ev.m_tmp3);
             }
@@ -642,7 +650,7 @@ namespace sls {
 
                     auto v1 = m_ev.bval1(e);
 
-                    CTRACE("bv", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";);
+                    CTRACE("bv_verbose", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";);
 
                     if (m_config.use_top_level_assertions) {
                         if (m_ev.get_bool_value(e) == v1)
@@ -681,7 +689,6 @@ namespace sls {
                 if (is_root(e)) {
                     double score = new_score(e);
                     m_top_score += get_weight(e) * (score - old_score(e));
-                    //verbose_stream() << "set score " << mk_bounded_pp(e, m) << " := " << score << "\n";
                     set_score(e, score);
                 }
             }

src/ast/sls/sls_bv_tracker.h

@@ -688,34 +688,45 @@ class sls_tracker {
             else
                 res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0;
         }            
-        else if (m_manager.is_and(n)) {
-            SASSERT(!negated);
+        else if (m_manager.is_and(n) && !negated) {
             /* Andreas: Seems to have no effect. But maybe you want to try it again at some point.
             double sum = 0.0;
             for (unsigned i = 0; i < a->get_num_args(); i++)
                 sum += get_score(args[i]);
             res = sum / (double) a->get_num_args(); */
             double min = 1.0;
             for (auto arg : *to_app(n)) 
-                min = std::min(get_score(arg), min);
+                min = std::min(score(arg), min);
 
             res = min;
         }
-        else if (m_manager.is_or(n)) {
-            SASSERT(!negated);
+        else if (m_manager.is_and(n) && negated) {
+            double r = 0.0;
+            for (auto arg : *to_app(n))
+                r = std::max(score(arg), r);
+            res = 1.0 - r;
+        }
+        else if (m_manager.is_or(n) && !negated) {
             double max = 0.0;
             for (auto arg : *to_app(n))
                 max = std::max(get_score(arg), max);
             res = max;
         }
+        else if (m_manager.is_or(n) && negated) {
+            double r = 1.0;
+            for (auto arg : *to_app(n))
+                r = std::min(get_score(arg), r);
+            res = 1.0 - r;
+        }
         else if (m_manager.is_ite(n)) {
-            SASSERT(!negated);
             app * a = to_app(n);
             SASSERT(a->get_num_args() == 3);
             const mpz & cond = get_value(a->get_arg(0));
             double s_t = get_score(a->get_arg(1));
             double s_f = get_score(a->get_arg(2));
             res = (m_mpz_manager.is_one(cond)) ? s_t : s_f;
+            if (negated)
+                res = 1.0 - res;
         }
         else if (m_manager.is_eq(n) || m_manager.is_iff(n)) {                
             app * a = to_app(n);
@@ -843,15 +854,10 @@ class sls_tracker {
             m_mpz_manager.del(y);                
         }
         else if (m_manager.is_not(n)) {                
-            SASSERT(!negated);
             app * a = to_app(n);
             SASSERT(a->get_num_args() == 1);
             expr * child = a->get_arg(0);
-            // Precondition: Assertion set is in NNF.
-            // Also: careful about the unsat assertion scaling further down.
-            if (m_manager.is_and(child) || m_manager.is_or(child)) 
-                NOT_IMPLEMENTED_YET();
-            res = score_bool(child, true);
+            res = score_bool(child, !negated);
         }
         else if (m_manager.is_distinct(n)) {
             app * a = to_app(n);

src/tactic/sls/sls_tactic.cpp

@@ -251,8 +251,9 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
                              mk_bv_size_reduction_tactic(m),
                              using_params(mk_simplify_tactic(m), simp2_p)),
                         using_params(mk_simplify_tactic(m), hoist_p),
-                        mk_max_bv_sharing_tactic(m),
-                        mk_nnf_tactic(m, p));
+                        mk_max_bv_sharing_tactic(m)//,
+    //                    mk_nnf_tactic(m, p)
+    );
 }
 
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {