Wrap a child AST node as an ExprRef with best-effort sort inference.
(child_ast: ASTNode, parent: ExprRef, idx: int)
| 2846 | |
| 2847 | |
| 2848 | def _child_expr(child_ast: ASTNode, parent: ExprRef, idx: int) -> ExprRef: |
| 2849 | """Wrap a child AST node as an ExprRef with best-effort sort inference.""" |
| 2850 | pvars = parent._vars |
| 2851 | |
| 2852 | # Literals: sort is known directly |
| 2853 | if isinstance(child_ast, IntLit): |
| 2854 | psort = parent._sort._ast_sort |
| 2855 | if isinstance(psort, RealASTSort): |
| 2856 | return ArithRef(child_ast, RealSort(), pvars) |
| 2857 | return ArithRef(child_ast, IntSort(), pvars) |
| 2858 | if isinstance(child_ast, NatLit): |
| 2859 | return ArithRef(child_ast, NatSort(), pvars) |
| 2860 | if isinstance(child_ast, BoolLit): |
| 2861 | return BoolRef(child_ast, pvars) |
| 2862 | if isinstance(child_ast, BvLit): |
| 2863 | return BitVecRef(child_ast, BitVecSort(child_ast.width), pvars) |
| 2864 | if isinstance(child_ast, StringLit): |
| 2865 | return StringRef(child_ast, pvars) |
| 2866 | |
| 2867 | # Variables: look up sort in parent's free vars |
| 2868 | if isinstance(child_ast, _AstVar): |
| 2869 | for vname, vsort in pvars: |
| 2870 | if vname == child_ast.name: |
| 2871 | s = _sort_from_ast_sort(vsort) |
| 2872 | return _make_typed_expr(child_ast, s, pvars) |
| 2873 | return ExprRef(child_ast, parent._sort, pvars) |
| 2874 | |
| 2875 | # Compound children: infer from parent node type |
| 2876 | past = parent._ast |
| 2877 | if isinstance(past, BinOpNode): |
| 2878 | if past.op in (BinOp.AND, BinOp.OR, BinOp.IMPLIES, BinOp.XOR): |
| 2879 | return BoolRef(child_ast, pvars) |
| 2880 | if past.op in (BinOp.LT, BinOp.LE, BinOp.GT, BinOp.GE, BinOp.EQ, BinOp.NE): |
| 2881 | return ExprRef(child_ast, SortRef(IntASTSort()), pvars) |
| 2882 | return _make_typed_expr(child_ast, parent._sort, pvars) |
| 2883 | if isinstance(past, UnOpNode): |
| 2884 | if past.op == UnOp.NOT: |
| 2885 | return BoolRef(child_ast, pvars) |
| 2886 | return _make_typed_expr(child_ast, parent._sort, pvars) |
| 2887 | if isinstance(past, IteNode): |
| 2888 | if idx == 0: |
| 2889 | return BoolRef(child_ast, pvars) |
| 2890 | return _make_typed_expr(child_ast, parent._sort, pvars) |
| 2891 | |
| 2892 | return ExprRef(child_ast, parent._sort, pvars) |
| 2893 | |
| 2894 | |
| 2895 | # --------------------------------------------------------------------------- |
no test coverage detected