Exception handling, more cvc5 functions, documentation, tests #4
Conversation
Cvc5Test/ApiTermManagerBlack.lean
Outdated
There was a problem hiding this comment.
Cvc5Test/TermManager.lean is good enough!
There was a problem hiding this comment.
Are you sure? I thought it would be better to use the same file name as the original test.
There was a problem hiding this comment.
Api and Black are C++ implementation specific. We don't have bindings for anything beyond the public API nor test any internal functionality. So, those parts of the name don't apply. This is also more consistent with the Java and Python naming conventions.
| @[extern "term_getOp"] | ||
| opaque getOp : Term → Op | ||
| private opaque getOp! : Term → Op |
There was a problem hiding this comment.
Shouldn't the default function be getOp : Term → Except Error Op? This version: getOp! : Term → Op should be defined in terms of the former (via a macro). I am thinking of something like:
defs getOp : Term → Except Error Opwhere defs is a macro that expands into:
@[extern "term_getOp"]
opaque getOp : Term → Except Error Op
def getOp! : Term → Op := Error.unwrap o getOp| @[extern "term_getSymbol"] | ||
| opaque getSymbol : Term → String | ||
| private opaque getSymbol! : Term → String |
| @[extern "term_getSkolemId"] | ||
| opaque getSkolemId : Term → SkolemId | ||
| opaque getSkolemId! : Term → SkolemId |
| -/ | ||
| @[extern "termManager_mkFloatingPointSort"] | ||
| opaque mkFloatingPointSort : TermManager → (exp sig : UInt32) → cvc5.Sort | ||
| private opaque mkFloatingPointSortUnsafe : TermManager → (exp sig : UInt32) → Except Error cvc5.Sort |
| - `base`: The base of the string representation of `size`. | ||
| -/ | ||
| @[extern "termManager_mkFiniteFieldSort"] | ||
| opaque mkFiniteFieldSortOfString |
There was a problem hiding this comment.
Just take a Int/Nat as input. No need for all these versions (or exceptions). Only BitVec and FloatingPoint need to use machine integers.
| @[extern "termManager_mkBoolean"] | ||
| opaque mkBoolean : TermManager → Bool → Term | ||
| opaque mkBoolean : TermManager → (b : Bool) → Except Error Term |
|
|
||
| - `i`: The integer constant. | ||
| -/ | ||
| def mkInteger (tm : TermManager) : (i : Int) → Except Error Term := |
| @[inherit_doc mkTermOfOp] | ||
| def mkTermOfOp! tm op children := | ||
| mkTermOfOp tm op children | ||
| |> Error.unwrap! |
There was a problem hiding this comment.
Use macro. Avoid use of |> if the number of consecutive parentheses is less than 3: (mkTermOfOp tm op children).unwrap!
1a79ef4 to
76a58ac
Compare
48f53fd to
319a41a
Compare
deal with C++ exceptions cleanly: many
TermManagerandSolverfunctions can now produce clean, lean-level errorsthis is both for a nicer user experience and to test failures using the test framework from Test framework #2 (C++ exceptions crash the lean server)
provide small, safe helpers for functions that now generate
Except Error Tinstead of plainTvalueslift many
TermManager/Solvercvc5 functionssignificant documentation effort
start adding C++ API tests:
Cvc5Test/ApiTermManagerBlack.lean(currently incomplete)