mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge pull request #1826 from dselsam/master

Browse source 
remove duplicate method definitions
This commit is contained in:
Nikolaj Bjorner 2018-09-13 18:38:17 -07:00 committed by GitHub
parent 6ea4aff622 2a8d207bf4
commit 19d3b5cfd1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6626,14 +6626,6 @@ class Solver(Z3PPObject):
def proof(self):
"""Return a proof for the last `check()`. Proof construction must be enabled."""
return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
def from_file(self, filename):
"""Parse assertions from a file"""
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
def from_string(self, s):
"""Parse assertions from a string"""
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
def assertions(self):
"""Return an AST vector containing all added constraints.