From a3a3921234d4f2cb7f365c267974ca13af1bc623 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 30 Jan 2025 23:25:19 +0100 Subject: [PATCH] Minor --- src/ast/sls/sls_seq_plugin.cpp | 6 ++---- src/solver/smt_logics.cpp | 5 +++-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index a226d9122..f429075d9 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -1075,10 +1075,9 @@ namespace sls { b += strval0(y); } - // std::cout << "Repair down " << mk_pp(eq, m) << ": \"" << a << "\" = \"" << b << "\"" << std::endl; - if (a == b) - return update(eq->get_arg(0), a) && update(eq->get_arg(1), b); + return true; + // return update(eq->get_arg(0), a) && update(eq->get_arg(1), b); unsigned diff = edit_distance(a, b); @@ -1473,7 +1472,6 @@ namespace sls { zstring sb = strval0(b); unsigned lena = sa.length(); unsigned lenb = sb.length(); - verbose_stream() << "repair prefixof " << mk_bounded_pp(e, m) << "\n"; if (ctx.is_true(e)) { unsigned n = std::min(lena, lenb); if (!is_value(a)) { diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 5e4015a4d..a5e477016 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -103,6 +103,7 @@ bool smt_logics::logic_has_bv(symbol const & s) { s == "QF_UFBV" || s == "QF_ABV" || s == "QF_AUFBV" || + s == "QF_UFBVDT" || s == "QF_BVRE" || s == "QF_FPBV" || s == "FP" || @@ -149,7 +150,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) { } bool smt_logics::logic_has_uf(symbol const & s) { - return s == "QF_UF" || s == "UF" || s == "QF_UFDT" || s == "SMTFD"; + return s == "QF_UF" || s == "UF" || s == "QF_UFDT" || s == "QF_UFBVDT" || s == "SMTFD"; } bool smt_logics::logic_has_horn(symbol const& s) { @@ -161,6 +162,6 @@ bool smt_logics::logic_has_pb(symbol const& s) { } bool smt_logics::logic_has_datatype(symbol const& s) { - return s == "QF_FD" || s == "QF_UFDT" || logic_is_all(s) || s == "QF_DT" || logic_has_horn(s); + return s == "QF_FD" || s == "QF_UFDT" || s == "QF_UFBVDT" || logic_is_all(s) || s == "QF_DT" || logic_has_horn(s); }