From 706a037bf4bc20e37f85978b6ae8912cb9f32e67 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Nov 2015 15:16:50 +0100 Subject: [PATCH 1/3] Python 3.x string decoding fix --- scripts/update_api.py | 2 +- src/api/python/z3printer.py | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index bb5935a1e..6e7b6d5f7 100644 --- a/scripts/update_api.py +++ b/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 "" diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index 5116046dd..2a242865e 100644 --- a/src/api/python/z3printer.py +++ b/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 From e8d37dba9cce90574ed5c9ad640968c0362c5c82 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Nov 2015 21:58:17 +0100 Subject: [PATCH 2/3] Added comments for quantifier constructors. Fixes #319. --- src/api/dotnet/Context.cs | 26 ++++++++++++++++-- src/api/java/Context.java | 58 +++++++++++++++++++++++---------------- 2 files changed, 57 insertions(+), 27 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 25c399d68..d56ba4af1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2613,8 +2613,13 @@ namespace Microsoft.Z3 /// is an array of patterns, is an array /// with the sorts of the bound variables, is an array with the /// 'names' of the bound variables, and 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 . + /// Z3 applies the convention that the last element in and + /// refers to the variable with index 0, the second to last element + /// of and refers to the variable + /// with index 1, etc. /// /// the sorts of the bound variables. /// names of the bound variables @@ -2644,6 +2649,11 @@ namespace Microsoft.Z3 /// /// Create a universal Quantifier. /// + /// + /// Creates a universal quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// 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 /// /// Create an existential Quantifier. /// - /// + /// + /// Creates an existential quantifier using de-Brujin indexed variables. + /// (). + /// 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 /// /// Create an existential Quantifier. /// + /// + /// Creates an existential quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// 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 /// /// Create a Quantifier. /// + /// 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 /// /// Create a Quantifier. /// + /// 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); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0f9a85799..4d8484ced 100644 --- a/src/api/java/Context.java +++ b/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) @@ -1722,9 +1722,9 @@ public class Context extends IDisposable **/ public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2) { - checkContextMatch(arg1); - checkContextMatch(arg2); - return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); + checkContextMatch(arg1); + checkContextMatch(arg2); + return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } @@ -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,17 +2035,22 @@ 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,