diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 01:22:01 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-05 23:22:01 -0800 |
| commit | 46bae5d2a8b22867f917c6f644e46e29884049f9 (patch) | |
| tree | a915862a8b8fda9d50b2fbed950640f8da280f7d /contrib/get-cryptominisat | |
| parent | 643e4d5369734923267694c55363ec0456f18263 (diff) | |
Introduce the Node-level Datatypes API (#3462)
This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.
Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.
Diffstat (limited to 'contrib/get-cryptominisat')
0 files changed, 0 insertions, 0 deletions