mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Managed API: Bugfixes and refactoring.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
c6303fc8f5
commit
c045214da2
|
@ -1533,6 +1533,7 @@ namespace Microsoft.Z3
|
|||
case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
|
||||
case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
|
||||
case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
|
||||
case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1544,6 +1545,7 @@ namespace Microsoft.Z3
|
|||
case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
|
||||
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
|
||||
case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
|
||||
}
|
||||
|
||||
return new Expr(ctx, obj);
|
||||
|
|
|
@ -181,8 +181,6 @@ namespace Microsoft.Z3
|
|||
if (sorts.Length != names.Length)
|
||||
throw new Z3Exception("Number of sorts does not match number of names");
|
||||
|
||||
IntPtr[] _patterns = AST.ArrayToNative(patterns);
|
||||
|
||||
if (noPatterns == null && quantifierID == null && skolemID == null)
|
||||
{
|
||||
NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
|
||||
|
|
Loading…
Reference in a new issue