mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

Replace tabs with spaces in python files.

Browse source
This commit is contained in:
Jens Steinhauser 2015-01-21 00:43:15 +01:00
parent 6a496a1bfb
commit e5b6b6d1d3
2 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -266,7 +266,7 @@ def param2dotnet(p):
elif k == OUT_ARRAY: elif k == OUT_ARRAY:
return "[Out] %s[]" % type2dotnet(param_type(p)) return "[Out] %s[]" % type2dotnet(param_type(p))
elif k == OUT_MANAGED_ARRAY: elif k == OUT_MANAGED_ARRAY:
return "[Out] out %s[]" % type2dotnet(param_type(p)) return "[Out] out %s[]" % type2dotnet(param_type(p))
else: else:
return type2dotnet(param_type(p)) return type2dotnet(param_type(p))

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

@ -298,8 +298,8 @@ class AstRef(Z3PPObject):
return self.ast return self.ast
def get_id(self): def get_id(self):
"""Return unique identifier for object. It can be used for hash-tables and maps.""" """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 Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def ctx_ref(self): def ctx_ref(self):
@ -453,7 +453,7 @@ class SortRef(AstRef):
return Z3_sort_to_ast(self.ctx_ref(), self.ast) return Z3_sort_to_ast(self.ctx_ref(), self.ast)
def get_id(self): 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): def kind(self):
@ -595,7 +595,7 @@ class FuncDeclRef(AstRef):
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
def get_id(self): 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): def as_func_decl(self):
return self.ast return self.ast
@ -743,7 +743,7 @@ class ExprRef(AstRef):
return self.ast return self.ast
def get_id(self): 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): def sort(self):
"""Return the sort of expression `self`. """Return the sort of expression `self`.
@ -1540,7 +1540,7 @@ class PatternRef(ExprRef):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast) return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
def get_id(self): 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): def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
@ -1605,7 +1605,7 @@ class QuantifierRef(BoolRef):
return self.ast return self.ast
def get_id(self): 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): def sort(self):
"""Return the Boolean sort.""" """Return the Boolean sort."""
@ -6033,20 +6033,20 @@ class Solver(Z3PPObject):
return Z3_solver_to_string(self.ctx.ref(), self.solver) return Z3_solver_to_string(self.ctx.ref(), self.solver)
def to_smt2(self): def to_smt2(self):
"""return SMTLIB2 formatted benchmark for solver's assertions""" """return SMTLIB2 formatted benchmark for solver's assertions"""
es = self.assertions() es = self.assertions()
sz = len(es) sz = len(es)
sz1 = sz sz1 = sz
if sz1 > 0: if sz1 > 0:
sz1 -= 1 sz1 -= 1
v = (Ast * sz1)() v = (Ast * sz1)()
for i in range(sz1): for i in range(sz1):
v[i] = es[i].as_ast() v[i] = es[i].as_ast()
if sz > 0: if sz > 0:
e = es[sz1].as_ast() e = es[sz1].as_ast()
else: else:
e = BoolVal(True, self.ctx).as_ast() 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 Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)