integrate lambda expressions

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

RELEASE_NOTES

@@ -27,6 +27,7 @@ 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.
 
 - Removed features:
   - interpolation API

src/api/api_array.cpp

@@ -47,6 +47,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+
     Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i) {
         Z3_TRY;
         LOG_Z3_mk_select(c, a, i);
@@ -99,6 +100,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+
     Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) {
         Z3_TRY;
         LOG_Z3_mk_store(c, a, i, v);
@@ -155,6 +157,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+
     Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
         Z3_TRY;
         LOG_Z3_mk_map(c, f, n, args);

src/api/api_ast.cpp

@@ -808,8 +808,7 @@ extern "C" {
         expr * a = to_expr(_a);
         expr * const * to   = to_exprs(_to);
         var_subst subst(m, false);
-        expr_ref new_a(m);
-        subst(a, num_exprs, to, new_a);
+        expr_ref new_a = subst(a, num_exprs, to);
         mk_c(c)->save_ast_trail(new_a);
         RETURN_Z3(of_expr(new_a.get()));
         Z3_CATCH_RETURN(nullptr);
@@ -910,6 +909,7 @@ extern "C" {
             case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR;
             case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY;
             case PR_QUANT_INTRO: return Z3_OP_PR_QUANT_INTRO;
+            case PR_BIND: return Z3_OP_PR_BIND;
             case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY;
             case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM;
             case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM;

src/api/api_opt.cpp

@@ -173,6 +173,7 @@ extern "C" {
         to_optimize_ptr(o)->get_model(_m);
         Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         if (_m) {
+            if (mk_c(c)->params().m_model_compress) _m->compress();
             m_ref->m_model = _m;
         }
         else {

src/api/api_quant.cpp

@@ -90,7 +90,7 @@ extern "C" {
         expr_ref result(mk_c(c)->m());
         if (num_decls > 0) {
             result = mk_c(c)->m().mk_quantifier(
-                (0 != is_forall),
+                is_forall ? forall_k : exists_k,
                 names.size(), ts, names.c_ptr(), to_expr(body),
                 weight,
                 qid,
@@ -144,6 +144,61 @@ extern "C" {
         return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body);
     }
 
+    Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
+                               unsigned num_decls, Z3_sort const types[],
+                               Z3_symbol const decl_names[],
+                               Z3_ast body) {
+
+        Z3_TRY;
+        LOG_Z3_mk_lambda(c, num_decls, types, decl_names, body);
+        RESET_ERROR_CODE();
+        expr_ref result(mk_c(c)->m());
+        if (num_decls == 0) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE);
+            RETURN_Z3(0);
+        }
+
+        sort* const* ts = reinterpret_cast<sort * const*>(types);
+        svector<symbol> names;
+        for (unsigned i = 0; i < num_decls; ++i) {
+            names.push_back(to_symbol(decl_names[i]));
+        }
+        result = mk_c(c)->m().mk_lambda(names.size(), ts, names.c_ptr(), to_expr(body));
+        mk_c(c)->save_ast_trail(result.get());
+        return of_ast(result.get());
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, 
+                                     unsigned num_decls, Z3_app const vars[],
+                                     Z3_ast body) {
+
+        Z3_TRY;
+        LOG_Z3_mk_lambda_const(c, num_decls, vars, body);
+        RESET_ERROR_CODE();
+        if (num_decls == 0) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE);
+            RETURN_Z3(0);
+        }
+
+        svector<symbol>  _names;
+        ptr_vector<sort> _vars;
+        ptr_vector<expr> _args;
+        for (unsigned i = 0; i < num_decls; ++i) {
+            app* a = to_app(vars[i]);
+            _names.push_back(to_app(a)->get_decl()->get_name());
+            _args.push_back(a);
+            _vars.push_back(mk_c(c)->m().get_sort(a));
+        }
+        expr_ref result(mk_c(c)->m());        
+        expr_abstract(mk_c(c)->m(), 0, num_decls, _args.c_ptr(), to_expr(body), result);
+
+        result = mk_c(c)->m().mk_lambda(_vars.size(), _vars.c_ptr(), _names.c_ptr(), result);
+        mk_c(c)->save_ast_trail(result.get());
+        return of_ast(result.get());
+        Z3_CATCH_RETURN(0);
+    }
+
 
     Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c,
                                             Z3_bool is_forall,
@@ -292,17 +347,27 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_is_quantifier_forall(c, a);
         RESET_ERROR_CODE();
-        ast * _a = to_ast(a);
-        if (_a->get_kind() == AST_QUANTIFIER) {
-            return to_quantifier(_a)->is_forall();
-        }
-        else {
-            SET_ERROR_CODE(Z3_SORT_ERROR);
-            return Z3_FALSE;
-        }
+        return ::is_forall(to_ast(a)) ? Z3_TRUE : Z3_FALSE;
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
+    Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_is_quantifier_exists(c, a);
+        RESET_ERROR_CODE();
+        return ::is_exists(to_ast(a))  ? Z3_TRUE : Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_is_lambda(c, a);
+        RESET_ERROR_CODE();
+        return ::is_lambda(to_ast(a))  ? Z3_TRUE : Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+
     unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_get_quantifier_weight(c, a);
@@ -485,3 +550,4 @@ extern "C" {
     }
 
 };
+

src/api/api_solver.cpp

@@ -433,6 +433,9 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_USAGE);
             RETURN_Z3(nullptr);
         }
+        if (_m) {
+            if (mk_c(c)->params().m_model_compress) _m->compress();
+        }
         Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         m_ref->m_model = _m;
         mk_c(c)->save_object(m_ref);

