From f2afb369bdf63c8db5dffc395aa2accfb0b96f73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Sep 2022 14:18:13 -0700 Subject: [PATCH] extend distinct check to ADT --- src/ast/datatype_decl_plugin.cpp | 22 ++++++++++++++++++++++ src/ast/datatype_decl_plugin.h | 2 ++ 2 files changed, 24 insertions(+) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 11c33d695..535500cae 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -635,6 +635,28 @@ namespace datatype { } } + bool plugin::are_distinct(app * a, app * b) const { + if (a == b) + return false; + if (is_unique_value(a) && is_unique_value(b)) + return true; + if (u().is_constructor(a) && u().is_constructor(b)) { + if (a->get_decl() != b->get_decl()) + return true; + for (unsigned i = a->get_num_args(); i-- > 0; ) { + if (!is_app(a->get_arg(i))) + continue; + if (!is_app(b->get_arg(i))) + continue; + app* _a = to_app(a->get_arg(i)); + app* _b = to_app(b->get_arg(i)); + if (m_manager->are_distinct(_a, _b)) + return true; + } + } + return false; + } + expr * plugin::get_some_value(sort * s) { SASSERT(u().is_datatype(s)); func_decl * c = u().get_non_rec_constructor(s); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 310175781..4561dfacf 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -233,6 +233,8 @@ namespace datatype { bool is_value(app* e) const override { return is_value_aux(false, e); } bool is_unique_value(app * e) const override { return is_value_aux(true, e); } + + bool are_distinct(app * a, app * b) const override; void get_op_names(svector & op_names, symbol const & logic) override;