Add missing API bindings: Python BvNand/BvNor/BvXnor, Go MkAsArray/MkRecFuncDecl/AddRecDef/Model.Translate, TS Array.fromFunc/Model.translate, OCaml Model.translate

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/go/array.go

@@ -64,3 +64,9 @@ func (c *Context) MkArrayDefault(array *Expr) *Expr {
 func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_array_ext(c.ptr, a1.ptr, a2.ptr))
 }
+
+// MkAsArray creates an array from a function declaration.
+// The resulting array maps each input to the output of the function.
+func (c *Context) MkAsArray(f *FuncDecl) *Expr {
+	return newExpr(c, C.Z3_mk_as_array(c.ptr, f.ptr))
+}

src/api/go/solver.go

@@ -511,3 +511,9 @@ func (m *Model) SortUniverse(sort *Sort) []*Expr {
 	}
 	return astVectorToExprs(m.ctx, vec)
 }
+
+// Translate creates a copy of the model in the target context.
+func (m *Model) Translate(target *Context) *Model {
+	ptr := C.Z3_model_translate(m.ctx.ptr, m.ptr, target.ptr)
+	return newModel(target, ptr)
+}

src/api/go/z3.go

@@ -471,6 +471,33 @@ func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDe
 	return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
 }
 
+// MkRecFuncDecl creates a recursive function declaration.
+// After creating, use AddRecDef to provide the function body.
+func (c *Context) MkRecFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl {
+	cDomain := make([]C.Z3_sort, len(domain))
+	for i, s := range domain {
+		cDomain[i] = s.ptr
+	}
+	var domainPtr *C.Z3_sort
+	if len(domain) > 0 {
+		domainPtr = &cDomain[0]
+	}
+	return newFuncDecl(c, C.Z3_mk_rec_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
+}
+
+// AddRecDef adds the definition (body) for a recursive function created with MkRecFuncDecl.
+func (c *Context) AddRecDef(f *FuncDecl, args []*Expr, body *Expr) {
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	var argsPtr *C.Z3_ast
+	if len(args) > 0 {
+		argsPtr = &cArgs[0]
+	}
+	C.Z3_add_rec_def(c.ptr, f.ptr, C.uint(len(args)), argsPtr, body.ptr)
+}
+
 // MkApp creates a function application.
 func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr {
 	cArgs := make([]C.Z3_ast, len(args))

src/api/js/src/high-level/high-level.ts

@@ -1093,6 +1093,9 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
       ): SMTArray<Name, [DomainSort], RangeSort> {
         return new ArrayImpl<[DomainSort], RangeSort>(check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr)));
       },
+      fromFunc(f: FuncDecl<Name>): SMTArray<Name> {
+        return new ArrayImpl(check(Z3.mk_as_array(contextPtr, f.ast)));
+      },
     };
     const Set = {
       // reference: https://z3prover.github.io/api/html/namespacez3py.html#a545f894afeb24caa1b88b7f2a324ee7e
@@ -2812,6 +2815,11 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
         return this.getUniverse(sort) as AstVector<Name, AnyExpr<Name>>;
       }
 
+      translate(target: Context<Name>): Model<Name> {
+        const ptr = check(Z3.model_translate(contextPtr, this.ptr, target.ptr));
+        return new (target.Model as unknown as new (ptr: Z3_model) => Model<Name>)(ptr);
+      }
+
       release() {
         Z3.model_dec_ref(contextPtr, this.ptr);
         this._ptr = null;

src/api/js/src/high-level/types.ts

@@ -1883,6 +1883,14 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
    */
   sortUniverse(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
 
+  /**
+   * Translate the model to a different context.
+   *
+   * @param target - The target context
+   * @returns A new model in the target context
+   */
+  translate(target: Context<Name>): Model<Name>;
+
   /**
    * Manually decrease the reference count of the model
    * This is automatically done when the model is garbage collected,
@@ -2915,6 +2923,12 @@ export interface SMTArrayCreation<Name extends string> {
     domain: DomainSort,
     value: SortToExprMap<RangeSort, Name>,
   ): SMTArray<Name, [DomainSort], RangeSort>;
+
+  /**
+   * Create an array from a function declaration.
+   * The resulting array maps each input to the output of the function.
+   */
+  fromFunc(f: FuncDecl<Name>): SMTArray<Name>;
 }
 
 export type NonEmptySortArray<Name extends string = 'main'> = [Sort<Name>, ...Array<Sort<Name>>];

src/api/ml/z3.ml

@@ -1692,6 +1692,8 @@ struct
     let av = Z3native.model_get_sort_universe (gc x) x s in
     AST.ASTVector.to_expr_list av
 
+  let translate (x:model) (to_ctx:context) = Z3native.model_translate (gc x) x to_ctx
+
   let to_string (x:model) = Z3native.model_to_string (gc x) x
 end
 

src/api/ml/z3.mli

@@ -3057,6 +3057,10 @@ sig
       @return A list of expressions, where each is an element of the universe of the sort *)
   val sort_universe : model -> Sort.sort -> Expr.expr list
 
+  (** Translate the model to a different context.
+      @return A new model in the target context *)
+  val translate : model -> context -> model
+
   (** Conversion of models to strings.
       @return A string representation of the model. *)
   val to_string : model -> string

src/api/python/z3/z3.py

@@ -4652,6 +4652,45 @@ def BVRedOr(a):
     return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
 
 
+def BvNand(a, b):
+    """Return the bitwise NAND of `a` and `b`.
+
+    >>> x = BitVec('x', 8)
+    >>> y = BitVec('y', 8)
+    >>> BvNand(x, y)
+    bvnand(x, y)
+    """
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BitVecRef(Z3_mk_bvnand(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+
+def BvNor(a, b):
+    """Return the bitwise NOR of `a` and `b`.
+
+    >>> x = BitVec('x', 8)
+    >>> y = BitVec('y', 8)
+    >>> BvNor(x, y)
+    bvnor(x, y)
+    """
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BitVecRef(Z3_mk_bvnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+
+def BvXnor(a, b):
+    """Return the bitwise XNOR of `a` and `b`.
+
+    >>> x = BitVec('x', 8)
+    >>> y = BitVec('y', 8)
+    >>> BvXnor(x, y)
+    bvxnor(x, y)
+    """
+    _check_bv_args(a, b)
+    a, b = _coerce_exprs(a, b)
+    return BitVecRef(Z3_mk_bvxnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+
 def BVAddNoOverflow(a, b, signed):
     """A predicate the determines that bit-vector addition does not overflow"""
     _check_bv_args(a, b)