Parse existentials in annotations

[coord-e]

No description provided.

[Copilot]

Pull request overview

This PR adds support for parsing existential quantifiers in annotation formulas, enabling specifications like exists x:int. result == 2 * x. The implementation extends both the parser and the core CHC (Constrained Horn Clauses) representation.

• Adds new Formula::Exists variant and Term::FormulaExistentialVar to support existentially quantified variables
• Implements parsing logic for exists syntax with variable declarations and sort annotations
• Integrates existential handling across CHC utilities (unboxing, SMT-LIB2 formatting, and context)

Reviewed changes

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

Show a summary per file

File	Description
tests/ui/pass/annot_exists.rs	Test case verifying correct parsing and verification of existential postconditions
tests/ui/fail/annot_exists.rs	Test case verifying detection of unsatisfiable existential postconditions
src/chc.rs	Adds Formula::Exists and Term::FormulaExistentialVar variants with supporting methods
src/annot.rs	Implements parse_exists and parse_sort methods to handle existential quantifier syntax
src/chc/unbox.rs	Extends unboxing transformation to handle new existential variants
src/chc/smtlib2.rs	Adds SMT-LIB2 formatting for existential formulas and variables
src/chc/format_context.rs	Handles existential variables in sort collection
.github/workflows/ci.yml	Configures Docker-based solver (thrust-pcsat-wrapper) for CI testing

---

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

[Copilot]

Pull request overview

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

---

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