From 32d806d500c8c1be4aacdd1541226a5b9bce7c77 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Jun 2026 21:20:31 -0700 Subject: [PATCH] fix warnings Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tptp_frontend.cpp | 55 ++++++++++++++++--------------- 1 file changed, 28 insertions(+), 27 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 0b61f06e90..16cd9dee2c 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -7,7 +7,6 @@ #include #include #include -#include #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" @@ -277,10 +276,10 @@ public: }; struct parsed_type { - std::vector domain; + ptr_vector domain; sort* range = nullptr; parsed_type(sort* s): range(s) {} - parsed_type(std::vector const& d, sort* r): domain(d), range(r) {} + parsed_type(ptr_vector const& d, sort* r): domain(d), range(r) {} }; class tptp_parser { @@ -298,7 +297,7 @@ class tptp_parser { std::unordered_map m_decls; func_decl_ref_vector m_pinned_decls; // prevents cached func_decls from being freed expr_ref_vector m_pinned_exprs; // prevents bound variable apps from being freed - std::unordered_map, sort*>> m_typed_decls; + std::unordered_map, sort*>> m_typed_decls; std::vector> m_bound; bool m_in_at_arg = false; // true when parsing inside @ argument (lambda body stops consuming @) struct implicit_var_scope { @@ -451,7 +450,7 @@ class tptp_parser { // For higher-order types like ($i > $o), create an uninterpreted sort // Function type A > B is represented as Array(A, B). // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried). - sort* get_ho_sort(std::vector const& domain, sort* range) { + sort* get_ho_sort(ptr_vector const& domain, sort* range) { sort* s = range; for (int i = (int)domain.size() - 1; i >= 0; --i) s = m_array.mk_array_sort(domain[i], s); @@ -515,7 +514,8 @@ class tptp_parser { if (itt != m_typed_decls.end()) { std::string typed_decl_key = mk_decl_key(name, arity, 'd'); auto itd = m_decls.find(typed_decl_key); - if (itd != m_decls.end()) return itd->second; + if (itd != m_decls.end()) + return itd->second; auto const& sig = itt->second; func_decl* f = m.mk_func_decl(symbol(name), sig.first.size(), sig.first.data(), sig.second); m_pinned_decls.push_back(f); @@ -527,7 +527,7 @@ class tptp_parser { auto itd = m_decls.find(key); if (itd != m_decls.end()) return itd->second; - std::vector dom(arity, m_univ); + ptr_vector dom(arity, m_univ); func_decl* f = m.mk_func_decl(symbol(name), arity, dom.data(), pred ? m.mk_bool_sort() : m_univ); m_pinned_decls.push_back(f); m_decls.emplace(key, f); @@ -707,14 +707,14 @@ class tptp_parser { // ::= $oType | $o | $iType | $i | $tType | $real | $rat | $int parsed_type parse_type_atom() { if (accept(token_kind::lparen)) { - std::vector prod = parse_type_product_raw(); + ptr_vector prod = parse_type_product_raw(); if (accept(token_kind::gt_tok)) { // Full function type inside parens: (A * B > C) or (A > B > C) parsed_type rhs = parse_type_expr(); - std::vector full_domain = prod; + ptr_vector full_domain = prod; if (!rhs.domain.empty()) { // Nested higher-order: (A > B > C) → flatten - full_domain.insert(full_domain.end(), rhs.domain.begin(), rhs.domain.end()); + full_domain.append(rhs.domain); } expect(token_kind::rparen, "')'"); // Return with domain/range preserved for proper flattening @@ -753,15 +753,15 @@ class tptp_parser { // Grammar: ::= * // | * // Product types form the domain in mapping types: (A * B) > C - std::vector parse_type_product_raw() { + ptr_vector parse_type_product_raw() { parsed_type first = parse_type_atom(); if (!first.domain.empty() && first.range == nullptr) { // Already a parenthesized product from nested parens - std::vector args = first.domain; + ptr_vector args = first.domain; while (accept(token_kind::star_tok)) { parsed_type t = parse_type_atom(); if (!t.domain.empty()) { - args.insert(args.end(), t.domain.begin(), t.domain.end()); + args.append(t.domain); } else { args.push_back(t.range); } @@ -771,28 +771,28 @@ class tptp_parser { if (!first.domain.empty()) { // Function type as first element of product — use ho_sort sort* ho = get_ho_sort(first.domain, first.range); - std::vector args; + ptr_vector args; args.push_back(ho); while (accept(token_kind::star_tok)) { parsed_type t = parse_type_atom(); if (!t.domain.empty() && t.range != nullptr) { args.push_back(get_ho_sort(t.domain, t.range)); } else if (!t.domain.empty()) { - args.insert(args.end(), t.domain.begin(), t.domain.end()); + args.append(t.domain); } else { args.push_back(t.range); } } return args; } - std::vector args; + ptr_vector args; args.push_back(first.range); while (accept(token_kind::star_tok)) { parsed_type t = parse_type_atom(); if (!t.domain.empty() && t.range != nullptr) { args.push_back(get_ho_sort(t.domain, t.range)); } else if (!t.domain.empty()) { - args.insert(args.end(), t.domain.begin(), t.domain.end()); + args.append(t.domain); } else { args.push_back(t.range); } @@ -811,7 +811,7 @@ class tptp_parser { return first; } // Build product vector - std::vector args; + ptr_vector args; if (!first.domain.empty() && first.range != nullptr) { // Function type used as element in a product args.push_back(get_ho_sort(first.domain, first.range)); @@ -826,7 +826,7 @@ class tptp_parser { if (!t.domain.empty() && t.range != nullptr) { args.push_back(get_ho_sort(t.domain, t.range)); } else if (!t.domain.empty()) { - args.insert(args.end(), t.domain.begin(), t.domain.end()); + args.append(t.domain); } else { args.push_back(t.range); } @@ -843,7 +843,7 @@ class tptp_parser { if (is(token_kind::type_forall_tok) || is(token_kind::type_exists_tok)) { next(); expect(token_kind::lbrack, "'['"); - std::vector type_params; + ptr_vector type_params; if (!accept(token_kind::rbrack)) { do { std::string tv = parse_name(); @@ -858,8 +858,8 @@ class tptp_parser { parsed_type inner = parse_type_expr(); // Prepend type params to domain if (!type_params.empty()) { - std::vector full_domain = type_params; - full_domain.insert(full_domain.end(), inner.domain.begin(), inner.domain.end()); + ptr_vector full_domain = type_params; + full_domain.append(inner.domain); return parsed_type(full_domain, inner.range); } return inner; @@ -868,7 +868,7 @@ class tptp_parser { if (accept(token_kind::gt_tok)) { parsed_type rhs = parse_type_expr(); // prod is either a product (domain non-empty, range==nullptr) or a single sort (domain empty) - std::vector domain; + ptr_vector domain; if (!prod.domain.empty() && prod.range == nullptr) { domain = prod.domain; } else if (!prod.domain.empty() && prod.range != nullptr) { @@ -879,7 +879,7 @@ class tptp_parser { } if (!rhs.domain.empty()) { // Higher-order result type: A > (B > C) flattened to (A, B) > C - domain.insert(domain.end(), rhs.domain.begin(), rhs.domain.end()); + domain.append(rhs.domain); return parsed_type(domain, rhs.range); } return parsed_type(domain, rhs.range); @@ -1222,7 +1222,7 @@ class tptp_parser { // --- Part 1: Parse type declarations --- std::vector let_names; - std::vector let_sorts; + ptr_vector let_sorts; auto parse_one_typing = [&]() { std::string name = parse_name(); @@ -1883,6 +1883,8 @@ class tptp_parser { else if (role == "logic") { // Modal logic declarations ($modal == [...]) — skip the formula body skip_annotations_until_rparen(); + warning_msg("non-classical logics are not supported"); + ++m_dropped_formulas; } else { try { @@ -1906,8 +1908,7 @@ class tptp_parser { // subsequent "sat" verdict is unsound: it may only hold because the // dropped formula was missing. The count is used to downgrade a sat // result to GaveUp rather than report a spurious CounterSatisfiable. - if (role != "conjecture") - ++m_dropped_formulas; + ++m_dropped_formulas; IF_VERBOSE(0, verbose_stream() << "skipping formula '" << formula_name << "' (role " << role << ") due to: " << ex.what() << "\n"); // Skip to '.' to resync the parser for the next annotated formula