From 95f1cfa5a6b7d13ff0ad927c3416450932f83b5b Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 27 Jul 2016 16:18:05 -0400
Subject: [PATCH] add theory_str::check_length_consistency, WIP

---
 src/smt/theory_str.cpp | 31 +++++++++++++++++++++++++++++--
 src/smt/theory_str.h   |  2 ++
 2 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3ff4ff2de..24aefe3a6 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4141,9 +4141,36 @@ bool theory_str::can_two_nodes_eq(expr * n1, expr * n2) {
     return true;
 }
 
+// was checkLength2ConstStr() in Z3str2
+// returns true if everything is OK, or false if inconsistency detected
+// - note that these are different from the semantics in Z3str2
+bool theory_str::check_length_const_string(expr * n1, expr * constStr) {
+	// TODO NEXT
+	NOT_IMPLEMENTED_YET(); return true;
+}
+
+// returns true if everything is OK, or false if inconsistency detected
+// - note that these are different from the semantics in Z3str2
+bool theory_str::check_length_eq_var_concat(expr * n1, expr * n2) {
+	// TODO NEXT
+	NOT_IMPLEMENTED_YET(); return true;
+}
+
+// returns false if an inconsistency is detected, or true if no inconsistencies were found
+// - note that these are different from the semantics of checkLengConsistency() in Z3str2
 bool theory_str::check_length_consistency(expr * n1, expr * n2) {
-    // TODO NEXT
-    NOT_IMPLEMENTED_YET(); return true;
+	if (m_strutil.is_string(n1) && m_strutil.is_string(n2)) {
+		// consistency has already been checked in can_two_nodes_eq().
+		return true;
+	} else if (m_strutil.is_string(n1) && (!m_strutil.is_string(n2))) {
+		return check_length_const_string(n2, n1);
+	} else if (m_strutil.is_string(n2) && (!m_strutil.is_string(n1))) {
+		return check_length_const_string(n1, n2);
+	} else {
+		// n1 and n2 are vars or concats
+		return check_length_eq_var_concat(n1, n2);
+	}
+	return 0;
 }
 
 void theory_str::check_concat_len_in_eqc(expr * concat) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index d213f6271..d4681856c 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -300,6 +300,8 @@ namespace smt {
         bool can_concat_eq_concat(expr * concat1, expr * concat2);
         void check_concat_len_in_eqc(expr * concat);
         bool check_length_consistency(expr * n1, expr * n2);
+        bool check_length_const_string(expr * n1, expr * constStr);
+        bool check_length_eq_var_concat(expr * n1, expr * n2);
 
         void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
         expr * simplify_concat(expr * node);