Merge branch 'contrib' of https://git01.codeplex.com/forks/jensste/z3 into contrib

scripts/update_api.py

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

src/api/python/z3.py

@@ -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)
 
 
 

src/api/python/z3util.py

@@ -29,9 +29,9 @@ def ehash(v):
     z3 expressions in some cases.
     
     >>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
-    >>> print x1.hash(),x2.hash(),x3.hash() #BAD: all same hash values
+    >>> print(x1.hash(),x2.hash(),x3.hash()) #BAD: all same hash values
     783810685 783810685 783810685
-    >>> print ehash(x1), ehash(x2), ehash(x3)
+    >>> print(ehash(x1), ehash(x2), ehash(x3))
     x_783810685_1 x_783810685_1 x_783810685_2
     
     """
@@ -174,9 +174,9 @@ def prove(claim,assume=None,verbose=0):
     (False, [(x, False), (y, True)])
 
     >>> r,m = prove(And(x,y),assume=y,verbose=0)
-    >>> print r
+    >>> print(r)
     False
-    >>> print model_str(m,as_str=True)
+    >>> print(model_str(m,as_str=True))
     x = False
     y = True
 
@@ -210,18 +210,18 @@ def prove(claim,assume=None,verbose=0):
 
 
     if verbose >= 2:
-        print 'assume: '
-        print assume
-        print 'claim: '
-        print claim
-        print 'to_prove: '
-        print to_prove
+        print('assume: ')
+        print(assume)
+        print('claim: ')
+        print(claim)
+        print('to_prove: ')
+        print(to_prove)
 
     f = Not(to_prove)
 
     models = get_models(f,k=1)
     if models is None: #unknown
-        print 'E: cannot solve !'
+        print('E: cannot solve !')
         return None, None
     elif models == False: #unsat
         return True,None   
@@ -438,7 +438,7 @@ def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b])
     
 
 
-Iff = lambda f,g: And(Implies(f,g),Implies(g,f))
+Iff = lambda f: And(Implies(f[0],f[1]),Implies(f[1],f[0]))
 
 
 
@@ -458,7 +458,7 @@ def model_str(m,as_str=True):
 
     if m :
         vs = [(v,m[v]) for v in m]
-        vs = sorted(vs,key=lambda (a,_): str(a)) 
+        vs = sorted(vs,key=lambda a: str(a[0]))
         if as_str:
             return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
         else: