Add bounded integer types and expressions to Lambda#154

Open

joscoh wants to merge 21 commits intomainfrom

Commits on Sep 16, 2025

Allow LTy to take in TypeRestrictions parameter
Josh Cohen
committed

Commits on Sep 17, 2025

Refactor bitvectors as type metadata
Josh Cohen
committed

Commits on Sep 22, 2025

Merge branch 'main' into josh/bounded
Josh Cohen
committed
Minor changes to fix bounded types after merge
Josh Cohen
committed
Initial version of bounded int expression translation
Josh Cohen
committed

Commits on Sep 24, 2025

Add bounded types to LTy, test cases for translateBounded
Josh Cohen
committed

Commits on Sep 25, 2025

Add lots of test cases, clean up code
Josh Cohen
committed

Commits on Sep 26, 2025

Some improvements to code and tests
Josh Cohen
committed

Commits on Sep 29, 2025

Fix bug in if-then-else, note about positivity
Josh Cohen
committed

Commits on Sep 30, 2025

Fix positivity issue, add tests
Josh Cohen
committed

Commits on Oct 1, 2025

Clean up application case a bit
Josh Cohen
committed

Commits on Oct 3, 2025

Clean up rest of translateBounded
Josh Cohen
committed
Clean up code, add comments
Josh Cohen
committed

Commits on Oct 6, 2025

Add back bitvector special case
Josh Cohen
committed
Add test for "and", move location
Josh Cohen
committed
Clean up BExpr, add clean translation for triggers
Josh Cohen
committed
Merge remote-tracking branch 'origin/main' into josh/bounded
Josh Cohen
committed
Fix changes from Lambda that had been introduced earlier
Josh Cohen
committed

Commits on Oct 7, 2025

Add bitvector to LTyRestrict
Josh Cohen
committed

Commits on Oct 10, 2025

Add missing type translation in output for abs, quant, ite
Josh Cohen
committed
Add copyright header to BExprTest
Josh Cohen
committed