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

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:
+        if k == 0:
-	    return ComplexExpr(1, 0)
+            return ComplexExpr(1, 0)
-	if k == 1:
+        if k == 1:
-	    return self
+            return self
-	if k < 0:
+        if k < 0:
-	    return (self ** (-k)).inv()
+            return (self ** (-k)).inv()
-	return reduce(lambda x, y: x * y, [self for _ in xrange(k)], ComplexExpr(1, 0))
+        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

src/api/dotnet/Microsoft.Z3.csproj

@@ -365,6 +365,7 @@
     <Compile Include="IntSymbol.cs" />
     <Compile Include="ListSort.cs" />
     <Compile Include="Model.cs" />
+    <Compile Include="Optimize.cs" />
     <Compile Include="Params.cs" />
     <Compile Include="ParamDescrs.cs" />
     <Compile Include="Pattern.cs" />

src/api/dotnet/Optimize.cs

@@ -85,43 +85,43 @@ namespace Microsoft.Z3
             Assert(constraints);
         }
 
-	/// <summary>
+        /// <summary>
-	/// Handle to objectives returned by objective functions.
+        /// Handle to objectives returned by objective functions.
-	/// </summary>
+        /// </summary>
-	public class Handle 
+        public class Handle
         {
-	    Optimize opt;
+            Optimize opt;
-	    uint     handle;
+            uint handle;
-	    internal Handle(Optimize opt, uint h) 
+            internal Handle(Optimize opt, uint h)
-	    {
+            {
-	        this.opt = opt;
+                this.opt = opt;
-	        this.handle = h;
+                this.handle = h;
-	    }
+            }
 
             /// <summary>
             /// Retrieve a lower bound for the objective handle.
             /// </summary>        	   	
-	    public ArithExpr Lower
+            public ArithExpr Lower
-	    {
+            {
-		get { return opt.GetLower(handle); }
+                get { return opt.GetLower(handle); }
-	    }
+            }
 
             /// <summary>
             /// Retrieve an upper bound for the objective handle.
             /// </summary>        	   	
-	    public ArithExpr Upper
+            public ArithExpr Upper
-	    {
+            {
-		get { return opt.GetUpper(handle); }
+                get { return opt.GetUpper(handle); }
-	    }
+            }
 
             /// <summary>
             /// Retrieve the value of an objective.
             /// </summary>        	   	
-	    public ArithExpr Value
+            public ArithExpr Value
-	    {
+            {
-		get { return Lower; }
+                get { return Lower; }
-	    }
+            }
-	}
+        }
 
         /// <summary>
         /// Assert soft constraint
@@ -132,20 +132,20 @@ namespace Microsoft.Z3
         public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
         {
             Context.CheckContextMatch(constraint);
-	        Symbol s = Context.MkSymbol(group);            
+            Symbol s = Context.MkSymbol(group);
-	        return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));            
+            return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
         }
 
 
-	///
+        /// <summary>
-	/// <summary>
+        /// Check satisfiability of asserted constraints.
-	/// Check satisfiability of asserted constraints.
+        /// Produce a model that (when the objectives are bounded and 
-	/// Produce a model that (when the objectives are bounded and 
+        /// don't use strict inequalities) meets the objectives.
-	/// don't use strict inequalities) meets the objectives.
+        /// </summary>
-	/// </summary>
+        ///
-	///
+        public Status Check()
-        public Status Check() {
+        {
-	        Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
+            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
             switch (r)
             {
                 case Z3_lbool.Z3_L_TRUE:
@@ -198,21 +198,21 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Declare an arithmetical maximization objective.
-	/// Return a handle to the objective. The handle is used as
+        /// Return a handle to the objective. The handle is used as
-	/// to retrieve the values of objectives after calling Check.
+        /// to retrieve the values of objectives after calling Check.
         /// </summary>        	
         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));
-	    }
+        }
 
         /// <summary>
         /// Declare an arithmetical minimization objective. 
-	/// Similar to MkMaximize.
+        /// Similar to MkMaximize.
         /// </summary>        	
         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));
         }
 
         /// <summary>

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" ||
@@ -550,9 +551,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
 }
 
 bool cmd_context::logic_has_horn(symbol const& s) const {
-    return
+    return s == "HORN";
-        s == "HORN";
-
 }
 
 bool cmd_context::logic_has_bv() const {
@@ -560,24 +559,26 @@ bool cmd_context::logic_has_bv() const {
 }
 
 bool cmd_context::logic_has_seq_core(symbol const& s) const {
-    return 
+    return s == "QF_BVRE";
-        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 {
+bool cmd_context::logic_has_fpa_core(symbol const& s) const {
-    return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV";
+    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 
         s == "QF_AX" ||
         s == "QF_AUFLIA" ||
+        s == "QF_ALIA" ||
         s == "QF_AUFLIRA" ||
         s == "QF_AUFNIA" ||
         s == "QF_AUFNIRA" ||
@@ -682,8 +683,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) ||
+        logic_has_horn(s) || logic_has_fpa_core(s);
-        s == "QF_FP" || s == "QF_FPBV";
 }
 
 bool cmd_context::set_logic(symbol const & s) {

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;