From 393c63fe0cc5afe1c32b2a46f154d8e0bce267e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jul 2022 09:33:39 -0700 Subject: [PATCH 1/5] fix #6114 --- examples/c++/example.cpp | 4 ++-- src/api/c++/z3++.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 0217c5cca..c71c3ff2f 100644 --- a/examples/c++/example.cpp +++ b/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; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index fc0601fe5..8aaeb31ab 100644 --- a/src/api/c++/z3++.h +++ b/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 args(n); for (unsigned i = 0; i < n; i++) From 7ded856bb14692c7310f62f89d167f76334fb0df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jul 2022 09:51:34 -0700 Subject: [PATCH 2/5] script to test jsdoc Signed-off-by: Nikolaj Bjorner --- scripts/jsdoctest.yml | 49 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 scripts/jsdoctest.yml diff --git a/scripts/jsdoctest.yml b/scripts/jsdoctest.yml new file mode 100644 index 000000000..1a3a5286f --- /dev/null +++ b/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) + From 7f1893d78175ee64bce836eb15a5daa9771a620c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jul 2022 10:21:27 -0700 Subject: [PATCH 3/5] add missing MkSub to NativeContext Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/NativeContext.cs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index 93180e583..afae66e46 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -100,6 +100,17 @@ namespace Microsoft.Z3 return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts); } + /// + /// Create an expression representing t[0] - t[1] - .... + /// + 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); + } + /// /// Create an expression representing t1 / t2. /// From afcfc80c4260db4041891ff2e7dce2be46a21efd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jul 2022 11:21:16 -0700 Subject: [PATCH 4/5] the relative path seems out of sync with how it is set up in node.ts --- src/api/js/src/jest.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/js/src/jest.ts b/src/api/js/src/jest.ts index 9cbab31f1..18f43e4c2 100644 --- a/src/api/js/src/jest.ts +++ b/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'; From dead0c9de230dc9ea03da8dc01d4b62f8646f261 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jul 2022 11:47:57 -0700 Subject: [PATCH 5/5] reverting relative path Signed-off-by: Nikolaj Bjorner --- src/api/js/src/jest.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/js/src/jest.ts b/src/api/js/src/jest.ts index 18f43e4c2..2de6cdab1 100644 --- a/src/api/js/src/jest.ts +++ b/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('./z3-built'); +import initModule = require('../z3-built'); export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level';