src/api/c++/z3++.h

@@ -252,7 +252,6 @@ namespace z3 {
         */
         sort array_sort(sort d, sort r);
         sort array_sort(sort_vector const& d, sort r);
-
         /**
            \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
            \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
@@ -675,7 +674,21 @@ namespace z3 {
            \brief Return true if this expression is a quantifier.
         */
         bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
+
+        /**
+           \brief Return true if this expression is a universal quantifier.
+        */
+        bool is_forall() const { return 0 != Z3_is_quantifier_forall(ctx(), m_ast); }
+        /**
+           \brief Return true if this expression is an existential quantifier.
+        */
+        bool is_exists() const { return 0 != Z3_is_quantifier_exists(ctx(), m_ast); }
+        /**
+           \brief Return true if this expression is a lambda expression.
+        */
+        bool is_lambda() const { return 0 != Z3_is_lambda(ctx(), m_ast); }
         /**
+
            \brief Return true if this expression is a variable.
         */
         bool is_var() const { return kind() == Z3_VAR_AST; }
@@ -1638,6 +1651,31 @@ namespace z3 {
         array<Z3_app> vars(xs);
         Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
     }
+    inline expr lambda(expr const & x, expr const & b) {
+        check_context(x, b);
+        Z3_app vars[] = {(Z3_app) x};
+        Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
+    }
+    inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
+        check_context(x1, b); check_context(x2, b);
+        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
+        Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
+    }
+    inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
+        check_context(x1, b); check_context(x2, b); check_context(x3, b);
+        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
+        Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
+    }
+    inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
+        check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
+        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
+        Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
+    }
+    inline expr lambda(expr_vector const & xs, expr const & b) {
+        array<Z3_app> vars(xs);
+        Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
+    }
+
     inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
         assert(es.size() > 0);
         context& ctx = es[0].ctx();
@@ -2521,7 +2559,6 @@ namespace z3 {
         array<Z3_sort> dom(d);
         Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s); 
     }
-
     inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
         array<Z3_symbol> _enum_names(n);
         for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
@@ -2785,12 +2822,8 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
-    inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
-    inline expr store(expr const & a, expr const & i, expr const & v) {
-        check_context(a, i); check_context(a, v);
-        Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
-        a.check_error();
-        return expr(a.ctx(), r);
+    inline expr select(expr const & a, int i) { 
+        return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); 
     }
     inline expr select(expr const & a, expr_vector const & i) {
         check_context(a, i);
@@ -2800,6 +2833,13 @@ namespace z3 {
         return expr(a.ctx(), r);
     }
 
+    inline expr store(expr const & a, expr const & i, expr const & v) {
+        check_context(a, i); check_context(a, v);
+        Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+
     inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
     inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
     inline expr store(expr const & a, int i, int v) {

src/api/dotnet/ArrayExpr.cs

@@ -37,6 +37,6 @@ internal ArrayExpr(Context ctx, IntPtr obj)
         {
             Contract.Requires(ctx != null);
         }
-        #endregion
+        #endregion	
     }
 }

src/api/dotnet/CMakeLists.txt

@@ -84,6 +84,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     IntNum.cs
     IntSort.cs
     IntSymbol.cs
+    Lambda.cs
     ListSort.cs
     Log.cs
     Model.cs

src/api/dotnet/Context.cs

@@ -3292,6 +3292,53 @@ public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body,
                 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
         }
 
+        /// <summary>
+        /// Create a lambda expression.
+        /// </summary>
+        /// <remarks>
+        /// Creates a lambda expression.
+        /// <paramref name="sorts"/> is an array
+        /// with the sorts of the bound variables, <paramref name="names"/> is an array with the
+        /// 'names' of the bound variables, and <paramref name="body"/> is the body of the
+        /// lambda. 
+        /// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>.
+        /// Z3 applies the convention that the last element in <paramref name="names"/> and
+        /// <paramref name="sorts"/> refers to the variable with index 0, the second to last element
+        /// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable
+        /// with index 1, etc.
+        /// </remarks>
+        /// <param name="sorts">the sorts of the bound variables.</param>
+        /// <param name="names">names of the bound variables</param>
+        /// <param name="body">the body of the quantifier.</param>
+        public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body)
+        {
+            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));
+            Contract.Ensures(Contract.Result<Lambda>() != null);
+            return new Lambda(this, sorts, names, body);
+        }
+
+        /// <summary>
+        /// Create a lambda expression.
+        /// </summary>
+        /// <remarks>
+        /// Creates a lambda expression using a list of constants that will
+        /// form the set of bound variables.
+        /// <seealso cref="MkLambda(Sort[], Symbol[], Expr)"/>
+        /// </remarks>
+        public Lambda MkLambda(Expr[] boundConstants, Expr body)
+        {
+            Contract.Requires(body != null);
+            Contract.Requires(boundConstants != null && Contract.ForAll(boundConstants, b => b != null));
+            Contract.Ensures(Contract.Result<Lambda>() != null);
+            return new Lambda(this, boundConstants, body);
+        }
+
+
         #endregion
 
         #endregion // Expr

src/api/dotnet/Quantifier.cs

@@ -41,7 +41,7 @@ public bool IsUniversal
         /// </summary>
         public bool IsExistential
         {
-            get { return !IsUniversal; }
+            get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; }
         }
 
         /// <summary>

src/api/java/CMakeLists.txt

@@ -141,6 +141,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   IntNum.java
   IntSort.java
   IntSymbol.java
+  Lambda.java
   ListSort.java
   Log.java
   ModelDecRefQueue.java