probably fix duplication of mk_string() terms

also implement Case 2 of solve_concat_eq_str()

src/ast/str_decl_plugin.cpp

@@ -99,11 +99,25 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     return mk_func_decl(k);
 }
 
+app * str_decl_plugin::mk_string(std::string & val) {
+	std::map<std::string, app*>::iterator it = string_cache.find(val);
+	if (it == string_cache.end()) {
+		char * new_buffer = alloc_svect(char, val.length() + 1);
+		strcpy(new_buffer, val.c_str());
+		parameter p[1] = {parameter(new_buffer)};
+		func_decl * d;
+		d = m_manager->mk_const_decl(m_strv_sym, m_str_decl, func_decl_info(m_family_id, OP_STR, 1, p));
+		app * str = m_manager->mk_const(d);
+		string_cache[val] = str;
+		return str;
+	} else {
+		return it->second;
+	}
+}
+
 app * str_decl_plugin::mk_string(const char * val) {
-    parameter p[1] = {parameter(val)};
+	std::string key(val);
-    func_decl * d;
+	return mk_string(key);
-    d = m_manager->mk_const_decl(m_strv_sym, m_str_decl, func_decl_info(m_family_id, OP_STR, 1, p));
-    return m_manager->mk_const(d);
 }
 
 void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {

src/ast/str_decl_plugin.h

@@ -19,6 +19,7 @@ Revision History:
 
 #include"ast.h"
 #include"arith_decl_plugin.h"
+#include<map>
 
 enum str_sort_kind {
    STRING_SORT,
@@ -44,6 +45,8 @@ protected:
     func_decl * m_concat_decl;
     func_decl * m_length_decl;
 
+    std::map<std::string, app*> string_cache;
+
     virtual void set_manager(ast_manager * m, family_id id);
 
     func_decl * mk_func_decl(decl_kind k);
@@ -58,6 +61,7 @@ public:
                                          unsigned arity, sort * const * domain, sort * range);
 
     app * mk_string(const char * val);
+    app * mk_string(std::string & 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);
@@ -90,6 +94,9 @@ public:
     app * mk_string(const char * val) {
         return m_plugin->mk_string(val);
     }
+    app * mk_string(std::string & val) {
+    	return m_plugin->mk_string(val);
+    }
     // TODO
 };
 

src/smt/theory_str.cpp

@@ -468,11 +468,48 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
         		expr_ref equality(ctx.mk_eq_atom(concat, str), m);
         		expr_ref diseq(m.mk_not(equality), m);
         		assert_axiom(diseq);
+        		return;
         	}
         } else if (!arg1_has_eqc_value && arg2_has_eqc_value) {
         	// Case 2: Concat(var, const) == const
         	TRACE("t_str", tout << "Case 2: Concat(var, const) == const" << std::endl;);
-        	NOT_IMPLEMENTED_YET();
+        	const char * str2;
+			m_strutil.is_string(arg2, & str2);
+			std::string arg2_str(str2);
+			int resultStrLen = const_str.length();
+			int arg2StrLen = arg2_str.length();
+			if (resultStrLen < arg2StrLen) {
+				// Inconsistency
+				TRACE("t_str", tout << "inconsistency detected: \""
+						 << arg2_str <<
+						"\" is longer than \"" << const_str << "\","
+						<< " so cannot be concatenated with anything to form it" << std::endl;);
+				expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
+				expr_ref diseq(m.mk_not(equality), m);
+				assert_axiom(diseq);
+				return;
+			} else {
+				int varStrLen = resultStrLen - arg2StrLen;
+				std::string firstPart = const_str.substr(0, varStrLen);
+				std::string secondPart = const_str.substr(varStrLen, arg2StrLen);
+				if (arg2_str != secondPart) {
+					// Inconsistency
+					TRACE("t_str", tout << "inconsistency detected: "
+							<< "suffix of concatenation result expected \"" << secondPart << "\", "
+							<< "actually \"" << arg2_str << "\""
+							<< std::endl;);
+					expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
+					expr_ref diseq(m.mk_not(equality), m);
+					assert_axiom(diseq);
+					return;
+				} else {
+					expr_ref tmpStrConst(m_strutil.mk_string(firstPart), m);
+					expr_ref premise(ctx.mk_eq_atom(newConcat, str), m);
+					expr_ref conclusion(ctx.mk_eq_atom(arg1, tmpStrConst), m);
+					assert_implication(premise, conclusion);
+					return;
+				}
+			}
         } else if (arg1_has_eqc_value && !arg2_has_eqc_value) {
         	// Case 3: Concat(const, var) == const
         	TRACE("t_str", tout << "Case 3: Concat(const, var) == const" << std::endl;);