From 6eae3f08632238976ae611bbd995b7d809e4bacc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 14 Nov 2024 21:40:00 -0800
Subject: [PATCH] add cases for unconstrained sequences and strings

---
 src/ast/converters/expr_inverter.cpp       | 24 ++++++++++++++++++++++
 src/ast/simplifiers/elim_unconstrained.cpp |  3 +--
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index a06d125a5..e2d6f0255 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -780,13 +780,37 @@ public:
             }            
             return true;
         }
+        case OP_SEQ_CONTAINS:
+            if (uncnstr(args[0])) {
+                // x contains y -> r or y is empty
+                mk_fresh_uncnstr_var_for(f, r);
+                expr_ref emp(seq.str.mk_is_empty(args[0]), m);
+                if (m_mc)
+                    add_def(args[0], m.mk_ite(r, args[1], seq.str.mk_empty(args[0]->get_sort())));
+                r = m.mk_or(r, emp);
+                return true;
+            }
+            if (uncnstr(args[1])) {
+                // x contains y -> r
+                // y -> if r then x else x + x
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc)
+                    add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0])));
+                return true;
+            }
+            return false;
         default:
+            verbose_stream() << f->get_name() << "\n";
             return false;                
             
         }
     }
     
     bool mk_diff(expr* t, expr_ref& r) override {
+        if (seq.is_string(t->get_sort())) {
+            r = seq.str.mk_concat(t, seq.str.mk_string(zstring("a")));
+            return true;
+        }
         return false;
     }
     
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 478eb0028..9ddee634a 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -286,8 +286,7 @@ void elim_unconstrained::init_nodes() {
     m_heap.reserve(max_id + 1);
 
     for (expr* e : subterms_postorder::all(terms)) {
-        node& n = get_node(e);
-        SASSERT(n.is_root());
+        SASSERT(get_node(e).is_root());
         if (is_uninterp_const(e))
             m_heap.insert(e->get_id());
     }