search

SemGuS-git / Semgus-Parser

Library and tool for parsing SemGuS specifications
MIT License
4 stars 1 forks source link

Cleaner and more extensible theory/logic definitions #77

Closed kjcjohnson closed 2 years ago

kjcjohnson commented 2 years ago

The goal of this change is to allow specifying theory and logic functions in a separate DSL instead of hard-coding everything in source. This will additionally allow us to handle :chainable and related declarations (e.g., and, closing #76), as well as "sugar" definitions like bvxor.

As a part of this, the S-Expressions project is being re-targeted to .NET Standard 2.0 and used in a source generator that consumes the new DSL and generates C# source files.

kjcjohnson commented 2 years ago

Source generators are a no-go for now, so backing those changes out. My attempt is saved at the kjcjohnson/source-generator-attempt tag. Basically, the tooling does not seem to be mature enough at this point to give a maintainable development experience going forward. I'm sure I could get it to work, but it doesn't seem like the best use of my time.

Re-opening this pull request to solve the same problems, but with going back to hard-coding the SMT definitions.

kjcjohnson commented 2 years ago

Lot of stuff changing here...but tests all pass!