3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
Nikolaj Bjorner 2022-08-19 18:15:54 -07:00
parent ea8b118eb1
commit b26420ed99

View file

@ -224,6 +224,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
function _toExpr(ast: Z3_ast): Bool<Name> | IntNum<Name> | RatNum<Name> | Arith<Name> | Expr<Name> {
const kind = check(Z3.get_ast_kind(contextPtr, ast));
if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
if (Z3.is_quantifier_forall(contextPtr, ast))
return BoolImpl(ast);
if (Z3.is_quantifier_exists(contextPtr, ast))
return BoolImpl(ast);
if (Z3.is_quantifier_lambda(contextPtr, ast))
return ExprImpl(ast);
assert(false);
}
const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));