better behavior on disequality and branch selection (#4605)

* better behavior on disequality and branch selection

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix loop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/seq_eq_solver.cpp

@@ -670,8 +670,8 @@ bool theory_seq::branch_binary_variable(eq const& e) {
     if (lenX <= rational(ys.size())) {
         expr_ref_vector Ys(m);
         Ys.append(ys.size(), ys.c_ptr());
-        branch_unit_variable(e.dep(), x, Ys);
+        if (branch_unit_variable(e.dep(), x, Ys))
-        return true;
+            return true;
     }
     expr_ref le(m_autil.mk_le(mk_len(x), m_autil.mk_int(ys.size())), m);
     literal lit = mk_literal(le);
@@ -698,13 +698,13 @@ bool theory_seq::branch_binary_variable(eq const& e) {
 bool theory_seq::branch_unit_variable() {
     bool result = false;
     for (auto const& e : m_eqs) {
-        if (is_unit_eq(e.ls(), e.rs())) {
+        if (is_unit_eq(e.ls(), e.rs()) && 
-            branch_unit_variable(e.dep(), e.ls()[0], e.rs());
+            branch_unit_variable(e.dep(), e.ls()[0], e.rs())) {
             result = true;
             break;
         }
-        else if (is_unit_eq(e.rs(), e.ls())) {
+        if (is_unit_eq(e.rs(), e.ls()) && 
-            branch_unit_variable(e.dep(), e.rs()[0], e.ls());
+            branch_unit_variable(e.dep(), e.rs()[0], e.ls())) {
             result = true;
             break;
         }
@@ -713,38 +713,41 @@ bool theory_seq::branch_unit_variable() {
     return result;
 }
 
-void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
+bool theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
     SASSERT(is_var(X));
     rational lenX;
     if (!get_length(X, lenX)) {
         TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";);
         add_length_to_eqc(X);
-        return;
+        return true;
     }
     if (lenX > rational(units.size())) {
         expr_ref le(m_autil.mk_le(mk_len(X), m_autil.mk_int(units.size())), m);
         TRACE("seq", tout << "propagate length on " << mk_bounded_pp(X, m, 2) << "\n";);
         propagate_lit(dep, 0, nullptr, mk_literal(le));
-        return;
+        return true;
     }
     SASSERT(lenX.is_unsigned());
     unsigned lX = lenX.get_unsigned();
     if (lX == 0) {
         TRACE("seq", tout << "set empty length " << mk_bounded_pp(X, m, 2) << "\n";);
         set_empty(X);
+        return true;
     }
-    else {
+
-        literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
+    literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
-        if (l_true == ctx.get_assignment(lit)) {
+    switch (ctx.get_assignment(lit)) {
-            expr_ref R = mk_concat(lX, units.c_ptr(), m.get_sort(X));
+    case l_true: {
-            propagate_eq(dep, lit, X, R);
+        expr_ref R = mk_concat(lX, units.c_ptr(), m.get_sort(X));     
-            TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
+        return propagate_eq(dep, lit, X, R);
-        }
+    }
-        else {
+    case l_undef: 
-            TRACE("seq", tout << "set phase " << mk_pp(X, m) << "\n";);
+        TRACE("seq", tout << "set phase " << mk_pp(X, m) << "\n";);
-            ctx.mark_as_relevant(lit);
+        ctx.mark_as_relevant(lit);
-            ctx.force_phase(lit);
+        ctx.force_phase(lit);
-        }
+        return true;
+    default:
+        return false;
     }
 }
 
@@ -1135,13 +1138,11 @@ bool theory_seq::branch_variable_eq(eq const& e) {
     TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
     bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
     insert_branch_start(2*id, s);
-    if (found) {
+    if (!found) {
-        return true;
+        s = find_branch_start(2*id + 1);
+        found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
+        insert_branch_start(2*id + 1, s);
     }
-    s = find_branch_start(2*id + 1);
-    found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
-    insert_branch_start(2*id + 1, s);
-    
     return found;
 }
 
@@ -1173,7 +1174,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
     expr_ref v0(m);
     v0 = m_util.str.mk_empty(m.get_sort(l));
     if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) {
-        if (l_false != assume_equality(l, v0)) {
+        if (assume_equality(l, v0)) {
             TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
             return true;
         }
@@ -1189,7 +1190,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
             continue;
         }
         v0 = mk_concat(j + 1, rs.c_ptr());
-        if (l_false != assume_equality(l, v0)) {
+        if (assume_equality(l, v0)) {
             TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
             ++start;
             return true;
@@ -1212,7 +1213,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
         for (literal lit : lits) {
             switch (ctx.get_assignment(lit)) {
             case l_true:  break;
-            case l_false: start = 0; return true;
+            case l_false: start = 0; return false;
             case l_undef: ctx.mark_as_relevant(lit); ctx.force_phase(~lit); start = 0; return true;
             }
         }
@@ -1253,42 +1254,39 @@ bool theory_seq::can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr*
 }
 
 
-lbool theory_seq::assume_equality(expr* l, expr* r) {
+bool theory_seq::assume_equality(expr* l, expr* r) {
     if (m_exclude.contains(l, r)) {
-        return l_false;
+        return false;
     }
 
     expr_ref eq(m.mk_eq(l, r), m);
     m_rewrite(eq);
     if (m.is_true(eq)) {
-        return l_true;
+        return false;
     }
     if (m.is_false(eq)) {
-        return l_false;
+        return false;
     }
 
     enode* n1 = ensure_enode(l);
     enode* n2 = ensure_enode(r);
     if (n1->get_root() == n2->get_root()) {
         TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " roots eq\n";);
-        return l_true;
+        return false;
     }
     if (ctx.is_diseq(n1, n2)) {
         TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " is_diseq\n";);
-        return l_false;
+        return false;
-    }
-    if (false && ctx.is_diseq_slow(n1, n2)) {
-        return l_false;
     }
     ctx.mark_as_relevant(n1);
     ctx.mark_as_relevant(n2);
     if (!ctx.assume_eq(n1, n2)) {
         TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " can't assume\n";);
-        return l_false;
+        return false;
     }
     lbool res = ctx.get_assignment(mk_eq(l, r, false));
     TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " literal assigned " << res << "\n";);
-    return res;
+    return res != l_false;
 }
 
 
@@ -1363,14 +1361,9 @@ bool theory_seq::check_length_coherence(expr* e) {
 bool theory_seq::check_length_coherence0(expr* e) {
     if (is_var(e) && m_rep.is_root(e)) {
         expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
-        lbool r = l_false;
         bool p = propagate_length_coherence(e);
 
-        if (!p) {
+        if (p || assume_equality(e, emp)) {
-            r = assume_equality(e, emp);
-        }
-
-        if (p || r != l_false) {
             if (!ctx.at_base_level()) {
                 m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
             }

src/smt/seq_ne_solver.cpp

@@ -53,6 +53,7 @@ bool theory_seq::check_ne_literals(unsigned idx, unsigned& num_undef_lits) {
             TRACE("seq", display_disequation(tout << "has false literal\n", n);
                   ctx.display_literal_verbose(tout, lit);
                   tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
+                  display(tout);
                   );
             return false;
         case l_true:
@@ -132,6 +133,13 @@ bool theory_seq::propagate_ne2eq(unsigned idx) {
 bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
     if (es.empty())
         return false;
+    for (expr* e : es) {
+        expr_ref len_e = mk_len(e);
+        rational lo;
+        if (lower_bound(len_e, lo) && lo > 0) {
+            return true;
+        }
+    }
     ne const& n = m_nqs[idx];
     expr_ref e(m), head(m), tail(m);
     e = mk_concat(es, m.get_sort(es[0]));
@@ -220,10 +228,8 @@ bool theory_seq::reduce_ne(unsigned idx) {
         }
     }
 
-
-    TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n););
-
     if (updated) {
+        TRACE("seq", display_disequation(tout, n););
         m_nqs.set(idx, ne(n.l(), n.r(), new_eqs, new_lits, new_deps));
         TRACE("seq", display_disequation(tout << "updated:\n", m_nqs[idx]););
     }

src/smt/smt_context.cpp

@@ -4560,7 +4560,6 @@ namespace smt {
         pop_to_search_lvl();
         if (m.is_bool(e)) {
             if (b_internalized(e)) {
-                bool_var v = get_bool_var(e);
                 switch (get_assignment(get_bool_var(e))) {
                 case l_true: e = m.mk_true(); break;
                 case l_false: e = m.mk_false(); break;

src/smt/theory_seq.cpp

@@ -110,32 +110,6 @@ Outline:
 
 using namespace smt;
 
-struct display_expr {
-    ast_manager& m;
-    display_expr(ast_manager& m): m(m) {}
-    std::ostream& display(std::ostream& out, sym_expr* e) const {
-        return e->display(out);
-    }
-};
-
-class seq_expr_solver : public expr_solver {
-    kernel m_kernel;
-public:
-    seq_expr_solver(ast_manager& m, smt_params& fp):
-        m_kernel(m, fp)
-    {}
-
-    lbool check_sat(expr* e) override {
-        m_kernel.push();
-        m_kernel.assert_expr(e);
-        lbool r = m_kernel.check();
-        m_kernel.pop(1);
-        IF_VERBOSE(11, verbose_stream() << "is " << r << " " << mk_pp(e, m_kernel.m()) << "\n");
-        return r;
-    }
-};
-
-
 void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
     if (e == r) {
         return;
@@ -332,7 +306,7 @@ void theory_seq::init() {
     m_arith_value.init(&ctx);
 }
 
-#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(31, verbose_stream() << s << "\n"); }
+#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(20, verbose_stream() << s << "\n"); }
 
 struct scoped_enable_trace {
     scoped_enable_trace() {

src/smt/theory_seq.h

@@ -431,7 +431,7 @@ namespace smt {
         bool check_length_coherence(expr* e);
         bool fixed_length(bool is_zero = false);
         bool fixed_length(expr* e, bool is_zero);
-        void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
+        bool branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
         bool branch_variable_eq(eq const& e);
         bool branch_binary_variable(eq const& e);
         bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
@@ -536,7 +536,7 @@ namespace smt {
         bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
         expr_ref_vector expand_strings(expr_ref_vector const& es);
         bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
-        lbool assume_equality(expr* l, expr* r);
+        bool assume_equality(expr* l, expr* r);
 
         // variable solving utilities
         bool occurs(expr* a, expr* b);