From 2ee416fc8ffb069a309bc36cd992b71be68f43cc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 May 2014 10:23:31 -0700
Subject: [PATCH] deal with infinite loop in diagonalization attempt in
 datatype factory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/proto_model/datatype_factory.cpp | 37 +++++++++++++++++++++---
 src/smt/proto_model/datatype_factory.h   |  2 ++
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index a45b53155..5e66ab738 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include"proto_model.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
+#include"expr_functors.h"
 
 datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
     struct_factory(m, m.mk_family_id("datatype"), md),
@@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) {
 */
 expr * datatype_factory::get_last_fresh_value(sort * s) {
     expr * val = 0;
-    if (m_last_fresh_value.find(s, val))
+    if (m_last_fresh_value.find(s, val)) {
+        TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
         return val;
+    }
     value_set * set = get_value_set(s);
     if (set->empty())
         val = get_some_value(s);
@@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
     return val;
 }
 
+bool datatype_factory::is_subterm_of_last_value(app* e) {
+    expr* last;
+    if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) {
+        return false;
+    }
+    contains_app contains(m_manager, e);
+    bool result = contains(last);
+    TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
+    return result;
+}
+
 /**
    \brief Create an almost fresh value. If s is recursive, then the result is not 0.
    It also updates m_last_fresh_value
@@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
             }
         }
         if (recursive || found_fresh_arg) {
-            expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
+            app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
             SASSERT(!found_fresh_arg || !set->contains(new_value));
             register_value(new_value);
-            if (m_util.is_recursive(s))
-                m_last_fresh_value.insert(s, new_value);
+            if (m_util.is_recursive(s)) {
+                if (is_subterm_of_last_value(new_value)) {
+                    new_value = static_cast<app*>(m_last_fresh_value.find(s));
+                }
+                else {
+                    m_last_fresh_value.insert(s, new_value);
+                }
+            }
+            TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
             return new_value;
         }
     }
@@ -181,12 +202,20 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                 expr_ref_vector args(m_manager);
                 bool found_sibling   = false;
                 unsigned num         = constructor->get_arity();
+                TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
                 for (unsigned i = 0; i < num; i++) {
                     sort * s_arg        = constructor->get_domain(i);
+                    TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " " 
+                          << mk_pp(s_arg, m_manager) << " are_siblings " 
+                          << m_util.are_siblings(s, s_arg) << "  is_datatype " 
+                          << m_util.is_datatype(s_arg) << " found_sibling " 
+                          << found_sibling << "\n";);
                     if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
                         expr * maybe_new_arg = get_almost_fresh_value(s_arg);
                         if (!maybe_new_arg) {
+                            TRACE("datatype_factory", 
+                                  tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
                             maybe_new_arg = m_model.get_some_value(s_arg);
                             found_sibling = false;
                         }
diff --git a/src/smt/proto_model/datatype_factory.h b/src/smt/proto_model/datatype_factory.h
index e8e1f2589..f70604ca8 100644
--- a/src/smt/proto_model/datatype_factory.h
+++ b/src/smt/proto_model/datatype_factory.h
@@ -29,6 +29,8 @@ class datatype_factory : public struct_factory {
     expr * get_last_fresh_value(sort * s);
     expr * get_almost_fresh_value(sort * s);
 
+    bool is_subterm_of_last_value(app* e);
+
 public:
     datatype_factory(ast_manager & m, proto_model & md);
     virtual ~datatype_factory() {}