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

Function solve

lean_py/z3/solver.py:744–748  ·  view source on GitHub ↗

Shorthand: create solver, add args, check.

(*args: BoolRef)

Source from the content-addressed store, hash-verified

742
743
744def solve(*args: BoolRef) -> CheckSatResult:
745 """Shorthand: create solver, add args, check."""
746 s = Solver()
747 s.add(*args)
748 return s.check()
749
750
751def simplify(expr: ExprRef) -> ExprRef:

Callers 2

test_solve_shorthandMethod · 0.90
test_solve_unsatMethod · 0.90

Calls 3

addMethod · 0.95
checkMethod · 0.95
SolverClass · 0.85

Tested by 2

test_solve_shorthandMethod · 0.72
test_solve_unsatMethod · 0.72