From bd8bed1759d823ed418e41050e6c95594e9d6ddf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Dec 2023 12:55:37 -0800 Subject: [PATCH] handle ac-op in legacy special relations procedure by adding warning Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 11 ++++++++--- src/smt/theory_special_relations.h | 1 + 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index b6370f153..6203df103 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -130,7 +130,11 @@ namespace smt { } bool theory_special_relations::internalize_term(app * term) { - verbose_stream() << mk_pp(term, m) << "\n"; + m_terms.push_back(term); + ctx.push_trail(push_back_vector(m_terms)); + std::stringstream strm; + strm << "term not not handled by special relations procedure. Use sat.smt=true " << mk_pp(term, m); + warning_msg(strm.str().c_str()); return false; } @@ -207,9 +211,10 @@ namespace smt { if (new_equality) { return FC_CONTINUE; } - else { + else if (!m_terms.empty()) + return FC_GIVEUP; + else return FC_DONE; - } } lbool theory_special_relations::final_check_lo(relation& r) { diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 73e889a5d..65ce17907 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -131,6 +131,7 @@ namespace smt { special_relations_util m_util; atoms m_atoms; unsigned_vector m_atoms_lim; + ptr_vector m_terms; obj_map m_relations; bool_var2atom m_bool_var2atom; bool m_can_propagate;