mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

use type constrsaints for co-variant subtying to enable .net 3.5

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-08-30 12:07:06 +08:00
parent d4539b8887
commit 310c0f31a1
8 changed files with 48 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/api/dotnet/Context.cs
View file

@ -286,8 +286,8 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<TupleSort>() != null);
CheckContextMatch(name);
CheckContextMatch(fieldNames);
CheckContextMatch(fieldSorts);
CheckContextMatch<Symbol>(fieldNames);
CheckContextMatch<Sort>(fieldSorts);
return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
}
@ -303,7 +303,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<EnumSort>() != null);
CheckContextMatch(name);
CheckContextMatch(enumNames);
CheckContextMatch<Symbol>(enumNames);
return new EnumSort(this, name, enumNames);
}
@ -423,7 +423,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<DatatypeSort>() != null);
CheckContextMatch(name);
CheckContextMatch(constructors);
CheckContextMatch<Constructor>(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<DatatypeSort>() != null);
CheckContextMatch(constructors);
CheckContextMatch<Constructor>(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<DatatypeSort[]>() != null);
CheckContextMatch(names);
CheckContextMatch<Symbol>(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>(constructor);
cla[i] = new ConstructorList(this, constructor);
n_constr[i] = cla[i].NativeObject;
}
@ -520,7 +520,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(name);
CheckContextMatch(domain);
CheckContextMatch<Sort>(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<FuncDecl>() != null);
CheckContextMatch(domain);
CheckContextMatch<Sort>(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<FuncDecl>() != null);
CheckContextMatch(domain);
CheckContextMatch<Sort>(domain);
CheckContextMatch(range);
return new FuncDecl(this, prefix, domain, range);
}
@ -811,7 +811,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(f);
CheckContextMatch(args);
CheckContextMatch<Expr>(args);
return Expr.Create(this, f, args);
}
@ -884,7 +884,7 @@ namespace Microsoft.Z3
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(args);
CheckContextMatch<Expr>(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<BoolExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<BoolExpr>(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<BoolExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<BoolExpr>(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<BoolExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<BoolExpr>(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<ArithExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ArithExpr>(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<ArithExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ArithExpr>(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<ArithExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ArithExpr>(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<ArithExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ArithExpr>(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<ArrayExpr>() != null);
CheckContextMatch(f);
CheckContextMatch(args);
CheckContextMatch<ArrayExpr>(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<ArrayExpr>(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<Expr>() != null);
CheckContextMatch(args);
CheckContextMatch<ArrayExpr>(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<SeqExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<SeqExpr>(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<ReExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ReExpr>(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<ReExpr>() != null);
CheckContextMatch(t);
CheckContextMatch<ReExpr>(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<BoolExpr[]>() != null);
CheckContextMatch(args);
CheckContextMatch<BoolExpr>(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<BoolExpr[]>() != null);
CheckContextMatch(args);
CheckContextMatch<BoolExpr>(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<Tactic>(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<Tactic>() != null);
CheckContextMatch(t);
CheckContextMatch<Tactic>(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<Z3Object> arr)
internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
{
Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));

8
src/api/dotnet/Expr.cs
View file

@ -98,7 +98,7 @@ namespace Microsoft.Z3
Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null));
Context.CheckContextMatch(args);
Context.CheckContextMatch<Expr>(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<Expr>() != null);
Context.CheckContextMatch(from);
Context.CheckContextMatch(to);
Context.CheckContextMatch<Expr>(from);
Context.CheckContextMatch<Expr>(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<Expr>() != null);
Context.CheckContextMatch(to);
Context.CheckContextMatch<Expr>(to);
return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
}

4
src/api/dotnet/Fixedpoint.cs
View file

@ -71,7 +71,7 @@ namespace Microsoft.Z3
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Context.CheckContextMatch(constraints);
Context.CheckContextMatch<BoolExpr>(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<FuncDecl>(relations);
Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
AST.ArrayLength(relations), AST.ArrayToNative(relations));
switch (r)

2
src/api/dotnet/FuncDecl.cs
View file

@ -339,7 +339,7 @@ namespace Microsoft.Z3
{
Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
Context.CheckContextMatch(args);
Context.CheckContextMatch<Expr>(args);
return Expr.Create(Context, this, args);
}

2
src/api/dotnet/Goal.cs
View file

@ -82,7 +82,7 @@ namespace Microsoft.Z3
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Context.CheckContextMatch(constraints);
Context.CheckContextMatch<BoolExpr>(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

12
src/api/dotnet/Quantifier.cs
View file

@ -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<Pattern>(patterns);
Context.CheckContextMatch<Expr>(noPatterns);
Context.CheckContextMatch<Sort>(sorts);
Context.CheckContextMatch<Symbol>(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<Expr>(noPatterns);
Context.CheckContextMatch<Pattern>(patterns);
//Context.CheckContextMatch(bound);
Context.CheckContextMatch(body);

6
src/api/dotnet/Solver.cs
View file

@ -111,7 +111,7 @@ namespace Microsoft.Z3
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Context.CheckContextMatch(constraints);
Context.CheckContextMatch<BoolExpr>(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<BoolExpr>(constraints);
Context.CheckContextMatch<BoolExpr>(ps);
if (constraints.Length != ps.Length)
throw new Z3Exception("Argument size mismatch");

2
src/api/dotnet/Z3Object.cs
View file

@ -138,7 +138,7 @@ namespace Microsoft.Z3
}
[Pure]
internal static IntPtr[] EnumToNative(IEnumerable<Z3Object> a)
internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T : Z3Object
{
Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Count());