#5467

src/ast/rewriter/seq_axioms.cpp

@@ -1142,8 +1142,8 @@ namespace seq {
 
     /**
        ~contains(a, b) => ~prefix(b, a)
-       ~contains(a, b) => ~contains(tail(a), b) or a = empty
-       ~contains(a, b) & a = empty => b != empty
+       ~contains(a, b) => ~contains(tail(a), b) 
+       a = empty => tail(a) = empty
        ~(a = empty) => a = head + tail 
     */
     void axioms::unroll_not_contains(expr* e) {
@@ -1165,7 +1165,7 @@ namespace seq {
         expr_ref bound_tracker = m_sk.mk_length_limit(s, k);
         expr* s0 = nullptr;
         if (seq.str.is_stoi(s, s0)) 
-            s = s0; 
+            s = s0;
         add_clause(~bound_tracker, mk_le(mk_len(s), k));
         return bound_tracker;
     }

src/ast/rewriter/seq_eq_solver.cpp

@@ -15,6 +15,7 @@ Module Name:
 
 --*/
 
+#include "ast/ast_pp.h"
 #include "ast/rewriter/seq_eq_solver.h"
 #include "ast/bv_decl_plugin.h"
 
@@ -675,7 +676,7 @@ namespace seq {
             if (rs.size() > i) {
                 unsigned diff = rs.size() - (i + 1);
                 for (unsigned j = 0; same && j < i; ++j) 
-                    same = !m.are_distinct(ls[j], rs[diff + j]);                               
+                    same = !m.are_distinct(ls[j], rs[diff + j]);
             }
             // ls = x ++ rs ++ y, diff = |x|
             else {
@@ -704,8 +705,9 @@ namespace seq {
             bool same = true;
             // ls = x ++ rs' && rs = rs' ++ y, diff = |x|
             if (rs.size() > i) {
-                for (unsigned j = 1; same && j <= i; ++j) 
-                    same = !m.are_distinct(ls[diff + j], rs[j]);                
+                for (unsigned j = 1; same && j <= i; ++j) {
+                    same = !m.are_distinct(ls[diff + j], rs[j]);
+                }
             }
             // ls = x ++ rs ++ y, diff = |x|
             else {
@@ -715,6 +717,7 @@ namespace seq {
             if (same)
                 return true;
         }
+
         return false;
     }
 

src/ast/rewriter/seq_skolem.cpp

@@ -28,8 +28,8 @@ skolem::skolem(ast_manager& m, th_rewriter& rw):
     m_tail           = "seq.tail";
     m_seq_first      = "seq.first";
     m_seq_last       = "seq.last";
-    m_indexof_left   = "seq.idx.left";
-    m_indexof_right  = "seq.idx.right";
+    m_indexof_left   = "seq.idx.l";
+    m_indexof_right  = "seq.idx.r";
     m_aut_step       = "aut.step";
     m_pre            = "seq.pre";  // (seq.pre s l):  prefix of string s of length l
     m_post           = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l

src/ast/rewriter/seq_skolem.h

@@ -77,8 +77,10 @@ namespace seq {
 
         expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); }
         expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); }
-        expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_left", t, s, offset); }
-        expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_right", t, s, offset); }
+        expr_ref mk_contains_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.l", t, s, offset); }
+        expr_ref mk_contains_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.r", t, s, offset); }
+        expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.l", t, s, offset); }
+        expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.r", t, s, offset); }
 
         expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
         expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }

src/smt/seq_eq_solver.cpp

@@ -684,11 +684,12 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
             cond = true;
     }
     // xs and ys cannot align
-    else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
+    else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys) && !can_align_from_lhs(ys, xs) && !can_align_from_rhs(ys, xs))
         cond = true;
 
     if (!cond)
         return false;
+
 
     literal_vector lits;
     if (xs == ys) {
@@ -724,7 +725,7 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
         }
     }
     else {
-        TRACE("seq", tout << mk_pp(x1, m) << " > " << mk_pp(y1, m) << "\n";);
+        TRACE("seq", tout << mk_pp(x1, m) << " >\n" << mk_pp(y1, m) << "\n";);
         if (ctx.get_assignment(lit3) == l_undef) {
             ctx.mark_as_relevant(lit3);
             return true;

src/smt/smt_conflict_resolution.cpp

@@ -474,7 +474,8 @@ namespace smt {
 
         TRACE("conflict",
               tout << "new scope level:     " << m_new_scope_lvl << "\n";
-              tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";);
+              tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";
+              tout << "lemma: " << m_lemma << "\n";);
 
         if (m.proofs_enabled())
             mk_conflict_proof(conflict, not_l);
@@ -761,6 +762,7 @@ namespace smt {
         m_lemma      .shrink(j);
         m_lemma_atoms.shrink(j);
         m_ctx.m_stats.m_num_minimized_lits += sz - j;
+        TRACE("conflict", tout << "lemma: " << m_lemma << "\n";);
     }
 
     /**

src/smt/smt_context_pp.cpp

@@ -113,9 +113,17 @@ namespace smt {
     }
 
     std::ostream& context::display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const {
-        for (unsigned i = 0; i < num_lits; ++i) {
+        out << literal_vector(num_lits, lits) << ":\n";
+#if 1
+        expr_ref_vector fmls(m);
+        for (unsigned i = 0; i < num_lits; ++i)
+            fmls.push_back(literal2expr(lits[i]));
+        expr_ref c = mk_or(fmls);
+        out << c << "\n";
+#else
+        for (unsigned i = 0; i < num_lits; ++i) 
             display_literal_smt2(out, lits[i]) << "\n";
-        }
+#endif
         return out;
     }
 

src/smt/smt_internalizer.cpp

@@ -1387,7 +1387,7 @@ namespace smt {
         default:
             break;
         }
-        TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";);
+        TRACE("mk_clause", display_literals_verbose(tout << "after simplification: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
 
         unsigned activity = 1;
         bool  lemma = is_lemma(k);

src/smt/theory_seq.cpp

@@ -726,7 +726,7 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
     svector<assumption> assumptions;
     const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
     for (assumption const& a : assumptions) {
-        if (a.lit != null_literal) {
+        if (a.lit != null_literal && a.lit != true_literal) {            
             lits.push_back(a.lit);
             SASSERT(ctx.get_assignment(a.lit) == l_true);
         }
@@ -743,7 +743,7 @@ bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
         return false;
     if (ctx.get_assignment(lit) == l_true)
         return false;
-    
+
     literal_vector lits(n, _lits);
 
     if (lit == false_literal) {
@@ -2858,7 +2858,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
 }
 
 void theory_seq::add_axiom(literal_vector & lits) {
-    TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
+    TRACE("seq", ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";);
     for (literal lit : lits)
         ctx.mark_as_relevant(lit);
 
@@ -2898,6 +2898,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
     if (n1->get_root() == n2->get_root()) {
         return false;
     }
+
     ctx.mark_as_relevant(n1);
     ctx.mark_as_relevant(n2);
 
@@ -2979,8 +2980,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         m_rewrite(se1);
         m_rewrite(se2);
         if (is_true) {
-            expr_ref f1 = m_sk.mk_indexof_left(se1, se2);
-            expr_ref f2 = m_sk.mk_indexof_right(se1, se2);
+            expr_ref f1 = m_sk.mk_contains_left(se1, se2);
+            expr_ref f2 = m_sk.mk_contains_right(se1, se2);
             f = mk_concat(f1, se2, f2);
             propagate_eq(lit, f, e1, true);
             propagate_eq(lit, mk_len(f), mk_len(e1), false);