| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Split explain utility, invariance tests.
* Split extended rewriter.
* Remove unused function.
* Minor
* Move generic term utilities to term_util.
* Documentation, minor.
* Make arguments private in eval invariance.
* Document
* More documentation.
* Clang format.
* Fix, improve.
* Format
* Address review.
* Address missed comment.
* Add line breaks
* Format
|
|
* Decouple sygus term database and term database.
* Clang format
* Fix include
|
|
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
|
|
* Initial infrastructure for static preprocessing for sygus conjectures.
* Initial infrastructure.
* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.
* Clang format
* Fixing comments, more initial infrastructure.
* More
* Minor
* New clang format.
* Address review.
|
|
* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.
* Change function names, simplify.
* Fix assertion, minor optimization
* Cleanup, documentation, simplification.
* Address review.
* Apply clang format.
|
|
* Move sygus grammar utilities to separate file.
* Minor
* Move includes
|
|
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.
|
|
|
