From e9f7d558e3e1ac45b53f33ad177073ad8b75bae9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 12:40:41 +0100 Subject: [PATCH 1/5] tabs, indentation --- examples/python/complex/complex.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/examples/python/complex/complex.py b/examples/python/complex/complex.py index 5d6283745..467d76c55 100644 --- a/examples/python/complex/complex.py +++ b/examples/python/complex/complex.py @@ -47,13 +47,13 @@ class ComplexExpr: return ComplexExpr(other.r*self.r - other.i*self.i, other.i*self.r + other.r*self.i) def __pow__(self, k): - if k == 0: - return ComplexExpr(1, 0) - if k == 1: - return self - if k < 0: - return (self ** (-k)).inv() - return reduce(lambda x, y: x * y, [self for _ in xrange(k)], ComplexExpr(1, 0)) + if k == 0: + return ComplexExpr(1, 0) + if k == 1: + return self + if k < 0: + return (self ** (-k)).inv() + return reduce(lambda x, y: x * y, [self for _ in xrange(k)], ComplexExpr(1, 0)) def inv(self): den = self.r*self.r + self.i*self.i From f0b699f03a153531a3a24c8d8c3b848df9491dfc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 12:41:51 +0100 Subject: [PATCH 2/5] Added Optimize.cs to to Microsoft.Z3.csproj --- src/api/dotnet/Microsoft.Z3.csproj | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 2b5e08173..937edb69d 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -365,6 +365,7 @@ + From a41a9c94dd92a018fe5af04106d6afe67c796ca8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 12:43:25 +0100 Subject: [PATCH 3/5] Formatting --- src/api/dotnet/Optimize.cs | 98 +++++++++++++++++++------------------- 1 file changed, 49 insertions(+), 49 deletions(-) diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index edd259100..dc94db78a 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -85,43 +85,43 @@ namespace Microsoft.Z3 Assert(constraints); } - /// - /// Handle to objectives returned by objective functions. - /// - public class Handle + /// + /// Handle to objectives returned by objective functions. + /// + public class Handle { - Optimize opt; - uint handle; - internal Handle(Optimize opt, uint h) - { - this.opt = opt; - this.handle = h; - } + Optimize opt; + uint handle; + internal Handle(Optimize opt, uint h) + { + this.opt = opt; + this.handle = h; + } /// /// Retrieve a lower bound for the objective handle. /// - public ArithExpr Lower - { - get { return opt.GetLower(handle); } - } + public ArithExpr Lower + { + get { return opt.GetLower(handle); } + } /// /// Retrieve an upper bound for the objective handle. /// - public ArithExpr Upper - { - get { return opt.GetUpper(handle); } - } + public ArithExpr Upper + { + get { return opt.GetUpper(handle); } + } /// /// Retrieve the value of an objective. /// - public ArithExpr Value - { - get { return Lower; } - } - } + public ArithExpr Value + { + get { return Lower; } + } + } /// /// Assert soft constraint @@ -132,29 +132,29 @@ namespace Microsoft.Z3 public Handle AssertSoft(BoolExpr constraint, uint weight, string group) { Context.CheckContextMatch(constraint); - Symbol s = Context.MkSymbol(group); - return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject)); + Symbol s = Context.MkSymbol(group); + return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject)); } - - /// - /// - /// Check satisfiability of asserted constraints. - /// Produce a model that (when the objectives are bounded and - /// don't use strict inequalities) meets the objectives. - /// - /// - public Status Check() { - Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject); + + /// + /// Check satisfiability of asserted constraints. + /// Produce a model that (when the objectives are bounded and + /// don't use strict inequalities) meets the objectives. + /// + /// + public Status Check() + { + Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject); switch (r) { - case Z3_lbool.Z3_L_TRUE: + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; - default: + default: return Status.UNKNOWN; - } + } } /// @@ -198,27 +198,27 @@ namespace Microsoft.Z3 /// /// Declare an arithmetical maximization objective. - /// Return a handle to the objective. The handle is used as - /// to retrieve the values of objectives after calling Check. + /// Return a handle to the objective. The handle is used as + /// to retrieve the values of objectives after calling Check. /// - public Handle MkMaximize(ArithExpr e) + public Handle MkMaximize(ArithExpr e) { - return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); - } + return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); + } /// /// Declare an arithmetical minimization objective. - /// Similar to MkMaximize. + /// Similar to MkMaximize. /// public Handle MkMinimize(ArithExpr e) { - return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); + return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); } /// /// Retrieve a lower bound for the objective handle. /// - private ArithExpr GetLower(uint index) + private ArithExpr GetLower(uint index) { return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); } @@ -236,7 +236,7 @@ namespace Microsoft.Z3 /// /// Print the context to a string (SMT-LIB parseable benchmark). /// - public override string ToString() + public override string ToString() { return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); } From db411eef25fae56f70d0ffd2ab8781824d3416b1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 13:35:19 +0100 Subject: [PATCH 4/5] Improved supported logics checks for FPA logics. --- src/cmd_context/cmd_context.cpp | 18 ++++++++---------- src/cmd_context/cmd_context.h | 1 + 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 788a8affd..651a84110 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -550,9 +550,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { } bool cmd_context::logic_has_horn(symbol const& s) const { - return - s == "HORN"; - + return s == "HORN"; } bool cmd_context::logic_has_bv() const { @@ -560,19 +558,20 @@ bool cmd_context::logic_has_bv() const { } bool cmd_context::logic_has_seq_core(symbol const& s) const { - return - s == "QF_BVRE"; - + return s == "QF_BVRE"; } bool cmd_context::logic_has_seq() const { return !has_logic() || logic_has_seq_core(m_logic); } -bool cmd_context::logic_has_fpa() const { - return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV"; +bool cmd_context::logic_has_fpa_core(symbol const& s) const { + return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP"; } +bool cmd_context::logic_has_fpa() const { + return !has_logic() || logic_has_fpa_core(m_logic); +} bool cmd_context::logic_has_array_core(symbol const & s) const { return @@ -682,8 +681,7 @@ bool cmd_context::supported_logic(symbol const & s) const { return s == "QF_UF" || s == "UF" || logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || - logic_has_horn(s) || - s == "QF_FP" || s == "QF_FPBV"; + logic_has_horn(s) || logic_has_fpa_core(s); } bool cmd_context::set_logic(symbol const & s) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 7758424e0..148bb61d9 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -250,6 +250,7 @@ protected: bool logic_has_bv_core(symbol const & s) const; bool logic_has_array_core(symbol const & s) const; bool logic_has_seq_core(symbol const & s) const; + bool logic_has_fpa_core(symbol const & s) const; bool logic_has_horn(symbol const& s) const; bool logic_has_arith() const; bool logic_has_bv() const; From 8f86542f2656f508b2666611cf050909a500c333 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 May 2015 13:38:26 +0100 Subject: [PATCH 5/5] Added QF_ALIA to supported logics. Fixes #90 --- src/cmd_context/cmd_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 651a84110..80aa10cde 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -500,6 +500,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_RDL" || s == "QF_IDL" || s == "QF_AUFLIA" || + s == "QF_ALIA" || s == "QF_AUFLIRA" || s == "QF_AUFNIA" || s == "QF_AUFNIRA" || @@ -577,6 +578,7 @@ bool cmd_context::logic_has_array_core(symbol const & s) const { return s == "QF_AX" || s == "QF_AUFLIA" || + s == "QF_ALIA" || s == "QF_AUFLIRA" || s == "QF_AUFNIA" || s == "QF_AUFNIRA" ||