Convert a Python ASTNode to a Lean Z3Expr value.
(lib: Any, node: ASTNode)
| 221 | |
| 222 | |
| 223 | def _marshal_expr(lib: Any, node: ASTNode) -> Any: |
| 224 | """Convert a Python ASTNode to a Lean Z3Expr value.""" |
| 225 | Z3Expr = lib.Z3Expr |
| 226 | if isinstance(node, Var): |
| 227 | return Z3Expr.var(node.name) |
| 228 | if isinstance(node, IntLit): |
| 229 | return Z3Expr.intLit(node.val) |
| 230 | if isinstance(node, NatLit): |
| 231 | return Z3Expr.natLit(node.val) |
| 232 | if isinstance(node, BoolLit): |
| 233 | return Z3Expr.boolLit(node.val) |
| 234 | if isinstance(node, BvLit): |
| 235 | return Z3Expr.bvLit(node.val, node.width) |
| 236 | if isinstance(node, BinOpNode): |
| 237 | op = _marshal_binop(lib, node.op) |
| 238 | lhs = _marshal_expr(lib, node.lhs) |
| 239 | rhs = _marshal_expr(lib, node.rhs) |
| 240 | return Z3Expr.binop(op, lhs, rhs) |
| 241 | if isinstance(node, UnOpNode): |
| 242 | op = _marshal_unop(lib, node.op) |
| 243 | arg = _marshal_expr(lib, node.arg) |
| 244 | return Z3Expr.unop(op, arg) |
| 245 | if isinstance(node, IteNode): |
| 246 | cond = _marshal_expr(lib, node.cond) |
| 247 | then_ = _marshal_expr(lib, node.then_) |
| 248 | else_ = _marshal_expr(lib, node.else_) |
| 249 | return Z3Expr.ite(cond, then_, else_) |
| 250 | if isinstance(node, ForAllNode): |
| 251 | sort = _marshal_sort(lib, node.sort) |
| 252 | body = _marshal_expr(lib, node.body) |
| 253 | return Z3Expr.forall_(node.name, sort, body) |
| 254 | if isinstance(node, ExistsNode): |
| 255 | sort = _marshal_sort(lib, node.sort) |
| 256 | body = _marshal_expr(lib, node.body) |
| 257 | return Z3Expr.exists_(node.name, sort, body) |
| 258 | if isinstance(node, AppNode): |
| 259 | func = _marshal_expr(lib, node.func) |
| 260 | args = [_marshal_expr(lib, a) for a in node.args] |
| 261 | return Z3Expr.app(func, args) |
| 262 | if isinstance(node, DistinctNode): |
| 263 | args = [_marshal_expr(lib, a) for a in node.args] |
| 264 | return Z3Expr.distinct(args) |
| 265 | if isinstance(node, SelectNode): |
| 266 | arr = _marshal_expr(lib, node.arr) |
| 267 | idx = _marshal_expr(lib, node.idx) |
| 268 | return Z3Expr.select(arr, idx) |
| 269 | if isinstance(node, StoreNode): |
| 270 | arr = _marshal_expr(lib, node.arr) |
| 271 | idx = _marshal_expr(lib, node.idx) |
| 272 | val = _marshal_expr(lib, node.val) |
| 273 | return Z3Expr.store(arr, idx, val) |
| 274 | if isinstance(node, ConstArrayNode): |
| 275 | dom_sort = _marshal_sort(lib, node.dom_sort) |
| 276 | val = _marshal_expr(lib, node.val) |
| 277 | return Z3Expr.constArray(dom_sort, val) |
| 278 | if isinstance(node, ExtractNode): |
| 279 | arg = _marshal_expr(lib, node.arg) |
| 280 | return Z3Expr.extract(node.hi, node.lo, arg) |
no test coverage detected