From 0d54e4e4ae99933b4330fba9df9224f9486ee361 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 27 Sep 2015 23:57:41 -0400
Subject: [PATCH] implement str_decl_plugin::is_value() and ::is_unique_value()
 we can now prove that (= "abc" "def") is unsatisfiable

---
 src/ast/str_decl_plugin.cpp | 12 ++++++++++++
 src/ast/str_decl_plugin.h   |  4 +++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 1502e3d3a..60db88b63 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -115,6 +115,18 @@ void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     sort_names.push_back(builtin_name("String", STRING_SORT));
 }
 
+bool str_decl_plugin::is_value(app * e) const {
+    if (e->get_family_id() != m_family_id) {
+        return false;
+    }
+    switch (e->get_decl_kind()) {
+    case OP_STR:
+        return true;
+    default:
+        return false;
+    }
+}
+
 bool str_recognizers::is_string(expr const * n, const char ** val) const {
     if (!is_app_of(n, m_afid, OP_STR))
             return false;
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index 7e75fbaf0..a64e0c05f 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -60,8 +60,10 @@ public:
     app * mk_string(const char * val);
 
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
-
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
+
+    virtual bool is_value(app * e) const;
+    virtual bool is_unique_value(app * e) const { return is_value(e); }
     // TODO
 };