From 310c0f31a10ba2336897ab969f2f00abea61638c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Aug 2016 12:07:06 +0800 Subject: [PATCH] use type constrsaints for co-variant subtying to enable .net 3.5 Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 60 ++++++++++++++++++------------------ src/api/dotnet/Expr.cs | 8 ++--- src/api/dotnet/Fixedpoint.cs | 4 +-- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Goal.cs | 2 +- src/api/dotnet/Quantifier.cs | 12 ++++---- src/api/dotnet/Solver.cs | 6 ++-- src/api/dotnet/Z3Object.cs | 2 +- 8 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b37dc12d7..6ca48fcb0 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -286,8 +286,8 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(fieldNames); - CheckContextMatch(fieldSorts); + CheckContextMatch(fieldNames); + CheckContextMatch(fieldSorts); return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts); } @@ -303,7 +303,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(enumNames); + CheckContextMatch(enumNames); return new EnumSort(this, name, enumNames); } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(constructors); + CheckContextMatch(constructors); return new DatatypeSort(this, name, constructors); } @@ -436,7 +436,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(constructors, c => c != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(constructors); + CheckContextMatch(constructors); return new DatatypeSort(this, MkSymbol(name), constructors); } @@ -454,7 +454,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(names, name => name != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(names); + CheckContextMatch(names); uint n = (uint)names.Length; ConstructorList[] cla = new ConstructorList[n]; IntPtr[] n_constr = new IntPtr[n]; @@ -462,7 +462,7 @@ namespace Microsoft.Z3 { Constructor[] constructor = c[i]; Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays"); - CheckContextMatch(constructor); + CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); n_constr[i] = cla[i].NativeObject; } @@ -520,7 +520,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, name, domain, range); } @@ -551,7 +551,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(domain, d => d != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, MkSymbol(name), domain, range); } @@ -582,7 +582,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(domain, d => d != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(domain); + CheckContextMatch(domain); CheckContextMatch(range); return new FuncDecl(this, prefix, domain, range); } @@ -811,7 +811,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(f); - CheckContextMatch(args); + CheckContextMatch(args); return Expr.Create(this, f, args); } @@ -884,7 +884,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -970,7 +970,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -982,7 +982,7 @@ namespace Microsoft.Z3 Contract.Requires(t != null); Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t))); } @@ -995,7 +995,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1025,7 +1025,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1051,7 +1051,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -1064,7 +1064,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); } @@ -1077,7 +1077,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2205,7 +2205,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(f); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args))); } @@ -2315,7 +2315,7 @@ namespace Microsoft.Z3 Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -2328,7 +2328,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -2429,7 +2429,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2593,7 +2593,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2606,7 +2606,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } @@ -2621,7 +2621,7 @@ namespace Microsoft.Z3 { Contract.Requires(args != null); Contract.Requires(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length, AST.ArrayToNative(args), k)); } @@ -2635,7 +2635,7 @@ namespace Microsoft.Z3 Contract.Requires(coeffs != null); Contract.Requires(args.Length == coeffs.Length); Contract.Requires(Contract.Result() != null); - CheckContextMatch(args); + CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, AST.ArrayToNative(args), coeffs, k)); @@ -3386,7 +3386,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - CheckContextMatch(ts); + CheckContextMatch(ts); IntPtr last = IntPtr.Zero; if (ts != null && ts.Length > 0) @@ -3577,7 +3577,7 @@ namespace Microsoft.Z3 Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null)); Contract.Ensures(Contract.Result() != null); - CheckContextMatch(t); + CheckContextMatch(t); return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); } @@ -4810,7 +4810,7 @@ namespace Microsoft.Z3 } [Pure] - internal void CheckContextMatch(IEnumerable arr) + internal void CheckContextMatch(IEnumerable arr) where T : Z3Object { Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null)); diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index c995a12bd..cac62d2f0 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -98,7 +98,7 @@ namespace Microsoft.Z3 Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); - Context.CheckContextMatch(args); + Context.CheckContextMatch(args); if (IsApp && args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args)); @@ -120,8 +120,8 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(to, t => t != null)); Contract.Ensures(Contract.Result() != null); - Context.CheckContextMatch(from); - Context.CheckContextMatch(to); + Context.CheckContextMatch(from); + Context.CheckContextMatch(to); if (from.Length != to.Length) throw new Z3Exception("Argument sizes do not match"); return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); @@ -152,7 +152,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(to, t => t != null)); Contract.Ensures(Contract.Result() != null); - Context.CheckContextMatch(to); + Context.CheckContextMatch(to); return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to))); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 66449ddbb..e2fb7fe5a 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -71,7 +71,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) { Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject); @@ -151,7 +151,7 @@ namespace Microsoft.Z3 Contract.Requires(relations != null); Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null)); - Context.CheckContextMatch(relations); + Context.CheckContextMatch(relations); Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 15b6a59db..2f5cd0ce8 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -339,7 +339,7 @@ namespace Microsoft.Z3 { Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); - Context.CheckContextMatch(args); + Context.CheckContextMatch(args); return Expr.Create(Context, this, args); } diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 5ee44f34b..521b453f8 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -82,7 +82,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr c in constraints) { Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index 38e435309..eb21ed2b9 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -172,10 +172,10 @@ namespace Microsoft.Z3 Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - Context.CheckContextMatch(patterns); - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(sorts); - Context.CheckContextMatch(names); + Context.CheckContextMatch(patterns); + Context.CheckContextMatch(noPatterns); + Context.CheckContextMatch(sorts); + Context.CheckContextMatch(names); Context.CheckContextMatch(body); if (sorts.Length != names.Length) @@ -212,8 +212,8 @@ namespace Microsoft.Z3 Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null)); - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(patterns); + Context.CheckContextMatch(noPatterns); + Context.CheckContextMatch(patterns); //Context.CheckContextMatch(bound); Context.CheckContextMatch(body); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index f8f340373..8cb7670d7 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -111,7 +111,7 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Context.CheckContextMatch(constraints); + Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) { Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject); @@ -142,8 +142,8 @@ namespace Microsoft.Z3 Contract.Requires(constraints != null); Contract.Requires(Contract.ForAll(constraints, c => c != null)); Contract.Requires(Contract.ForAll(ps, c => c != null)); - Context.CheckContextMatch(constraints); - Context.CheckContextMatch(ps); + Context.CheckContextMatch(constraints); + Context.CheckContextMatch(ps); if (constraints.Length != ps.Length) throw new Z3Exception("Argument size mismatch"); diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index cd6803341..f32ba30af 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -138,7 +138,7 @@ namespace Microsoft.Z3 } [Pure] - internal static IntPtr[] EnumToNative(IEnumerable a) + internal static IntPtr[] EnumToNative(IEnumerable a) where T : Z3Object { Contract.Ensures(a == null || Contract.Result() != null); Contract.Ensures(a == null || Contract.Result().Length == a.Count());