add unconstrained elimination for sequences

src/api/api_tactic.cpp

@@ -24,7 +24,7 @@ Revision History:
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
-#include "ast/simplifiers/seq_simplifier.h"
+#include "ast/simplifiers/then_simplifier.h"
 
 Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c) {
 }
@@ -589,7 +589,7 @@ extern "C" {
         auto fac1 = *to_simplifier_ref(t1);
         auto fac2 = *to_simplifier_ref(t2);
         auto new_s = [fac1, fac2](auto& m, auto& p, auto& st) {
-            auto* r = alloc(seq_simplifier, m, p, st);
+            auto* r = alloc(then_simplifier, m, p, st);
             r->add_simplifier(fac1(m, p, st));
             r->add_simplifier(fac2(m, p, st));
             return r;

src/ast/converters/expr_inverter.cpp

@@ -19,6 +19,7 @@ Module Name:
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_util.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/seq_decl_plugin.h"
 #include "ast/converters/expr_inverter.h"
 
 class basic_expr_inverter : public iexpr_inverter {
@@ -742,6 +743,53 @@ class dt_expr_inverter : public iexpr_inverter {
 };
 
 
+class seq_expr_inverter : public iexpr_inverter {
+    seq_util seq;
+public:
+    seq_expr_inverter(ast_manager& m) : iexpr_inverter(m), seq(m) {}
+
+    family_id get_fid() const override { return seq.get_family_id(); }
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
+        switch (f->get_decl_kind()) {
+        case _OP_STRING_CONCAT:
+        case OP_SEQ_CONCAT: {
+            expr* x, *y;
+
+            if (uncnstr(args[0]) && num == 2 &&
+                seq.str.is_concat(args[1], x, y) &&
+                uncnstr(x)) {
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc) {
+                    add_def(args[0], seq.str.mk_empty(args[0]->get_sort()));
+                    add_def(x, r);
+                }
+                r = seq.str.mk_concat(r, y);
+                return true;                
+            }
+
+            if (!uncnstr(num, args)) 
+                return false;
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc) {
+                add_def(args[0], r);
+                for (unsigned i = 1; i < num; ++i)
+                    add_def(args[i], seq.str.mk_empty(args[0]->get_sort()));
+            }            
+            return true;
+        }
+        default:
+            return false;                
+
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        return false;
+    }
+
+};
+
 
 expr_inverter::~expr_inverter() {
     for (auto* v : m_inverters)
@@ -796,6 +844,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
     add(alloc(array_expr_inverter, m, *this));
     add(alloc(dt_expr_inverter, m));
     add(alloc(basic_expr_inverter, m, *this));
+    add(alloc(seq_expr_inverter, m));
 }
 
 

src/ast/euf/euf_egraph.cpp

@@ -67,6 +67,8 @@ namespace euf {
     }
 
     enode_bool_pair egraph::insert_table(enode* p) {
+        TRACE("euf", tout << bpp(p) << "\n");
+        //SASSERT(!m_table.contains_ptr(p));
         auto rc = m_table.insert(p);
         p->m_cg = rc.first;
         return rc;
@@ -280,6 +282,7 @@ namespace euf {
         if (!m.is_bool(n->get_sort()))
             return;
         if (enable_merge_tf != n->merge_tf()) {
+            TRACE("euf", tout << "set tf " << enable_merge_tf << " " << bpp(n) << "\n");
             n->set_merge_tf(enable_merge_tf);
             m_updates.push_back(update_record(n, update_record::toggle_merge_tf()));
         }
@@ -487,6 +490,7 @@ namespace euf {
     }
 
     void egraph::remove_parents(enode* r) {
+        TRACE("euf", tout << bpp(r) << "\n");
         for (enode* p : enode_parents(r)) {
             if (p->is_marked1())
                 continue;
@@ -496,6 +500,7 @@ namespace euf {
                 SASSERT(m_table.contains_ptr(p));
                 p->mark1();
                 erase_from_table(p);
+                CTRACE("euf", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
                 SASSERT(!m_table.contains_ptr(p));
             }
             else if (p->is_equality())

src/ast/rewriter/seq_rewriter.cpp

@@ -5518,6 +5518,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
         reduce_front(ls, rs, eqs) &&
         reduce_itos(ls, rs, eqs) &&
         reduce_itos(rs, ls, eqs) &&
+        reduce_value_clash(ls, rs, eqs) && 
         reduce_by_length(ls, rs, eqs) &&
         reduce_subsequence(ls, rs, eqs) &&
         reduce_non_overlap(ls, rs, eqs) && 
@@ -5943,6 +5944,41 @@ bool seq_rewriter::reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs,
     return true;
 }
 
+
+/**
+ * partial check for value clash.
+ * checks that elements that do not occur in 
+ * other sequence are non-values.
+ * The check could be extended to take non-value 
+ * characters (units) into account.
+ */
+bool seq_rewriter::reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {
+    ptr_buffer<expr> es;
+    if (ls.empty() || rs.empty())
+        return true;
+    es.append(ls.size(), ls.data());
+    auto remove = [&](expr* r) {
+        for (unsigned i = 0; i < es.size(); ++i) {
+            if (r == es[i]) {
+                es[i] = es.back();
+                es.pop_back();
+                return true;
+            }
+        }
+        return false;                
+    };
+    auto is_unit_value = [&](expr* r) {
+        return m().is_value(r) && str().is_unit(r);
+    };
+    for (expr* r : rs) {
+        if (remove(r))
+            continue;
+        if (!is_unit_value(r))
+            return true;
+    }
+    return any_of(es, [&](expr* e) { return is_unit_value(e); });
+}
+
 bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs) {
 
     if (ls.size() > rs.size()) 

src/ast/rewriter/seq_rewriter.h

@@ -340,6 +340,7 @@ class seq_rewriter {
     bool is_sequence(expr* e, expr_ref_vector& seq);
     bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
+    bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
     bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
     bool reduce_front(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
     void remove_empty_and_concats(expr_ref_vector& es);

src/ast/simplifiers/elim_unconstrained.cpp

@@ -73,7 +73,7 @@ void elim_unconstrained::eliminate() {
         node& n = get_node(v);
         if (n.m_refcount == 0)
             continue;
-        if (n.m_refcount > 1)
+        if (n.m_refcount > 1) 
             return;
 
         if (n.m_parents.empty()) {
@@ -90,10 +90,10 @@ void elim_unconstrained::eliminate() {
         unsigned sz = m_args.size();
         for (expr* arg : *to_app(t))
             m_args.push_back(reconstruct_term(get_node(arg)));
-        bool inverted = m_inverter(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz, r);
+        bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r);
         proof_ref pr(m);
         if (inverted && m_enable_proofs) {
-            expr * s    = m.mk_app(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz);
+            expr * s    = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz);
             expr * eq   = m.mk_eq(s, r);
             proof * pr1 = m.mk_def_intro(eq);
             proof * pr  = m.mk_apply_def(s, r, pr1);

src/ast/simplifiers/seq_simplifier.h → src/ast/simplifiers/then_simplifier.h

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    seq_simplifier.h
+    then_simplifier.h
 
 Abstract:
 
@@ -21,7 +21,7 @@ Module Name:
 #include "ast/simplifiers/dependent_expr_state.h"
 
 
-class seq_simplifier : public dependent_expr_simplifier {
+class then_simplifier : public dependent_expr_simplifier {
     scoped_ptr_vector<dependent_expr_simplifier> m_simplifiers;
 
     struct collect_stats {
@@ -53,7 +53,7 @@ class seq_simplifier : public dependent_expr_simplifier {
 
 public:
 
-    seq_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+    then_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
         dependent_expr_simplifier(m, fmls) {
     }
 

src/cmd_context/simplifier_cmds.cpp

@@ -21,7 +21,7 @@ Module Name:
 #include "cmd_context/parametric_cmd.h"
 #include "model/model_smt2_pp.h"
 #include "ast/ast_smt2_pp.h"
-#include "ast/simplifiers/seq_simplifier.h"
+#include "ast/simplifiers/then_simplifier.h"
 #include "solver/simplifier_solver.h"
 
 typedef dependent_expr_simplifier simplifier;
@@ -37,7 +37,7 @@ static simplifier_factory mk_and_then(cmd_context & ctx, sexpr * n) {
     for (unsigned i = 1; i < num_children; i++)
         args.push_back(sexpr2simplifier(ctx, n->get_child(i)));
     simplifier_factory result = [args](ast_manager& m, const params_ref& p, dependent_expr_state& st) {
-        scoped_ptr<seq_simplifier> s = alloc(seq_simplifier, m, p, st);
+        scoped_ptr<then_simplifier> s = alloc(then_simplifier, m, p, st);
         for (auto &  simp : args)
             s->add_simplifier(simp(m, p, st));
         return s.detach();

src/solver/simplifier_solver.cpp

@@ -23,7 +23,7 @@ Module Name:
 #include "ast/ast_util.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/simplifiers/dependent_expr_state.h"
-#include "ast/simplifiers/seq_simplifier.h"
+#include "ast/simplifiers/then_simplifier.h"
 #include "solver/solver.h"
 #include "solver/simplifier_solver.h"
 #include "solver/solver_preprocess.h"
@@ -91,7 +91,7 @@ class simplifier_solver : public solver {
     solver_ref  s;
     vector<dependent_expr>      m_fmls;
     dep_expr_state              m_preprocess_state;
-    seq_simplifier              m_preprocess;
+    then_simplifier             m_preprocess;
     expr_ref_vector             m_assumptions;
     model_converter_ref         m_mc;
     bool                        m_inconsistent = false;

src/solver/solver_preprocess.cpp

@@ -45,7 +45,7 @@ Module Name:
 #include "solver/solver_preprocess.h"
 #include "qe/lite/qe_lite_tactic.h"
 
-void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
+void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, dependent_expr_state& st) {
 
     smt_params smtp(p);
     s.add_simplifier(alloc(rewriter_simplifier, m, p, st));

src/solver/solver_preprocess.h

@@ -19,7 +19,7 @@ Module Name:
 
 #pragma once
 
-#include "ast/simplifiers/seq_simplifier.h"
+#include "ast/simplifiers/then_simplifier.h"
 
-void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st);
+void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, dependent_expr_state& st);
 

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -24,6 +24,7 @@ Module Name:
 #include "ast/recfun_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/seq_decl_plugin.h"
 #include "tactic/core/collect_occs.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -44,6 +45,7 @@ class elim_uncnstr_tactic : public tactic {
         bv_util                m_bv_util;
         array_util             m_ar_util;
         datatype_util          m_dt_util;
+        seq_util               m_seq_util;
         app_ref_vector         m_fresh_vars;
         obj_map<app, app*>     m_cache;
         app_ref_vector         m_cache_domain;
@@ -60,6 +62,7 @@ class elim_uncnstr_tactic : public tactic {
             m_bv_util(m),
             m_ar_util(m),
             m_dt_util(m),
+            m_seq_util(m),
             m_fresh_vars(m),
             m_cache_domain(m),
             m_max_memory(max_memory),
@@ -792,6 +795,43 @@ class elim_uncnstr_tactic : public tactic {
             }
             return nullptr;
         }
+
+        // x ++ y -> z, x -> z, y -> eps
+        app * process_seq_app(func_decl * f, unsigned num, expr * const * args) {
+            switch (f->get_decl_kind()) {
+            case _OP_STRING_CONCAT:
+            case OP_SEQ_CONCAT: {
+                app * r = nullptr;
+                expr* x, *y;
+                if (uncnstr(args[0]) && num == 2 &&
+                    m_seq_util.str.is_concat(args[1], x, y) &&
+                    uncnstr(x)) {
+                    if (!mk_fresh_uncnstr_var_for(f, num, args, r))
+                        return r;
+
+                    if (m_mc) {
+                        add_def(args[0], r);
+                        add_def(x, m_seq_util.str.mk_empty(args[0]->get_sort()));
+                    }
+                    r = m_seq_util.str.mk_concat(r, y);                        
+                    return r;
+
+                }
+                if (!uncnstr(num, args))
+                    return nullptr;
+                if (!mk_fresh_uncnstr_var_for(f, num, args, r))
+                    return r;
+
+                expr_ref id(m_seq_util.str.mk_empty(args[0]->get_sort()), m());
+                add_defs(num, args, r, id);
+
+                return r;
+            }
+            default:
+                return nullptr;
+            }            
+        }
+
 
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
             if (num == 0)
@@ -817,7 +857,8 @@ class elim_uncnstr_tactic : public tactic {
                 u = process_array_app(f, num, args);
             else if (fid == m_dt_util.get_family_id())
                 u = process_datatype_app(f, num, args);
-
+            else if (fid == m_seq_util.get_family_id())
+                u = process_seq_app(f, num, args);
             if (u == nullptr)
                 return BR_FAILED;