From a85c5f0faca721532c00afc3539e67d6dad5b289 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 24 Jul 2016 17:29:17 -0700
Subject: [PATCH] add handling of recognizers to enumeration types

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/bv/dt2bv_tactic.cpp | 35 +++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 5a6c4e5fd..6f20fc609 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -15,6 +15,8 @@ Author:
 
 Revision History:
 
+    Possible extension is to handle tuple types over finite domains.
+
 --*/
 
 #include "dt2bv_tactic.h"
@@ -28,19 +30,6 @@ Revision History:
 #include "var_subst.h"
 #include "ast_util.h"
 
-#if 0
-
-enumeration types:
-
-a = x: 
-     x = y
-
-forall x . phi
-
-    f(x,y) = z ->      
-
-#endif
-
 
 class dt2bv_tactic : public tactic {
 
@@ -53,7 +42,7 @@ class dt2bv_tactic : public tactic {
     expr_ref_vector     m_bounds;
     ref<extension_model_converter> m_ext;
     ref<filter_model_converter>    m_filter;
-    unsigned                       m_num_transformed;
+    unsigned                       m_num_translated;
 
     struct rw_cfg : public default_rewriter_cfg {
         dt2bv_tactic& m_t;
@@ -75,6 +64,12 @@ class dt2bv_tactic : public tactic {
                 result = m.mk_eq(a0, a1);
                 return BR_DONE;
             }
+            else if (m_t.m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
+                unsigned idx = m_t.m_dt.get_recognizer_constructor_idx(f);
+                a1 = m_t.m_bv.mk_numeral(rational(idx), get_sort(a0));
+                result = m.mk_eq(a0, a1);
+                return BR_DONE;
+            }
             else {
                 return BR_FAILED;
             }
@@ -122,7 +117,7 @@ class dt2bv_tactic : public tactic {
                 m_t.m_filter->insert(to_app(result)->get_decl());
             }
             m_cache.insert(a, result);
-            ++m_t.m_num_transformed;
+            ++m_t.m_num_translated;
             return true;
         }
 
@@ -208,6 +203,12 @@ class dt2bv_tactic : public tactic {
             if (m.is_eq(a)) {
                 return;
             }
+            if (m_t.m_dt.is_recognizer(a->get_decl()) &&
+                m_t.is_fd(a->get_arg(0))) {
+                m_t.m_fd_sorts.insert(get_sort(a->get_arg(0)));
+                return;
+            }
+
             if (m_t.is_fd(a)) {
                 m_t.m_fd_sorts.insert(get_sort(a));
             }
@@ -265,7 +266,7 @@ public:
         }
         if (!m_fd_sorts.empty()) {
             m_bounds.reset();
-            m_num_transformed = 0;
+            m_num_translated = 0;
             m_ext = alloc(extension_model_converter, m);
             m_filter = alloc(filter_model_converter, m);
             scoped_ptr<rw> r = alloc(rw, *this, m, m_params);
@@ -283,7 +284,7 @@ public:
                 g->assert_expr(m_bounds[i].get());
             }
             mc = concat(m_filter.get(), m_ext.get());
-            report_tactic_progress(":fd-num-translated", m_num_transformed);
+            report_tactic_progress(":fd-num-translated", m_num_translated);
         }
         g->inc_depth();
         result.push_back(g.get());