mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fixed problem with Python 3.4.x complainging of inconsistent use of spaces/tabs.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
53cfa47214
commit
59dfd2abe4
|
@ -298,8 +298,8 @@ class AstRef(Z3PPObject):
|
|||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
"""Return unique identifier for object. It can be used for hash-tables and maps."""
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
"""Return unique identifier for object. It can be used for hash-tables and maps."""
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
|
||||
def ctx_ref(self):
|
||||
|
@ -453,7 +453,7 @@ class SortRef(AstRef):
|
|||
return Z3_sort_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
|
||||
def kind(self):
|
||||
|
@ -595,7 +595,7 @@ class FuncDeclRef(AstRef):
|
|||
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def as_func_decl(self):
|
||||
return self.ast
|
||||
|
@ -743,7 +743,7 @@ class ExprRef(AstRef):
|
|||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def sort(self):
|
||||
"""Return the sort of expression `self`.
|
||||
|
@ -1540,7 +1540,7 @@ class PatternRef(ExprRef):
|
|||
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def is_pattern(a):
|
||||
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
|
||||
|
@ -1605,7 +1605,7 @@ class QuantifierRef(BoolRef):
|
|||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def sort(self):
|
||||
"""Return the Boolean sort."""
|
||||
|
@ -6033,20 +6033,20 @@ class Solver(Z3PPObject):
|
|||
return Z3_solver_to_string(self.ctx.ref(), self.solver)
|
||||
|
||||
def to_smt2(self):
|
||||
"""return SMTLIB2 formatted benchmark for solver's assertions"""
|
||||
es = self.assertions()
|
||||
sz = len(es)
|
||||
sz1 = sz
|
||||
if sz1 > 0:
|
||||
sz1 -= 1
|
||||
v = (Ast * sz1)()
|
||||
for i in range(sz1):
|
||||
v[i] = es[i].as_ast()
|
||||
if sz > 0:
|
||||
e = es[sz1].as_ast()
|
||||
else:
|
||||
e = BoolVal(True, self.ctx).as_ast()
|
||||
return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
|
||||
"""return SMTLIB2 formatted benchmark for solver's assertions"""
|
||||
es = self.assertions()
|
||||
sz = len(es)
|
||||
sz1 = sz
|
||||
if sz1 > 0:
|
||||
sz1 -= 1
|
||||
v = (Ast * sz1)()
|
||||
for i in range(sz1):
|
||||
v[i] = es[i].as_ast()
|
||||
if sz > 0:
|
||||
e = es[sz1].as_ast()
|
||||
else:
|
||||
e = BoolVal(True, self.ctx).as_ast()
|
||||
return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
|
||||
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue