Wrap an AST node into the correct ExprRef subclass based on sort.
(ast: ASTNode, sort: SortRef, vars_: frozenset)
| 882 | |
| 883 | |
| 884 | def _wrap_expr(ast: ASTNode, sort: SortRef, vars_: frozenset) -> ExprRef: |
| 885 | """Wrap an AST node into the correct ExprRef subclass based on sort.""" |
| 886 | s = sort._ast_sort |
| 887 | if isinstance(s, PropSort): |
| 888 | return BoolRef(ast, vars_) |
| 889 | if isinstance(s, (IntASTSort, NatASTSort, RealASTSort)): |
| 890 | return ArithRef(ast, sort, vars_) # type: ignore[arg-type] |
| 891 | if isinstance(s, BitvecASTSort): |
| 892 | return BitVecRef(ast, sort, vars_) # type: ignore[arg-type] |
| 893 | if isinstance(s, ArrowASTSort): |
| 894 | return ArrayRef(ast, sort, vars_) # type: ignore[arg-type] |
| 895 | return ExprRef(ast, sort, vars_) |
| 896 | |
| 897 | |
| 898 | class FuncDeclRef: |