From faf4ba83093ee828e636a953e882ad902e9b9b18 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 May 2019 12:25:36 +0400
Subject: [PATCH] add check for contravariance to fix #2256

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 45 ++++++++++++++++++++++++++++++++
 src/ast/datatype_decl_plugin.h   |  2 ++
 2 files changed, 47 insertions(+)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 6aaa13349..9f048ff1b 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -446,6 +446,9 @@ namespace datatype {
             if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) {
                 m_manager->raise_exception("datatype is not well-founded");
             }
+            if (!u().is_covariant(sorts.size(), sorts.c_ptr())) {
+                m_manager->raise_exception("datatype is not co-variant");
+            }
 
             u().compute_datatype_size_functions(m_def_block);
             for (symbol const& s : m_def_block) {
@@ -851,6 +854,48 @@ namespace datatype {
         return num_well_founded == num_types;
     }
 
+    /**
+       \brief Return true if the inductive datatype is co-variant.
+       Pre-condition: The given argument constrains the parameters of an inductive datatype.
+    */
+    bool util::is_covariant(unsigned num_types, sort* const* sorts) const {
+        ast_mark mark;
+        ptr_vector<sort> subsorts;
+
+        for (unsigned tid = 0; tid < num_types; tid++) {
+            mark.mark(sorts[tid], true);
+        }
+        
+        for (unsigned tid = 0; tid < num_types; tid++) {
+            sort* s = sorts[tid];
+            def const& d = get_def(s);
+            for (constructor const* c : d) {
+                for (accessor const* a : *c) {
+                    if (!is_covariant(mark, subsorts, a->range())) {
+                        return false;
+                    }
+                }
+            }
+        }
+        return true;
+    }
+
+    bool util::is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const {
+        array_util autil(m);
+        if (!autil.is_array(s)) {
+            return true;
+        }
+        unsigned n = get_array_arity(s);
+        subsorts.reset();
+        for (unsigned i = 0; i < n; ++i) {
+            get_subsorts(get_array_domain(s, i), subsorts);
+        }
+        for (sort* r : subsorts) {
+            if (mark.is_marked(r)) return false;
+        }
+        return is_covariant(mark, subsorts, get_array_range(s));
+    }
+
     def const& util::get_def(sort* s) const {
         return m_plugin->get_def(s);
     }
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 63a850ea8..748688804 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -314,6 +314,8 @@ namespace datatype {
         void compute_datatype_size_functions(svector<symbol> const& names);
         param_size::size* get_sort_size(sort_ref_vector const& params, sort* s);
         bool is_well_founded(unsigned num_types, sort* const* sorts);
+        bool is_covariant(unsigned num_types, sort* const* sorts) const;
+        bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
         def& get_def(symbol const& s) { return m_plugin->get_def(s); }
         void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;