Simplify algebraic identities involving commutative operators by tautschnig · Pull Request #8951 · diffblue/cbmc

tautschnig · 2026-04-02T10:28:28Z

Recognize commutativity (ab == ba), distributivity (a*(b+c) == ab+ac), and associativity ((ab)c == a(bc)) in the expression simplifier and reduce them to true/false before bit-blasting. This applies to all commutative operators: mult, plus, bitand, bitor, bitxor.

These simplifications make verification of algebraic properties instant at any bitwidth, matching the word-level reasoning that SMT solvers like Z3 perform internally.

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.

Copilot

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

Recognize commutativity (a*b == b*a), distributivity (a*(b+c) == a*b+a*c), and associativity ((a*b)*c == a*(b*c)) in the expression simplifier and reduce them to true/false before bit-blasting. This applies to all commutative operators: mult, plus, bitand, bitor, bitxor. These simplifications make verification of algebraic properties instant at any bitwidth, matching the word-level reasoning that SMT solvers like Z3 perform internally. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

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

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

Copilot · 2026-04-03T15:52:39Z

src/util/simplify_expr_int.cpp

+        std::sort(leaves0.begin(), leaves0.end());
+        std::sort(leaves1.begin(), leaves1.end());


std::sort requires a strict-weak-ordering comparator. Unless exprt provides a stable operator< (not guaranteed), this can fail to compile or sort inconsistently. Prefer sorting using an explicit comparator based on the project’s structural compare (e.g., an irept/exprt compare helper used elsewhere for maps/sets) so the ordering is well-defined and deterministic.

Suggested change

std::sort(leaves0.begin(), leaves0.end());

std::sort(leaves1.begin(), leaves1.end());

const auto expr_less = [](const exprt &lhs, const exprt &rhs) {

return lhs.compare(rhs) < 0;

};

std::sort(leaves0.begin(), leaves0.end(), expr_less);

std::sort(leaves1.begin(), leaves1.end(), expr_less);

Copilot · 2026-04-03T15:52:39Z

src/util/simplify_expr_int.cpp

+      if(
+        leaves0.size() == leaves1.size() && leaves0.size() >= 2 &&
+        leaves0.size() <= 8)


The <= 8 cutoff is an undocumented magic number that changes when this simplification triggers. Make this a named constant (and briefly justify it, e.g., to cap cost), or consider a cost-based limit (e.g., total nodes visited) so future changes to operand normalization don’t require re-tuning an arbitrary threshold.

Suggested change

if(

leaves0.size() == leaves1.size() && leaves0.size() >= 2 &&

leaves0.size() <= 8)

// Keep the flatten-and-sort comparison cheap; larger expressions are

// left to the general simplifier rather than paying this extra cost.

constexpr std::size_t max_commutative_leaf_count_for_sort_compare = 8;

if(

leaves0.size() == leaves1.size() && leaves0.size() >= 2 &&

leaves0.size() <= max_commutative_leaf_count_for_sort_compare)

Copilot · 2026-04-03T15:52:40Z

src/util/simplify_expr_int.cpp

+      for(int i = 0; i < 2; ++i)
+      {
+        const exprt &factor = e.operands()[i];
+        const exprt &sum = e.operands()[1 - i];
+        if(sum.id() == ID_plus && sum.operands().size() == 2)
+        {
+          mult_exprt prod0(factor, sum.operands()[0]);
+          prod0.type() = e.type();
+          mult_exprt prod1(factor, sum.operands()[1]);
+          prod1.type() = e.type();
+          plus_exprt result(std::move(prod0), std::move(prod1));
+          result.type() = e.type();
+          return std::move(result);
+        }
+      }
+      return {};


Use an unsigned/index type for indexing (std::size_t) or avoid indexing entirely (two explicit cases) to prevent signed/unsigned mixing and make the intent clearer. This is small here, but this code is in a core simplification path and benefits from consistently safe indexing patterns.

Suggested change

for(int i = 0; i < 2; ++i)

{

const exprt &factor = e.operands()[i];

const exprt &sum = e.operands()[1 - i];

if(sum.id() == ID_plus && sum.operands().size() == 2)

{

mult_exprt prod0(factor, sum.operands()[0]);

prod0.type() = e.type();

mult_exprt prod1(factor, sum.operands()[1]);

prod1.type() = e.type();

plus_exprt result(std::move(prod0), std::move(prod1));

result.type() = e.type();

return std::move(result);

}

}

