From dda5dd7ccf16e41c60d691f9f899a9c5310ed346 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Sep 2024 13:54:04 -0700 Subject: [PATCH] Add support for handling 'distinct' expressions in SLS context and user sort plugin --- src/ast/sls/sls_context.cpp | 2 ++ src/ast/sls/sls_user_sort_plugin.cpp | 15 +++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 90755652a..2ed898add 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -181,6 +181,8 @@ namespace sls { family_id fid = to_app(e)->get_family_id(); if (m.is_eq(e)) fid = to_app(e)->get_arg(0)->get_sort()->get_family_id(); + if (m.is_distinct(e)) + fid = to_app(e)->get_arg(0)->get_sort()->get_family_id(); return fid; } diff --git a/src/ast/sls/sls_user_sort_plugin.cpp b/src/ast/sls/sls_user_sort_plugin.cpp index 018a5822a..af84f1b58 100644 --- a/src/ast/sls/sls_user_sort_plugin.cpp +++ b/src/ast/sls/sls_user_sort_plugin.cpp @@ -77,6 +77,21 @@ namespace sls { ctx.flip(flit.var()); } } + else if (e && m.is_distinct(e) && !lit.sign()) { + auto n = to_app(e)->get_num_args(); + for (unsigned i = 0; i < n; ++i) { + auto a = m_g->find(to_app(e)->get_arg(i)); + for (unsigned j = i + 1; j < n; ++j) { + auto b = m_g->find(to_app(e)->get_arg(j)); + if (a->get_root() == b->get_root()) { + verbose_stream() << "block " << mk_bounded_pp(e, m) << "\n"; + auto flit = block(a, b); + if (flit != sat::null_literal) + ctx.flip(flit.var()); + } + } + } + } else if (e && lit.sign()) { auto a = m_g->find(e); auto b = m_g->find(m.mk_true());