From c85e2ee2bdb06ac7bec6692e4a2d6a722a87d991 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Jun 2026 09:50:41 -0700 Subject: [PATCH] sort constraint Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 +--- src/smt/smt_internalizer.cpp | 12 ++---------- 2 files changed, 3 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 559b329b05..f11b54aeb1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -880,9 +880,7 @@ namespace smt { void undo_mk_enode(); - void apply_sort_cnstr(app * term, enode * e); - - void apply_sort_cnstr(quantifier *term, enode *e); + void apply_sort_cnstr(expr * term, enode * e); bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 59d10e1c3e..3bb498882a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1085,22 +1085,14 @@ namespace smt { /** \brief Apply sort constraints on e. */ - void context::apply_sort_cnstr(app * term, enode * e) { - sort * s = term->get_decl()->get_range(); + void context::apply_sort_cnstr(expr * term, enode * e) { + sort * s = term->get_sort(); theory * th = m_theories.get_plugin(s->get_family_id()); if (th) { th->apply_sort_cnstr(e, s); } } - void context::apply_sort_cnstr(quantifier *lambda_term, enode *e) { - sort *s = lambda_term->get_sort(); - theory *th = m_theories.get_plugin(s->get_family_id()); - if (th) { - th->apply_sort_cnstr(e, s); - } - } - /** \brief Return the literal associated with n. */