Define rty::Formula and replace UnboundAssumption and Refinement with it

[coord-e]

• chc::Body: atoms with chc::Formula (formerly rty::FormulaWithAtoms)
• rty::Formula: chc::Body with existentials
• UnboundAssumption -> Assumption = rty::Formula
• Refinement = rty::Formula

It may be confusing that chc::Formula and rty::Formula have the same name but have different roles; however, I couldn't come up with a better name.

[Copilot]

Pull Request Overview

This PR refactors the formula representation by defining rty::Formula and replacing UnboundAssumption and Refinement with type aliases to this new structure. The refactoring consolidates different formula representations under a unified type hierarchy.

• Introduces rty::Formula<V> containing existentials and a chc::Body
• Replaces FormulaWithAtoms with chc::Body
• Converts UnboundAssumption and Refinement to type aliases of rty::Formula

Reviewed Changes

Copilot reviewed 12 out of 12 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/rty/params.rs	Updates refinement extension to use push_conj method
src/rty/clause_builder.rs	Updates import and method calls to use new chc::Body structure
src/rty.rs	Major refactor introducing Formula<V> and removing old types
src/refine/template.rs	Updates field access from formula to body
src/refine/env.rs	Replaces UnboundAssumption with Assumption type alias
src/refine.rs	Updates public exports to use new Assumption type
src/chc/unbox.rs	Adds unbox_body function and updates clause handling
src/chc/smtlib2.rs	Adds Body formatter and updates clause formatting
src/chc/format_context.rs	Updates atom iteration to use new iter_atoms method
src/chc/clause_builder.rs	Consolidates body handling into single add_body method
src/chc.rs	Introduces Body<V> struct and updates Clause structure
src/analyze/basic_block.rs	Updates to use new Assumption type and field names

---

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}