From e92bda3a60261732ae97162f9bf5453a510026b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 31 Jul 2025 08:34:44 +0000 Subject: [PATCH] Work around Z3 not producing models for some quantified expressions Until the Z3 bug-fix (see Z3Prover/z3#7743) is available widely work around the problem that Z3's preprocessing introduces by adding extra symbols. This may cause solving to take longer, to be determined empirically. Fixes: #8679 --- src/solvers/smt2/smt2_conv.cpp | 171 +++++++++++++++++++-------------- src/solvers/smt2/smt2_conv.h | 1 + 2 files changed, 99 insertions(+), 73 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 80a9b973847..84a00cc4a16 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -67,6 +67,7 @@ smt2_convt::smt2_convt( use_datatypes(false), use_lambda_for_array(false), emit_set_logic(true), + quantifier_as_defined_expr(false), ns(_ns), out(_out), benchmark(_benchmark), @@ -136,6 +137,7 @@ smt2_convt::smt2_convt( use_lambda_for_array = true; emit_set_logic = false; use_datatypes = true; + quantifier_as_defined_expr = true; break; } @@ -888,16 +890,6 @@ void smt2_convt::convert_address_of_rec( expr.id_string()); } -static bool has_quantifier(const exprt &expr) -{ - bool result = false; - expr.visit_post([&result](const exprt &node) { - if(node.id() == ID_exists || node.id() == ID_forall) - result = true; - }); - return result; -} - literalt smt2_convt::convert(const exprt &expr) { PRECONDITION(expr.is_boolean()); @@ -928,28 +920,16 @@ literalt smt2_convt::convert(const exprt &expr) // Note that here we are always converting, so we do not need to consider // other literal kinds, only "|B###|" - // Z3 refuses get-value when a defined symbol contains a quantifier. - if(has_quantifier(prepared_expr)) - { - out << "(declare-fun "; - convert_literal(l); - out << " () Bool)\n"; - out << "(assert (= "; - convert_literal(l); - out << ' '; - convert_expr(prepared_expr); - out << "))\n"; - } - else - { - auto identifier = - convert_identifier(std::string{"B"} + std::to_string(l.var_no())); + auto identifier = + convert_identifier(std::string{"B"} + std::to_string(l.var_no())); + // we might already have put expr in defined_expressions via + // prepare_for_convert_expr + if(defined_expressions.find(expr) == defined_expressions.end()) defined_expressions[expr] = identifier; - smt2_identifiers.insert(identifier); - out << "(define-fun " << identifier << " () Bool "; - convert_expr(prepared_expr); - out << ")\n"; - } + smt2_identifiers.insert(identifier); + out << "(define-fun " << identifier << " () Bool "; + convert_expr(prepared_expr); + out << ")\n"; return l; } @@ -2439,36 +2419,50 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_forall || expr.id()==ID_exists) { - const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr); + bool already_converted = false; + if(quantifier_as_defined_expr) + { + defined_expressionst::const_iterator it = defined_expressions.find(expr); + if(it != defined_expressions.end()) + { + already_converted = true; + out << it->second; + } + } - if(solver==solvert::MATHSAT) - // NOLINTNEXTLINE(readability/throw) - throw "MathSAT does not support quantifiers"; + if(!already_converted) + { + const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr); - if(quantifier_expr.id() == ID_forall) - out << "(forall "; - else if(quantifier_expr.id() == ID_exists) - out << "(exists "; + if(solver == solvert::MATHSAT) + // NOLINTNEXTLINE(readability/throw) + throw "MathSAT does not support quantifiers"; + + if(quantifier_expr.id() == ID_forall) + out << "(forall "; + else if(quantifier_expr.id() == ID_exists) + out << "(exists "; - out << '('; - bool first = true; - for(const auto &bound : quantifier_expr.variables()) - { - if(first) - first = false; - else - out << ' '; out << '('; - convert_expr(bound); - out << ' '; - convert_type(bound.type()); - out << ')'; - } - out << ") "; + bool first = true; + for(const auto &bound : quantifier_expr.variables()) + { + if(first) + first = false; + else + out << ' '; + out << '('; + convert_expr(bound); + out << ' '; + convert_type(bound.type()); + out << ')'; + } + out << ") "; - convert_expr(quantifier_expr.where()); + convert_expr(quantifier_expr.where()); - out << ')'; + out << ')'; + } } else if( const auto object_size = expr_try_dynamic_cast(expr)) @@ -5137,30 +5131,61 @@ void smt2_convt::find_symbols(const exprt &expr) if(expr.id() == ID_exists || expr.id() == ID_forall) { + if( + quantifier_as_defined_expr && + defined_expressions.find(expr) != defined_expressions.end()) + { + return; + } + std::unordered_map> shadowed_syms; // do not declare the quantified symbol, but record // as 'bound symbol' const auto &q_expr = to_quantifier_expr(expr); - for(const auto &symbol : q_expr.variables()) - { - const auto identifier = symbol.get_identifier(); - auto id_entry = - identifier_map.insert({identifier, identifiert{symbol.type(), true}}); - shadowed_syms.insert( - {identifier, - id_entry.second ? std::nullopt - : std::optional{id_entry.first->second}}); - } - find_symbols(q_expr.where()); - for(const auto &[id, shadowed_val] : shadowed_syms) - { - auto previous_entry = identifier_map.find(id); - if(!shadowed_val.has_value()) - identifier_map.erase(previous_entry); - else - previous_entry->second = std::move(*shadowed_val); + if(!quantifier_as_defined_expr) + { + for(const auto &symbol : q_expr.variables()) + { + const auto identifier = symbol.get_identifier(); + auto id_entry = + identifier_map.insert({identifier, identifiert{symbol.type(), true}}); + shadowed_syms.insert( + {identifier, + id_entry.second ? std::nullopt + : std::optional{id_entry.first->second}}); + } + find_symbols(q_expr.where()); + for(const auto &[id, shadowed_val] : shadowed_syms) + { + auto previous_entry = identifier_map.find(id); + if(!shadowed_val.has_value()) + identifier_map.erase(previous_entry); + else + previous_entry->second = std::move(*shadowed_val); + } + } + else + { + find_symbols(q_expr.where()); + + const irep_idt id = + "quantified_expr." + std::to_string(defined_expressions.size()); + + out << "; the following is a workaround for solvers removing quantified " + "expression during preprocessing\n"; + out << "(declare-fun " << id << " () Bool)\n"; + + out << "(assert (=> " << id << ' '; + convert_expr(expr); + out << "))\n"; + out << "(assert (=> "; + convert_expr(expr); + out << ' ' << id << "))\n"; + + defined_expressions[expr] = id; } + return; } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index a2a8168c8aa..1f04b5f908b 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -71,6 +71,7 @@ class smt2_convt : public stack_decision_proceduret bool use_datatypes; bool use_lambda_for_array; bool emit_set_logic; + bool quantifier_as_defined_expr; exprt handle(const exprt &expr) override; void set_to(const exprt &expr, bool value) override;