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

Function solve_using

lean_py/z3/solver.py:774–777  ·  view source on GitHub ↗

Solve using a specific solver instance.

(s: Solver, *args: BoolRef)

Source from the content-addressed store, hash-verified

772
773
774def solve_using(s: Solver, *args: BoolRef) -> CheckSatResult:
775 """Solve using a specific solver instance."""
776 s.add(*args)
777 return s.check()
778
779
780def parse_smt2_string(s: str, sorts: dict | None = None, decls: dict | None = None) -> list:

Callers 1

test_solve_usingMethod · 0.90

Calls 2

addMethod · 0.45
checkMethod · 0.45

Tested by 1

test_solve_usingMethod · 0.72