mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
remove lower case files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a8e864a3e6
commit
1c1357af7d
|
|
@ -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
|
||||
{
|
||||
/// <summary>
|
||||
/// Lambda expressions.
|
||||
/// </summary>
|
||||
[ContractVerification(true)]
|
||||
public class Lambda : ArrayExpr
|
||||
{
|
||||
/// <summary>
|
||||
/// The number of bound variables.
|
||||
/// </summary>
|
||||
public uint NumBound
|
||||
{
|
||||
get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The symbols for the bound variables.
|
||||
/// </summary>
|
||||
public Symbol[] BoundVariableNames
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<Symbol[]>() != 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;
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The sorts of the bound variables.
|
||||
/// </summary>
|
||||
public Sort[] BoundVariableSorts
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<Sort[]>() != 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;
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The body of the lambda.
|
||||
/// </summary>
|
||||
public Expr Body
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<BoolExpr>() != null);
|
||||
|
||||
return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Translates (copies) the lambda to the Context <paramref name="ctx"/>.
|
||||
/// </summary>
|
||||
/// <param name="ctx">A context</param>
|
||||
/// <returns>A copy of the lambda which is associated with <paramref name="ctx"/></returns>
|
||||
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<Sort>(sorts);
|
||||
Context.CheckContextMatch<Symbol>(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<Expr>(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
|
||||
}
|
||||
}
|
||||
|
|
@ -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);
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Reference in a new issue