Replace add_axioms_for_is_empty body with length(s) == 0 form

[tautschnig]

Adopt the encoding the 2017 \deprecated tag on string_constraint_generatort::add_axioms_for_is_empty was pointing at — "should use string_length s == 0 instead" — and drop the deprecation now that the body matches the recommendation.

The previous body introduced a fresh boolean symbol is_empty and constrained it via two existentials is_empty ⇒ |s|=0 and |s|=0 ⇒ is_empty, then returned a typecast of that symbol. The two implications together define is_empty ⇔ (length(s) == 0), so the auxiliary symbol was pure indirection. Replace this with a direct return of length(s) == 0:

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_is_empty(
  const function_application_exprt &f)
{
  PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
  PRECONDITION(f.arguments().size() == 1);
  const array_string_exprt s = get_string_expr(array_pool, f.arguments()[0]);
  return {
    typecast_exprt::conditional_cast(
      equal_to(array_pool.get_or_create_length(s), 0), f.type()),
    {}};
}

Observable behaviour is unchanged (the SMT-level value of is_empty(s) still denotes length(s) == 0); the encoding now generates one fewer boolean variable and zero existential constraints per call site. The DEPRECATED macro is removed because the body is no longer the discouraged form.

add_axioms_for_is_empty is restored as a non-deprecated private helper on string_constraint_generatort, and the previously-inlined block in add_axioms_for_function_application is replaced with a single-line dispatch, matching the surrounding else if(id == ID_X) return add_axioms_for_X(expr); pattern of every other branch in the chain.

Test coverage

A new CORE-tagged regression test, jbmc/regression/jbmc-strings/java_isempty_nondet/, exercises add_axioms_for_is_empty for a non-constant string. The pre-existing java_empty/ and ConstantEvaluationIsEmpty/ tests use literal strings, which simplify_string_is_empty in src/util/simplify_expr.cpp constant-folds before the call reaches the string-refinement loop — so they do not cover the helper. The new test passes a nondet String argument through --function test_isempty_nondet.checkIsEmpty, defeating simplification and forcing the dispatch arm to be taken.

Coverage was confirmed by temporarily planting INVARIANT(false, ...) at the start of the helper: the new test triggers the invariant violation in the string-refinement loop, while java_empty/ runs to completion (the simplifier folds the call before the helper is reached). With the real implementation restored, both tests pass.

Fixes: #8019

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.60%. Comparing base (5453820) to head (9f5e2ba).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8915   +/-   ##
========================================
  Coverage    80.60%   80.60%           
========================================
  Files         1711     1711           
  Lines       189466   189464    -2     
  Branches        73       73           
========================================
+ Hits        152719   152721    +2     
+ Misses       36747    36743    -4     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[Copilot]

Pull request overview

Removes the deprecated add_axioms_for_is_empty helper from the string constraint generator and keeps is_empty support by inlining its logic in the function-application dispatch.

Changes:

• Removed the add_axioms_for_is_empty declaration from the public generator interface.
• Deleted the deprecated add_axioms_for_is_empty implementation from string_constraint_generator_testing.cpp.
• Inlined the is_empty constraint generation directly into add_axioms_for_function_application.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
src/solvers/strings/string_constraint_generator.h	Drops the deprecated add_axioms_for_is_empty method declaration.
src/solvers/strings/string_constraint_generator_testing.cpp	Removes the deprecated method definition and adjusts includes accordingly.
src/solvers/strings/string_constraint_generator_main.cpp	Replaces the call to the removed method with equivalent inlined constraint-generation logic.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.