SMT2 back-end: declare a quantified logic when quantifiers are emitted

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;
+}

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;
+}

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.

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.

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'],

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;

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 << " ";

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 -

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();

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)
   {