From 67827bfe560eb40fce2eba0b6479ef5e8d5f9dd8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Jan 2025 08:37:14 -0800
Subject: [PATCH] restore nyi trace

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_lookahead.cpp | 20 ++++++++++++++------
 src/params/sls_params.pyg        |  2 +-
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 6e104cc2d..bb48e4a07 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -344,7 +344,13 @@ namespace sls {
         //verbose_stream() << "compute score " << mk_bounded_pp(a, m) << " is-true " << is_true << " is-true-new " << is_true_new << "\n";
         if (is_true == is_true_new)
             return 1;
-        expr* x, * y;
+        if (is_uninterp(a))
+            return 0;
+        if (m.is_true(a))
+            return is_true ? 1 : 0;
+        if (m.is_false(a))
+            return is_true ? 0 : 1;
+        expr* x, * y, * z;
         if (m.is_not(a, x))
             return new_score(x, !is_true);
         if ((m.is_and(a) && is_true) || (m.is_or(a) && !is_true)) {
@@ -364,6 +370,10 @@ namespace sls {
             auto v1 = m_ev.get_bool_value(y);
             return (is_true == (v0 == v1)) ? 1 : 0;
         }
+        if (m.is_ite(a, x, y, z)) {
+            auto v0 = m_ev.get_bool_value(x);
+            return v0 ? new_score(y, is_true) : new_score(z, is_true);
+        }
 
         if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
             auto const& vx = wval(x);
@@ -377,6 +387,9 @@ namespace sls {
             //verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n";
             return d;
         }
+        else if (!is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
+            return 0;
+        }
         else if (bv.is_ule(a, x, y)) {
             auto const& vx = wval(x);
             auto const& vy = wval(y);
@@ -430,7 +443,6 @@ namespace sls {
             rational n = m_ev.m_tmp3.get_value(vx.nw);
             n /= rational(rational::power_of_two(vx.bw));
             double dbl = n.get_double();
-            verbose_stream() << mk_bounded_pp(a, m) << " x:" <<vx << " y:" << vy << " " << dbl << "\n";
             return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
         }
         else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
@@ -446,10 +458,6 @@ namespace sls {
             }
             return nd / np;
         }
-        else {
-            verbose_stream() << "new score not implemented for " << mk_bounded_pp(a, m) << "\n";
-            NOT_IMPLEMENTED_YET();
-        }
 
         return 0;
     }
diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg
index 29f64d566..5a87bd745 100644
--- a/src/params/sls_params.pyg
+++ b/src/params/sls_params.pyg
@@ -25,7 +25,7 @@ def_module_params('sls',
                         ('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
                         ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
                         ('random_seed', UINT, 0, 'random seed'),
-                        ('bv_use_top_level_assertions', BOOL, False, 'use top-level assertions for BV lookahead solver'),
+                        ('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'),
                         ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
                         ('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'),
                         ('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update')