From 2daa6be1098534d9c5e76808fd9216447711f910 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Oct 2026 17:34:52 +0000 Subject: [PATCH] SMT2 back-end: declare a quantified logic when quantifiers are emitted The generic SMT2 encoding (--smt2 --outfile, and external solvers that take a declared logic) writes `(set-logic QF_AUFBV)', yet emits universally quantified assertions as the substitute for array_of and array_comprehension when neither `as const' nor lambdas are available, and for forall/exists expressions. A logic named QF_... admits no quantifiers: z3 and cvc5 rejected such files ("logic does not support quantifiers"; cvc5: "... which doesn't include THEORY_QUANTIFIERS"), e.g. for regression/unit-proofs/bigint_arith. The header used to be written by the constructor, before the encoding is known. A converter constructed for a complete problem (the outfile and stdout paths of the solver factory, and smt2_dect) with a QF_ logic now holds its output back and writes the header when solving (and on destruction), with the QF_ prefix dropped if a quantifier was emitted. Streaming users (unit tests, the cprover and horn encodings) are unchanged. Test: regression/cbmc/smt2_logic_with_quantifiers (AUFBV with a quantified array initialisation, QF_AUFBV without). Co-authored-by: Kiro --- .../cbmc/smt2_logic_with_quantifiers/main.c | 11 ++++++ .../quantifier_free.c | 6 ++++ .../smt2_logic_with_quantifiers/test.desc | 15 ++++++++ .../test_quantifier_free.desc | 12 +++++++ regression/validate-trace-xml-schema/check.py | 2 ++ src/goto-checker/solver_factory.cpp | 6 ++-- src/solvers/smt2/smt2_conv.cpp | 36 ++++++++++++++++--- src/solvers/smt2/smt2_conv.h | 36 +++++++++++++++++-- src/solvers/smt2/smt2_dec.cpp | 2 ++ src/solvers/smt2/smt2_dec.h | 9 ++++- 10 files changed, 126 insertions(+), 9 deletions(-) create mode 100644 regression/cbmc/smt2_logic_with_quantifiers/main.c create mode 100644 regression/cbmc/smt2_logic_with_quantifiers/quantifier_free.c create mode 100644 regression/cbmc/smt2_logic_with_quantifiers/test.desc create mode 100644 regression/cbmc/smt2_logic_with_quantifiers/test_quantifier_free.desc diff --git a/regression/cbmc/smt2_logic_with_quantifiers/main.c b/regression/cbmc/smt2_logic_with_quantifiers/main.c new file mode 100644 index 000000000000..f6c7830ffe8d --- /dev/null +++ b/regression/cbmc/smt2_logic_with_quantifiers/main.c @@ -0,0 +1,11 @@ +int main() +{ + unsigned n; + __CPROVER_assume(n > 0 && n < 8); + int a[n]; + __CPROVER_array_set(a, 0); + unsigned i; + __CPROVER_assume(i < n); + __CPROVER_assert(a[i] == 0, "zero"); + return 0; +} diff --git a/regression/cbmc/smt2_logic_with_quantifiers/quantifier_free.c b/regression/cbmc/smt2_logic_with_quantifiers/quantifier_free.c new file mode 100644 index 000000000000..9fb81ad4de95 --- /dev/null +++ b/regression/cbmc/smt2_logic_with_quantifiers/quantifier_free.c @@ -0,0 +1,6 @@ +int main() +{ + unsigned x; + __CPROVER_assert(x + 1 != 0 || x == 0xffffffffu, "p"); + return 0; +} diff --git a/regression/cbmc/smt2_logic_with_quantifiers/test.desc b/regression/cbmc/smt2_logic_with_quantifiers/test.desc new file mode 100644 index 000000000000..ea868087b76f --- /dev/null +++ b/regression/cbmc/smt2_logic_with_quantifiers/test.desc @@ -0,0 +1,15 @@ +CORE broken-smt-backend no-new-smt +main.c +--smt2 --outfile - +^\(set-logic AUFBV\)$ +^\(assert \(forall +^EXIT=0$ +^SIGNAL=0$ +-- +QF_AUFBV +-- +The generic SMT2 encoding writes a zero-initialised array of symbolic size +(array_of without `as const') as a universally quantified assertion. A +logic named QF_... admits no quantifiers, so the declared logic is AUFBV; +z3 and cvc5 rejected the file ("logic does not support quantifiers"). +broken-smt-backend: the test inspects the generic output only. diff --git a/regression/cbmc/smt2_logic_with_quantifiers/test_quantifier_free.desc b/regression/cbmc/smt2_logic_with_quantifiers/test_quantifier_free.desc new file mode 100644 index 000000000000..5565d71719ea --- /dev/null +++ b/regression/cbmc/smt2_logic_with_quantifiers/test_quantifier_free.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend no-new-smt paths-lifo-expected-failure +quantifier_free.c +--smt2 --outfile - +^\(set-logic QF_AUFBV\)$ +^EXIT=0$ +^SIGNAL=0$ +-- +forall +-- +Without a quantifier the declared logic stays quantifier-free. +With --paths lifo the assertion is decided during symbolic execution and no +formula is written, hence paths-lifo-expected-failure. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 8ede2e47dd33..94aedbf7ad83 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -15,6 +15,8 @@ # these tests dump the raw SMT2 output (using --outfile) ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'], ['deterministic-smt-output', 'test.desc'], + ['smt2_logic_with_quantifiers', 'test.desc'], + ['smt2_logic_with_quantifiers', 'test_quantifier_free.desc'], ['z3-lambda-unflatten', 'test.desc'], # these tests expect input from stdin ['json-interface1', 'test_wrong_option.desc'], diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 3e18d0468123..cd12e10603e8 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -548,7 +548,8 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) std::string("Generated by CBMC ") + CBMC_VERSION, "QF_AUFBV", solver, - std::cout); + std::cout, + /*complete_problem=*/true); if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; @@ -565,7 +566,8 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) std::string("Generated by CBMC ") + CBMC_VERSION, "QF_AUFBV", solver, - *out); + *out, + /*complete_problem=*/true); if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e3abf106e7df..93ebed2eaea1 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -65,9 +65,16 @@ smt2_convt::smt2_convt( const std::string &_notes, const std::string &_logic, solvert _solver, - std::ostream &_out) + std::ostream &_out, + bool _complete_problem) : ns(_ns), - out(_out), + final_out(_out), + // only solvers whose header declares the (quantifier-free) logic + defer_output( + _complete_problem && _solver != solvert::BITWUZLA && + _solver != solvert::CPROVER_SMT2 && _solver != solvert::Z3 && + _solver != solvert::CVC5 && _logic.rfind("QF_", 0) == 0), + out(defer_output ? deferred_output : _out), benchmark(_benchmark), notes(_notes), logic(_logic), @@ -133,7 +140,8 @@ smt2_convt::smt2_convt( break; } - write_header(); + if(!defer_output) + write_header(); } std::string smt2_convt::decision_procedure_text() const @@ -164,8 +172,24 @@ tvt smt2_convt::l_get(literalt l) const return tvt(boolean_assignment[l.var_no()]^l.sign()); } +void smt2_convt::flush_deferred_output() +{ + if(!defer_output) + return; + if(!header_written) + { + if(quantifier_emitted && logic.rfind("QF_", 0) == 0) + logic = logic.substr(3); + write_header(); + } + final_out << deferred_output.str(); + deferred_output.str(std::string{}); +} + void smt2_convt::write_header() { + header_written = true; + std::ostream &out = final_out; out << "; SMT 2" << "\n"; switch(solver) @@ -297,7 +321,8 @@ decision_proceduret::resultt smt2_convt::dec_solve(const exprt &assumption) assumptions.pop_back(); } - out.flush(); + flush_deferred_output(); + final_out.flush(); return decision_proceduret::resultt::D_ERROR; } @@ -2610,6 +2635,7 @@ void smt2_convt::convert_expr(const exprt &expr) // NOLINTNEXTLINE(readability/throw) throw "MathSAT does not support quantifiers"; + quantifier_emitted = true; if(quantifier_expr.id() == ID_forall) out << "(forall "; else if(quantifier_expr.id() == ID_exists) @@ -5888,6 +5914,7 @@ void smt2_convt::find_symbols(const exprt &expr) if(!is_zero_width(array_type.element_type(), ns)) { // use a quantifier-based initialization instead of lambda + quantifier_emitted = true; out << "(assert (forall ((i "; convert_type(array_type.index_type()); out << ")) (= (select " << id << " i) "; @@ -5926,6 +5953,7 @@ void smt2_convt::find_symbols(const exprt &expr) out << "; the following is a substitute for lambda i . x(i)\n"; out << "; universally quantified initialization of the array\n"; + quantifier_emitted = true; out << "(assert (forall (("; convert_expr(array_comprehension.arg()); out << " "; diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ca94493a6be4..cd6d7ef5d33e 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -53,15 +53,32 @@ class smt2_convt : public stack_decision_proceduret Z3 }; + /// \param _ns: namespace for looking up symbols and types + /// \param _benchmark: benchmark name, for the header + /// \param _notes: notes, for the header + /// \param _logic: the SMT-LIB logic to declare + /// \param _solver: the solver the output is meant for + /// \param _out: the output stream + /// \param _complete_problem: the output is a complete problem, written + /// in one go when solving (and on destruction): a quantifier-free + /// logic declared in the header (`QF_...`) is then replaced by its + /// quantified form if the encoding emits a quantifier. Otherwise the + /// output is streamed as it is produced. smt2_convt( const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, - std::ostream &_out); + std::ostream &_out, + bool _complete_problem = false); - ~smt2_convt() override = default; + ~smt2_convt() override + { + // output held back but never solved (e.g. every property simplified + // away) is still written + flush_deferred_output(); + } bool use_FPA_theory = false; bool use_array_of_bool = false; @@ -97,6 +114,17 @@ class smt2_convt : public stack_decision_proceduret protected: const namespacet &ns; + /// The stream given to the constructor. When the declared logic is + /// quantifier-free (`QF_...`) the output is held back in + /// `deferred_output` until it is complete enough to know whether a + /// quantifier was emitted (see `flush_deferred_output`). + std::ostream &final_out; + std::stringstream deferred_output; + const bool defer_output; + bool header_written = false; + /// A `forall` or `exists` was emitted (also as the substitute for + /// `array_of` / `array_comprehension` without `as const` or lambdas). + bool quantifier_emitted = false; std::ostream &out; std::string benchmark, notes, logic; solvert solver; @@ -112,6 +140,10 @@ class smt2_convt : public stack_decision_proceduret resultt dec_solve(const exprt &) override; void write_header(); + /// Write the header -- with the logic made quantified if a quantifier was + /// emitted (an SMT-LIB logic named `QF_...` admits no quantifiers) -- and + /// the output held back so far to `final_out`. + void flush_deferred_output(); /// Writes the end of the SMT file to the `smt_convt::out` stream. These parts /// of the output may be changed when using multiple rounds of solving. They /// include the following parts of the output file - diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index cbe6ecb8ebc3..a947fc5dba6e 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -45,10 +45,12 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) if(assumption.is_not_nil()) assumptions.push_back(convert(assumption)); + flush_deferred_output(); cached_output << stringstream.str(); stringstream.str(std::string{}); write_footer(); + flush_deferred_output(); if(assumption.is_not_nil()) assumptions.pop_back(); diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index 2b51118aee25..4fd13058be17 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -33,7 +33,14 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt solvert _solver, const std::string &_solver_binary_or_empty, message_handlert &_message_handler) - : smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream), + : smt2_convt( + _ns, + _benchmark, + _notes, + _logic, + _solver, + stringstream, + /*complete_problem=*/true), solver_binary_or_empty(_solver_binary_or_empty), message_handler(_message_handler) {