MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / Or

Function Or

lean_py/z3/core.py:1323–1334  ·  view source on GitHub ↗
(*args: BoolRef)

Source from the content-addressed store, hash-verified

1321
1322
1323def Or(*args: BoolRef) -> BoolRef:
1324 if len(args) == 1 and isinstance(args[0], list):
1325 args = tuple(args[0])
1326 if len(args) == 0:
1327 return BoolVal(False)
1328 if len(args) == 1:
1329 return args[0]
1330 merged: frozenset[tuple[str, ASTSort]] = frozenset().union(*(a._vars for a in args))
1331 ast: ASTNode = args[0]._ast
1332 for a in args[1:]:
1333 ast = BinOpNode(BinOp.OR, ast, a._ast)
1334 return BoolRef(ast, merged)
1335
1336
1337def Not(a: BoolRef) -> BoolRef:

Callers 15

_applyMethod · 0.90
as_exprMethod · 0.90
test_and_or_notMethod · 0.90
test_demorgan_proofMethod · 0.90
test_demorgan2_proofMethod · 0.90
test_excluded_middleMethod · 0.90
test_xor_definitionMethod · 0.90
test_prove_tautologyMethod · 0.90
test_conflictMethod · 0.90
test_is_logical_opsMethod · 0.90
test_or_listMethod · 0.90
test_or_emptyMethod · 0.90

Calls 3

BinOpNodeClass · 0.90
BoolValFunction · 0.85
BoolRefClass · 0.85

Tested by 15

test_and_or_notMethod · 0.72
test_demorgan_proofMethod · 0.72
test_demorgan2_proofMethod · 0.72
test_excluded_middleMethod · 0.72
test_xor_definitionMethod · 0.72
test_prove_tautologyMethod · 0.72
test_conflictMethod · 0.72
test_is_logical_opsMethod · 0.72
test_or_listMethod · 0.72
test_or_emptyMethod · 0.72
test_or_singleMethod · 0.72
test_or_childrenMethod · 0.72