Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
|
|
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback