mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Add solver::interrupt to Python's API. (#6739)

Browse source
This commit is contained in:
Manuel Carrasco 2023-05-28 20:04:36 +01:00 • committed by GitHub
parent 5e1869d8eb
commit 230306ddfc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/python/z3/z3.py
View file

@ -7136,6 +7136,13 @@ class Solver(Z3PPObject):
"""Import model converter from other into the current solver"""
Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
def interrupt(self):
"""Interrupt the execution of the solver object.
Remarks: This ensures that the interrupt applies only
to the given solver object and it applies only if it is running.
"""
Z3_solver_interrupt(self.ctx.ref(), self.solver)
def unsat_core(self):
"""Return a subset (as an AST vector) of the assumptions provided to the last check().