return {};

const auto try_distribute =

[&e](const exprt &factor, const exprt &sum) -> std::optional<exprt>

{

if(sum.id() != ID_plus || sum.operands().size() != 2)

return {};

mult_exprt prod0(factor, sum.operands()[0]);

prod0.type() = e.type();

mult_exprt prod1(factor, sum.operands()[1]);

prod1.type() = e.type();

plus_exprt result(std::move(prod0), std::move(prod1));

result.type() = e.type();

return std::move(result);

};

if(auto distributed = try_distribute(e.operands()[0], e.operands()[1]))

return distributed;

return try_distribute(e.operands()[1], e.operands()[0]);

Copilot · 2026-04-03T15:52:40Z

unit/util/simplify_expr.cpp

+  SECTION("Commutativity: a * b == b * a")
+  {
+    const equal_exprt eq{mult_exprt{a, b}, mult_exprt{b, a}};
+    REQUIRE(simplify_expr(eq, ns) == true_exprt{});
+  }


The implementation extends commutativity/associativity handling to bitand, bitor, and bitxor, and also adds associativity-based flattening (up to the leaf limit). There’s only one bitwise commutativity test and no coverage for bitwise associativity (e.g., (a & b) & c == a & (b & c)), bitwise operand permutations beyond 2 operands, or != cases for associativity/flattening. Adding a few targeted sections for these would better lock in the new behavior.

codecov · 2026-04-03T16:13:51Z

Codecov Report

❌ Patch coverage is 96.80000% with 4 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.48%. Comparing base (803f904) to head (cb50af3).
⚠️ Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/util/simplify_expr_int.cpp	95.06%	4 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8951      +/-   ##
===========================================
+ Coverage    80.47%   80.48%   +0.01%     
===========================================
  Files         1704     1704              
  Lines       188694   188819     +125     
  Branches        73       73              
===========================================
+ Hits        151843   151964     +121     
- Misses       36851    36855       +4

☔ View full report in Codecov by Sentry.
📢 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.

tautschnig self-assigned this Apr 2, 2026

tautschnig requested review from kroening and peterschrammel as code owners April 2, 2026 10:28

Copilot AI review requested due to automatic review settings April 2, 2026 10:28

Copilot started reviewing on behalf of tautschnig April 2, 2026 10:29 View session

Copilot AI reviewed Apr 2, 2026

View reviewed changes

tautschnig force-pushed the simplify-algebraic-identities branch from aa47b06 to cb50af3 Compare April 3, 2026 15:45

tautschnig requested a review from Copilot April 3, 2026 15:45

Copilot AI reviewed Apr 3, 2026

View reviewed changes

Copilot started reviewing on behalf of tautschnig April 3, 2026 16:04 View session

tautschnig marked this pull request as draft April 3, 2026 20:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Simplify algebraic identities involving commutative operators#8951

Simplify algebraic identities involving commutative operators#8951
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:simplify-algebraic-identities

tautschnig commented Apr 2, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 3, 2026

Uh oh!

Copilot AI Apr 3, 2026

Uh oh!

Copilot AI Apr 3, 2026

Uh oh!

Copilot AI Apr 3, 2026

Uh oh!

codecov bot commented Apr 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		std::sort(leaves0.begin(), leaves0.end());
		std::sort(leaves1.begin(), leaves1.end());

-        std::sort(leaves0.begin(), leaves0.end());
-        std::sort(leaves1.begin(), leaves1.end());
+        const auto expr_less = [](const exprt &lhs, const exprt &rhs) {
+          return lhs.compare(rhs) < 0;
+        };
+        std::sort(leaves0.begin(), leaves0.end(), expr_less);
+        std::sort(leaves1.begin(), leaves1.end(), expr_less);

-      if(
-        leaves0.size() == leaves1.size() && leaves0.size() >= 2 &&
-        leaves0.size() <= 8)
+      // Keep the flatten-and-sort comparison cheap; larger expressions are
+      // left to the general simplifier rather than paying this extra cost.
+      constexpr std::size_t max_commutative_leaf_count_for_sort_compare = 8;
+      if(
+        leaves0.size() == leaves1.size() && leaves0.size() >= 2 &&
+        leaves0.size() <= max_commutative_leaf_count_for_sort_compare)

Conversation

tautschnig commented Apr 2, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Apr 3, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants