add missing files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

RELEASE_NOTES

@@ -27,7 +27,10 @@ Version 4.8.0
      Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
      as lemmas (redundant) and are garbage collected if their glue level is high.
    - Substantial overhaul of the spacer horn clause engine.
-   - Added basic features to support Lambda expressions.
+   - Added basic features to support Lambda bindings.
+   - Added model compression to eliminate local function definitions in models when
+     inlining them does not incur substantial overhead. The old behavior, where models are left
+     uncompressed can be replayed by setting the top-level parameter model_compress=false.
 
 - Removed features:
   - interpolation API

src/api/dotnet/lambda.cs

@@ -0,0 +1,152 @@
+/*++
+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
+    }
+}

src/api/java/lambda.java

@@ -0,0 +1,134 @@
+/**
+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);
+    }
+
+}