Merge branch 'master' of https://github.com/Z3Prover/z3

examples/c++/example.cpp

@@ -929,8 +929,8 @@ void enum_sort_example() {
     sort s = ctx.enumeration_sort("enumT", 3, enum_names, enum_consts, enum_testers);
     // enum_consts[0] is a func_decl of arity 0.
     // we convert it to an expression using the operator()
-    expr a = enum_consts[0]();
-    expr b = enum_consts[1]();
+    expr a = enum_consts[0u]();
+    expr b = enum_consts[1u]();
     expr x = ctx.constant("x", s);
     expr test = (x==a) && (x==b);
     std::cout << "1: " << test << std::endl;

scripts/jsdoctest.yml

@@ -0,0 +1,49 @@
+variables:
+
+  Major: '4'
+  Minor: '9'
+  Patch: '2'
+  NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
+
+stages:
+- stage: Build
+  jobs:
+
+  - job: UbuntuDoc
+    displayName: "Ubuntu Doc build"
+    pool:
+      vmImage: "Ubuntu-latest"
+    steps:
+# TODO setup emscripten with no-install, then run
+    - script: npm --prefix=src/api/js ci
+    - script: npm --prefix=src/api/js run build:ts
+
+    - script: sudo apt-get install ocaml opam libgmp-dev
+    - script: opam init -y
+    - script: eval `opam config env`; opam install zarith ocamlfind -y
+    - script: eval `opam config env`; python scripts/mk_make.py --ml
+    - script: sudo apt-get install doxygen
+    - script: sudo apt-get install graphviz
+    - script: |
+        set -e
+        cd build
+        eval `opam config env` 
+        make -j3
+        make -j3 examples
+        make -j3 test-z3
+        cd ..
+    - script: |
+        set -e
+        eval `opam config env` 
+        cd doc
+        python mk_api_doc.py --mld --z3py-package-path=../build/python/z3 --js
+        mkdir api/html/ml
+        ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build/api/ml ../build/api/ml/z3enums.mli ../build/api/ml/z3.mli
+        cd ..
+    - script: zip -r z3doc.zip doc/api
+    - script: cp z3doc.zip $(Build.ArtifactStagingDirectory)/.
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'UbuntuDoc'
+        targetPath: $(Build.ArtifactStagingDirectory)
+

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

@@ -2894,7 +2894,7 @@ namespace z3 {
             if (n == 0)
                 return ctx().bool_val(true);
             else if (n == 1)
-                return operator[](0);
+                return operator[](0u);
             else {
                 array<Z3_ast> args(n);
                 for (unsigned i = 0; i < n; i++)

src/api/dotnet/NativeContext.cs

@@ -100,6 +100,17 @@ namespace Microsoft.Z3
             return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts);
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t[0] - t[1] - ...</c>.
+        /// </summary>
+	public Z3_ast MkSub(params Z3_ast[] t)
+        {
+            Debug.Assert(t != null);
+            Debug.Assert(t.All(a => a != IntPtr.Zero));
+            var ts = t.ToArray();
+	    return Native.Z3_mk_sub(nCtx, (uint)(ts?.Length ?? 0), ts);
+	}
+
         /// <summary>
         /// Create an expression representing <c>t1 / t2</c>.
         /// </summary>

src/api/js/src/jest.ts

@@ -3,7 +3,7 @@
 // @ts-ignore no-implicit-any
 import { createApi, Z3HighLevel } from './high-level';
 import { init as initWrapper, Z3LowLevel } from './low-level';
-import initModule = require('../build/z3-built');
+import initModule = require('../z3-built');
 
 export * from './high-level/types';
 export { Z3Core, Z3LowLevel } from './low-level';