Merge branch 'master' of https://github.com/Z3Prover/z3

scripts/update_api.py

@@ -99,7 +99,7 @@ else:
      if s != None:
         enc = sys.stdout.encoding
         if enc != None: return s.decode(enc)
-        else: return s
+        else: return s.decode('ascii')
      else:
         return ""
 

src/api/dotnet/Context.cs

@@ -2613,8 +2613,13 @@ namespace Microsoft.Z3
         /// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
         /// with the sorts of the bound variables, <paramref name="names"/> is an array with the
         /// 'names' of the bound variables, and <paramref name="body"/> is the body of the
-        /// quantifier. Quantifiers are associated with weights indicating
-        /// the importance of using the quantifier during instantiation.
+        /// quantifier. Quantifiers are associated with weights indicating the importance of 
+        /// using the quantifier during instantiation.
+        /// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>. 
+        /// Z3 applies the convention that the last element in <paramref name="names"/> and 
+        /// <paramref name="sorts"/> refers to the variable with index 0, the second to last element 
+        /// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable 
+        /// with index 1, etc. 
         /// </remarks>
         /// <param name="sorts">the sorts of the bound variables.</param>
         /// <param name="names">names of the bound variables</param>
@@ -2644,6 +2649,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a universal Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates a universal quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2659,7 +2669,10 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
-        /// <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
+        /// <remarks>
+        /// Creates an existential quantifier using de-Brujin indexed variables. 
+        /// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
+        /// </remarks>
         public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(sorts != null);
@@ -2678,6 +2691,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates an existential quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2693,6 +2711,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2716,6 +2735,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);

src/api/java/Context.java

@@ -433,8 +433,8 @@ public class Context extends IDisposable
     /**
      * Creates a fresh function declaration with a name prefixed with
      * {@code prefix}. 
-     * @see mkFuncDecl(String,Sort,Sort)
-     * @see mkFuncDecl(String,Sort[],Sort)
+     * @see #mkFuncDecl(String,Sort,Sort)
+     * @see #mkFuncDecl(String,Sort[],Sort)
      **/
     public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
            
@@ -2025,6 +2025,7 @@ public class Context extends IDisposable
 
     /**
      * Create a universal Quantifier.
+     *
      * @param sorts the sorts of the bound variables. 
      * @param names names of the bound variables 
      * @param body the body of the quantifier. 
@@ -2034,13 +2035,18 @@ public class Context extends IDisposable
      * @param quantifierID optional symbol to track quantifier. 
      * @param skolemID optional symbol to track skolem constants.
      * 
-     * Remarks:  Creates a forall formula, where
-     * {@code weight"/> is the weight, <paramref name="patterns} is
+     * @return Creates a forall formula, where
+     * {@code weight} is the weight, {@code patterns} is
      * an array of patterns, {@code sorts} is an array with the sorts
      * of the bound variables, {@code names} is an array with the
      * 'names' of the bound variables, and {@code body} is the body
      * of the quantifier. Quantifiers are associated with weights indicating the
      * importance of using the quantifier during instantiation.
+     * Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
+     * Z3 applies the convention that the last element in {@code names} and 
+     * {@code sorts} refers to the variable with index 0, the second to last element 
+     * of {@code names} and {@code sorts} refers to the variable 
+     * with index 1, etc. 
      **/
     public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
                                int weight, Pattern[] patterns, Expr[] noPatterns,
@@ -2052,7 +2058,8 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a universal Quantifier.
+     * Creates a universal quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
                                Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
@@ -2064,7 +2071,7 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier. 
+     * Creates an existential quantifier using de-Brujin indexed variables. 
      * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
@@ -2077,7 +2084,8 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier.
+     * Creates an existential quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
                                Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
@@ -2090,6 +2098,7 @@ public class Context extends IDisposable
 
     /**
      * Create a Quantifier.
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
                                    Symbol[] names, Expr body, int weight, Pattern[] patterns,
@@ -2106,7 +2115,8 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a Quantifier.
+     * Create a Quantifier
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
                                    Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,

src/api/python/z3.py

@@ -4862,7 +4862,7 @@ class Goal(Z3PPObject):
         elif sz == 1:
             return self.get(0)
         else:
-            return And([ self.get(i) for i in range(len(self)) ])
+            return And([ self.get(i) for i in range(len(self)) ], self.ctx)
 
 #########################################
 #

src/api/python/z3printer.py

@@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
 def obj_to_string(a):
     out = io.StringIO()
     _PP(out, _Formatter(a))
-    return out.getvalue()
+    r = out.getvalue()
+    if sys.version < '3':
+        return r
+    else:
+        enc = sys.stdout.encoding
+        if enc != None: return r.decode(enc)
+        return r
 
 _html_out = None