From c9ac4d6f75119ecae98fe74b5c6099c1fd4adf0e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jan 2025 16:34:17 -0800 Subject: [PATCH 1/3] pre-flatten use list before iterating over m_unsat select_max_same_sign accesses the use-list which may cause it to be flattened. --- src/ast/sls/sat_ddfw.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index da6d567f8..1e9c484af 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -558,6 +558,7 @@ namespace sat { void ddfw::shift_weights() { ++m_shifts; bool shifted = false; + flatten_use_list(); for (unsigned to_idx : m_unsat) { SASSERT(!m_clauses[to_idx].is_true()); unsigned from_idx = select_max_same_sign(to_idx); From eb825855face337a760ead61754ae77b893e28d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jan 2025 16:34:36 -0800 Subject: [PATCH 2/3] increase the log level on callbacks with bit-indices that get set --- src/ast/sls/sls_smt_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index 9d614f773..8ec7bb11d 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -343,7 +343,7 @@ namespace sls { m_ddfw->add(1, &sls_lit); } else { - IF_VERBOSE(0, verbose_stream() << "value restriction " << lit << " " + IF_VERBOSE(4, verbose_stream() << "value restriction " << lit << " " << mk_bounded_pp(ctx.bool_var2expr(lit.var()), m) << "\n"); } } From 1ce6e66ac9b73e57ad93be95fa7797e4b1588c3e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jan 2025 16:34:54 -0800 Subject: [PATCH 3/3] generalize logic detection to use sub-string matching --- src/solver/smt_logics.cpp | 95 ++++++++++----------------------------- 1 file changed, 24 insertions(+), 71 deletions(-) diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 5e4015a4d..02c884268 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -30,83 +30,38 @@ bool smt_logics::supported_logic(symbol const & s) { bool smt_logics::logic_has_reals_only(symbol const& s) { return - s == "QF_RDL" || - s == "QF_LRA" || - s == "UFLRA" || - s == "LRA" || - s == "RDL" || - s == "NRA" || - s == "QF_NRA" || - s == "QF_UFNRA" || - s == "QF_UFLRA"; + s.str().find("LRA") != std::string::npos || + s.str().find("LRA") != std::string::npos || + s.str().find("NRA") != std::string::npos || + s.str().find("RDL") != std::string::npos; } bool smt_logics::logic_has_arith(symbol const & s) { return - s == "QF_LRA" || - s == "QF_LIA" || - s == "QF_RDL" || - s == "QF_IDL" || - s == "QF_AUFLIA" || - s == "QF_ALIA" || - s == "QF_AUFLIRA" || - s == "QF_AUFNIA" || - s == "QF_AUFNIRA" || - s == "QF_ANIA" || - s == "QF_LIRA" || - s == "QF_UFLIA" || - s == "QF_UFLRA" || - s == "QF_UFIDL" || - s == "QF_UFRDL" || - s == "QF_NIA" || - s == "QF_NRA" || - s == "QF_NIRA" || - s == "QF_UFNRA" || - s == "QF_UFNIA" || - s == "QF_UFNIRA" || + s.str().find("LRA") != std::string::npos || + s.str().find("LIRA") != std::string::npos || + s.str().find("LIA") != std::string::npos || + s.str().find("LRA") != std::string::npos || + s.str().find("NRA") != std::string::npos || + s.str().find("NIRA") != std::string::npos || + s.str().find("NIA") != std::string::npos || + s.str().find("IDL") != std::string::npos || + s.str().find("RDL") != std::string::npos || s == "QF_BVRE" || - s == "QF_SNIA" || - s == "ALIA" || - s == "AUFLIA" || - s == "AUFLIRA" || - s == "AUFNIA" || - s == "AUFNIRA" || - s == "UFLIA" || - s == "UFLRA" || - s == "UFNRA" || - s == "UFNIRA" || - s == "NIA" || - s == "NRA" || - s == "UFNIA" || - s == "LIA" || - s == "LRA" || - s == "UFIDL" || s == "QF_FP" || s == "FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_S" || - s == "QF_SLIA" || logic_is_all(s) || s == "QF_FD" || - s == "HORN" || - s == "QF_FPLRA"; + s == "HORN"; } bool smt_logics::logic_has_bv(symbol const & s) { return - s == "UFBV" || - s == "AUFBV" || - s == "ABV" || - s == "BV" || - s == "QF_BV" || - s == "QF_UFBV" || - s == "QF_ABV" || - s == "QF_AUFBV" || - s == "QF_BVRE" || - s == "QF_FPBV" || + s.str().find("BV") != std::string::npos || s == "FP" || - s == "QF_BVFP" || logic_is_all(s) || s == "QF_FD" || s == "SMTFD" || @@ -115,13 +70,7 @@ bool smt_logics::logic_has_bv(symbol const & s) { bool smt_logics::logic_has_array(symbol const & s) { return - s == "QF_AX" || - s == "QF_AUFLIA" || - s == "QF_ANIA" || - s == "QF_ALIA" || - s == "QF_AUFLIRA" || - s == "QF_AUFNIA" || - s == "QF_AUFNIRA" || + s.str().find("QF_A") != std::string::npos || s == "ALIA" || s == "AUFLIA" || s == "AUFLIRA" || @@ -130,8 +79,6 @@ bool smt_logics::logic_has_array(symbol const & s) { s == "AUFBV" || s == "ABV" || logic_is_all(s) || - s == "QF_ABV" || - s == "QF_AUFBV" || s == "SMTFD" || s == "HORN"; } @@ -149,7 +96,9 @@ 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.str().find("UF") != std::string::npos || + s == "SMTFD"; } bool smt_logics::logic_has_horn(symbol const& s) { @@ -161,6 +110,10 @@ 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.str().find("DT") != std::string::npos || + s == "QF_FD" || + logic_is_all(s) || + logic_has_horn(s); }