Deepen formula semantic invariant properties (#112)

[leynos]

Summary

This branch deepens the property coverage for issue #112 by making the sempai
semantic invariant generators produce formula trees with at least four levels of
nesting. It keeps proptest as the existing crates/sempai dev-dependency,
adds depth-enforced generators for positive, constraint-only and atomless
formula shapes, and asserts the depth guarantee inside each property.

Closes #112.

Review walkthrough

• Start with crates/sempai/src/tests/property_tests.rs to review the new depth-enforced strategies and tree_depth assertion helper.
• Then review the three property tests in the same file to see how InvalidNotInOr, MissingPositiveTermInAnd, and valid positive trees now exercise nested formula structures.

Validation

• cargo test -p sempai: passed.
• make check-fmt: passed.
• make lint: passed.
• make test: passed; nextest ran 1,389 tests and workspace doctests passed.
• git diff --check: passed.

Notes

coderabbit review --agent was attempted three times after the implementation
milestone, including after the reported wait windows. Each attempt stopped before
review with a recoverable CodeRabbit rate-limit error, so there were no review
concerns to clear locally.

Summary by Sourcery

Strengthen semantic invariant property tests by generating and asserting on deeper, more complex formula trees.

Enhancements:

• Introduce depth-aware formula generator helpers for various formula shapes used in property tests.

Tests:

• Enforce a minimum tree depth for key formula-generating strategies and assert this invariant in the relevant property tests to exercise nested structures more thoroughly.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: a82eacbd-1f28-4d1a-a1b0-d2acfea6e71c

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch issue-112-property-tests-for-formula-semantic-invariants

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[sourcery-ai]

Reviewer's Guide

Deepens the semantic-invariant property tests by introducing depth-enforced formula generators and asserting a minimum tree depth across three key properties, ensuring they exercise sufficiently nested formula structures.

File-Level Changes

Change	Details	Files
Introduce reusable depth-enforced generators for different formula shapes (atoms, constraint-only, positive, and atomless) to ensure generated trees meet a minimum depth.	Add MIN_PROPERTY_DEPTH constant to define the minimum depth required by property tests. Implement helper constructors for unary nodes (including a validity-preserving version) to factor formula creation logic. Add deep_atom, deep_constraint_atom, deep_positive_atom, and deep_atomless strategies that recursively wrap children until the requested minimum depth is reached.	crates/sempai/src/tests/property_tests.rs
Update existing proptest strategies to use the new depth-enforced generators so property tests operate on sufficiently deep trees.	Change tree_with_not to wrap a deep atom as its child rather than an arbitrary formula tree. Modify and_without_positive_descendant to require at least one deep atomless child while limiting other branches, ensuring the AND has a deep structure. Adjust valid_no_not_tree and positive_tree roots and subcomponents (constraints and OR branches) to be built from deep_* generators instead of shallow atom strategies.	crates/sempai/src/tests/property_tests.rs
Add a depth computation helper and assert minimum depth invariants inside each property test.	Introduce tree_depth helper to compute the depth of a Decorated tree by recursing through unary and n-ary nodes. Add prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH) to the three property tests so that any regression in generators that violates depth guarantees is caught.	crates/sempai/src/tests/property_tests.rs

Assessment against linked issues

Issue	Objective	Addressed	Explanation
#112	Add proptest as a dev-dependency to crates/sempai so semantic invariants of validate_formula can be tested with property-based tests.	✅
#112	Implement property-based strategies that generate arbitrarily nested Decorated<Formula> trees, including shapes needed to exercise the semantic invariants.	✅
#112	Add property tests that verify the InvalidNotInOr and MissingPositiveTermInAnd invariants (and valid-positive cases) across formula trees with at least 4 levels of nesting, and ensure cargo test -p sempai passes.	✅

---

Tips and commands

Interacting with Sourcery

• Trigger a new review: Comment @sourcery-ai review on the pull request.
• Continue discussions: Reply directly to Sourcery's review comments.
• Generate a GitHub issue from a review comment: Ask Sourcery to create an
  issue from a review comment by replying to it. You can also reply to a
  review comment with @sourcery-ai issue to create an issue from it.
• Generate a pull request title: Write @sourcery-ai anywhere in the pull
  request title to generate a title at any time. You can also comment
  @sourcery-ai title on the pull request to (re-)generate the title at any time.
• Generate a pull request summary: Write @sourcery-ai summary anywhere in
  the pull request body to generate a PR summary at any time exactly where you
  want it. You can also comment @sourcery-ai summary on the pull request to
  (re-)generate the summary at any time.
• Generate reviewer's guide: Comment @sourcery-ai guide on the pull
  request to (re-)generate the reviewer's guide at any time.
• Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
  pull request to resolve all Sourcery comments. Useful if you've already
  addressed all the comments and don't want to see them anymore.
• Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
  request to dismiss all existing Sourcery reviews. Especially useful if you
  want to start fresh with a new review - don't forget to comment
  @sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

• Enable or disable review features such as the Sourcery-generated pull request
  summary, the reviewer's guide, and others.
• Change the review language.
• Add, remove or edit custom review instructions.
• Adjust other review settings.

Getting Help

• Contact our support team for questions or feedback.
• Visit our documentation for detailed guides and information.
• Keep in touch with the Sourcery team by following us on X/Twitter, LinkedIn or GitHub.

[leynos]

@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response.

crates/sempai/src/tests/property_tests.rs

Comment on lines +197 to +199

        vec(atomless_tree_without_not_in_or(), 0..=2),
        deep_atomless(MIN_PROPERTY_DEPTH - 1),
        vec(atomless_tree_without_not_in_or(), 0..=2),

❌ New issue: Code Duplication
The module contains 2 functions with similar structure: and_without_positive_descendant,or_with_not_descendant