Model construction has to respect the length constraints

scripts/compare_seq_solvers.py

@@ -71,9 +71,12 @@ def determine_status(res_nseq: str, res_seq: str, smtlib_status: str) -> str:
 
 def _parse_result(output: str) -> str:
     """Extract the first sat/unsat/unknown line from solver output."""
+    has_invalid_model = "an invalid model was generated" in output
     for line in output.splitlines():
         tok = line.strip().lower()
         if tok in ("sat", "unsat"):
+            if tok == "sat" and has_invalid_model:
+                return "invalid"
             return tok
         if tok == "unknown":
             return "timeout"
@@ -121,6 +124,9 @@ def run_zipt(zipt_bin: str, smt_file: Path, timeout_s: int = DEFAULT_TIMEOUT) ->
 
 def classify(res_nseq: str, res_seq: str, res_nseq_p: str | None = None) -> str:
     """Classify a pair of results into a category."""
+    if res_nseq == "invalid_model" or res_seq == "invalid_model" or res_nseq_p == "invalid_model":
+        return "invalid_model"
+
     timed_nseq = res_nseq == "timeout"
     timed_seq  = res_seq  == "timeout"
     
@@ -234,6 +240,7 @@ def main():
 
     # ── Summary ──────────────────────────────────────────────────────────────
     categories = {
+        "invalid_model":                  [],
         "all_timeout":                    [],
         "both_timeout":                   [],
         "only_seq_terminates":            [],
@@ -276,6 +283,9 @@ def main():
             _print_file_list("ZIPT TIMES OUT", zipt_timeouts)
     if both_to:
         _print_file_list("BOTH Z3 SOLVERS TIME OUT", both_to)
+    invalid_models = categories.get("invalid_model", [])
+    if invalid_models:
+        _print_file_list("INVALID MODEL GENERATED", invalid_models)
     if zipt_bin:
         all_to = [r for r in results
                   if r["nseq"] == "timeout" and r["seq"] == "timeout" and r["zipt"] == "timeout"]

src/smt/seq/seq_nielsen.cpp

@@ -231,8 +231,18 @@ namespace seq {
         );
         m_subst.push_back(s);
         nielsen_graph& g = src()->graph();
-        if (s.is_eliminating())
+        if (s.is_eliminating()) {
+            // TODO: Is this entirely correct?
             m_len_updates.push_back(g.a.mk_int(0));
+            add_side_constraint(constraint(g.a.mk_eq(
+                g.a.mk_int(0),
+                g.a.mk_sub(
+                    g.compute_length_expr(s.m_var),
+                    g.compute_length_expr(s.m_replacement)
+                    )), s.m_dep, g.get_manager()));
+            std::cout << "Adding side condition: " << mk_pp(m_side_constraints.back().fml, g.get_manager()) << std::endl;
+            0 == 0;
+        }
         else {
             expr_ref sum(
                  g.a.mk_sub(
@@ -242,10 +252,9 @@ namespace seq {
             th_rewriter th(g.get_manager());
             th(sum);
             m_len_updates.push_back(sum);
-            std::cout
+            add_side_constraint(constraint(g.a.mk_le(g.a.mk_int(0), sum), s.m_dep, g.get_manager()));
-                << mk_pp(s.m_var->get_expr(), src()->graph().get_manager()) << " => "
+            std::cout << "Adding side condition: " << mk_pp(m_side_constraints.back().fml, g.get_manager()) << std::endl;
-                << mk_pp(sum, src()->graph().get_manager())
+            0 == 0;
-                << " using " << mk_pp(s.m_replacement->get_expr(), src()->graph().get_manager()) << std::endl;
         }
     }
 
@@ -302,6 +311,8 @@ namespace seq {
 
     void nielsen_node::add_constraint(constraint const &c) {
         auto& m = graph().get_manager();
+        if (m.is_true(c.fml))
+            return;
         // TODO: Is it possible that we miss a conflict if we decompose?
         if (m.is_and(c.fml)) {
             // We have to add all - even if some of it conflict
@@ -311,12 +322,6 @@ namespace seq {
             }
             return;
         }
-        expr* l, *r;
-        if (m.is_eq(c.fml, l, r)) {
-            // To avoid filling memory with tautologies (that would happen quite often)
-            if (l == r)
-                return;
-        }
         m_constraints.push_back(c);
     }
 
@@ -3992,6 +3997,7 @@ namespace seq {
             auto& c = node->constraints()[i];
             m_solver.assert_expr(c.fml);
             auto lit = m_literal_if_false(c.fml);
+            std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << std::endl;
             if (lit != sat::null_literal)
                 node->set_external_conflict(lit, c.dep);
         }
@@ -4007,6 +4013,7 @@ namespace seq {
         if (node == m_root)
             return;
 
+        // TODO: Do we really need this?
         uint_set seen_vars;
 
         for (str_eq const& eq : node->str_eqs()) {

src/smt/seq/seq_nielsen.h

@@ -486,10 +486,17 @@ namespace seq {
         expr_ref    fml;   // the formula (eq, le, or ge, unit-diseq expression)
         dep_tracker dep;   // tracks which input constraints contributed
 
+        static expr_ref simplify(expr* f, ast_manager& m) {
+            th_rewriter th(m);
+            expr_ref fml(f, m);
+            th(fml);
+            return fml;
+        }
+
         constraint(ast_manager& m):
             fml(m), dep(nullptr) {}
         constraint(expr* f, dep_tracker const& d, ast_manager& m):
-            fml(f, m), dep(d) {}
+            fml(simplify(f, m)), dep(d) {}
 
         std::ostream& display(std::ostream& out) const;
     };

src/smt/seq_model.cpp

@@ -495,6 +495,29 @@ namespace smt {
         if (m_var_regex.find(key, re) && re) {
             expr* re_expr = re->get_expr();
             SASSERT(re_expr);
+
+            arith_util arith(m);
+            expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m);
+            rational len_val;
+            bool has_len = false;
+            if (dep_values) {
+                expr* dval = nullptr;
+                enode* dep = find_root_enode(m_ctx, len_expr);
+                if (dep && dep_values->find(dep, dval) && dval && arith.is_numeral(dval, len_val))
+                    has_len = true;
+            }
+            if (!has_len && m_mg) {
+                expr_ref eval_len(m);
+                if (m_mg->get_model().eval(len_expr, eval_len, true) && arith.is_numeral(eval_len, len_val))
+                    has_len = true;
+            }
+
+            if (has_len && len_val.is_unsigned()) {
+                unsigned n = len_val.get_unsigned();
+                expr_ref loop(m_seq.re.mk_loop(m_seq.re.mk_full_char(re_expr->get_sort()), n, n), m);
+                re_expr = m_seq.re.mk_inter(re_expr, loop);
+            }
+
             expr_ref witness(m);
             // We checked non-emptiness during Nielsen already
             lbool wr = m_rewriter.some_seq_in_re(re_expr, witness);
@@ -503,7 +526,7 @@ namespace smt {
                 m_factory->register_value(witness);
                 return witness;
             }
-            IF_VERBOSE(1, verbose_stream() << "witness extraction failed: " << wr << "\n" << mk_pp(re_expr, m) << "\n");
+            IF_VERBOSE(1, verbose_stream() << "witness extraction failed: " << wr << " with len " << (has_len ? len_val.to_string() : "unknown") << "\n" << mk_pp(re_expr, m) << "\n");
             UNREACHABLE();
         }
 

src/smt/theory_nseq.cpp

@@ -736,6 +736,7 @@ namespace smt {
                 }
             }
 
+            std::cout << "[" << m_num_final_checks << "]" << std::endl;
             IF_VERBOSE(1, verbose_stream() << "nseq final_check: calling solve()\n";);
 
             // here the actual Nielsen solving happens
@@ -763,12 +764,15 @@ namespace smt {
                 // Nielsen found a consistent assignment for positive constraints.
                 SASSERT(has_eq_or_mem); // we should have axiomatized them
 
-                add_nielsen_assumptions();
+                bool all_sat = add_nielsen_assumptions();
 
                 if (!check_length_coherence())
                     return FC_CONTINUE;
 
                 CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n"));
+                if (!all_sat)
+                    return FC_CONTINUE;
+
                 if (!has_unhandled_preds())
                     return FC_DONE;
             }
@@ -786,7 +790,7 @@ namespace smt {
     }
 
 
-    void theory_nseq::add_nielsen_assumptions() {
+    bool theory_nseq::add_nielsen_assumptions() {
         m_nielsen_literals.reset();
         struct reset_vector : public trail {
             sat::literal_vector &v;
@@ -796,8 +800,10 @@ namespace smt {
             }
         };
         //std::cout << "Nielsen assumptions:\n";
+        bool all_sat = true;
         ctx.push_trail(reset_vector(m_nielsen_literals));
         for (auto const& c : m_nielsen.sat_node()->constraints()) {
+            std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
             auto lit = mk_literal(c.fml);   
             m_nielsen_literals.push_back(lit);
             // Ensure Nielsen assumptions participate in SAT search instead of
@@ -812,6 +818,7 @@ namespace smt {
                 // Commit the chosen Nielsen assumption to the SAT core so it
                 // cannot remain permanently undefined in a partial model.
                 ctx.force_phase(lit);
+                all_sat = false;
                 IF_VERBOSE(2, verbose_stream() << 
                     "nseq final_check: adding nielsen assumption " << c.fml << "\n";);
                 TRACE(seq, tout << "assign: " << c.fml << "\n");
@@ -820,12 +827,14 @@ namespace smt {
                 // this should not happen because nielsen checks for this before returning a satisfying path.
                 // or maybe it can happen if we have a "le" dependency
                 TRACE(seq, tout << "nseq final_check: nielsen assumption " << c.fml << " is false; internalized - " << ctx.e_internalized(c.fml) << "\n");
+                all_sat = false;
                 std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
                 ctx.push_trail(value_trail(m_should_internalize));
                 m_should_internalize = true;
                 break;
             }
         }
+        return all_sat;
     }
 
     // -----------------------------------------------------------------------

src/smt/theory_nseq.h

@@ -118,7 +118,7 @@ namespace smt {
         void explain_nielsen_conflict();
         void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
         void set_propagate(enode_pair_vector const &eqs, literal_vector const &lits, literal p);
-        void add_nielsen_assumptions();
+        bool add_nielsen_assumptions();
         euf::snode* get_snode(expr* e);
 
         // propagation dispatch helpers