From 1c1357af7d21a4d9c009cde3bb6b514a820bcdda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Jun 2018 07:52:02 -0700 Subject: [PATCH] remove lower case files Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/lambda.cs | 152 --------------------------------------- src/api/java/lambda.java | 134 ---------------------------------- 2 files changed, 286 deletions(-) delete mode 100644 src/api/dotnet/lambda.cs delete mode 100644 src/api/java/lambda.java diff --git a/src/api/dotnet/lambda.cs b/src/api/dotnet/lambda.cs deleted file mode 100644 index b3dc6c01c..000000000 --- a/src/api/dotnet/lambda.cs +++ /dev/null @@ -1,152 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - Lambda.cs - -Abstract: - - Z3 Managed API: Lambda - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-19 - -Notes: - ---*/ - -using System; -using System.Diagnostics.Contracts; - -namespace Microsoft.Z3 -{ - /// - /// Lambda expressions. - /// - [ContractVerification(true)] - public class Lambda : ArrayExpr - { - /// - /// The number of bound variables. - /// - public uint NumBound - { - get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); } - } - - /// - /// The symbols for the bound variables. - /// - public Symbol[] BoundVariableNames - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumBound; - Symbol[] res = new Symbol[n]; - for (uint i = 0; i < n; i++) - res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i)); - return res; - } - } - - /// - /// The sorts of the bound variables. - /// - public Sort[] BoundVariableSorts - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumBound; - Sort[] res = new Sort[n]; - for (uint i = 0; i < n; i++) - res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i)); - return res; - } - } - - /// - /// The body of the lambda. - /// - public Expr Body - { - get - { - Contract.Ensures(Contract.Result() != null); - - return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); - } - } - - /// - /// Translates (copies) the lambda to the Context . - /// - /// A context - /// A copy of the lambda which is associated with - new public Lambda Translate(Context ctx) - { - return (Lambda)base.Translate(ctx); - } - - #region Internal - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug - internal Lambda(Context ctx, Sort[] sorts, Symbol[] names, Expr body) - : base(ctx, IntPtr.Zero) - { - Contract.Requires(ctx != null); - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Context.CheckContextMatch(sorts); - Context.CheckContextMatch(names); - Context.CheckContextMatch(body); - - if (sorts.Length != names.Length) - throw new Z3Exception("Number of sorts does not match number of names"); - - NativeObject = Native.Z3_mk_lambda(ctx.nCtx, - AST.ArrayLength(sorts), AST.ArrayToNative(sorts), - Symbol.ArrayToNative(names), - body.NativeObject); - - } - - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug - internal Lambda(Context ctx, Expr[] bound, Expr body) - : base(ctx, IntPtr.Zero) - { - Contract.Requires(ctx != null); - Contract.Requires(body != null); - - Contract.Requires(bound != null && bound.Length > 0 && Contract.ForAll(bound, n => n != null)); - - Context.CheckContextMatch(bound); - Context.CheckContextMatch(body); - - NativeObject = Native.Z3_mk_lambda_const(ctx.nCtx, - AST.ArrayLength(bound), AST.ArrayToNative(bound), - body.NativeObject); - } - - - internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - -#if DEBUG - internal override void CheckNativeObject(IntPtr obj) - { - if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) - throw new Z3Exception("Underlying object is not a quantifier"); - base.CheckNativeObject(obj); - } -#endif - #endregion - } -} diff --git a/src/api/java/lambda.java b/src/api/java/lambda.java deleted file mode 100644 index 45375fb29..000000000 --- a/src/api/java/lambda.java +++ /dev/null @@ -1,134 +0,0 @@ -/** -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - Lambda.java - -Abstract: - - Z3 Java API: Lambda - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-19 - -Notes: - -**/ - -package com.microsoft.z3; - -import com.microsoft.z3.enumerations.Z3_ast_kind; - - -/** - * Lambda expressions. -*/public class Lambda extends ArrayExpr -{ - - /** - * The number of bound variables. - **/ - public int getNumBound() - { - return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject()); - } - - /** - * The symbols for the bound variables. - * - * @throws Z3Exception - **/ - public Symbol[] getBoundVariableNames() - { - int n = getNumBound(); - Symbol[] res = new Symbol[n]; - for (int i = 0; i < n; i++) - res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName( - getContext().nCtx(), getNativeObject(), i)); - return res; - } - - /** - * The sorts of the bound variables. - * - * @throws Z3Exception - **/ - public Sort[] getBoundVariableSorts() - { - int n = getNumBound(); - Sort[] res = new Sort[n]; - for (int i = 0; i < n; i++) - res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort( - getContext().nCtx(), getNativeObject(), i)); - return res; - } - - /** - * The body of the quantifier. - * - * @throws Z3Exception - **/ - public BoolExpr getBody() - { - return new BoolExpr(getContext(), Native.getQuantifierBody(getContext() - .nCtx(), getNativeObject())); - } - - - /** - * Translates (copies) the quantifier to the Context {@code ctx}. - * - * @param ctx A context - * - * @return A copy of the quantifier which is associated with {@code ctx} - * @throws Z3Exception on error - **/ - public Lambda translate(Context ctx) - { - return (Lambda) super.translate(ctx); - } - - - public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) - { - ctx.checkContextMatch(sorts); - ctx.checkContextMatch(names); - ctx.checkContextMatch(body); - - if (sorts.length != names.length) - throw new Z3Exception("Number of sorts does not match number of names"); - - - long nativeObject = Native.mkLambda(ctx.nCtx(), - AST.arrayLength(sorts), AST.arrayToNative(sorts), - Symbol.arrayToNative(names), - body.getNativeObject()); - - return new Lambda(ctx, nativeObject); - } - - /** - * @param ctx Context to create the lambda on. - * @param bound Bound variables. - * @param body Body of the lambda expression. - */ - - public static Lambda of(Context ctx, Expr[] bound, Expr body) { - ctx.checkContextMatch(body); - - - long nativeObject = Native.mkLambdaConst(ctx.nCtx(), - AST.arrayLength(bound), AST.arrayToNative(bound), - body.getNativeObject()); - return new Lambda(ctx, nativeObject); - } - - - private Lambda(Context ctx, long obj) - { - super(ctx, obj); - } - -}