Enhance bv_sls_eval with improved repair and logging, refine is_bv_predicate in sls_bv_plugin

src/ast/sls/bv_sls_eval.cpp

@@ -97,8 +97,6 @@ namespace bv {
         if (m.is_eq(e, x, y))
             return bv.is_bv(x);
         if (m.is_ite(e))
-            return bv.is_bv(e);
-        if (m.is_distinct(e))
             return bv.is_bv(e->get_arg(0));
         if (e->get_family_id() == bv.get_fid()) {
             switch (e->get_decl_kind()) {
@@ -659,9 +657,17 @@ namespace bv {
     }
     
     bool sls_eval::repair_down(app* e, unsigned i) {      
+        expr* arg = e->get_arg(i);
+        if (m.is_value(arg))
+            return false;
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
-            commit_eval(to_app(e->get_arg(i)));     
+            commit_eval(to_app(arg));
-            ctx.new_value_eh(e->get_arg(i));
+            ctx.new_value_eh(arg);
+            return true;
+        }
+        if (m.is_eq(e) && bv.is_bv(arg) && try_repair_eq(e, i)) {
+            commit_eval(to_app(arg));
+            ctx.new_value_eh(arg);
             return true;
         }
         return false;
@@ -839,24 +845,16 @@ namespace bv {
         }
     }
 
-#if 0
     bool sls_eval::try_repair_eq(app* e, unsigned i) {
         auto child = e->get_arg(i);        
         auto is_true = bval0(e);
-        if (m.is_bool(child)) {
+        if (bv.is_bv(child)) {
-            SASSERT(!is_fixed0(child));               
-            auto bv = bval0(e->get_arg(1 - i));
-            m_eval[child->get_id()] = is_true == bv;
-            return true;
-        }
-        else if (bv.is_bv(child)) {
             auto & a = wval(e->get_arg(i));
             auto & b = wval(e->get_arg(1 - i));
             return try_repair_eq(is_true, a, b);
         }
         return false;
     }
-#endif
 
     bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {

src/ast/sls/bv_sls_eval.h

@@ -108,6 +108,7 @@ namespace bv {
         bool try_repair_extract(bvect const& e, bvval& a, unsigned lo);
         bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_eq(bool is_true, bvval& a, bvval const& b);
+        bool try_repair_eq(app* e, unsigned i);
         bool try_repair_int2bv(bvect const& e, expr* arg);
         void add_p2_1(bvval const& a, bvect& t) const;
 

src/ast/sls/sls_basic_plugin.cpp

@@ -43,6 +43,7 @@ namespace sls {
 
     void basic_plugin::register_term(expr* e) {
         expr* c, * th, * el;
+        verbose_stream() << "register term " << mk_bounded_pp(e, m) << "\n";
         if (m.is_ite(e, c, th, el) && !m.is_bool(e)) {
             ctx.add_clause(m.mk_or(mk_not(m, c), m.mk_eq(e, th)));
             ctx.add_clause(m.mk_or(c, m.mk_eq(e, el)));

src/ast/sls/sls_bv_plugin.cpp

@@ -40,7 +40,14 @@ namespace sls {
     }
 
     bool bv_plugin::is_bv_predicate(expr* e) {
-        return e && is_app(e) && to_app(e)->get_family_id() == bv.get_family_id();
+        if (!e || !is_app(e))
+            return false;
+        auto a = to_app(e);
+        if (a->get_family_id() == bv.get_family_id())
+            return true;
+        if (m.is_eq(e) && bv.is_bv(a->get_arg(0)))
+            return true;
+        return false;
     }
 
     void bv_plugin::propagate_literal(sat::literal lit) {       
@@ -50,6 +57,7 @@ namespace sls {
             return;
         auto a = to_app(e);
 
+        // verbose_stream() << "propagate " << mk_bounded_pp(e, m) << " " << m_eval.eval_is_correct(a) << "\n";
         if (!m_eval.eval_is_correct(a))
             ctx.new_value_eh(e);
     }