| 1306 | |
| 1307 | |
| 1308 | def And(*args: BoolRef) -> BoolRef: |
| 1309 | if len(args) == 1 and isinstance(args[0], list): |
| 1310 | args = tuple(args[0]) |
| 1311 | if len(args) == 0: |
| 1312 | return BoolVal(True) |
| 1313 | if len(args) == 1: |
| 1314 | return args[0] |
| 1315 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(*(a._vars for a in args)) |
| 1316 | # Build left-associated And chain |
| 1317 | ast: ASTNode = args[0]._ast |
| 1318 | for a in args[1:]: |
| 1319 | ast = BinOpNode(BinOp.AND, ast, a._ast) |
| 1320 | return BoolRef(ast, merged) |
| 1321 | |
| 1322 | |
| 1323 | def Or(*args: BoolRef) -> BoolRef: |