From 6beec7b642706cdcb830594151131869b6ddc683 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2020 02:04:44 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_justification.h | 1 + src/ast/seq_decl_plugin.cpp | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/euf/euf_justification.h b/src/ast/euf/euf_justification.h index dff67a4d5..68d7d214f 100644 --- a/src/ast/euf/euf_justification.h +++ b/src/ast/euf/euf_justification.h @@ -53,6 +53,7 @@ namespace euf { bool is_external() const { return m_kind == external_t; } bool is_congruence() const { return m_kind == congruence_t; } + bool is_commutative() const { return m_comm; } template T* ext() const { SASSERT(is_external()); return static_cast(m_external); } }; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index df11184a4..e9d02611e 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1855,8 +1855,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) const { if (is_known()) { if (i.is_known()) { - unsigned ite_min_length = std::min(min_length, i.min_length); - lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef); + // unsigned ite_min_length = std::min(min_length, i.min_length); + // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef); //TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height)); }