Merge remote-tracking branch 'origin/master' into polysat

.github/workflows/docker-image.yml

@@ -41,7 +41,7 @@ jobs:
             type=edge
             type=sha,prefix=ubuntu-20.04-bare-z3-sha-
       - name: Build and push Bare Z3 Docker Image
-        uses: docker/build-push-action@v5.0.0
+        uses: docker/build-push-action@v5.1.0
         with:  
           context: .
           push: true

.github/workflows/wasm-release.yml

@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Setup node
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: "lts/*"
           registry-url: "https://registry.npmjs.org"
@@ -36,7 +36,7 @@ jobs:
           cp ../../../LICENSE.txt .
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v12
+        uses: mymindstorm/setup-emsdk@v13
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

.github/workflows/wasm.yml

@@ -24,12 +24,12 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Setup node
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: "lts/*"
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v12
+        uses: mymindstorm/setup-emsdk@v13
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

CMakeLists.txt

@@ -1,8 +1,8 @@
 # Enforce some CMake policies
-cmake_minimum_required(VERSION 3.4)
+cmake_minimum_required(VERSION 3.16)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.12.3.0 LANGUAGES CXX C)
+project(Z3 VERSION 4.12.5.0 LANGUAGES CXX C)
 
 ################################################################################
 # Project version
@@ -41,19 +41,22 @@ list(APPEND CMAKE_MODULE_PATH "${PROJECT_SOURCE_DIR}/cmake/modules")
 ################################################################################
 include(${PROJECT_SOURCE_DIR}/cmake/git_utils.cmake)
 macro(disable_git_describe)
+  if(Z3_INCLUDE_GIT_DESCRIBE)
     message(WARNING "Disabling Z3_INCLUDE_GIT_DESCRIBE")
     set(Z3_INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output" FORCE)
+  endif()
 endmacro()
 macro(disable_git_hash)
+  if(Z3_INCLUDE_GIT_HASH)
     message(WARNING "Disabling Z3_INCLUDE_GIT_HASH")
     set(Z3_INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output" FORCE)
-  unset(Z3GITHASH) # Used in configure_file()
+  endif()
 endmacro()
 option(Z3_INCLUDE_GIT_HASH "Include git hash in version output" ON)
 option(Z3_INCLUDE_GIT_DESCRIBE "Include git describe output in version output" ON)
 
 set(GIT_DIR "${PROJECT_SOURCE_DIR}/.git")
-if (EXISTS "${GIT_DIR}")
+if ((Z3_INCLUDE_GIT_HASH OR Z3_INCLUDE_GIT_HASH) AND EXISTS "${GIT_DIR}")
   # Try to make CMake configure depend on the current git HEAD so that
   # a re-configure is triggered when the HEAD changes.
   add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
@@ -63,13 +66,13 @@ if (EXISTS "${GIT_DIR}")
       if (NOT Z3GITHASH)
         message(WARNING "Failed to get Git hash")
         disable_git_hash()
-      endif()
+      else()
         message(STATUS "Using Git hash in version output: ${Z3GITHASH}")
         # This mimics the behaviour of the old build system.
         set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3GITHASH}")
+      endif()
     else()
       message(STATUS "Not using Git hash in version output")
-      unset(Z3GITHASH) # Used in configure_file()
     endif()
     if (Z3_INCLUDE_GIT_DESCRIBE)
       get_git_head_describe("${GIT_DIR}" Z3_GIT_DESCRIPTION)
@@ -93,6 +96,9 @@ else()
   disable_git_describe()
   disable_git_hash()
 endif()
+if(NOT Z3_INCLUDE_GIT_HASH)
+  unset(Z3GITHASH) # Used in configure_file()
+endif()
 
 ################################################################################
 # Useful CMake functions/Macros
@@ -153,8 +159,8 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEAS
 ################################################################################
 # Find Python
 ################################################################################
-find_package(PythonInterp 3 REQUIRED)
+find_package(Python3 REQUIRED COMPONENTS Interpreter)
-message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
+message(STATUS "Python3_EXECUTABLE: ${Python3_EXECUTABLE}")
 
 ################################################################################
 # Target architecture detection

README-CMake.md

@@ -277,7 +277,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute.
 * ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``).
 * ``CMAKE_INSTALL_API_BINDINGS_DOC`` - STRING. The path to install documentation for API bindings.
-* ``PYTHON_EXECUTABLE`` - STRING. The python executable to use during the build.
+* ``Python3_EXECUTABLE`` - STRING. The python executable to use during the build.
 * ``Z3_ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
 * ``Z3_BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
 * ``Z3_ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
@@ -303,7 +303,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will
     fail on other compilers. This requires Z3_LINK_TIME_OPTIMIZATION to also be enabled.
 * ``Z3_API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
-* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
+* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``ON`` compiler warnings will be treated as errors. If set to ``OFF`` compiler warnings will not be treated as errors.
     If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
 * ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker.
 * ``Z3_BUILD_EXECUTABLE`` - BOOL. If set to ``TRUE`` build the z3 executable. Defaults to ``TRUE`` unless z3 is being built as a submodule in which case it defaults to ``FALSE``.

README.md

@@ -230,6 +230,7 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g
 * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
 * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
 * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html))
+* [Rust](https://github.com/prove-rs/z3.rs)
 * C
 * OCaml
 * [Julia](https://github.com/ahumenberger/Z3.jl)

RELEASE_NOTES.md

@@ -10,9 +10,34 @@ Version 4.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
-Version 4.12.3
+Version 4.12.5
 ==============
 
+Version 4.12.4
+==============
+- Re-release fixing a few issues with 4.12:
+  - Python dependency on importlib.resources vs importlib_resources break automatic pypi installations. Supposedly fixed by conditioning dependency on Python 3.9 where the feature is built-in.
+  - Missing release of arm64 for Ubuntu.
+  - Futile attempt to streamline adding readme.md file as part of Nuget distribution. Nuget.org now requires a readme file. I was able to integrate the readme with the cmake build, but the cross-platform repackage in scripts/mk_nuget_task.py does not ingest a similar readme file with the CI pipelines.
+
+Version 4.12.3
+==============
+- Alpha support for polymorphism.
+  - SMTLIB3-ish, C, Python
+  It adds the new command `(declare-type-var A)` that declares a symbol (in this case `A`) globally as a polymorphic type variable.
+  The C API contains a new function `Z3_mk_type_variable` and a new enumeration case `Z3_TYPE_VAR` as a kind associated with sorts.
+  All occurrences of `A` are treated as type variables. A function declaration whose signature uses `A` is treated as a shorthand
+  for declarations of all functions that use instances of `A`.
+  Assertions that use type variables are shorthands for assertions covering all instantiations.
+- Various (ongoing) performance fixes and improvements to smt.arith.solver=6
+- A working version of solver.proof.trim=true option. Proofs logs created when using sat.smt=true may be trimmed by running z3
+  on the generated proof log using the option solver.proof.trim=true. 
+- Optimizations LIA and NIA (linear integer arithmetic and non-linear integer (and real) arithmetic reasoning).
+  smt.arith.solver=6 is the default for most use cases. It trails smt.arith.solver=2 in some scenarios and the gap has been either removed or reduced.
+  smt.arith.solver=6 is complete for integrations of non-linear real arithmetic and theories, smt.arith.solver=2 is not. 
+- qel: Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.
+- added real-closed fields features to C API, exposed more RCF over OCaml API
+- fixes to FP
 
 Version 4.12.2
 ==============

cmake/z3_add_component.cmake

@@ -116,7 +116,7 @@ macro(z3_add_component component_name)
     set(_full_output_file_path "${CMAKE_CURRENT_BINARY_DIR}/${_output_file}")
     message(STATUS "Adding rule to generate \"${_output_file}\"")
     add_custom_command(OUTPUT "${_output_file}"
-      COMMAND "${PYTHON_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}"
+      COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}"
       MAIN_DEPENDENCY "${_full_pyg_file_path}"
       DEPENDS "${PROJECT_SOURCE_DIR}/scripts/pyg2hpp.py"
               ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
@@ -275,7 +275,7 @@ macro(z3_add_install_tactic_rule)
   string(REPLACE ";" "\n" _tactic_header_files "${_tactic_header_files}")
   file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files})
   add_custom_command(OUTPUT "install_tactic.cpp"
-    COMMAND "${PYTHON_EXECUTABLE}"
+    COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
     "${CMAKE_CURRENT_BINARY_DIR}"
     "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
@@ -313,7 +313,7 @@ macro(z3_add_memory_initializer_rule)
   endforeach()
 
   add_custom_command(OUTPUT "mem_initializer.cpp"
-    COMMAND "${PYTHON_EXECUTABLE}"
+    COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
     "${CMAKE_CURRENT_BINARY_DIR}"
     ${_mem_init_finalize_headers}
@@ -349,7 +349,7 @@ macro(z3_add_gparams_register_modules_rule)
   unset(_component_register_module_header_files)
 
   add_custom_command(OUTPUT "gparams_register_modules.cpp"
-    COMMAND "${PYTHON_EXECUTABLE}"
+    COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
     "${CMAKE_CURRENT_BINARY_DIR}"
     ${_register_module_header_files}

doc/CMakeLists.txt

@@ -58,7 +58,7 @@ endif()
 
 add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
   COMMAND
-  "${PYTHON_EXECUTABLE}" "${MK_API_DOC_SCRIPT}"
+  "${Python3_EXECUTABLE}" "${MK_API_DOC_SCRIPT}"
   --build "${PROJECT_BINARY_DIR}"
   --doxygen-executable "${DOXYGEN_EXECUTABLE}"
   --output-dir "${DOC_DEST_DIR}"

examples/ml/ml_example.ml

@@ -19,7 +19,6 @@ open Z3.Arithmetic.Integer
 open Z3.Arithmetic.Real
 open Z3.BitVector
 
-
 exception TestFailedException of string
 
 (**
@@ -315,6 +314,67 @@ let fpa_example ( ctx : context ) =
 	  Printf.printf "Test passed.\n"
   )
 
+(**
+	A basic example of RCF usage
+**)
+let rcf_example ( ctx : context ) =
+  Printf.printf "RCFExample\n" ;
+  let pi = RCF.mk_pi ctx in
+  let e = RCF.mk_e ctx in
+  let inf0 = RCF.mk_infinitesimal ctx in
+  let inf1 = RCF.mk_infinitesimal ctx in
+  let r = RCF.mk_rational ctx "42.001" in
+  let pi_div_e = RCF.div ctx pi e in
+  let pi_div_r = RCF.div ctx pi r in
+  (Printf.printf "e: %s,  pi: %s, e==pi: %b, e < pi: %b\n"
+    (RCF.num_to_string ctx e true false)
+    (RCF.num_to_string ctx pi true false)
+    (RCF.eq ctx e pi)
+    (RCF.lt ctx e pi)) ;
+  Printf.printf "pi_div_e: %s.\n" (RCF.num_to_string ctx pi_div_e true false);
+  Printf.printf "pi_div_r: %s.\n" (RCF.num_to_string ctx pi_div_r true false);
+  Printf.printf "inf0: %s.\n" (RCF.num_to_string ctx inf0 true false);
+  Printf.printf "(RCF.is_rational ctx pi): %b.\n" (RCF.is_rational ctx pi);
+  Printf.printf "(RCF.is_algebraic ctx pi): %b.\n" (RCF.is_algebraic ctx pi);
+  Printf.printf "(RCF.is_transcendental ctx pi): %b.\n" (RCF.is_transcendental ctx pi);
+  Printf.printf "(RCF.is_rational ctx r): %b.\n" (RCF.is_rational ctx r);
+  Printf.printf "(RCF.is_algebraic ctx r): %b.\n" (RCF.is_algebraic ctx r);
+  Printf.printf "(RCF.is_transcendental ctx r): %b.\n" (RCF.is_transcendental ctx r);
+  Printf.printf "(RCF.is_infinitesimal ctx inf0): %b.\n" (RCF.is_infinitesimal ctx inf0);
+  Printf.printf "(RCF.extension_index ctx inf0): %d.\n" (RCF.extension_index ctx inf0);
+  Printf.printf "(RCF.extension_index ctx inf1): %d.\n" (RCF.extension_index ctx inf1);
+  let poly:RCF.rcf_num list = [ e; pi; inf0 ] in
+  let rs:RCF.root list = RCF.roots ctx poly in
+  let print_root (x:RCF.root) =
+    begin
+    Printf.printf "root: %s\n%!" (RCF.num_to_string ctx x.obj true false);
+    if RCF.is_algebraic ctx x.obj then (
+      (match x.interval with
+      | Some ivl -> Printf.printf "  interval: (%b, %b, %s, %b, %b, %s)\n"
+                                  ivl.lower_is_inf
+                                  ivl.lower_is_open
+                                  (RCF.num_to_string ctx ivl.lower true false)
+                                  ivl.upper_is_inf
+                                  ivl.upper_is_open
+                                  (RCF.num_to_string ctx ivl.upper true false);
+      | None -> ());
+      Printf.printf "  polynomial coefficients:";
+      List.iter (fun c -> Printf.printf " %s" (RCF.num_to_string ctx c false false)) x.polynomial;
+      Printf.printf "\n";
+      Printf.printf "  sign conditions:";
+      List.iter
+        (fun (poly, sign) ->
+          List.iter (fun p -> Printf.printf " %s" (RCF.num_to_string ctx p true false)) poly;
+          Printf.printf " %s" (if sign > 0 then "> 0" else if sign < 0 then "< 0" else "= 0"))
+        x.sign_conditions;
+      Printf.printf "\n")
+    end
+  in
+  List.iter print_root rs;
+  RCF.del_roots ctx rs;
+  RCF.del_list ctx [pi; e; inf0; inf1; r; pi_div_e; pi_div_r];
+  Printf.printf "Test passed.\n"
+
 let _ =
   try (
     if not (Log.open_ "z3.log") then
@@ -340,6 +400,7 @@ let _ =
 	basic_tests ctx ;
 	quantifier_example1 ctx ;
 	fpa_example ctx ;
+  rcf_example ctx ;
 	Printf.printf "Disposing...\n";
 	Gc.full_major ()
       );
@@ -350,3 +411,4 @@ let _ =
     exit 1
   )
 ;;
+

package-lock.json

@@ -1,27 +0,0 @@
-{
-  "requires": true,
-  "lockfileVersion": 1,
-  "dependencies": {
-    "async-mutex": {
-      "version": "0.3.2",
-      "resolved": "https://registry.npmjs.org/async-mutex/-/async-mutex-0.3.2.tgz",
-      "integrity": "sha512-HuTK7E7MT7jZEh1P9GtRW9+aTWiDWWi9InbZ5hjxrnRa39KS4BW04+xLBhYNS2aXhHUIKZSw3gj4Pn1pj+qGAA==",
-      "requires": {
-        "tslib": "^2.3.1"
-      }
-    },
-    "tslib": {
-      "version": "2.4.0",
-      "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.4.0.tgz",
-      "integrity": "sha512-d6xOpEDfsi2CZVlPQzGeux8XMwLT9hssAsaPYExaQMuYskwb+x1x7J371tWlbBdWHroy99KnVB6qIkUbs5X3UQ=="
-    },
-    "z3-solver": {
-      "version": "4.9.0",
-      "resolved": "https://registry.npmjs.org/z3-solver/-/z3-solver-4.9.0.tgz",
-      "integrity": "sha512-clSV0uyHsfrO84pSbHxoqvmd5HgSG4CoSJG2f8U65hBVylbV6p/0svctQWee9W2fWo0IsxHYRjxz2Z85GT0LAA==",
-      "requires": {
-        "async-mutex": "^0.3.2"
-      }
-    }
-  }
-}

scripts/mk_nuget_task.py

@@ -24,14 +24,16 @@ def mk_dir(d):
 os_info = {  'ubuntu-latest' : ('so', 'linux-x64'),
              'ubuntu-18' : ('so', 'linux-x64'),
              'ubuntu-20' : ('so', 'linux-x64'),
-             'glibc' : ('so', 'linux-x64'),
+             'x64-glibc-2.35' : ('so', 'linux-x64'),
-             #'glibc-2.35' : ('so', 'linux-x64'),
              'x64-win' : ('dll', 'win-x64'),
              'x86-win' : ('dll', 'win-x86'),
              'x64-osx' : ('dylib', 'osx-x64'),
-             'arm64-osx' : ('dylib', 'osx-arm64'),
              'debian' : ('so', 'linux-x64') }
 
+# Nuget not supported for ARM
+#'arm-glibc-2.35' : ('so', 'linux-arm64'),
+#'arm64-osx' : ('dylib', 'osx-arm64'),
+
         
 
 def classify_package(f, arch):
@@ -87,6 +89,11 @@ def mk_icon(source_root):
     mk_dir("out/content")
     shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
 
+def mk_readme(source_root):
+    mk_dir("out/content")
+    shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/README.md")
+
+
     
 def create_nuget_spec(version, repo, branch, commit, symbols, arch):
     arch = f".{arch}" if arch == "x86" else ""
@@ -142,6 +149,7 @@ class Env:
         unpack(self.packages, self.symbols, self.arch)
         mk_targets(self.source_root)
         mk_icon(self.source_root)
+#       mk_readme(self.source_root)
         create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch)
         
 def main():

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 12, 3, 0) # express a default build version or pick up ci build version
+    set_version(4, 12, 5, 0) # express a default build version or pick up ci build version
     
 # Z3 Project definition
 def init_project_def():

scripts/mk_util.py

@@ -1736,6 +1736,7 @@ class DotNetDLLComponent(Component):
     <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
     <Authors>Microsoft</Authors>
     <Company>Microsoft</Company>
+    <PackageReadmeFile>README.md</PackageReadmeFile>
     <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
     <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
     <Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
@@ -1745,9 +1746,10 @@ class DotNetDLLComponent(Component):
 
   <ItemGroup>
     <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
+    <None Include="..\%s\README.md" Pack="true" PackagePath="/"/>
   </ItemGroup>
 
-</Project>""" % (version, key, self.to_src_dir)
+</Project>""" % (version, key, self.to_src_dir, self.to_src_dir)
 
         mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
         csproj = os.path.join('dotnet', 'z3.csproj')
@@ -2519,19 +2521,19 @@ def mk_config():
                 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
+                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
+                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
         else:
             # Windows Release mode
             LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
@@ -2544,19 +2546,19 @@ def mk_config():
                 extra_opt = '%s /D _TRACE ' % extra_opt
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c%s %s /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
+                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
-                    'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
+                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/c%s %s /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
+                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
 
         config.write('CFLAGS=$(CXXFLAGS)\n')
 
@@ -2664,7 +2666,7 @@ def mk_config():
             LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
         if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
             CXXFLAGS = '%s -fpic' % CXXFLAGS
-        if IS_OSX and IS_ARCH_ARM64:
+        if IS_ARCH_ARM64 and IS_OSX:
             print("Setting arm64")
             CXXFLAGS = '%s -arch arm64' % CXXFLAGS
             LDFLAGS = '%s -arch arm64' % LDFLAGS

scripts/nightly.yaml

@@ -1,7 +1,7 @@
 variables:
   Major: '4'
   Minor: '12'
-  Patch: '3'
+  Patch: '5'
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
 
@@ -63,11 +63,29 @@ stages:
         artifactName: 'Ubuntu'
         targetPath: $(Build.ArtifactStagingDirectory)
 
+  - job: UbuntuArm64
+    displayName: "Ubuntu ARM64 build"
+    pool:
+      vmImage: "ubuntu-latest"
+    steps:
+    - script: sudo apt update
+    - script: sudo apt install gcc-arm-none-eabi -y
+    - script: sudo apt install gcc-arm-linux-gnueabihf -y
+    - script: sudo apt install gcc-aarch64-linux-gnu -y
+    - script: sudo apt install g++-aarch64-linux-gnu -y
+    - script: CXX=aarch64-linux-gnu-g++ CC=aarch64-linux-gnu-gcc python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
+    - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'UbuntuArm64'
+        targetPath: $(Build.ArtifactStagingDirectory)
+
   - job: UbuntuDoc
     displayName: "Ubuntu Doc build"
     pool:
       vmImage: "ubuntu-latest"
     steps:
+    - script: pip3 install importlib-resources
     - script: sudo apt-get install ocaml opam libgmp-dev
     - script: opam init -y
     - script: eval `opam config env`; opam install zarith ocamlfind -y
@@ -86,8 +104,8 @@ stages:
         set -e
         eval `opam config env` 
         cd doc
-        python mk_api_doc.py --mld --z3py-package-path=../build/python/z3
+        python3 mk_api_doc.py --mld --z3py-package-path=../build/python/z3
-        python mk_params_doc.py 
+        python3 mk_params_doc.py 
         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 ..
@@ -238,6 +256,16 @@ stages:
       inputs:
         artifact: 'Ubuntu'
         path: $(Agent.TempDirectory)\package
+    - task: DownloadPipelineArtifact@2
+      displayName: 'Download Ubuntu 20.04 Build'
+      inputs:
+        artifact: 'Ubuntu-20.04'
+        path: $(Agent.TempDirectory)\package
+    - task: DownloadPipelineArtifact@2
+      displayName: 'Download Ubuntu ARM64 Build'
+      inputs:
+        artifact: 'UbuntuArm64'
+        path: $(Agent.TempDirectory)\package
     - task: DownloadPipelineArtifact@2
       displayName: 'Download macOS Build'
       inputs:
@@ -521,6 +549,11 @@ stages:
       inputs:
         artifactName: 'MacArm64'
         targetPath: tmp
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download Ubuntu Arm64"
+      inputs:
+        artifactName: 'UbuntuArm64'
+        targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download Ubuntu"
       inputs:

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.12.3'
+  ReleaseVersion: '4.12.5'
 
 stages:
 
@@ -114,11 +114,26 @@ stages:
         artifactName: 'UbuntuBuild20'
         targetPath: $(Build.ArtifactStagingDirectory)
 
+  - job: UbuntuArm64
+    displayName: "Ubuntu ARM64 build"
+    pool:
+      vmImage: "ubuntu-latest"
+    steps:
+    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
+    - script: git clone https://github.com/z3prover/z3test z3test
+    - script: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2    
+    - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'UbuntuArm64'
+        targetPath: $(Build.ArtifactStagingDirectory)
+
   - job: UbuntuDoc
     displayName: "Ubuntu Doc build"
     pool:
       vmImage: "ubuntu-latest"
     steps:
+    - script: pip3 install importlib-resources
     - script: sudo apt-get install ocaml opam libgmp-dev
     - script: opam init -y
     - script: eval `opam config env`; opam install zarith ocamlfind -y
@@ -137,8 +152,8 @@ stages:
         set -e
         eval `opam config env` 
         cd doc
-        python mk_api_doc.py --mld --z3py-package-path=../build/python/z3
+        python3 mk_api_doc.py --mld --z3py-package-path=../build/python/z3
-        python mk_params_doc.py 
+        python3 mk_params_doc.py 
         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 ..
@@ -225,6 +240,11 @@ stages:
       inputs:
         artifact: 'UbuntuBuild20'
         path: $(Agent.TempDirectory)\package
+    - task: DownloadPipelineArtifact@2
+      displayName: 'Download Ubuntu ARM64 Build'
+      inputs:
+        artifact: 'UbuntuArm64'
+        path: $(Agent.TempDirectory)\package	
     - task: DownloadPipelineArtifact@2
       displayName: 'Download macOS Build'
       inputs:
@@ -480,6 +500,11 @@ stages:
       inputs:
         artifact: 'UbuntuBuild'
         path: $(Agent.TempDirectory)
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download Ubuntu Arm64"
+      inputs:
+        artifactName: 'UbuntuArm64'
+        path: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       displayName: "Download Doc"
       inputs:

scripts/test-java-cmake.yml

@@ -3,7 +3,7 @@ steps:
     cd build
     mkdir -p examples/java
     cp ../examples/java/JavaExample.java examples/java/
-    javac examples/java/Javaexamplejava -classpath com.microsoft.z3.jar
+    javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar
     export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
     java -cp .:examples/java:com.microsoft.z3.jar JavaExample
     cd ..

scripts/update_api.py

@@ -1,4 +1,4 @@
-#  - !/usr/bin/env python
+#!/usr/bin/env python
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
 #
@@ -426,6 +426,7 @@ def mk_dotnet(dotnet):
     dotnet.write('    {\n\n')
 
     for name, ret, sig in Closures:
+        sig = sig.replace("unsigned const*","uint[]")
         sig = sig.replace("void*","voidp").replace("unsigned","uint")
         sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
         ret = ret.replace("void*","voidp").replace("unsigned","uint")        
@@ -1826,17 +1827,28 @@ def write_core_py_preamble(core_py):
   core_py.write(
 """
 # Automatically generated file
+import atexit
 import sys, os
+import contextlib
 import ctypes
-import pkg_resources
+if sys.version_info >= (3, 9):
+    import importlib.resources as importlib_resources
+else:
+    import importlib_resources
 from .z3types import *
 from .z3consts import *
 
+_file_manager = contextlib.ExitStack()
+atexit.register(_file_manager.close)
 _ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
 _lib = None
+_z3_lib_resource = importlib_resources.files('z3').joinpath('lib')
+_z3_lib_resource_path = _file_manager.enter_context(
+    importlib_resources.as_file(_z3_lib_resource)
+)
 _default_dirs = ['.',
                  os.path.dirname(os.path.abspath(__file__)),
-                 pkg_resources.resource_filename('z3', 'lib'),
+                 _z3_lib_resource_path,
                  os.path.join(sys.prefix, 'lib'),
                  None]
 _all_dirs = []
@@ -1886,10 +1898,10 @@ if _lib is None:
   print("  - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
   if sys.version < '3':
     print("    import __builtin__")
-    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
   else:
     print("    import builtins")
-    print("    builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
   print(_failures)
   raise Z3Exception("libz3.%s not found." % _ext)
 
@@ -1919,7 +1931,7 @@ _error_handler_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
 _lib.Z3_set_error_handler.restype  = None
 _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
-Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
+Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.POINTER(ctypes.c_uint), ctypes.c_void_p)
 Z3_push_eh  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
 Z3_pop_eh   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
 Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)

src/CMakeLists.txt

@@ -220,7 +220,7 @@ if (MSVC)
   set(dll_module_exports_file "${CMAKE_CURRENT_BINARY_DIR}/api_dll.def")
   add_custom_command(OUTPUT "${dll_module_exports_file}"
     COMMAND
-      "${PYTHON_EXECUTABLE}"
+      "${Python3_EXECUTABLE}"
       "${PROJECT_SOURCE_DIR}/scripts/mk_def_file.py"
       "${dll_module_exports_file}"
       "libz3"

src/ackermannization/ackr_helper.h

@@ -18,6 +18,7 @@
 
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
+#include "ast/ast_ll_pp.h"
 
 class ackr_helper {
 public:
@@ -40,11 +41,9 @@ public:
     inline bool is_uninterp_fn(app const * a) const {
         if (is_uninterp(a))
             return true;
-        else {
         decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
         return p->is_considered_uninterpreted(a->get_decl());        
     }
-    }
 
     /**
        \brief determines if a term is a candidate select for Ackerman reduction
@@ -64,11 +63,10 @@ public:
             }
         }
         else {
-            for (expr* arg : *a) {
+            for (expr* arg : *a) 
                 non_select.mark(arg, true);
         }
     }
-    }
 
     void prune_non_select(obj_map<app, app_set*> & sels, expr_mark& non_select) {
         ptr_vector<app> nons;
@@ -112,7 +110,8 @@ public:
     }
 
     void insert(fun2terms_map& f2t, sel2terms_map& s2t, app* a) {
-        if (a->get_num_args() == 0) return;
+        if (a->get_num_args() == 0)
+            return;
         ast_manager& m = m_bvutil.get_manager();
         app_set* ts = nullptr;
         bool is_const_args = true;
@@ -129,22 +128,19 @@ public:
                 ts = alloc(app_set);
                 f2t.insert(fd, ts);
             }
-            is_const_args = m.is_value(a->get_arg(0));
+            is_const_args = m.is_unique_value(a->get_arg(0));
         }
-        else {
+        else 
             return;
-        }
-        for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) {
-            is_const_args &= m.is_value(a->get_arg(i));
-        }
         
-        if (is_const_args) {
+        for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) 
+            is_const_args &= m.is_unique_value(a->get_arg(i));
+        
+        if (is_const_args) 
             ts->const_args.insert(a);
-        }
+        else 
-        else {
             ts->var_args.insert(a);
     }
-    }
     
 private:
     bv_util                              m_bvutil;

src/ackermannization/lackr.cpp

@@ -22,6 +22,8 @@
 #include "ackermannization/ackr_info.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_util.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "model/model_smt2_pp.h"
 
 lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
@@ -143,9 +145,9 @@ bool lackr::ackr(app * const t1, app * const t2) {
 //
 void lackr::eager_enc() {
     TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << " #sels: " << m_sel2terms.size() << std::endl;);
-    for (auto const& kv : m_fun2terms) {
+    for (auto const& [k,v] : m_fun2terms) {
         checkpoint();
-        ackr(kv.get_value());
+        ackr(v);
     }
     for (auto const& kv : m_sel2terms) {
         checkpoint();
@@ -172,14 +174,13 @@ void lackr::ackr(app_set const* ts) {
 }
 
 void lackr::abstract_fun(fun2terms_map const& apps) {
-    for (auto const& kv : apps) {
+    for (auto const& [fd, v] : apps) {
-        func_decl* fd = kv.m_key;
+        for (app * t : v->var_args) {
-        for (app * t : kv.m_value->var_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
         }
-        for (app * t : kv.m_value->const_args) {
+        for (app * t : v->const_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);

src/api/CMakeLists.txt

@@ -18,7 +18,7 @@ foreach (gen_file ${generated_files})
 endforeach()
 
 add_custom_command(OUTPUT ${generated_files}
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
   "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
   ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
   "--api_output_dir"

src/api/api_ast.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/polymorphism_util.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/expr_safe_replace.h"
@@ -88,6 +89,16 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol name) {
+        Z3_TRY;
+        LOG_Z3_mk_type_variable(c, name);
+        RESET_ERROR_CODE();
+        sort* ty = mk_c(c)->m().mk_type_var(to_symbol(name));
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast s1, Z3_ast s2) {
         RESET_ERROR_CODE();
         return s1 == s2;
@@ -180,7 +191,20 @@ extern "C" {
             arg_list.push_back(to_expr(args[i]));
         }
         func_decl* _d = reinterpret_cast<func_decl*>(d);
-        app* a = mk_c(c)->m().mk_app(_d, num_args, arg_list.data());
+        ast_manager& m = mk_c(c)->m();
+        if (_d->is_polymorphic()) {
+            polymorphism::util u(m);
+            polymorphism::substitution sub(m);
+            ptr_buffer<sort> domain;
+            for (unsigned i = 0; i < num_args; ++i) {
+                if (!sub.match(_d->get_domain(i), arg_list[i]->get_sort())) 
+                    SET_ERROR_CODE(Z3_INVALID_ARG, "failed to match argument of polymorphic function");
+                domain.push_back(arg_list[i]->get_sort());
+            }
+            sort_ref range = sub(_d->get_range());
+            _d = m.instantiate_polymorphic(_d, num_args, domain.data(), range);
+        }
+        app* a = m.mk_app(_d, num_args, arg_list.data());
         mk_c(c)->save_ast_trail(a);
         check_sorts(c, a);
         RETURN_Z3(of_ast(a));
@@ -728,6 +752,9 @@ extern "C" {
         else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) {
             return Z3_CHAR_SORT;
         }
+        else if (fid == poly_family_id) {
+            return Z3_TYPE_VAR;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }

src/api/api_bv.cpp

@@ -227,6 +227,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
     Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         RESET_ERROR_CODE();
+        // l1 := t1 <s 0
+        // l2 := t2 <s 0
+        // l1 & l2 => t1 + t2 <s 0
         Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
         Z3_inc_ref(c, zero);
         Z3_ast r = Z3_mk_bvadd(c, t1, t2);
@@ -255,6 +258,10 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
     Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         RESET_ERROR_CODE();
+        // x := t2 = min_int
+        // y := t1 <s 0
+        // z := no_overflow(t1 + -t2)
+        // if x y z
         Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
         Z3_inc_ref(c, minus_t2);
         Z3_sort s = Z3_get_sort(c, t2);
@@ -284,6 +291,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_TRY;
         RESET_ERROR_CODE();
         if (is_signed) {
+            // x := 0 <s -t2
+            // y := no_underflow(x + -t2)
+            // x => y
             Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
             Z3_inc_ref(c, zero);
             Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);

src/api/api_context.cpp

@@ -78,6 +78,11 @@ namespace api {
             m().dec_ref(a);
     }
 
+    // flush_objects can only be called in the main thread.
+    // This ensures that the calls to m().dec_ref() and dealloc(o)
+    // only happens in the main thread.
+    // Calls to dec_ref are allowed in other threads when m_concurrent_dec_ref is
+    // set to true.
     void context::flush_objects() {
 #ifndef SINGLE_THREAD
         if (!m_concurrent_dec_ref)
@@ -157,6 +162,9 @@ namespace api {
         flush_objects();
         for (auto& kv : m_allocated_objects) {
             api::object* val = kv.m_value;
+#ifdef SINGLE_THREAD
+# define m_concurrent_dec_ref false
+#endif
             DEBUG_CODE(if (!m_concurrent_dec_ref) warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
             dealloc(val);
         }

src/api/api_datatype.cpp

@@ -241,6 +241,20 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    unsigned Z3_API Z3_constructor_num_fields(Z3_context c, Z3_constructor constr) {
+        Z3_TRY;
+        LOG_Z3_constructor_num_fields(c, constr);
+        RESET_ERROR_CODE();
+        mk_c(c)->reset_last_result();
+        if (!constr) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            return 0;
+        }
+        constructor* c = reinterpret_cast<constructor*>(constr);
+        return c->m_field_names.size();
+        Z3_CATCH_RETURN(0);
+    }
+
 
     void Z3_API Z3_query_constructor(Z3_context c,
                                      Z3_constructor constr,

src/api/api_numeral.cpp

@@ -29,13 +29,12 @@ bool is_numeral_sort(Z3_context c, Z3_sort ty) {
     if (!ty) return false;
     sort * _ty = to_sort(ty);
     family_id fid  = _ty->get_family_id();
-    if (fid != mk_c(c)->get_arith_fid() &&
+    return 
-        fid != mk_c(c)->get_bv_fid() &&
+        fid == mk_c(c)->get_arith_fid() ||
-        fid != mk_c(c)->get_datalog_fid() &&
+        fid == mk_c(c)->get_bv_fid() ||
-        fid != mk_c(c)->get_fpa_fid()) {
+        fid == mk_c(c)->get_datalog_fid() ||
-        return false;
+        fid == mk_c(c)->get_fpa_fid();
-    }
+
-    return true;
 }
 
 static bool check_numeral_sort(Z3_context c, Z3_sort ty) {
@@ -152,7 +151,7 @@ extern "C" {
             mk_c(c)->bvutil().is_numeral(e) ||
             mk_c(c)->fpautil().is_numeral(e) ||
             mk_c(c)->fpautil().is_rm_numeral(e) ||
-            mk_c(c)->datalog_util().is_numeral_ext(e);
+            mk_c(c)->datalog_util().is_numeral(e);
         Z3_CATCH_RETURN(false);
     }
 

src/api/api_quant.cpp

@@ -383,6 +383,36 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_get_quantifier_skolem_id(c, a);
+        RESET_ERROR_CODE();
+        ast * _a = to_ast(a);
+        if (_a->get_kind() == AST_QUANTIFIER) {
+            return of_symbol(to_quantifier(_a)->get_skid());
+        }
+        else {
+            SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
+            return of_symbol(symbol::null);
+        }
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
+    }
+
+    Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_get_quantifier_skolem_id(c, a);
+        RESET_ERROR_CODE();
+        ast * _a = to_ast(a);
+        if (_a->get_kind() == AST_QUANTIFIER) {
+            return of_symbol(to_quantifier(_a)->get_qid());
+        }
+        else {
+            SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
+            return of_symbol(symbol::null);
+        }
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
+    }
+
     unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_get_quantifier_num_patterns(c, a);

src/api/api_rcf.cpp

@@ -302,4 +302,139 @@ extern "C" {
         Z3_CATCH;
     }
 
+    bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_is_rational(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).is_rational(to_rcnumeral(a));
+        Z3_CATCH_RETURN(false);
+    }
+
+    bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_is_algebraic(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).is_algebraic(to_rcnumeral(a));
+        Z3_CATCH_RETURN(false);
+    }
+
+    bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_is_infinitesimal(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).is_infinitesimal(to_rcnumeral(a));
+        Z3_CATCH_RETURN(false);
+    }
+
+    bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_is_transcendental(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).is_transcendental(to_rcnumeral(a));
+        Z3_CATCH_RETURN(false);
+    }
+
+    unsigned Z3_API Z3_rcf_extension_index(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_extension_index(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).extension_index(to_rcnumeral(a));
+        Z3_CATCH_RETURN(false);
+    }
+
+    Z3_symbol Z3_API Z3_rcf_transcendental_name(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_transcendental_name(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return of_symbol(rcfm(c).transcendental_name(to_rcnumeral(a)));
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
+    }
+
+    Z3_symbol Z3_API Z3_rcf_infinitesimal_name(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_infinitesimal_name(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return of_symbol(rcfm(c).infinitesimal_name(to_rcnumeral(a)));
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
+    }
+
+    unsigned Z3_API Z3_rcf_num_coefficients(Z3_context c, Z3_rcf_num a)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_num_coefficients(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).num_coefficients(to_rcnumeral(a));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_rcf_num Z3_API Z3_rcf_coefficient(Z3_context c, Z3_rcf_num a, unsigned i)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_coefficient(c, a, i);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return from_rcnumeral(rcfm(c).get_coefficient(to_rcnumeral(a), i));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper) {
+        Z3_TRY;
+        LOG_Z3_rcf_interval(c, a, lower_is_inf, lower_is_open, lower, upper_is_inf, upper_is_open, upper);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        rcnumeral r_lower, r_upper;
+        bool r = rcfm(c).get_interval(to_rcnumeral(a), *lower_is_inf, *lower_is_open, r_lower, *upper_is_inf, *upper_is_open, r_upper);
+        *lower = from_rcnumeral(r_lower);
+        *upper = from_rcnumeral(r_upper);
+        return r;
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_rcf_num_sign_conditions(Z3_context c, Z3_rcf_num a)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_num_sign_conditions(c, a);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).num_sign_conditions(to_rcnumeral(a));
+        Z3_CATCH_RETURN(0);
+    }
+
+    int Z3_API Z3_rcf_sign_condition_sign(Z3_context c, Z3_rcf_num a, unsigned i)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_sign_condition_sign(c, a, i);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).get_sign_condition_sign(to_rcnumeral(a), i);
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_rcf_num_sign_condition_coefficients(Z3_context c, Z3_rcf_num a, unsigned i)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_num_sign_condition_coefficients(c, a, i);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return rcfm(c).num_sign_condition_coefficients(to_rcnumeral(a), i);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_rcf_num Z3_API Z3_rcf_sign_condition_coefficient(Z3_context c, Z3_rcf_num a, unsigned i, unsigned j)
+    {
+        Z3_TRY;
+        LOG_Z3_rcf_sign_condition_coefficient(c, a, i, j);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        return from_rcnumeral(rcfm(c).get_sign_condition_coefficient(to_rcnumeral(a), i, j));
+        Z3_CATCH_RETURN(nullptr);
+    }
 };

src/api/api_solver.cpp

@@ -984,14 +984,14 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);     
-        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned n, expr* const* _literals) {
+        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned nd, unsigned const* deps, unsigned n, expr* const* _literals) {
             Z3_ast_vector_ref * literals = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
             mk_c(c)->save_object(literals);
             expr_ref pr(proof, mk_c(c)->m());
             scoped_ast_vector _sc(literals);
             for (unsigned i = 0; i < n; ++i)
                 literals->m_ast_vector.push_back(_literals[i]);
-            on_clause_eh(user_ctx, of_expr(pr.get()), of_ast_vector(literals));
+            on_clause_eh(user_ctx, of_expr(pr.get()), nd, deps, of_ast_vector(literals));
         };
         to_solver_ref(s)->register_on_clause(user_context, _on_clause);
         auto& solver = *to_solver(s);

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

@@ -368,7 +368,7 @@ namespace z3 {
         func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
 
         /**
-         * \brief add function definition body to declaration decl. decl needs to be declared using context::<recfun>.
+         * \brief add function definition body to declaration decl. decl needs to be declared using context::recfun.
          * @param decl
          * @param args
          * @param body
@@ -4214,17 +4214,20 @@ namespace z3 {
         return expr(ctx(), r);
     }
 
-    typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t;
+    typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t;
 
     class on_clause {
         context& c;
         on_clause_eh_t m_on_clause;
 
-        static void _on_clause_eh(void* _ctx, Z3_ast _proof, Z3_ast_vector _literals) {
+        static void _on_clause_eh(void* _ctx, Z3_ast _proof, unsigned n, unsigned const* dep, Z3_ast_vector _literals) {
             on_clause* ctx = static_cast<on_clause*>(_ctx);
             expr_vector lits(ctx->c, _literals);
             expr proof(ctx->c, _proof);
-            ctx->m_on_clause(proof, lits);
+            std::vector<unsigned> deps;
+            for (unsigned i = 0; i < n; ++i)
+                deps.push_back(dep[i]);
+            ctx->m_on_clause(proof, deps, lits);
         }
     public:
         on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {

src/api/dotnet/CMakeLists.txt

@@ -9,7 +9,7 @@ set(VER_TWEAK "${Z3_VERSION_TWEAK}")
 # Generate Native.cs
 set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
 add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--dotnet-output-dir"
@@ -25,7 +25,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
 # Generate Enumerations.cs
 set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs")
 add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--dotnet-output-dir"

src/api/dotnet/Constructor.cs

@@ -91,8 +91,14 @@ namespace Microsoft.Z3
         /// </summary>
         ~Constructor()
         {
+	    if (Context.nCtx != IntPtr.Zero) {
+               lock (Context) 
+	       { 
+                   if (Context.nCtx != IntPtr.Zero) 
                        Native.Z3_del_constructor(Context.nCtx, NativeObject);
                }
+            }
+        }        
 
         #region Internal
         private uint n = 0;

src/api/dotnet/Microsoft.Z3.csproj.in

@@ -7,6 +7,8 @@
     <AssemblyName>Microsoft.Z3</AssemblyName>
     <RootNamespace>Microsoft.Z3</RootNamespace>
 
+    <PackageReadmeFile>README.md</PackageReadmeFile>
+
     <Title>Z3 .NET Interface</Title>
     <AssemblyTitle>Z3 .NET Interface</AssemblyTitle>
 
@@ -15,8 +17,8 @@
     <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
     <AssemblyDescription>.NET Interface to the Z3 Theorem Prover</AssemblyDescription>
 
-    <Copyright>Copyright (C) 2006-2019 Microsoft Corporation</Copyright>
+    <Copyright>Copyright (C) 2006- Microsoft Corporation</Copyright>
-    <AssemblyCopyright>Copyright (C) 2006-2019 Microsoft Corporation</AssemblyCopyright>
+    <AssemblyCopyright>Copyright (C) 2006- Microsoft Corporation</AssemblyCopyright>
 
     <Company>Microsoft Corporation</Company>
     <AssemblyCompany>Microsoft Corporation</AssemblyCompany>
@@ -65,6 +67,11 @@
 ${Z3_DOTNET_COMPILE_ITEMS}
   </ItemGroup>
 
+  <!-- Readme -->
+  <ItemGroup>
+  <None Include="${CMAKE_CURRENT_LIST_DIR}/README.md" Pack="true" PackagePath="\"/>
+  </ItemGroup>
+
   <!-- Legacy .NET framework native library helper routines  -->
   <ItemGroup>
     <Content Include="${CMAKE_CURRENT_LIST_DIR}/Microsoft.Z3.props">

src/api/dotnet/OnClause.cs

@@ -30,6 +30,7 @@ namespace Microsoft.Z3
     using Z3_context = System.IntPtr;
     using Z3_solver = System.IntPtr;
     using voidp = System.IntPtr;
+    using uintp = System.IntPtr;
     using Z3_ast = System.IntPtr;
     using Z3_ast_vector = System.IntPtr;
 
@@ -60,7 +61,7 @@ namespace Microsoft.Z3
 
         Native.Z3_on_clause_eh on_clause_eh;
 
-	static void _on_clause(voidp ctx, Z3_ast _proof_hint, Z3_ast_vector _clause) 
+	static void _on_clause(voidp ctx, Z3_ast _proof_hint, uint n, uint[] deps, Z3_ast_vector _clause) 
         {
              var onc = (OnClause)GCHandle.FromIntPtr(ctx).Target;
              using var proof_hint = Expr.Create(onc.ctx, _proof_hint);

src/api/dotnet/Optimize.cs

@@ -220,7 +220,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Check satisfiability of asserted constraints.
         /// Produce a model that (when the objectives are bounded and 
-        /// don't use strict inequalities) meets the objectives.
+        /// don't use strict inequalities) is optimal.
         /// </summary>
         ///
         public Status Check(params Expr[] assumptions)

src/api/dotnet/README.md

@@ -0,0 +1,3 @@
+# Z3 Nuget Package
+
+For more information see [the Z3 github page](https://github.com/z3prover/z3.git)

src/api/java/CMakeLists.txt

@@ -16,7 +16,7 @@ set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
 set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
 set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
 add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--java-input-dir"
@@ -74,7 +74,7 @@ foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
   )
 endforeach()
 add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--java-output-dir"

src/api/java/Optimize.java

@@ -193,7 +193,7 @@ public class Optimize extends Z3Object {
     /**
      * Check satisfiability of asserted constraints.
      * Produce a model that (when the objectives are bounded and 
-     * don't use strict inequalities) meets the objectives.
+     * don't use strict inequalities) is optimal.
      **/
     public Status Check(Expr<BoolSort>... assumptions)
     {

src/api/js/package-lock.json

@@ -1,7 +1,8 @@
 {
   "name": "z3-solver",
-  "requires": true,
+  "version": "0.1.0",
   "lockfileVersion": 1,
+  "requires": true,
   "dependencies": {
     "@ampproject/remapping": {
       "version": "2.2.0",
@@ -109,25 +110,6 @@
       "integrity": "sha512-3r/aACDJ3fhQ/EVgFy0hpj8oHyHpQc+LPtJoY9SzTThAsStm4Ptegq92vqKoE3vD706ZVFWITnMnxucw+S9Ipg==",
       "dev": true
     },
-    "@babel/helper-function-name": {
-      "version": "7.19.0",
-      "resolved": "https://registry.npmjs.org/@babel/helper-function-name/-/helper-function-name-7.19.0.tgz",
-      "integrity": "sha512-WAwHBINyrpqywkUH0nTnNgI5ina5TFn85HKS0pbPDfxFfhyR/aNQEn4hGi1P1JyT//I0t4OgXUlofzWILRvS5w==",
-      "dev": true,
-      "requires": {
-        "@babel/template": "^7.18.10",
-        "@babel/types": "^7.19.0"
-      }
-    },
-    "@babel/helper-hoist-variables": {
-      "version": "7.18.6",
-      "resolved": "https://registry.npmjs.org/@babel/helper-hoist-variables/-/helper-hoist-variables-7.18.6.tgz",
-      "integrity": "sha512-UlJQPkFqFULIcyW5sbzgbkxn2FKRgwWiRexcuaR8RNJRy8+LLveqPjwZV/bwrLZCN0eUHD/x8D0heK1ozuoo6Q==",
-      "dev": true,
-      "requires": {
-        "@babel/types": "^7.18.6"
-      }
-    },
     "@babel/helper-module-imports": {
       "version": "7.18.6",
       "resolved": "https://registry.npmjs.org/@babel/helper-module-imports/-/helper-module-imports-7.18.6.tgz",
@@ -361,21 +343,141 @@
       }
     },
     "@babel/traverse": {
-      "version": "7.19.4",
+      "version": "7.23.2",
-      "resolved": "https://registry.npmjs.org/@babel/traverse/-/traverse-7.19.4.tgz",
+      "resolved": "https://registry.npmjs.org/@babel/traverse/-/traverse-7.23.2.tgz",
-      "integrity": "sha512-w3K1i+V5u2aJUOXBFFC5pveFLmtq1s3qcdDNC2qRI6WPBQIDaKFqXxDEqDO/h1dQ3HjsZoZMyIy6jGLq0xtw+g==",
+      "integrity": "sha512-azpe59SQ48qG6nu2CzcMLbxUudtN+dOM9kDbUqGq3HXUJRlo7i8fvPoxQUzYgLZ4cMVmuZgm8vvBpNeRhd6XSw==",
       "dev": true,
       "requires": {
-        "@babel/code-frame": "^7.18.6",
+        "@babel/code-frame": "^7.22.13",
-        "@babel/generator": "^7.19.4",
+        "@babel/generator": "^7.23.0",
-        "@babel/helper-environment-visitor": "^7.18.9",
+        "@babel/helper-environment-visitor": "^7.22.20",
-        "@babel/helper-function-name": "^7.19.0",
+        "@babel/helper-function-name": "^7.23.0",
-        "@babel/helper-hoist-variables": "^7.18.6",
+        "@babel/helper-hoist-variables": "^7.22.5",
-        "@babel/helper-split-export-declaration": "^7.18.6",
+        "@babel/helper-split-export-declaration": "^7.22.6",
-        "@babel/parser": "^7.19.4",
+        "@babel/parser": "^7.23.0",
-        "@babel/types": "^7.19.4",
+        "@babel/types": "^7.23.0",
         "debug": "^4.1.0",
         "globals": "^11.1.0"
+      },
+      "dependencies": {
+        "@babel/code-frame": {
+          "version": "7.22.13",
+          "resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.22.13.tgz",
+          "integrity": "sha512-XktuhWlJ5g+3TJXc5upd9Ks1HutSArik6jf2eAjYFyIOf4ej3RN+184cZbzDvbPnuTJIUhPKKJE3cIsYTiAT3w==",
+          "dev": true,
+          "requires": {
+            "@babel/highlight": "^7.22.13",
+            "chalk": "^2.4.2"
+          }
+        },
+        "@babel/generator": {
+          "version": "7.23.0",
+          "resolved": "https://registry.npmjs.org/@babel/generator/-/generator-7.23.0.tgz",
+          "integrity": "sha512-lN85QRR+5IbYrMWM6Y4pE/noaQtg4pNiqeNGX60eqOfo6gtEj6uw/JagelB8vVztSd7R6M5n1+PQkDbHbBRU4g==",
+          "dev": true,
+          "requires": {
+            "@babel/types": "^7.23.0",
+            "@jridgewell/gen-mapping": "^0.3.2",
+            "@jridgewell/trace-mapping": "^0.3.17",
+            "jsesc": "^2.5.1"
+          }
+        },
+        "@babel/helper-environment-visitor": {
+          "version": "7.22.20",
+          "resolved": "https://registry.npmjs.org/@babel/helper-environment-visitor/-/helper-environment-visitor-7.22.20.tgz",
+          "integrity": "sha512-zfedSIzFhat/gFhWfHtgWvlec0nqB9YEIVrpuwjruLlXfUSnA8cJB0miHKwqDnQ7d32aKo2xt88/xZptwxbfhA==",
+          "dev": true
+        },
+        "@babel/helper-function-name": {
+          "version": "7.23.0",
+          "resolved": "https://registry.npmjs.org/@babel/helper-function-name/-/helper-function-name-7.23.0.tgz",
+          "integrity": "sha512-OErEqsrxjZTJciZ4Oo+eoZqeW9UIiOcuYKRJA4ZAgV9myA+pOXhhmpfNCKjEH/auVfEYVFJ6y1Tc4r0eIApqiw==",
+          "dev": true,
+          "requires": {
+            "@babel/template": "^7.22.15",
+            "@babel/types": "^7.23.0"
+          }
+        },
+        "@babel/helper-hoist-variables": {
+          "version": "7.22.5",
+          "resolved": "https://registry.npmjs.org/@babel/helper-hoist-variables/-/helper-hoist-variables-7.22.5.tgz",
+          "integrity": "sha512-wGjk9QZVzvknA6yKIUURb8zY3grXCcOZt+/7Wcy8O2uctxhplmUPkOdlgoNhmdVee2c92JXbf1xpMtVNbfoxRw==",
+          "dev": true,
+          "requires": {
+            "@babel/types": "^7.22.5"
+          }
+        },
+        "@babel/helper-split-export-declaration": {
+          "version": "7.22.6",
+          "resolved": "https://registry.npmjs.org/@babel/helper-split-export-declaration/-/helper-split-export-declaration-7.22.6.tgz",
+          "integrity": "sha512-AsUnxuLhRYsisFiaJwvp1QF+I3KjD5FOxut14q/GzovUe6orHLesW2C7d754kRm53h5gqrz6sFl6sxc4BVtE/g==",
+          "dev": true,
+          "requires": {
+            "@babel/types": "^7.22.5"
+          }
+        },
+        "@babel/helper-string-parser": {
+          "version": "7.22.5",
+          "resolved": "https://registry.npmjs.org/@babel/helper-string-parser/-/helper-string-parser-7.22.5.tgz",
+          "integrity": "sha512-mM4COjgZox8U+JcXQwPijIZLElkgEpO5rsERVDJTc2qfCDfERyob6k5WegS14SX18IIjv+XD+GrqNumY5JRCDw==",
+          "dev": true
+        },
+        "@babel/helper-validator-identifier": {
+          "version": "7.22.20",
+          "resolved": "https://registry.npmjs.org/@babel/helper-validator-identifier/-/helper-validator-identifier-7.22.20.tgz",
+          "integrity": "sha512-Y4OZ+ytlatR8AI+8KZfKuL5urKp7qey08ha31L8b3BwewJAoJamTzyvxPR/5D+KkdJCGPq/+8TukHBlY10FX9A==",
+          "dev": true
+        },
+        "@babel/highlight": {
+          "version": "7.22.20",
+          "resolved": "https://registry.npmjs.org/@babel/highlight/-/highlight-7.22.20.tgz",
+          "integrity": "sha512-dkdMCN3py0+ksCgYmGG8jKeGA/8Tk+gJwSYYlFGxG5lmhfKNoAy004YpLxpS1W2J8m/EK2Ew+yOs9pVRwO89mg==",
+          "dev": true,
+          "requires": {
+            "@babel/helper-validator-identifier": "^7.22.20",
+            "chalk": "^2.4.2",
+            "js-tokens": "^4.0.0"
+          }
+        },
+        "@babel/parser": {
+          "version": "7.23.0",
+          "resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.23.0.tgz",
+          "integrity": "sha512-vvPKKdMemU85V9WE/l5wZEmImpCtLqbnTvqDS2U1fJ96KrxoW7KrXhNsNCblQlg8Ck4b85yxdTyelsMUgFUXiw==",
+          "dev": true
+        },
+        "@babel/template": {
+          "version": "7.22.15",
+          "resolved": "https://registry.npmjs.org/@babel/template/-/template-7.22.15.tgz",
+          "integrity": "sha512-QPErUVm4uyJa60rkI73qneDacvdvzxshT3kksGqlGWYdOTIUOwJ7RDUL8sGqslY1uXWSL6xMFKEXDS3ox2uF0w==",
+          "dev": true,
+          "requires": {
+            "@babel/code-frame": "^7.22.13",
+            "@babel/parser": "^7.22.15",
+            "@babel/types": "^7.22.15"
+          }
+        },
+        "@babel/types": {
+          "version": "7.23.0",
+          "resolved": "https://registry.npmjs.org/@babel/types/-/types-7.23.0.tgz",
+          "integrity": "sha512-0oIyUfKoI3mSqMvsxBdclDwxXKXAUA8v/apZbc+iSyARYou1o8ZGDxbUYyLFoW2arqS2jDGqJuZvv1d/io1axg==",
+          "dev": true,
+          "requires": {
+            "@babel/helper-string-parser": "^7.22.5",
+            "@babel/helper-validator-identifier": "^7.22.20",
+            "to-fast-properties": "^2.0.0"
+          }
+        },
+        "@jridgewell/gen-mapping": {
+          "version": "0.3.3",
+          "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.3.tgz",
+          "integrity": "sha512-HLhSWOLRi875zjjMG/r+Nv0oCW8umGb0BgEhyX3dDX3egwZtB8PqLnjz3yedt8R5StBrzcg4aBpnh8UA9D1BoQ==",
+          "dev": true,
+          "requires": {
+            "@jridgewell/set-array": "^1.0.1",
+            "@jridgewell/sourcemap-codec": "^1.4.10",
+            "@jridgewell/trace-mapping": "^0.3.9"
+          }
+        }
       }
     },
     "@babel/types": {

src/api/js/scripts/build-wasm.ts

@@ -69,7 +69,7 @@ const fns = JSON.stringify(exportedFuncs());
 const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
 const libz3a = path.normalize('../../../build/libz3.a');
 spawnSync(
-  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js`,
+  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
 );
 
 fs.rmSync(ccWrapperPath);

src/api/ml/z3.ml

@@ -62,6 +62,9 @@ let mk_context (settings:(string * string) list) =
   Z3native.enable_concurrent_dec_ref res;
   res
 
+let interrupt (ctx:context) =
+    Z3native.interrupt ctx
+
 module Symbol =
 struct
   type symbol = Z3native.symbol
@@ -855,15 +858,6 @@ struct
   module Constructor =
   struct
     type constructor = Z3native.constructor
-
-    module FieldNumTable = Hashtbl.Make(struct
-        type t = AST.ast
-        let equal x y = AST.compare x y = 0
-        let hash = AST.hash
-      end)
-
-    let _field_nums = FieldNumTable.create 0
-
     let create (ctx:context) (name:Symbol.symbol) (recognizer:Symbol.symbol) (field_names:Symbol.symbol list) (sorts:Sort.sort option list) (sort_refs:int list) =
       let n = List.length field_names in
       if n <> List.length sorts then
@@ -879,10 +873,9 @@ struct
             (let f x = match x with None -> Z3native.mk_null_ast ctx | Some s -> s in
              List.map f sorts)
             sort_refs in
-        FieldNumTable.add _field_nums no n;
         no
 
-    let get_num_fields (x:constructor) = FieldNumTable.find _field_nums x
+    let get_num_fields (x:constructor) = Z3native.constructor_num_fields (gc x) x
 
     let get_constructor_decl (x:constructor) =
       let (a, _, _) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in
@@ -1509,10 +1502,12 @@ struct
     in
     Z3native.apply_result_inc_ref (gc x) arn;
     let sg = Z3native.apply_result_get_num_subgoals (gc x) arn in
-    let res = if sg = 0 then
+    if sg = 0 then (
-        raise (Error "No subgoals")
+      Z3native.apply_result_dec_ref (gc x) arn;
+      Z3native.tactic_dec_ref (gc x) tn;
+      raise (Error "No subgoals"))
     else
-        Z3native.apply_result_get_subgoal (gc x) arn 0 in
+      let res:goal = Z3native.apply_result_get_subgoal (gc x) arn 0 in
       Z3native.apply_result_dec_ref (gc x) arn;
       Z3native.tactic_dec_ref (gc x) tn;
       res
@@ -1916,6 +1911,9 @@ struct
   let add_simplifier = Z3native.solver_add_simplifier
   let translate x = Z3native.solver_translate (gc x) x
   let to_string x = Z3native.solver_to_string (gc x) x
+
+  let interrupt (ctx:context) (s:solver) =
+    Z3native.solver_interrupt ctx s
 end
 
 
@@ -2077,6 +2075,123 @@ struct
 end
 
 
+module RCF =
+struct
+  type rcf_num = Z3native.rcf_num
+
+  let del (ctx:context) (a:rcf_num) = Z3native.rcf_del ctx a
+  let del_list (ctx:context) (ns:rcf_num list) = List.iter (fun a -> Z3native.rcf_del ctx a) ns
+  let mk_rational (ctx:context) (v:string) = Z3native.rcf_mk_rational ctx v
+  let mk_small_int (ctx:context) (v:int) = Z3native.rcf_mk_small_int ctx v
+
+  let mk_pi (ctx:context) = Z3native.rcf_mk_pi ctx
+  let mk_e (ctx:context) = Z3native.rcf_mk_e ctx
+  let mk_infinitesimal (ctx:context) = Z3native.rcf_mk_infinitesimal ctx
+
+  let mk_roots (ctx:context) (a:rcf_num list) =
+    let n, r = Z3native.rcf_mk_roots ctx (List.length a) a in
+    List.init n (fun x -> List.nth r x)
+
+  let add (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_add ctx a b
+  let sub (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_sub ctx a b
+  let mul (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_mul ctx a b
+  let div (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_div ctx a b
+
+  let neg (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+  let inv (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+
+  let power (ctx:context) (a:rcf_num) (k:int) = Z3native.rcf_power ctx a k
+
+  let lt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_lt ctx a b
+  let gt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_gt ctx a b
+  let le (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_le ctx a b
+  let ge (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_ge ctx a b
+  let eq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_eq ctx a b
+  let neq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_neq ctx a b
+
+  let num_to_string (ctx:context) (a:rcf_num) (compact:bool) (html:bool) = Z3native.rcf_num_to_string ctx a compact html
+  let num_to_decimal_string (ctx:context) (a:rcf_num) (prec:int) = Z3native.rcf_num_to_decimal_string ctx a prec
+  let get_numerator_denominator (ctx:context) (a:rcf_num) = Z3native.rcf_get_numerator_denominator ctx a
+
+  let is_rational (ctx:context) (a:rcf_num) = Z3native.rcf_is_rational ctx a
+  let is_algebraic (ctx:context) (a:rcf_num) = Z3native.rcf_is_algebraic ctx a
+  let is_infinitesimal (ctx:context) (a:rcf_num) = Z3native.rcf_is_infinitesimal ctx a
+  let is_transcendental (ctx:context) (a:rcf_num) = Z3native.rcf_is_transcendental ctx a
+
+  let extension_index (ctx:context) (a:rcf_num) =  Z3native.rcf_extension_index ctx a
+  let transcendental_name (ctx:context) (a:rcf_num) = Z3native.rcf_transcendental_name ctx a
+  let infinitesimal_name (ctx:context) (a:rcf_num) = Z3native.rcf_infinitesimal_name ctx a
+
+  let num_coefficients (ctx:context) (a:rcf_num) = Z3native.rcf_num_coefficients ctx a
+  let get_coefficient (ctx:context) (a:rcf_num) (i:int) = Z3native.rcf_coefficient ctx a i
+
+  let coefficients (ctx:context) (a:rcf_num) =
+    List.init (num_coefficients ctx a) (fun i -> Z3native.rcf_coefficient ctx a i)
+
+  type interval = {
+      lower_is_inf : bool;
+      lower_is_open : bool;
+      lower : rcf_num;
+      upper_is_inf : bool;
+      upper_is_open : bool;
+      upper : rcf_num;
+  }
+
+  let root_interval (ctx:context) (a:rcf_num) =
+    let ok, linf, lopen, l, uinf, uopen, u = Z3native.rcf_interval ctx a in
+    let i:interval = {
+      lower_is_inf = linf != 0;
+      lower_is_open = lopen != 0;
+      lower = l;
+      upper_is_inf = uinf != 0;
+      upper_is_open = uopen != 0;
+      upper = u } in
+    if ok != 0 then Some i else None
+
+  let sign_condition_sign (ctx:context) (a:rcf_num) (i:int) = Z3native.rcf_sign_condition_sign ctx a i
+
+  let sign_condition_coefficient (ctx:context) (a:rcf_num) (i:int) (j:int) = Z3native.rcf_sign_condition_coefficient ctx a i j
+
+  let num_sign_condition_coefficients (ctx:context) (a:rcf_num) (i:int) = Z3native.rcf_num_sign_condition_coefficients ctx a i
+
+  let sign_condition_coefficients (ctx:context) (a:rcf_num) (i:int) =
+    let n = Z3native.rcf_num_sign_condition_coefficients ctx a i in
+    List.init n (fun j -> Z3native.rcf_sign_condition_coefficient ctx a i j)
+
+  let sign_conditions (ctx:context) (a:rcf_num) =
+    let n = Z3native.rcf_num_sign_conditions ctx a in
+    List.init n (fun i ->
+      (let nc = Z3native.rcf_num_sign_condition_coefficients ctx a i in
+       List.init nc (fun j -> Z3native.rcf_sign_condition_coefficient ctx a i j)),
+      Z3native.rcf_sign_condition_sign ctx a i)
+
+  type root = {
+    obj : rcf_num;
+    polynomial : rcf_num list;
+    interval : interval option;
+    sign_conditions : (rcf_num list * int) list;
+  }
+
+  let roots (ctx:context) (a:rcf_num list) =
+      let rs = mk_roots ctx a in
+      List.map
+        (fun r -> {
+          obj = r;
+          polynomial = coefficients ctx r;
+          interval = root_interval ctx r;
+          sign_conditions = sign_conditions ctx r})
+        rs
+
+  let del_root (ctx:context) (r:root) =
+    del ctx r.obj;
+    List.iter (fun n -> del ctx n) r.polynomial;
+    List.iter (fun (ns, _) -> del_list ctx ns) r.sign_conditions
+
+  let del_roots (ctx:context) (rs:root list) =
+    List.iter (fun r -> del_root ctx r) rs
+end
+
+
 let set_global_param = Z3native.global_param_set
 
 let get_global_param id =

src/api/ml/z3.mli

@@ -48,6 +48,12 @@ type context
 *)
 val mk_context : (string * string) list -> context
 
+(** Interrupt the execution of a Z3 procedure.
+
+    This procedure can be used to interrupt: solvers, simplifiers and tactics.
+    Note: Tactic.interrupt is an alias for this. *)
+val interrupt: context -> unit
+
 (** Interaction logging for Z3
     Interaction logs are used to record calls into the API into a text file.
     The text file can be replayed using z3. It has to be the same version of z3
@@ -3342,6 +3348,15 @@ sig
 
   (** A string representation of the solver. *)
   val to_string : solver -> string
+
+  (** Solver local interrupt.
+
+      Normally you should use Z3_interrupt to cancel solvers because only
+      one solver is enabled concurrently per context.
+      However, per GitHub issue #1006, there are use cases where
+      it is more convenient to cancel a specific solver. Solvers
+      that are not selected for interrupts are left alone.*)
+  val interrupt: context -> solver -> unit
 end
 
 (** Fixedpoint solving *)
@@ -3466,7 +3481,7 @@ sig
   (** Add minimization objective. *)
   val minimize : optimize -> Expr.expr -> handle
 
-  (** Checks whether the assertions in the context are satisfiable and solves objectives. *)
+  (** Check consistency and produce optimal values. *)
   val check : optimize -> Solver.status
 
   (** Retrieve model from satisfiable context *)
@@ -3535,6 +3550,151 @@ sig
   val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
 end
 
+(** Real closed field *)
+module RCF :
+sig
+  type rcf_num
+
+  (** Delete a RCF numeral created using the RCF API. *)
+  val del : context -> rcf_num -> unit
+
+  (** Delete RCF numerals created using the RCF API. *)
+  val del_list : context -> rcf_num list -> unit
+
+  (** Return a RCF rational using the given string. *)
+  val mk_rational : context -> string -> rcf_num
+
+  (** Return a RCF small integer. *)
+  val mk_small_int : context -> int -> rcf_num
+
+  (** Return Pi *)
+  val mk_pi : context -> rcf_num
+
+  (** Return e (Euler's constant) *)
+  val mk_e : context -> rcf_num
+
+  (** Return a new infinitesimal that is smaller than all elements in the Z3 field. *)
+  val mk_infinitesimal : context -> rcf_num
+
+  (** Extract the roots of a polynomial. Precondition: The input polynomial is not the zero polynomial. *)
+  val mk_roots : context -> rcf_num list -> rcf_num list
+
+  (** Addition *)
+  val add : context -> rcf_num -> rcf_num -> rcf_num
+
+  (** Subtraction *)
+  val sub : context -> rcf_num -> rcf_num -> rcf_num
+
+  (** Multiplication *)
+  val mul : context -> rcf_num -> rcf_num -> rcf_num
+
+  (** Division *)
+  val div : context -> rcf_num -> rcf_num -> rcf_num
+
+  (** Negation *)
+  val neg : context -> rcf_num -> rcf_num
+
+  (** Multiplicative Inverse *)
+  val inv : context -> rcf_num -> rcf_num
+
+  (** Power *)
+  val power : context -> rcf_num -> int -> rcf_num
+
+  (** less-than *)
+  val lt : context -> rcf_num -> rcf_num -> bool
+
+  (** greater-than *)
+  val gt : context -> rcf_num -> rcf_num -> bool
+
+  (** less-than or equal *)
+  val le : context -> rcf_num -> rcf_num -> bool
+
+  (** greater-than or equal *)
+  val ge : context -> rcf_num -> rcf_num -> bool
+
+  (** equality *)
+  val eq : context -> rcf_num -> rcf_num -> bool
+
+  (** not equal *)
+  val neq : context -> rcf_num -> rcf_num -> bool
+
+  (** Convert the RCF numeral into a string. *)
+  val num_to_string : context -> rcf_num -> bool -> bool -> string
+
+  (** Convert the RCF numeral into a string in decimal notation. *)
+  val num_to_decimal_string : context -> rcf_num -> int -> string
+
+  (** Extract the "numerator" and "denominator" of the given RCF numeral.
+      We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions. *)
+  val get_numerator_denominator : context -> rcf_num -> (rcf_num * rcf_num)
+
+  (** Return \c true if \c a represents a rational number. *)
+  val is_rational : context -> rcf_num -> bool
+
+  (** Return \c true if \c a represents an algebraic number. *)
+  val is_algebraic : context -> rcf_num -> bool
+
+  (** Return \c true if \c a represents an infinitesimal. *)
+  val is_infinitesimal : context -> rcf_num -> bool
+
+  (** Return \c true if \c a represents a transcendental number. *)
+  val is_transcendental : context -> rcf_num -> bool
+
+  (** Return the index of a field extension. *)
+  val extension_index : context -> rcf_num -> int
+
+  (** Return the name of a transcendental. *)
+  val transcendental_name : context -> rcf_num -> Symbol.symbol
+
+  (** Return the name of an infinitesimal. *)
+  val infinitesimal_name : context -> rcf_num -> Symbol.symbol
+
+  (** Return the number of coefficients in an algebraic number. *)
+  val num_coefficients : context -> rcf_num -> int
+
+  (** Extract a coefficient from an algebraic number. *)
+  val get_coefficient : context -> rcf_num -> int -> rcf_num
+
+  (** Extract the coefficients from an algebraic number. *)
+  val coefficients : context -> rcf_num -> rcf_num list
+
+  (** Extract the sign of a sign condition from an algebraic number. *)
+  val sign_condition_sign : context -> rcf_num -> int -> int
+
+  (** Return the size of a sign condition polynomial. *)
+  val num_sign_condition_coefficients : context -> rcf_num -> int -> int
+
+  (** Extract a sign condition polynomial coefficient from an algebraic number. *)
+  val sign_condition_coefficient : context -> rcf_num -> int -> int -> rcf_num
+
+  (** Extract sign conditions from an algebraic number. *)
+  val sign_conditions : context -> rcf_num -> (rcf_num list * int) list
+
+  (** Extract the interval from an algebraic number. *)
+  type interval = {
+    lower_is_inf : bool;
+    lower_is_open : bool;
+    lower : rcf_num;
+    upper_is_inf : bool;
+    upper_is_open : bool;
+    upper : rcf_num;
+  }
+
+  val root_interval : context -> rcf_num -> interval option
+
+  type root = {
+    obj : rcf_num;
+    polynomial : rcf_num list;
+    interval : interval option;
+    sign_conditions : (rcf_num list * int) list;
+  }
+
+  val roots : context -> rcf_num list -> root list
+
+  val del_root : context -> root -> unit
+
+  val del_roots : context -> root list -> unit
+end
 
 (** Set a global (or module) parameter, which is shared by all Z3 contexts.
 

src/api/ml/z3native_stubs.c.pre

@@ -2,6 +2,12 @@
 #include <string.h>
 #include <assert.h>
 
+#ifndef __STDC_NO_ATOMICS__
+#include <stdatomic.h>
+#else
+#define _Atomic(T) T
+#endif
+
 #ifdef __cplusplus
 extern "C" {
 #endif
@@ -118,7 +124,7 @@ int compare_pointers(void* pt1, void* pt2) {
    blocks that get copied. */
 typedef struct {
   Z3_context ctx;
-  unsigned long obj_count;
+  _Atomic(unsigned long) obj_count;
 } Z3_context_plus_data;
 
 /* A context is wrapped to an OCaml value by storing a pointer

src/api/python/CMakeLists.txt

@@ -33,7 +33,7 @@ endforeach()
 
 # Generate z3core.py
 add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--z3py-output-dir"
@@ -49,7 +49,7 @@ list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}
 
 # Generate z3consts.py
 add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "--z3py-output-dir"
@@ -96,7 +96,7 @@ if (Z3_INSTALL_PYTHON_BINDINGS)
   if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
     message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
     execute_process(
-      COMMAND "${PYTHON_EXECUTABLE}" "-c"
+      COMMAND "${Python3_EXECUTABLE}" "-c"
         "import sysconfig; print(sysconfig.get_path('purelib'))"
       RESULT_VARIABLE exit_code
       OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR

src/api/python/setup.py

@@ -18,7 +18,7 @@ from setuptools.command.bdist_egg import bdist_egg as _bdist_egg
 
 build_env = dict(os.environ)
 build_env['PYTHON'] = sys.executable
-build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++11"
+build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++17"
 
 # determine where we're building and where sources are
 ROOT_DIR = os.path.abspath(os.path.dirname(__file__))

src/api/python/z3/z3.py

@@ -683,6 +683,8 @@ def _to_sort_ref(s, ctx):
         return SeqSortRef(s, ctx)
     elif k == Z3_CHAR_SORT:
         return CharSortRef(s, ctx)
+    elif k == Z3_TYPE_VAR:
+        return TypeVarRef(s, ctx)
     return SortRef(s, ctx)
 
 
@@ -708,6 +710,26 @@ def DeclareSort(name, ctx=None):
     ctx = _get_ctx(ctx)
     return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
 
+class TypeVarRef(SortRef):
+    """Type variable reference"""
+
+    def subsort(self, other):
+        return True
+    
+    def cast(self, val):
+        return val
+    
+
+def DeclareTypeVar(name, ctx=None):
+    """Create a new type variable named `name`.
+
+    If `ctx=None`, then the new sort is declared in the global Z3Py context.
+
+    """
+    ctx = _get_ctx(ctx)
+    return TypeVarRef(Z3_mk_type_variable(ctx.ref(), to_symbol(name, ctx)), ctx)
+
+
 #########################################
 #
 # Function Declarations
@@ -1549,6 +1571,14 @@ class BoolRef(ExprRef):
     def sort(self):
         return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 
+    def __add__(self, other):
+        if isinstance(other, BoolRef):
+            other = If(other, 1, 0)
+        return If(self, 1, 0) + other
+
+    def __radd__(self, other):
+        return self + other
+ 
     def __rmul__(self, other):
         return self * other
 
@@ -1563,6 +1593,20 @@ class BoolRef(ExprRef):
             other = If(other, 1, 0)
         return If(self, other, 0)
         
+    def __and__(self, other):
+        return And(self, other)
+    
+    def __or__(self, other):
+        return Or(self, other)
+
+    def __xor__(self, other):
+        return Xor(self, other)
+    
+    def __invert__(self):
+        return Not(self)
+    
+    
+
     
 def is_bool(a):
     """Return `True` if `a` is a Z3 Boolean expression.
@@ -2059,6 +2103,16 @@ class QuantifierRef(BoolRef):
         """
         return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
 
+    def skolem_id(self):
+        """Return the skolem id of `self`.
+        """
+        return _symbol2py(self.ctx, Z3_get_quantifier_skolem_id(self.ctx_ref(), self.ast))
+
+    def qid(self):
+        """Return the quantifier id of `self`.
+        """
+        return _symbol2py(self.ctx, Z3_get_quantifier_id(self.ctx_ref(), self.ast))
+
     def num_patterns(self):
         """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
 
@@ -6909,6 +6963,13 @@ class Solver(Z3PPObject):
         if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
             Z3_solver_dec_ref(self.ctx.ref(), self.solver)
 
+    def __enter__(self):
+        self.push()
+        return self
+
+    def __exit__(self, *exc_info):
+        self.pop()
+
     def set(self, *args, **keys):
         """Set a configuration option.
         The method `help()` return a string containing all available options.
@@ -7993,7 +8054,7 @@ class Optimize(Z3PPObject):
         Z3_optimize_pop(self.ctx.ref(), self.optimize)
 
     def check(self, *assumptions):
-        """Check satisfiability while optimizing objective functions."""
+        """Check consistency and produce optimal values."""
         assumptions = _get_args(assumptions)
         num = len(assumptions)
         _assumptions = (Ast * num)()
@@ -11416,11 +11477,12 @@ def to_AstVectorObj(ptr,):
 # for UserPropagator we use a global dictionary, which isn't great code.
 
 _my_hacky_class = None
-def on_clause_eh(ctx, p, clause):
+def on_clause_eh(ctx, p, n, dep, clause):
     onc = _my_hacky_class
     p = _to_expr_ref(to_Ast(p), onc.ctx)
     clause = AstVector(to_AstVectorObj(clause), onc.ctx)
-    onc.on_clause(p, clause)
+    deps = [dep[i] for i in range(n)]
+    onc.on_clause(p, deps, clause)
     
 _on_clause_eh = Z3_on_clause_eh(on_clause_eh)
 

src/api/z3.h

@@ -20,7 +20,6 @@ Notes:
 
 #pragma once
 
-#include <stdio.h>
 #include <stdbool.h>
 #include <stdint.h>
 #include "z3_macros.h"

src/api/z3_api.h

@@ -5,7 +5,6 @@
 #pragma once
 
 DEFINE_TYPE(Z3_symbol);
-DEFINE_TYPE(Z3_literals);
 DEFINE_TYPE(Z3_config);
 DEFINE_TYPE(Z3_context);
 DEFINE_TYPE(Z3_sort);
@@ -151,6 +150,7 @@ typedef enum
     Z3_SEQ_SORT,
     Z3_RE_SORT,
     Z3_CHAR_SORT,
+    Z3_TYPE_VAR,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -1397,7 +1397,6 @@ typedef enum
   def_Type('FUNC_DECL',        'Z3_func_decl',        'FuncDecl')
   def_Type('PATTERN',          'Z3_pattern',          'Pattern')
   def_Type('MODEL',            'Z3_model',            'ModelObj')
-  def_Type('LITERALS',         'Z3_literals',         'Literals')
   def_Type('CONSTRUCTOR',      'Z3_constructor',      'Constructor')
   def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList')
   def_Type('SOLVER',           'Z3_solver',           'SolverObj')
@@ -1436,7 +1435,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_as
 Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase));
-Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, Z3_ast_vector literals));
+Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
 
 
 /**
@@ -1883,6 +1882,17 @@ extern "C" {
     */
     Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
 
+    /**
+       \brief Create a type variable.
+
+       Functions using type variables can be applied to instantiations that match the signature 
+       of the function. Assertions using type variables correspond to assertions over all possible
+       instantiations.
+
+       def_API('Z3_mk_type_variable', SORT, (_in(CONTEXT), _in(SYMBOL)))
+    */
+    Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s);
+
     /**
        \brief Create the Boolean type.
 
@@ -2072,6 +2082,16 @@ extern "C" {
                                             unsigned sort_refs[]
                                             );
 
+    /**
+       \brief Retrieve the number of fields of a constructor
+
+       \param c logical context.
+       \param constr constructor.
+
+       def_API('Z3_constructor_num_fields', UINT, (_in(CONTEXT), _in(CONSTRUCTOR)))
+    */
+    unsigned Z3_API Z3_constructor_num_fields(Z3_context c, Z3_constructor constr);
+
     /**
        \brief Reclaim memory allocated to constructor.
 
@@ -5186,6 +5206,24 @@ extern "C" {
     */
     unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
 
+    /**
+       \brief Obtain skolem id of quantifier.
+
+       \pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST
+
+       def_API('Z3_get_quantifier_skolem_id', SYMBOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a);
+
+    /**
+       \brief Obtain id of quantifier.
+
+       \pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST
+
+       def_API('Z3_get_quantifier_id', SYMBOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a);
+
     /**
        \brief Return number of patterns used in quantifier.
 
@@ -5584,14 +5622,14 @@ extern "C" {
     void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
 
     /**
-       \brief Increment the reference counter of the given Z3_func_interp object.
+       \brief Increment the reference counter of the given \c Z3_func_interp object.
 
        def_API('Z3_func_interp_inc_ref', VOID, (_in(CONTEXT), _in(FUNC_INTERP)))
     */
     void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
 
     /**
-       \brief Decrement the reference counter of the given Z3_func_interp object.
+       \brief Decrement the reference counter of the given \c Z3_func_interp object.
 
        def_API('Z3_func_interp_dec_ref', VOID, (_in(CONTEXT), _in(FUNC_INTERP)))
     */

src/api/z3_fpa.h

@@ -32,6 +32,12 @@ extern "C" {
 
         \param c logical context
 
+        \sa Z3_mk_fpa_round_nearest_ties_to_away or Z3_mk_fpa_rna
+        \sa Z3_mk_fpa_round_nearest_ties_to_even or Z3_mk_fpa_rne
+        \sa Z3_mk_fpa_round_toward_negative or Z3_mk_fpa_rtn
+        \sa Z3_mk_fpa_round_toward_positive or Z3_mk_fpa_rtp
+        \sa Z3_mk_fpa_round_toward_zero or Z3_mk_fpa_rtz
+
         def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
@@ -39,8 +45,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
 
+        This is the same as #Z3_mk_fpa_rne.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_round_nearest_ties_to_away
+        \sa Z3_mk_fpa_round_toward_negative
+        \sa Z3_mk_fpa_round_toward_positive
+        \sa Z3_mk_fpa_round_toward_zero
+
         def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
@@ -48,8 +62,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
 
+        This is the same as #Z3_mk_fpa_round_nearest_ties_to_even.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_rna
+        \sa Z3_mk_fpa_rtn
+        \sa Z3_mk_fpa_rtp
+        \sa Z3_mk_fpa_rtz
+
         def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);
@@ -57,8 +79,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
 
+        This is the same as #Z3_mk_fpa_rna.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_round_nearest_ties_to_even
+        \sa Z3_mk_fpa_round_toward_negative
+        \sa Z3_mk_fpa_round_toward_positive
+        \sa Z3_mk_fpa_round_toward_zero
+
         def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
@@ -66,8 +96,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
 
+        This is the same as #Z3_mk_fpa_round_nearest_ties_to_away.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_rne
+        \sa Z3_mk_fpa_rtn
+        \sa Z3_mk_fpa_rtp
+        \sa Z3_mk_fpa_rtz
+
         def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);
@@ -75,8 +113,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
 
+        This is the same as #Z3_mk_fpa_rtp.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_round_nearest_ties_to_away
+        \sa Z3_mk_fpa_round_nearest_ties_to_even
+        \sa Z3_mk_fpa_round_toward_negative
+        \sa Z3_mk_fpa_round_toward_zero
+
         def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
@@ -84,8 +130,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
 
+        This is the same as #Z3_mk_fpa_round_toward_positive.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_rna
+        \sa Z3_mk_fpa_rne
+        \sa Z3_mk_fpa_rtn
+        \sa Z3_mk_fpa_rtz
+
         def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);
@@ -93,8 +147,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
 
+        This is the same as #Z3_mk_fpa_rtn.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_round_nearest_ties_to_away
+        \sa Z3_mk_fpa_round_nearest_ties_to_even
+        \sa Z3_mk_fpa_round_toward_positive
+        \sa Z3_mk_fpa_round_toward_zero
+
         def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);
@@ -102,8 +164,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
 
+        This is the same as #Z3_mk_fpa_round_toward_negative.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_rna
+        \sa Z3_mk_fpa_rne
+        \sa Z3_mk_fpa_rtp
+        \sa Z3_mk_fpa_rtz
+
         def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);
@@ -111,8 +181,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
 
+        This is the same as #Z3_mk_fpa_rtz.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_round_nearest_ties_to_away
+        \sa Z3_mk_fpa_round_nearest_ties_to_even
+        \sa Z3_mk_fpa_round_toward_negative
+        \sa Z3_mk_fpa_round_toward_positive
+
         def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
@@ -120,8 +198,16 @@ extern "C" {
     /**
         \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
 
+        This is the same as #Z3_mk_fpa_round_toward_zero.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_rounding_mode_sort
+        \sa Z3_mk_fpa_rna
+        \sa Z3_mk_fpa_rne
+        \sa Z3_mk_fpa_rtn
+        \sa Z3_mk_fpa_rtp
+
         def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
     */
     Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);
@@ -135,6 +221,11 @@ extern "C" {
 
         \remark \c ebits must be larger than 1 and \c sbits must be larger than 2.
 
+        \sa Z3_mk_fpa_sort_half or Z3_mk_fpa_sort_16
+        \sa Z3_mk_fpa_sort_single or Z3_mk_fpa_sort_32
+        \sa Z3_mk_fpa_sort_double or Z3_mk_fpa_sort_64
+        \sa Z3_mk_fpa_sort_quadruple or Z3_mk_fpa_sort_128
+
         def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
@@ -142,8 +233,15 @@ extern "C" {
     /**
         \brief Create the half-precision (16-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_16.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_single
+        \sa Z3_mk_fpa_sort_double
+        \sa Z3_mk_fpa_sort_quadruple
+
         def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);
@@ -151,8 +249,15 @@ extern "C" {
     /**
         \brief Create the half-precision (16-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_half.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_32
+        \sa Z3_mk_fpa_sort_64
+        \sa Z3_mk_fpa_sort_128
+
         def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);
@@ -160,8 +265,15 @@ extern "C" {
     /**
         \brief Create the single-precision (32-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_32.
+
         \param c logical context.
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_half
+        \sa Z3_mk_fpa_sort_double
+        \sa Z3_mk_fpa_sort_quadruple
+
         def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);
@@ -169,8 +281,15 @@ extern "C" {
     /**
         \brief Create the single-precision (32-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_single.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_16
+        \sa Z3_mk_fpa_sort_64
+        \sa Z3_mk_fpa_sort_128
+
         def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);
@@ -178,8 +297,15 @@ extern "C" {
     /**
         \brief Create the double-precision (64-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_64.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_half
+        \sa Z3_mk_fpa_sort_single
+        \sa Z3_mk_fpa_sort_quadruple
+
         def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);
@@ -187,8 +313,15 @@ extern "C" {
     /**
         \brief Create the double-precision (64-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_double.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_16
+        \sa Z3_mk_fpa_sort_32
+        \sa Z3_mk_fpa_sort_128
+
         def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);
@@ -196,8 +329,15 @@ extern "C" {
     /**
         \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_128.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_half
+        \sa Z3_mk_fpa_sort_single
+        \sa Z3_mk_fpa_sort_double
+
         def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);
@@ -205,8 +345,15 @@ extern "C" {
     /**
         \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
 
+        This is the same as #Z3_mk_fpa_sort_quadruple.
+
         \param c logical context
 
+        \sa Z3_mk_fpa_sort
+        \sa Z3_mk_fpa_sort_16
+        \sa Z3_mk_fpa_sort_32
+        \sa Z3_mk_fpa_sort_64
+
         def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
     */
     Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
@@ -218,6 +365,7 @@ extern "C" {
         \param s target sort
 
         \sa Z3_mk_fpa_inf
+        \sa Z3_mk_fpa_is_nan
         \sa Z3_mk_fpa_zero
 
         def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
@@ -233,6 +381,7 @@ extern "C" {
 
         When \c negative is \c true, -oo will be generated instead of +oo.
 
+        \sa Z3_mk_fpa_is_infinite
         \sa Z3_mk_fpa_nan
         \sa Z3_mk_fpa_zero
 
@@ -250,6 +399,7 @@ extern "C" {
         When \c negative is \c true, -zero will be generated instead of +zero.
 
         \sa Z3_mk_fpa_inf
+        \sa Z3_mk_fpa_is_zero
         \sa Z3_mk_fpa_nan
 
         def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
@@ -397,6 +547,10 @@ extern "C" {
         \param c logical context
         \param t term of FloatingPoint sort
 
+        \sa Z3_mk_fpa_is_negative
+        \sa Z3_mk_fpa_is_positive
+        \sa Z3_mk_fpa_neg
+
         def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
@@ -407,6 +561,10 @@ extern "C" {
         \param c logical context
         \param t term of FloatingPoint sort
 
+        \sa Z3_mk_fpa_abs
+        \sa Z3_mk_fpa_is_negative
+        \sa Z3_mk_fpa_is_positive
+
         def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
@@ -533,6 +691,8 @@ extern "C" {
 
         \c t1, \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_max
+
         def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -546,6 +706,8 @@ extern "C" {
 
         \c t1, \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_min
+
         def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -559,6 +721,11 @@ extern "C" {
 
         \c t1 and \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_eq
+        \sa Z3_mk_fpa_geq
+        \sa Z3_mk_fpa_gt
+        \sa Z3_mk_fpa_lt
+
         def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -572,6 +739,11 @@ extern "C" {
 
         \c t1 and \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_eq
+        \sa Z3_mk_fpa_geq
+        \sa Z3_mk_fpa_gt
+        \sa Z3_mk_fpa_leq
+
         def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -585,6 +757,11 @@ extern "C" {
 
         \c t1 and \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_eq
+        \sa Z3_mk_fpa_gt
+        \sa Z3_mk_fpa_leq
+        \sa Z3_mk_fpa_lt
+
         def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -598,6 +775,11 @@ extern "C" {
 
         \c t1 and \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_eq
+        \sa Z3_mk_fpa_geq
+        \sa Z3_mk_fpa_leq
+        \sa Z3_mk_fpa_lt
+
         def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -613,6 +795,11 @@ extern "C" {
 
         \c t1 and \c t2 must have the same FloatingPoint sort.
 
+        \sa Z3_mk_fpa_geq
+        \sa Z3_mk_fpa_gt
+        \sa Z3_mk_fpa_leq
+        \sa Z3_mk_fpa_lt
+
         def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
@@ -625,6 +812,11 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_is_infinite
+        \sa Z3_mk_fpa_is_nan
+        \sa Z3_mk_fpa_is_subnormal
+        \sa Z3_mk_fpa_is_zero
+
         def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
@@ -637,6 +829,11 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_is_infinite
+        \sa Z3_mk_fpa_is_nan
+        \sa Z3_mk_fpa_is_normal
+        \sa Z3_mk_fpa_is_zero
+
         def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
@@ -649,6 +846,12 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_is_infinite
+        \sa Z3_mk_fpa_is_nan
+        \sa Z3_mk_fpa_is_normal
+        \sa Z3_mk_fpa_is_subnormal
+        \sa Z3_mk_fpa_zero
+
         def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
@@ -661,6 +864,12 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_inf
+        \sa Z3_mk_fpa_is_nan
+        \sa Z3_mk_fpa_is_normal
+        \sa Z3_mk_fpa_is_subnormal
+        \sa Z3_mk_fpa_is_zero
+
         def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
@@ -673,6 +882,12 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_is_infinite
+        \sa Z3_mk_fpa_is_normal
+        \sa Z3_mk_fpa_is_subnormal
+        \sa Z3_mk_fpa_is_zero
+        \sa Z3_mk_fpa_nan
+
         def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
@@ -685,6 +900,10 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_abs
+        \sa Z3_mk_fpa_is_positive
+        \sa Z3_mk_fpa_neg
+
         def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
@@ -697,6 +916,10 @@ extern "C" {
 
         \c t must have FloatingPoint sort.
 
+        \sa Z3_mk_fpa_abs
+        \sa Z3_mk_fpa_is_negative
+        \sa Z3_mk_fpa_neg
+
         def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);
@@ -848,6 +1071,8 @@ extern "C" {
         \param c logical context
         \param s FloatingPoint sort
 
+        \sa Z3_fpa_get_sbits
+
         def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
     */
     unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);
@@ -858,6 +1083,8 @@ extern "C" {
         \param c logical context
         \param s FloatingPoint sort
 
+        \sa Z3_fpa_get_ebits
+
         def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
     */
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
@@ -868,6 +1095,11 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_inf
+        \sa Z3_fpa_is_numeral_normal
+        \sa Z3_fpa_is_numeral_subnormal
+        \sa Z3_fpa_is_numeral_zero
+
         def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
@@ -878,6 +1110,11 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_nan
+        \sa Z3_fpa_is_numeral_normal
+        \sa Z3_fpa_is_numeral_subnormal
+        \sa Z3_fpa_is_numeral_zero
+
         def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
@@ -888,6 +1125,11 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_inf
+        \sa Z3_fpa_is_numeral_nan
+        \sa Z3_fpa_is_numeral_normal
+        \sa Z3_fpa_is_numeral_subnormal
+
         def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
@@ -898,6 +1140,11 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_inf
+        \sa Z3_fpa_is_numeral_nan
+        \sa Z3_fpa_is_numeral_subnormal
+        \sa Z3_fpa_is_numeral_zero
+
         def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
@@ -908,6 +1155,11 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_inf
+        \sa Z3_fpa_is_numeral_nan
+        \sa Z3_fpa_is_numeral_normal
+        \sa Z3_fpa_is_numeral_zero
+
         def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
@@ -918,6 +1170,8 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_negative
+
         def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
@@ -928,6 +1182,8 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
+        \sa Z3_fpa_is_numeral_positive
+
         def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
     */
     bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);

src/api/z3_rcf.h

@@ -196,6 +196,122 @@ extern "C" {
    */
    void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
 
+   /**
+       \brief Return \c true if \c a represents a rational number.
+
+       def_API('Z3_rcf_is_rational', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return \c true if \c a represents an algebraic number.
+
+       def_API('Z3_rcf_is_algebraic', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return \c true if \c a represents an infinitesimal.
+
+       def_API('Z3_rcf_is_infinitesimal', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return \c true if \c a represents a transcendental number.
+
+       def_API('Z3_rcf_is_transcendental', BOOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return the index of a field extension.
+
+      def_API('Z3_rcf_extension_index', UINT, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   unsigned Z3_API Z3_rcf_extension_index(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return the name of a transcendental.
+
+       \pre Z3_rcf_is_transcendtal(ctx, a);
+
+       def_API('Z3_rcf_transcendental_name', SYMBOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   Z3_symbol Z3_API Z3_rcf_transcendental_name(Z3_context c, Z3_rcf_num a);
+
+    /**
+       \brief Return the name of an infinitesimal.
+
+       \pre Z3_rcf_is_infinitesimal(ctx, a);
+
+       def_API('Z3_rcf_infinitesimal_name', SYMBOL, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   Z3_symbol Z3_API Z3_rcf_infinitesimal_name(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Return the number of coefficients in an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_num_coefficients', UINT, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   unsigned Z3_API Z3_rcf_num_coefficients(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Extract a coefficient from an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_coefficient', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
+   */
+   Z3_rcf_num Z3_API Z3_rcf_coefficient(Z3_context c, Z3_rcf_num a, unsigned i);
+
+   /**
+       \brief Extract an interval from an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM)))
+   */
+   int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper);
+
+   /**
+       \brief Return the number of sign conditions of an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_num_sign_conditions', UINT, (_in(CONTEXT), _in(RCF_NUM)))
+   */
+   unsigned Z3_API Z3_rcf_num_sign_conditions(Z3_context c, Z3_rcf_num a);
+
+   /**
+       \brief Extract the sign of a sign condition from an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_sign_condition_sign', INT, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
+   */
+   int Z3_API Z3_rcf_sign_condition_sign(Z3_context c, Z3_rcf_num a, unsigned i);
+
+   /**
+       \brief Return the number of sign condition polynomial coefficients of an algebraic number.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_num_sign_condition_coefficients', UINT, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
+   */
+   unsigned Z3_API Z3_rcf_num_sign_condition_coefficients(Z3_context c, Z3_rcf_num a, unsigned i);
+
+   /**
+       \brief Extract the j-th polynomial coefficient of the i-th sign condition.
+
+       \pre Z3_rcf_is_algebraic(ctx, a);
+
+       def_API('Z3_rcf_sign_condition_coefficient', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT), _in(UINT)))
+   */
+   Z3_rcf_num Z3_API Z3_rcf_sign_condition_coefficient(Z3_context c, Z3_rcf_num a, unsigned i, unsigned j);
+
     /**@}*/
     /**@}*/
 

src/ast/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(ast
     act_cache.cpp
     arith_decl_plugin.cpp
     array_decl_plugin.cpp
+    array_peq.cpp
     ast.cpp
     ast_ll_pp.cpp
     ast_lt.cpp
@@ -37,6 +38,8 @@ z3_add_component(ast
     num_occurs.cpp
     occurs.cpp
     pb_decl_plugin.cpp
+    polymorphism_inst.cpp
+    polymorphism_util.cpp
     pp.cpp
     quantifier_stat.cpp
     recfun_decl_plugin.cpp

src/ast/arith_decl_plugin.cpp

@@ -801,6 +801,29 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
     return result;
 }
 
+bool arith_util::is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
+    if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && !is_numeral(args[1])) {
+        f_out = mk_div0();
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_IDIV) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_MOD) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    return false;
+}
+
 bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
     rational r;
     if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {

src/ast/arith_decl_plugin.h

@@ -517,6 +517,8 @@ public:
 
     bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
 
+    bool is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
+
     bool is_underspecified(expr* e) const;
 
     bool is_bounded(expr* e) const;

src/ast/array_decl_plugin.cpp

@@ -633,6 +633,12 @@ bool array_decl_plugin::is_value(app * _e) const {
     }
 }
 
+bool array_decl_plugin::is_unique_value(app* _e) const {
+    array_util u(*m_manager);
+    expr* e = _e;
+    return u.is_const(e, e) && m_manager->is_unique_value(e);
+}
+
 
 func_decl * array_recognizers::get_as_array_func_decl(expr * n) const { 
     SASSERT(is_as_array(n)); 

src/ast/array_decl_plugin.h

@@ -137,6 +137,8 @@ class array_decl_plugin : public decl_plugin {
 
     bool is_value(app * e) const override;
 
+    bool is_unique_value(app* e) const override;
+
 };
 
 class array_recognizers {
@@ -184,6 +186,21 @@ public:
 
     bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
 
+
+    bool is_select1(expr* n) const { return is_select(n) && to_app(n)->get_num_args() == 2; }
+    
+    bool is_select1(expr* n, expr*& a, expr*& i) const {
+        return is_select1(n) && (a = to_app(n)->get_arg(0), i = to_app(n)->get_arg(1), true);
+    }
+
+    bool is_store1(expr* n) const { return is_store(n) && to_app(n)->get_num_args() == 3; }
+    
+    bool is_store1(expr* n, expr*& a, expr*& i, expr*& v) const {
+        app* _n;
+        return is_store1(n) && (_n = to_app(n), a = _n->get_arg(0), i = _n->get_arg(1), v = _n->get_arg(2), true);
+    }
+
+
     MATCH_BINARY(is_subset);
 };
 
@@ -211,6 +228,11 @@ public:
         return mk_store(args.size(), args.data());
     }
 
+    app * mk_select(expr* a, expr* i) const {
+        expr* args[2] = { a, i };
+        return mk_select(2, args);
+    }
+
     app * mk_select(unsigned num_args, expr * const * args) const {
         return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
     }

src/ast/array_peq.cpp

@@ -0,0 +1,107 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    array_peq.cpp
+
+Abstract:
+
+  Partial equality for arrays
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-06-13
+    Hari Govind V K
+
+Revision History:
+
+--*/
+#include "ast/array_peq.h"
+
+#define PARTIAL_EQ "!partial_eq"
+bool is_partial_eq(const func_decl *f) {
+    SASSERT(f);
+    return f->get_name() == PARTIAL_EQ;
+}
+
+bool is_partial_eq(const app *a) {
+    SASSERT(a);
+    return is_partial_eq(a->get_decl());
+}
+
+app_ref mk_peq(expr *e0, expr *e1, vector<expr_ref_vector> const &indices,
+               ast_manager &m) {
+    peq p(e0, e1, indices, m);
+    return p.mk_peq();
+}
+
+app_ref peq::mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs) {
+    if (!m_eq) {
+        expr_ref lhs(m_lhs, m), rhs(m_rhs, m);
+        if (!stores_on_rhs) { std::swap(lhs, rhs); }
+        // lhs = (...(store (store rhs i0 v0) i1 v1)...)
+        sort *val_sort = get_array_range(lhs->get_sort());
+        for (expr_ref_vector const &diff : m_diff_indices) {
+            ptr_vector<expr> store_args;
+            store_args.push_back(rhs);
+            store_args.append(diff.size(), diff.data());
+            app_ref val(m.mk_fresh_const("diff", val_sort), m);
+            store_args.push_back(val);
+            aux_consts.push_back(val);
+            rhs = m_arr_u.mk_store(store_args);
+        }
+        m_eq = m.mk_eq(lhs, rhs);
+    }
+    return m_eq;
+}
+
+app_ref peq::mk_peq() {
+    if (!m_peq) {
+        ptr_vector<expr> args;
+        args.push_back(m_lhs);
+        args.push_back(m_rhs);
+        for (auto const &v : m_diff_indices) {
+            args.append(v.size(), v.data());
+        }
+        m_peq = m.mk_app(m_decl, args.size(), args.data());
+    }
+    return m_peq;
+}
+
+peq::peq(expr *lhs, expr *rhs, vector<expr_ref_vector> const &diff_indices,
+         ast_manager &m)
+    : m(m), m_lhs(lhs, m), m_rhs(rhs, m), m_diff_indices(diff_indices),
+      m_decl(m), m_peq(m), m_eq(m), m_arr_u(m) {
+    SASSERT(m_arr_u.is_array(lhs));
+    SASSERT(m_arr_u.is_array(rhs));
+    SASSERT(lhs->get_sort() == rhs->get_sort());
+    ptr_vector<sort> sorts;
+    sorts.push_back(m_lhs->get_sort());
+    sorts.push_back(m_rhs->get_sort());
+
+    for (auto const &v : diff_indices) {
+        SASSERT(v.size() == get_array_arity(m_lhs->get_sort()));
+        for (expr *e : v) sorts.push_back(e->get_sort());
+    }
+    m_decl = m.mk_func_decl(symbol(PARTIAL_EQ), sorts.size(), sorts.data(),
+                            m.mk_bool_sort());
+}
+
+peq::peq(app *p, ast_manager &m)
+    : m(m), m_lhs(p->get_arg(0), m), m_rhs(p->get_arg(1), m),
+      m_decl(p->get_decl(), m), m_peq(p, m), m_eq(m), m_arr_u(m),
+      m_name(symbol(PARTIAL_EQ)) {
+    SASSERT(is_partial_eq(p));
+
+    SASSERT(m_arr_u.is_array(m_lhs));
+    SASSERT(m_arr_u.is_array(m_rhs));
+    SASSERT(m_lhs->get_sort() == m_rhs->get_sort());
+    unsigned arity = get_array_arity(m_lhs->get_sort());
+    for (unsigned i = 2; i < p->get_num_args(); i += arity) {
+        SASSERT(arity + i <= p->get_num_args());
+        expr_ref_vector vec(m);
+        vec.append(arity, p->get_args() + i);
+        m_diff_indices.push_back(std::move(vec));
+    }
+}

src/ast/array_peq.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    array_peq.h
+
+Abstract:
+
+  Partial equality for arrays
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-06-13
+    Hari Govind V K
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/array_decl_plugin.h"
+#include "ast/ast.h"
+
+/**
+ * \brief utility class for partial equalities
+ *
+ * A partial equality (a ==I b), for two arrays a, b and a finite set of indices
+ * I holds iff (forall i :: i \not\in I => a[i] == b[i]). In other words, peq is
+ * a restricted form of the extensionality axiom
+ *
+ * Using this class, we denote (a =I b) as f(a,b,i0,i1,...),
+ * where f is an uninterpreted predicate with the name PARTIAL_EQ and
+ * I = {i0,i1,...}
+ */
+
+class peq {
+    ast_manager &m;
+    expr_ref m_lhs;
+    expr_ref m_rhs;
+    vector<expr_ref_vector> m_diff_indices;
+    func_decl_ref m_decl; // the partial equality declaration
+    app_ref m_peq;        // partial equality application
+    app_ref m_eq;         // equivalent std equality using def. of partial eq
+    array_util m_arr_u;
+    symbol m_name;
+
+  public:
+    peq(app *p, ast_manager &m);
+
+    peq(expr *lhs, expr *rhs, vector<expr_ref_vector> const &diff_indices,
+        ast_manager &m);
+
+    expr_ref lhs() { return m_lhs; }
+
+    expr_ref rhs() { return m_rhs; }
+
+    void get_diff_indices(vector<expr_ref_vector> &result) {
+        result.append(m_diff_indices);
+    }
+
+    /** Convert peq into a peq expression */
+    app_ref mk_peq();
+
+    /** Convert peq into an equality
+
+        For peq of the form (a =I b) returns (a = b[i0 := v0, i1 := v1, ...])
+        where i0, i1 \in I, and v0, v1 are fresh skolem constants
+
+        Skolems are returned in aux_consts
+
+        The left and right hand arguments are reversed when stores_on_rhs is
+       false
+     */
+    app_ref mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs = true);
+};
+
+/**
+ * mk (e0 ==indices e1)
+ *
+ * result has stores if either e0 or e1 or an index term has stores
+ */
+app_ref mk_peq(expr *e0, expr *e1, vector<expr_ref_vector> const &indices,
+               ast_manager &m);
+
+bool is_partial_eq(const func_decl *f);
+
+bool is_partial_eq(const app *a);
+
+inline bool is_peq(const func_decl *f) { return is_partial_eq(f); }
+inline bool is_peq(const app *a) { return is_partial_eq(a); }

src/ast/ast.cpp

@@ -202,8 +202,7 @@ unsigned decl_info::hash() const {
 
 bool decl_info::operator==(decl_info const & info) const {
     return m_family_id == info.m_family_id && m_kind == info.m_kind &&
-        m_parameters.size() == info.m_parameters.size() && 
+           m_parameters == info.m_parameters;
-        compare_arrays<parameter>(m_parameters.begin(), info.m_parameters.begin(), m_parameters.size());
 }
 
 std::ostream & operator<<(std::ostream & out, decl_info const & info) {
@@ -255,7 +254,8 @@ func_decl_info::func_decl_info(family_id family_id, decl_kind k, unsigned num_pa
     m_injective(false),
     m_idempotent(false),
     m_skolem(false),
-    m_lambda(false) {
+    m_lambda(false),
+    m_polymorphic(false) {
 }
 
 bool func_decl_info::operator==(func_decl_info const & info) const {
@@ -283,6 +283,7 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
     if (info.is_idempotent()) out << " :idempotent ";
     if (info.is_skolem()) out << " :skolem ";
     if (info.is_lambda()) out << " :lambda ";
+    if (info.is_polymorphic()) out << " :polymorphic ";
     return out;
 }
 
@@ -477,15 +478,15 @@ bool compare_nodes(ast const * n1, ast const * n2) {
         return
             q1->get_kind()         == q2->get_kind() &&
             q1->get_num_decls()    == q2->get_num_decls() &&
+            q1->get_expr()         == q2->get_expr() &&
+            q1->get_weight()       == q2->get_weight() &&
+            q1->get_num_patterns() == q2->get_num_patterns() &&
             compare_arrays(q1->get_decl_sorts(),
                            q2->get_decl_sorts(),
                            q1->get_num_decls()) &&
             compare_arrays(q1->get_decl_names(),
                            q2->get_decl_names(),
                            q1->get_num_decls()) &&
-            q1->get_expr()         == q2->get_expr() &&
-            q1->get_weight()       == q2->get_weight() &&
-            q1->get_num_patterns() == q2->get_num_patterns() &&
             ((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) ||
              (q1->get_qid() == q2->get_qid())) && 
             compare_arrays(q1->get_patterns(),
@@ -540,22 +541,6 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v
     } }
 }
 
-unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init) {
-    return ast_array_hash<ast>(ns, sz, init);
-}
-unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init) {
-    return ast_array_hash<app>(ns, sz, init);
-}
-unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init) {
-    return ast_array_hash<expr>(ns, sz, init);
-}
-unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init) {
-    return ast_array_hash<sort>(ns, sz, init);
-}
-unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init) {
-    return ast_array_hash<func_decl>(ns, sz, init);
-}
-
 unsigned get_node_hash(ast const * n) {
     unsigned a, b, c;
 
@@ -1309,10 +1294,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
     m_expr_array_manager(*this, m_alloc),
     m_expr_dependency_manager(*this, m_alloc),
     m_expr_dependency_array_manager(*this, m_alloc),
-    m_proof_mode(m),
+    m_proof_mode(m) {
-    m_trace_stream(nullptr),
-    m_trace_stream_owner(false),
-    m_lambda_def(":lambda-def") {
 
     if (trace_file) {
         m_trace_stream       = alloc(std::fstream, trace_file, std::ios_base::out);
@@ -1333,9 +1315,7 @@ ast_manager::ast_manager(proof_gen_mode m, std::fstream * trace_stream, bool is_
     m_expr_dependency_manager(*this, m_alloc),
     m_expr_dependency_array_manager(*this, m_alloc),
     m_proof_mode(m),
-    m_trace_stream(trace_stream),
+    m_trace_stream(trace_stream) {
-    m_trace_stream_owner(false),
-    m_lambda_def(":lambda-def") {
 
     if (!is_format_manager)
         m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true);
@@ -1350,9 +1330,7 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
     m_expr_dependency_manager(*this, m_alloc),
     m_expr_dependency_array_manager(*this, m_alloc),
     m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode),
-    m_trace_stream(src.m_trace_stream),
+    m_trace_stream(src.m_trace_stream) {
-    m_trace_stream_owner(false),
-    m_lambda_def(":lambda-def") {
     SASSERT(!src.is_format_manager());
     m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true);
     init();
@@ -1880,6 +1858,8 @@ void ast_manager::delete_node(ast * n) {
             break;
         case AST_FUNC_DECL: {
             func_decl* f = to_func_decl(n);
+            if (f->is_polymorphic())
+                m_poly_roots.erase(f);
             if (f->m_info != nullptr) {
                 func_decl_info * info = f->get_info();
                 if (info->is_lambda()) {
@@ -2020,10 +2000,6 @@ sort * ast_manager::mk_uninterpreted_sort(symbol const & name, unsigned num_para
     return plugin->mk_sort(kind, num_parameters, parameters);
 }
 
-sort * ast_manager::mk_type_var(symbol const& name) {
-    sort_info si(poly_family_id, 0);
-    return mk_sort(name, &si);
-}
 
 func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
                                       bool assoc, bool comm, bool inj) {
@@ -2035,13 +2011,30 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort
 }
 
 func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info * info) {
-    SASSERT(arity == 1 || info == 0 || !info->is_injective());
+    SASSERT(arity == 1 || !info || !info->is_injective());
-    SASSERT(arity == 2 || info == 0 || !info->is_associative());
+    SASSERT(arity == 2 || !info || !info->is_associative());
-    SASSERT(arity == 2 || info == 0 || !info->is_commutative());
+    SASSERT(arity == 2 || !info || !info->is_commutative());
     unsigned sz               = func_decl::get_obj_size(arity);
     void * mem                = allocate_node(sz);
+
+    // determine if function is a polymorphic root object.
+    // instances of polymorphic functions are automatically tagged as polymorphic and
+    // inserted into the m_poly_roots table.
+    bool is_polymorphic_root = false;
+    func_decl_info info0;
+    if (has_type_var(arity, domain, range)) {
+        if (!info)
+            info = &info0;
+        if (!info->is_polymorphic()) {
+            info->set_polymorphic(true);
+            is_polymorphic_root = true;
+        }
+    }
     func_decl* new_node = new (mem) func_decl(name, arity, domain, range, info);
-    return register_node(new_node);
+    new_node = register_node(new_node);
+    if (is_polymorphic_root) 
+        m_poly_roots.insert(new_node, new_node);
+    return new_node;
 }
 
 void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
@@ -2306,9 +2299,10 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const
     func_decl_info info(null_family_id, null_decl_kind);
     info.m_skolem = skolem;
     SASSERT(skolem == info.is_skolem());
+    func_decl_info* infop = skolem ? &info : nullptr;
     func_decl * d;
     if (prefix == symbol::null && suffix == symbol::null) {
-        d = mk_func_decl(symbol(m_fresh_id), arity, domain, range, &info);
+        d = mk_func_decl(symbol(m_fresh_id), arity, domain, range, infop);
     }
     else {
         string_buffer<64> buffer;
@@ -2320,10 +2314,10 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const
         if (suffix != symbol::null)
             buffer << suffix << "!";
         buffer << m_fresh_id;
-        d = mk_func_decl(symbol(buffer.c_str()), arity, domain, range, &info);
+        d = mk_func_decl(symbol(buffer.c_str()), arity, domain, range, infop);
     }
     m_fresh_id++;
-    SASSERT(d->get_info());
+    SASSERT(!skolem || d->get_info());
     SASSERT(skolem == d->is_skolem());
     return d;
 }
@@ -2725,6 +2719,49 @@ bool ast_manager::is_fully_interp(sort * s) const {
     return false;
 }
 
+// -----------------------------------------
+// Polymorphism
+// -----------------------------------------
+sort * ast_manager::mk_type_var(symbol const& name) {
+    m_has_type_vars = true;
+    sort_info si(poly_family_id, 0);
+    return mk_sort(name, &si);
+}
+
+bool ast_manager::has_type_var(sort* s) const {
+    if (is_type_var(s))
+        return true;
+    for (parameter const& p : s->parameters()) 
+        if (p.is_ast() && is_sort(p.get_ast()) && has_type_var(to_sort(p.get_ast())))
+            return true;   
+    return false;
+}
+
+bool ast_manager::has_type_var(func_decl* f) const {
+    return has_type_var(f->get_arity(), f->get_domain(), f->get_range());
+}
+
+bool ast_manager::has_type_var(unsigned n, sort* const* domain, sort* range) const {
+    if (!has_type_vars())
+        return false;
+    for (unsigned i = n; i-- > 0; )
+        if (has_type_var(domain[i]))
+            return true;
+    return has_type_var(range);    
+}
+
+/**
+ * \brief create an instantiation of polymorphic function f.
+ */
+
+func_decl* ast_manager::instantiate_polymorphic(func_decl* f, unsigned arity, sort * const* domain, sort * range) {
+    SASSERT(f->is_polymorphic());
+    func_decl* g = mk_func_decl(f->get_name(), arity, domain, range, f->get_info());
+    m_poly_roots.insert(g, f);
+    // SASSERT(g->is_polymorphic());
+    return g;
+}
+
 // -----------------------------------
 //
 // Proof generation
@@ -2847,29 +2884,40 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
     SASSERT(has_fact(p2));
     SASSERT(is_app(get_fact(p1)));
     SASSERT(is_app(get_fact(p2)));
-    SASSERT(to_app(get_fact(p1))->get_num_args() == 2);
+    app* fact1 = to_app(get_fact(p1));
-    SASSERT(to_app(get_fact(p2))->get_num_args() == 2);
+    app* fact2 = to_app(get_fact(p2));
-    CTRACE("mk_transitivity", to_app(get_fact(p1))->get_decl() != to_app(get_fact(p2))->get_decl(),
+    SASSERT(fact1->get_num_args() == 2);
-           tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n";
+    SASSERT(fact2->get_num_args() == 2);
-           tout << mk_pp(to_app(get_fact(p1))->get_decl(), *this) << "\n";
+    CTRACE("mk_transitivity", fact1->get_decl() != fact2->get_decl(),
-           tout << mk_pp(to_app(get_fact(p2))->get_decl(), *this) << "\n";);
+           tout << mk_pp(fact1, *this) << "\n\n" << mk_pp(fact2, *this) << "\n";
-    SASSERT(to_app(get_fact(p1))->get_decl() == to_app(get_fact(p2))->get_decl() ||
+           tout << mk_pp(fact1->get_decl(), *this) << "\n";
-            ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) &&
+           tout << mk_pp(fact2->get_decl(), *this) << "\n";);
-              (is_eq(get_fact(p2)) || is_oeq(get_fact(p2)))));
+    SASSERT(fact1->get_decl() == fact2->get_decl() ||
-    CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0),
+            ( (is_eq(fact1) || is_oeq(fact1)) &&
-           tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n";
+              (is_eq(fact2) || is_oeq(fact2))));
+    CTRACE("mk_transitivity", fact1->get_arg(1) != fact2->get_arg(0),
+           tout << mk_pp(fact1, *this) << "\n\n" << mk_pp(fact2, *this) << "\n";
            tout << p1->get_id() << ": " << mk_bounded_pp(p1, *this, 5) << "\n\n";
            tout << p2->get_id() << ": " << mk_bounded_pp(p2, *this, 5) << "\n\n";
     );
-    SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0));
     if (is_reflexivity(p1))
         return p2;
     if (is_reflexivity(p2))
         return p1;
+    // local fixup to admit inline simplifications of not(not(e)) to e
+    expr* e;
+    if (is_not(fact1->get_arg(1), e) && is_not(e, e) && e == fact2->get_arg(0))
+        p1 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0)));
+    else if (is_not(fact2->get_arg(0), e) && is_not(e, e) && e == fact1->get_arg(1))
+        p1 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0)));
+    else {                                            
+        SASSERT(fact1->get_arg(1) == fact2->get_arg(0));
+    }
     // OEQ is compatible with EQ for transitivity.
-    func_decl* f = to_app(get_fact(p1))->get_decl();
+    func_decl* f = fact1->get_decl();
-    if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl();
+    if (is_oeq(fact2))
-    return  mk_app(basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1)));
+        f = fact2->get_decl();
+    return  mk_app(basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, fact1->get_arg(0), fact2->get_arg(1)));
 
 }
 

src/ast/ast.h

@@ -400,6 +400,7 @@ struct func_decl_info : public decl_info {
     bool m_idempotent:1;
     bool m_skolem:1;
     bool m_lambda:1;
+    bool m_polymorphic:1;
 
     func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
 
@@ -414,6 +415,7 @@ struct func_decl_info : public decl_info {
     bool is_idempotent() const { return m_idempotent; }
     bool is_skolem() const { return m_skolem; }
     bool is_lambda() const { return m_lambda; }
+    bool is_polymorphic() const { return m_polymorphic; }
 
     void set_associative(bool flag = true) { m_left_assoc = flag; m_right_assoc = flag; }
     void set_left_associative(bool flag = true) { m_left_assoc = flag; }
@@ -426,6 +428,7 @@ struct func_decl_info : public decl_info {
     void set_idempotent(bool flag = true) { m_idempotent = flag; }
     void set_skolem(bool flag = true) { m_skolem = flag; }
     void set_lambda(bool flag = true) { m_lambda = flag; }
+    void set_polymorphic(bool flag = true) { m_polymorphic = flag; }
 
     bool operator==(func_decl_info const & info) const;
 
@@ -655,6 +658,7 @@ public:
     bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); }
     bool is_lambda() const { return get_info() != nullptr && get_info()->is_lambda(); }
     bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); }
+    bool is_polymorphic() const { return get_info() != nullptr && get_info()->is_polymorphic(); }
     unsigned get_arity() const { return m_arity; }
     sort * get_domain(unsigned idx) const { SASSERT(idx < get_arity()); return m_domain[idx]; }
     sort * const * get_domain() const { return m_domain; }
@@ -966,11 +970,6 @@ inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n
 unsigned get_node_hash(ast const * n);
 bool compare_nodes(ast const * n1, ast const * n2);
 unsigned get_node_size(ast const * n);
-unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init);
-unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init);
-unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init);
-unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init);
-unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init);
 
 // This is the internal comparison functor for hash-consing AST nodes.
 struct ast_eq_proc {
@@ -1511,13 +1510,15 @@ protected:
     unsigned                  m_fresh_id;
     bool                      m_debug_ref_count;
     u_map<unsigned>           m_debug_free_indices;
-    std::fstream*             m_trace_stream;
+    std::fstream*             m_trace_stream = nullptr;
-    bool                      m_trace_stream_owner;
+    bool                      m_trace_stream_owner = false;
+    bool                      m_has_type_vars = false;
 #ifdef Z3DEBUG
     bool slow_not_contains(ast const * n);
 #endif
     ast_manager *             m_format_manager; // hack for isolating format objects in a different manager.
-    symbol                    m_lambda_def;
+    symbol                    m_lambda_def = symbol(":lambda-def");
+    obj_map<func_decl, func_decl*> m_poly_roots;
 
     void init();
 
@@ -1734,12 +1735,27 @@ public:
 
     bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == user_sort_family_id; }
 
+    bool is_type_var(sort const* s) const { return s->get_family_id() == poly_family_id; }
+
+    bool has_type_vars() const { return m_has_type_vars; }
+
+    func_decl* poly_root(func_decl* f) const { SASSERT(f->is_polymorphic()); return m_poly_roots[f]; }
+
+
+    func_decl* instantiate_polymorphic(func_decl* f, unsigned arity, sort * const* domain, sort * range);
+
     /**
        \brief A sort is "fully" interpreted if it is interpreted,
        and doesn't depend on other uninterpreted sorts.
     */
     bool is_fully_interp(sort * s) const;
 
+    bool has_type_var(sort* s) const;
+
+    bool has_type_var(func_decl* f) const;
+
+    bool has_type_var(unsigned n, sort* const* domain, sort* range) const;
+
     func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
                              unsigned arity, sort * const * domain, sort * range = nullptr);
 

src/ast/ast_translation.cpp

@@ -65,6 +65,13 @@ void ast_translation::collect_decl_extra_children(decl * d) {
 }
 
 void ast_translation::push_frame(ast * n) {
+    // ensure poly roots are pushed first.
+    if (m_from_manager.has_type_vars() && n->get_kind() == AST_FUNC_DECL && to_func_decl(n)->is_polymorphic()) {
+        func_decl* g = m_from_manager.poly_root(to_func_decl(n));
+        if (n != g && m_cache.contains(g)) {
+            m_frame_stack.push_back(frame(n, 0, m_extra_children_stack.size(), m_result_stack.size()));
+        }
+    }
     m_frame_stack.push_back(frame(n, 0, m_extra_children_stack.size(), m_result_stack.size()));
     switch (n->get_kind()) {
     case AST_SORT:
@@ -153,6 +160,10 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
                                           new_domain,
                                           new_range);
     }
+    else if (f->is_polymorphic() && m_from_manager.poly_root(f) != f) {
+        func_decl* fr = to_func_decl(m_cache[m_from_manager.poly_root(f)]);
+        new_f = m_to_manager.instantiate_polymorphic(fr, f->get_arity(), new_domain, new_range);
+    }
     else {
         buffer<parameter> ps;
         copy_params(f, fr.m_rpos, ps);

src/ast/converters/model_converter.cpp

@@ -24,7 +24,8 @@ Notes:
  * Add or overwrite value in model.
  */
 void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
-    VERIFY(e);
+    if (!e)
+        return;
     VERIFY(f->get_range() == e->get_sort());
     ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
 }

src/ast/euf/euf_egraph.cpp

@@ -39,8 +39,10 @@ namespace euf {
         }
         m_expr2enode.setx(f->get_id(), n, nullptr);
         push_node(n);
-        for (unsigned i = 0; i < num_args; ++i) 
+        for (unsigned i = 0; i < num_args; ++i) {
             set_cgc_enabled(args[i], true);      
+            args[i]->get_root()->set_is_shared(l_undef);
+        }                       
         return n;
     }
 
@@ -70,7 +72,7 @@ namespace euf {
     }
 
     enode_bool_pair egraph::insert_table(enode* p) {
-        TRACE("euf", tout << bpp(p) << "\n");
+        TRACE("euf", tout << "insert_table " << bpp(p) << "\n");
         //SASSERT(!m_table.contains_ptr(p));
         auto rc = m_table.insert(p);
         p->m_cg = rc.first;
@@ -84,7 +86,12 @@ namespace euf {
     void egraph::reinsert_equality(enode* p) {
         SASSERT(p->is_equality());        
         if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) 
-            add_literal(p, nullptr);
+            queue_literal(p, nullptr);
+    }
+
+    void egraph::queue_literal(enode* p, enode* ante) {        
+        if (m_on_propagate_literal)
+            m_to_merge.push_back(to_merge(p, ante));
     }
 
     void egraph::force_push() {
@@ -128,8 +135,7 @@ namespace euf {
         if (n2 == n) 
             update_children(n);        
         else 
-            push_merge(n, n2, justification::congruence(comm, 0));
+            push_merge(n, n2, comm);
-        // merge(n, n2, justification::congruence(comm, m_congruence_timestamp++));
     
         return n;
     }
@@ -145,18 +151,9 @@ namespace euf {
             memory::deallocate(m_tmp_node);
     }
 
-    void egraph::add_plugins() {
+    void egraph::add_plugin(plugin* p) {
-        if (!m_plugins.empty())
-            return;
-
-        auto insert = [&](plugin* p) {
         m_plugins.reserve(p->get_id() + 1);
         m_plugins.set(p->get_id(), p);       
-        };
-
-        insert(alloc(bv_plugin, *this));
-        insert(alloc(arith_plugin, *this));
-        insert(alloc(specrel_plugin, *this));
     }
 
     void egraph::propagate_plugins() {
@@ -188,28 +185,24 @@ namespace euf {
     }
 
     void egraph::add_literal(enode* n, enode* ante) {
+        TRACE("euf", tout << "propagate " << bpp(n) << " " << bpp(ante) << "\n");
         if (!m_on_propagate_literal)
             return;
         if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
         if (!ante)
             m_on_propagate_literal(n, ante);
         else if (m.is_true(ante->get_expr()) || m.is_false(ante->get_expr())) {
-            for (enode* k : enode_class(n)) {
+            for (enode* k : enode_class(n)) 
-                if (k != ante) {
+                if (k != ante) 
-                    //verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
                     m_on_propagate_literal(k, ante);           
         }
-            }
-        }
         else {
             for (enode* k : enode_class(n)) {
-                if (k->value() != ante->value()) {
+                if (k->value() != ante->value()) 
-                    //verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
                     m_on_propagate_literal(k, ante);                
             }
         }
     }
-    }
 
     void egraph::new_diseq(enode* n) {
         SASSERT(n->is_equality());
@@ -516,6 +509,7 @@ namespace euf {
             c->m_root = r2;
         std::swap(r1->m_next, r2->m_next);
         r2->inc_class_size(r1->class_size());   
+        r2->set_is_shared(l_undef);
         merge_th_eq(r1, r2, j);
         reinsert_parents(r1, r2);
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
@@ -532,6 +526,7 @@ namespace euf {
 
     void egraph::remove_parents(enode* r) {
         TRACE("euf", tout << bpp(r) << "\n");
+        SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
         for (enode* p : enode_parents(r)) {
             if (p->is_marked1())
                 continue;
@@ -558,7 +553,7 @@ namespace euf {
             if (p->cgc_enabled()) {
                 auto [p_other, comm] = insert_table(p);
                 SASSERT(m_table.contains_ptr(p) == (p_other == p));
-                TRACE("euf", tout << "other " << bpp(p_other) << "\n";);
+                CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
                 if (p_other != p) 
                     m_to_merge.push_back(to_merge(p_other, p, comm));                
                 else
@@ -594,6 +589,7 @@ namespace euf {
         enode* r2 = r1->get_root();
         TRACE("euf", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
         r2->dec_class_size(r1->class_size());
+        r2->set_is_shared(l_undef);
         std::swap(r1->m_next, r2->m_next);
         auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents();
         for (auto it = begin; it != end; ++it) {
@@ -615,18 +611,29 @@ namespace euf {
         unmerge_justification(n1);
     }
 
+
     bool egraph::propagate() {
         force_push();
+        unsigned i = 0;
+        bool change = true;
+        while (change) {
+            change = false;
             propagate_plugins();
-        for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
+            for (; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
                 auto const& w = m_to_merge[i];
-            if (w.j.is_congruence())
+                switch (w.t) {
-                merge(w.a, w.b, justification::congruence(w.j.is_commutative(), m_congruence_timestamp++));
+                case to_merge_plain:
-            else
+                case to_merge_comm:
+                    merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++));
+                    break;
+                case to_justified:
                     merge(w.a, w.b, w.j);
-            
+                    break;
-            if (i + 1 == m_to_merge.size())
+                case to_add_literal:
-                propagate_plugins();
+                    add_literal(w.a, w.b);
+                    break;
+                }                
+            }
         }
         m_to_merge.reset();
         return 
@@ -642,7 +649,7 @@ namespace euf {
         m_updates.push_back(update_record(false, update_record::inconsistent()));
         m_n1 = n1;
         m_n2 = n2;
-        TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << "\n");
+        TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << " " << n1->get_root()->value() << " " << n2->get_root()->value() << "\n");
         m_justification = j;
     }
 

src/ast/euf/euf_egraph.h

@@ -88,11 +88,15 @@ namespace euf {
 
         typedef ptr_vector<trail> trail_stack;
 
+        enum to_merge_t { to_merge_plain, to_merge_comm, to_justified, to_add_literal };
         struct to_merge {
             enode* a, * b;
+            to_merge_t t;
             justification j;
-            to_merge(enode* a, enode* b, bool c) : a(a), b(b), j(justification::congruence(c, 0)) {}
+            bool commutativity() const { return t == to_merge_comm; }
-            to_merge(enode* a, enode* b, justification j) : a(a), b(b), j(j) {}
+            to_merge(enode* a, enode* b, bool c) : a(a), b(b), t(c ? to_merge_comm : to_merge_plain) {}
+            to_merge(enode* a, enode* b, justification j): a(a), b(b), t(to_justified), j(j) {}
+            to_merge(enode* p, enode* ante): a(p), b(ante), t(to_add_literal) {}
         };
 
         struct stats {
@@ -215,6 +219,7 @@ namespace euf {
         // plugin related methods
         void push_plugin_undo(unsigned th_id) { m_updates.push_back(update_record(th_id, update_record::plugin_undo())); }
         void push_merge(enode* a, enode* b, justification j) { m_to_merge.push_back({ a, b, j }); }
+        void push_merge(enode* a, enode* b, bool comm) { m_to_merge.push_back({ a, b, comm }); }
         void propagate_plugins();
 
         void add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r);
@@ -222,6 +227,7 @@ namespace euf {
         void add_th_diseqs(theory_id id, theory_var v1, enode* r);
         bool th_propagates_diseqs(theory_id id) const;
         void add_literal(enode* n, enode* ante);
+        void queue_literal(enode* n, enode* ante);
         void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents);
         void undo_add_th_var(enode* n, theory_id id);
         enode* mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args);
@@ -256,8 +262,10 @@ namespace euf {
     public:
         egraph(ast_manager& m);
         ~egraph();
-        void add_plugins();
+
+        void add_plugin(plugin* p);
         plugin* get_plugin(family_id fid) const { return m_plugins.get(fid, nullptr); }
+
         enode* find(expr* f) const { return m_expr2enode.get(f->get_id(), nullptr); }
         enode* find(expr* f, unsigned n, enode* const* args);
         enode* mk(expr* f, unsigned generation, unsigned n, enode *const* args);
@@ -284,6 +292,7 @@ namespace euf {
            of new equalities.
         */
         bool propagate();
+        bool can_propagate() const { return !m_to_merge.empty(); }
         bool inconsistent() const { return m_inconsistent; }
 
         /**

src/ast/euf/euf_enode.h

@@ -52,6 +52,7 @@ namespace euf {
         bool          m_merge_tf_enabled = false;
         bool          m_is_equality = false;    // Does the expression represent an equality
         bool          m_is_relevant = false;
+        lbool         m_is_shared = l_undef;
         lbool         m_value = l_undef;        // Assignment by SAT solver for Boolean node
         sat::bool_var m_bool_var = sat::null_bool_var;    // SAT solver variable associated with Boolean node
         unsigned      m_class_size = 1;         // Size of the equivalence class if the enode is the root.
@@ -96,6 +97,7 @@ namespace euf {
             for (unsigned i = 0; i < num_args; ++i) {
                 SASSERT(to_app(f)->get_arg(i) == args[i]->get_expr());
                 n->m_args[i] = args[i];
+                n->m_args[i]->get_root()->set_is_shared(l_undef);
             }
             return n;
         }
@@ -181,6 +183,9 @@ namespace euf {
         void unmark3() { m_mark3 = false; }
         bool is_marked3() { return m_mark3; }
 
+        lbool is_shared() const { return m_is_shared; }
+        void set_is_shared(lbool s) { m_is_shared = s; }
+
         template<bool m> void mark1_targets() {
             enode* n = this;
             while (n) {

src/ast/euf/euf_etable.cpp

@@ -237,6 +237,8 @@ namespace euf {
             UNTAG(table*, t)->erase(n);
             break;
         }
+        CTRACE("euf", contains_ptr(n), display(tout));
+        SASSERT(!contains_ptr(n));
     }
 
     bool etable::contains(enode* n) const {

src/ast/for_each_expr.cpp

@@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) {
 
 subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {}
 subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); }
-subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
+subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); }
-subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
+subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); }
-subterms::iterator::iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
+subterms::iterator::iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
     if (!esp)
         m_esp = &m_es;
     else

src/ast/for_each_expr.h

@@ -186,7 +186,7 @@ public:
         expr_mark         m_visited;   
         expr_mark*        m_visitedp = nullptr;
     public:
-        iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
+        iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
         expr* operator*();
         iterator operator++(int);
         iterator& operator++();
@@ -198,8 +198,8 @@ public:
     static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
     static subterms all(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
     static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
-    iterator begin();
+    iterator begin() const;
-    iterator end();
+    iterator end() const;
 };
 
 class subterms_postorder {

src/ast/fpa/bv2fpa_converter.cpp

@@ -508,7 +508,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
         }
     }
 
-    TRACE("bv2fpa", tout << "Target model: " << *target_model; );
+    TRACE("bv2fpa", tout << "Target model: " << *target_model << std::endl; );
 }
 
 void bv2fpa_converter::display(std::ostream & out) {

src/ast/fpa/fpa2bv_converter.cpp

@@ -147,36 +147,11 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a
 
 void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 0);
-    sort* s = f->get_range();
-    if (f->get_num_parameters() == 1) {
-        SASSERT(f->get_parameter(0).is_external());
-        unsigned p_id = f->get_parameter(0).get_ext_id();
-        mpf const& v = m_plugin->get_value(p_id);
-        mk_numeral(s, v, result);
-        return;
-    }
     scoped_mpf v(m_mpf_manager);
-    unsigned ebits = m_util.get_ebits(s), sbits = m_util.get_sbits(s);
+    expr_ref a(m);
-    switch (f->get_decl_kind()) {
+    a = m.mk_app(f, num, args);
-    case OP_FPA_PLUS_INF:
+    m_util.is_numeral(a, v);
-        m_util.fm().mk_pinf(ebits, sbits, v);
+    mk_numeral(f->get_range(), v, result);
-        break;
-    case OP_FPA_MINUS_INF:
-        m_util.fm().mk_ninf(ebits, sbits, v);
-        break;
-    case OP_FPA_NAN:        
-        m_util.fm().mk_nan(ebits, sbits, v);
-        break;
-    case OP_FPA_PLUS_ZERO:
-        m_util.fm().mk_pzero(ebits, sbits, v);
-        break;
-    case OP_FPA_MINUS_ZERO:
-        m_util.fm().mk_nzero(ebits, sbits, v);
-        break;
-    default:
-        UNREACHABLE();
-    }
-    mk_numeral(s, v, result);
 }
 
 void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
@@ -941,8 +916,8 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
     dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos);
     dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf);
 
-    expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
+    expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m), c8(m);
-    expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
+    expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m), v9(m);
 
     // (x is NaN) || (y is NaN) -> NaN
     m_simp.mk_or(x_is_nan, y_is_nan, c1);
@@ -998,6 +973,9 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
     a_sig_ext = m_bv_util.mk_concat(a_sig, m_bv_util.mk_numeral(0, sbits + extra_bits));
     b_sig_ext = m_bv_util.mk_zero_extend(sbits + extra_bits, b_sig);
 
+    dbg_decouple("fpa2bv_div_a_sig_ext", a_sig_ext);
+    dbg_decouple("fpa2bv_div_b_sig_ext", b_sig_ext);
+
     expr_ref a_exp_ext(m), b_exp_ext(m);
     a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
     b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
@@ -1017,14 +995,21 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
     expr_ref quotient(m);
     // b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
     quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext);
-
     dbg_decouple("fpa2bv_div_quotient", quotient);
 
     SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits));
 
-    expr_ref sticky(m);
+    expr_ref sticky(m), upper(m), upper_reduced(m), too_large(m);
     sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient));
     res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky);
+    upper = m_bv_util.mk_extract(sbits + sbits + extra_bits-1, extra_bits+sbits+2, quotient);
+    upper_reduced = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, upper.get());
+    too_large = m.mk_eq(upper_reduced, m_bv_util.mk_numeral(1, 1));
+    c8 = too_large;
+    mk_ite(signs_xor, ninf, pinf, v8);
+    dbg_decouple("fpa2bv_div_res_sig_p4", res_sig);
+    dbg_decouple("fpa2bv_div_upper", upper);
+    dbg_decouple("fpa2bv_div_too_large", too_large);
 
     SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
 
@@ -1042,10 +1027,14 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
     m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
     m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
 
-    round(s, rm, res_sgn, res_sig, res_exp, v8);
+    dbg_decouple("fpa2bv_div_res_sig", res_sig);
+    dbg_decouple("fpa2bv_div_res_exp", res_exp);
+
+    round(s, rm, res_sgn, res_sig, res_exp, v9);
 
     // And finally, we tie them together.
-    mk_ite(c7, v7, v8, result);
+    mk_ite(c8, v8, v9, result);
+    mk_ite(c7, v7, result, result);
     mk_ite(c6, v6, result, result);
     mk_ite(c5, v5, result, result);
     mk_ite(c4, v4, result, result);
@@ -2809,8 +2798,46 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
 
         expr * e = m.mk_eq(m_util.mk_to_real(result), x);
         m_extra_assertions.push_back(e);
-        // x = 0 -> result = 0+
+
-        m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_eq(result, m_util.mk_pzero(result->get_sort()))));
+        expr_ref r_is_nan(m);
+        mk_is_nan(result, r_is_nan);
+        m_extra_assertions.push_back(m.mk_not(r_is_nan));
+
+        rational min_real, max_real;
+        const mpz& max_exp_z = m_mpf_manager.m_powers2.m1(ebits-1);
+        SASSERT(m_mpz_manager.is_uint(max_exp_z));
+        unsigned max_exp = m_mpz_manager.get_uint(max_exp_z);
+        rational max_sig = m_mpf_manager.m_powers2.m1(sbits) / m_mpf_manager.m_powers2(sbits-1);
+        max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp));
+        TRACE("fpa2bv_to_real", tout << "max exp: " << max_exp << " max real: " << max_real << std::endl;);
+
+        expr_ref r_is_pinf(m), r_is_ninf(m);
+        mk_is_pinf(result, r_is_pinf);
+        mk_is_ninf(result, r_is_ninf);
+
+        expr_ref e_max_real(m), e_max_real_neg(m);
+        e_max_real = m_arith_util.mk_numeral(max_real, false);
+        e_max_real_neg = m_arith_util.mk_numeral(-max_real, false);
+
+        expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
+        mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_nta);
+        mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_nte);
+        mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_tp);
+        mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn);
+        mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz);
+
+        expr_ref implies_gt_max_real(m), implies_lt_min_real(m);
+        implies_gt_max_real = m.mk_implies(r_is_pinf, m.mk_and(rm_tp, m_arith_util.mk_gt(x, e_max_real)));
+        implies_lt_min_real = m.mk_implies(r_is_ninf, m.mk_and(rm_tn, m_arith_util.mk_lt(x, e_max_real_neg)));
+
+        m_extra_assertions.push_back(implies_gt_max_real);
+        m_extra_assertions.push_back(implies_lt_min_real);
+
+        // x = 0 -> result = +0/-0
+        expr_ref pzero(m), nzero(m);
+        mk_pzero(result->get_sort(), pzero);
+        mk_nzero(result->get_sort(), nzero);
+        m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_or(m.mk_eq(result, pzero), m.mk_eq(result, nzero))));
     }
 
     SASSERT(is_well_sorted(m, result));
@@ -2854,19 +2881,13 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
         m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, e.to_mpq().numerator(), q.to_mpq());
         m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, e.to_mpq().numerator(), q.to_mpq());
 
-        app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
-        a_nte = m_plugin->mk_numeral(nte);
-        a_nta = m_plugin->mk_numeral(nta);
-        a_tp = m_plugin->mk_numeral(tp);
-        a_tn = m_plugin->mk_numeral(tn);
-        a_tz = m_plugin->mk_numeral(tz);
-
         expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
-        mk_numeral(a_nte->get_decl(), 0, nullptr, bv_nte);
+        sort *s = f->get_range();
-        mk_numeral(a_nta->get_decl(), 0, nullptr, bv_nta);
+        mk_numeral(s, nte, bv_nte);
-        mk_numeral(a_tp->get_decl(), 0, nullptr, bv_tp);
+        mk_numeral(s, nta, bv_nta);
-        mk_numeral(a_tn->get_decl(), 0, nullptr, bv_tn);
+        mk_numeral(s, tp, bv_tp);
-        mk_numeral(a_tz->get_decl(), 0, nullptr, bv_tz);
+        mk_numeral(s, tn, bv_tn);
+        mk_numeral(s, tz, bv_tz);
 
         expr_ref c1(m), c2(m), c3(m), c4(m);
         c1 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3));
@@ -3003,27 +3024,34 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
     unsigned bv_sz = m_bv_util.get_bv_size(x);
     SASSERT(m_bv_util.get_bv_size(rm) == 3);
 
+    expr_ref rm_is_to_neg(m);
+    mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
+
     expr_ref bv1_1(m), bv0_sz(m);
     bv1_1 = m_bv_util.mk_numeral(1, 1);
     bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
 
-    expr_ref is_zero(m), pzero(m);
+    expr_ref is_zero(m), pzero(m), nzero(m);
     is_zero = m.mk_eq(x, bv0_sz);
     mk_pzero(f, pzero);
+    mk_nzero(f, nzero);
 
-    // Special case: x == 0 -> p/n zero
+    // Special case: x == 0 -> +zero
     expr_ref c1(m), v1(m);
     c1 = is_zero;
-    v1 = pzero;
+    v1 = pzero; // No -zero (IEEE754)
 
     // Special case: x != 0
-    expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
+    expr_ref sign_bit(m), exp_too_large(m), sig_4(m), exp_2(m), rest(m);
     expr_ref is_neg(m), x_abs(m), neg_x(m);
-    is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
+    sign_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
-    is_neg = m.mk_eq(is_neg_bit, bv1_1);
+    rest = m_bv_util.mk_extract(bv_sz - 2, 0, x);
-    neg_x = m_bv_util.mk_bv_neg(x); // overflow problem?
+    dbg_decouple("fpa2bv_to_fp_signed_rest", rest);
+    is_neg = m.mk_eq(sign_bit, bv1_1);
+    neg_x = m_bv_util.mk_bv_neg(x); // overflow ok, x_abs is now unsigned.
     x_abs = m.mk_ite(is_neg, neg_x, x);
     dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg);
+    dbg_decouple("fpa2bv_to_fp_signed_x_abs", x_abs);
     // x_abs has an extra bit in the front.
     // x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2)
     // bv_sz-2 is the "1.0" bit for the rounder.
@@ -3075,7 +3103,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
 
     TRACE("fpa2bv_to_fp_signed", tout << "exp worst case sz: " << exp_worst_case_sz << std::endl;);
 
-    if (exp_sz < exp_worst_case_sz) {
+    if (exp_sz <= exp_worst_case_sz) {
         // exp_sz < exp_worst_case_sz and exp >= 0.
         // Take the maximum legal exponent; this
         // allows us to keep the most precision.
@@ -3093,7 +3121,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
     dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large);
 
     expr_ref sgn(m), sig(m), exp(m);
-    sgn = is_neg_bit;
+    sgn = sign_bit;
     sig = sig_4;
     exp = exp_2;
 
@@ -3132,6 +3160,9 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
     rm = to_app(args[0])->get_arg(0);
     x = args[1];
 
+    expr_ref rm_is_to_neg(m);
+    mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
+
     dbg_decouple("fpa2bv_to_fp_unsigned_x", x);
 
     unsigned ebits = m_util.get_ebits(f->get_range());
@@ -3143,14 +3174,15 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
     bv0_1 = m_bv_util.mk_numeral(0, 1);
     bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
 
-    expr_ref is_zero(m), pzero(m);
+    expr_ref is_zero(m), pzero(m), nzero(m);
     is_zero = m.mk_eq(x, bv0_sz);
     mk_pzero(f, pzero);
+    mk_nzero(f, nzero);
 
-    // Special case: x == 0 -> p/n zero
+    // Special case: x == 0 -> +zero
     expr_ref c1(m), v1(m);
     c1 = is_zero;
-    v1 = pzero;
+    v1 = pzero; // No -zero (IEEE754)
 
     // Special case: x != 0
     expr_ref exp_too_large(m), sig_4(m), exp_2(m);
@@ -3194,7 +3226,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
     unsigned exp_sz = ebits + 2; // (+2 for rounder)
     exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp);
     // the remaining bits are 0 if ebits is large enough.
-    exp_too_large = m.mk_false(); // This is always in range.
+    exp_too_large = m.mk_false();
 
                                   // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
                                   // exp < bv_sz (+sign bit which is [0])

src/ast/fpa/fpa2bv_converter.h

@@ -208,6 +208,7 @@ protected:
 
 private:
     void mk_nan(sort * s, expr_ref & result);
+
     void mk_nzero(sort * s, expr_ref & result);
     void mk_pzero(sort * s, expr_ref & result);
     void mk_zero(sort * s, expr_ref & sgn, expr_ref & result);

src/ast/normal_forms/elim_term_ite.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/rewriter/rewriter_def.h"
 
 br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) {
     if (!m.is_term_ite(f)) {
@@ -38,3 +39,4 @@ br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const*
     return BR_DONE;
 }
 
+template class rewriter_tpl<elim_term_ite_cfg>;

src/ast/normal_forms/nnf.cpp

@@ -28,6 +28,7 @@ Notes:
 #include "ast/rewriter/var_subst.h"
 #include "ast/normal_forms/name_exprs.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include <array>
 
 /**
@@ -149,7 +150,7 @@ class skolemizer {
         p = nullptr;
         if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 
-                p = m.mk_skolemization(mk_not(m, q), m.mk_not(r));
+                p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
             else
                 p = m.mk_skolemization(q, r);
         }

src/ast/occurs.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include "ast/occurs.h"
 
 #include "ast/for_each_expr.h"
+#include "ast/for_each_ast.h"
 
 // -----------------------------------
 //
@@ -49,6 +50,15 @@ namespace {
         void operator()(quantifier const * n) { }
     };
 
+
+    struct sort_proc {
+        sort* m_s;
+        sort_proc(sort* s) :m_s(s) {}
+        void operator()(sort const* s2) { if (m_s == s2) throw found(); }
+        void operator()(ast*) {}
+    };
+
+
 }
 
 // Return true if n1 occurs in n2
@@ -74,6 +84,17 @@ bool occurs(func_decl * d, expr * n) {
     return false;
 }
 
+bool occurs(sort* s1, sort* s2) {
+    sort_proc p(s1);
+    try {
+        for_each_ast(p, s2, true);
+    }
+    catch (const found&) {
+        return true;
+    }
+    return false;
+}
+
 void mark_occurs(ptr_vector<expr>& to_check, expr* v, expr_mark& occ) {
     expr_fast_mark2 visited;
     occ.mark(v, true);

src/ast/occurs.h

@@ -31,6 +31,11 @@ bool occurs(expr * n1, expr * n2);
 */
 bool occurs(func_decl * d, expr * n);
 
+/**
+* \brief Return true if s1 occurs in s2
+*/
+bool occurs(sort* s1, sort* s2);
+
 /**
 * \brief Mark sub-expressions of to_check by whether v occurs in these.
 */

src/ast/pattern/CMakeLists.txt

@@ -7,7 +7,7 @@ if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h")
 endif()
 
 add_custom_command(OUTPUT "database.h"
-  COMMAND "${PYTHON_EXECUTABLE}"
+  COMMAND "${Python3_EXECUTABLE}"
           "${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py"
           "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
           "${CMAKE_CURRENT_BINARY_DIR}/database.h"

src/ast/pattern/pattern_inference.cpp

@@ -624,9 +624,11 @@ bool pattern_inference_cfg::reduce_quantifier(
     proof_ref & result_pr) {
 
     TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
-    if (!is_forall(q)) {
+    if (!m_params.m_pi_enabled)
+        return false;
+
+    if (!is_forall(q)) 
         return false;
-    }
 
     int weight = q->get_weight();
 
@@ -653,9 +655,8 @@ bool pattern_inference_cfg::reduce_quantifier(
         }
     }
 
-    if (q->get_num_patterns() > 0) {
+    if (q->get_num_patterns() > 0) 
         return false;
-    }
 
     if (m_params.m_pi_nopat_weight >= 0)
         weight = m_params.m_pi_nopat_weight;

src/ast/polymorphism_inst.cpp

@@ -0,0 +1,139 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    polymorphism_inst.cpp
+
+Abstract:
+
+    Utilities for instantiating polymorphic assertions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2023-7-8
+
+
+--*/
+#include "ast/polymorphism_inst.h"
+#include "ast/ast_pp.h"
+
+namespace polymorphism {
+    
+    void inst::add(expr* e) {
+        if (!m.has_type_vars())
+            return;
+
+        if (m_from_instantiation.contains(e))
+            return;
+
+        instances inst;
+        u.collect_poly_instances(e, inst.m_poly_fns);
+        if (inst.m_poly_fns.empty())
+            return;
+        if (m_instances.contains(e))
+            return;
+        
+        add_instantiations(e, inst.m_poly_fns);
+
+        if (!u.has_type_vars(e))
+            return;
+        
+        // insert e into the occurs list for polymorphic roots
+        ast_mark seen;
+        for (auto* f : inst.m_poly_fns) {
+            f = m.poly_root(f);
+            if (seen.is_marked(f))
+                continue;
+            seen.mark(f, true);
+            if (!m_occurs.contains(f)) {
+                m_occurs.insert(f, ptr_vector<expr>());
+                t.push(insert_map(m_occurs, f));
+            }
+            auto& es = m_occurs.find(f);
+            es.push_back(e);
+            t.push(remove_back(m_occurs, f));
+        }
+        m_assertions.push_back(e);
+        t.push(push_back_vector(m_assertions));
+        u.collect_type_vars(e, inst.m_tvs);
+        inst.m_subst = alloc(substitutions);
+        inst.m_subst->insert(alloc(substitution, m));
+        m_instances.insert(e, inst);            
+        t.push(new_obj_trail(inst.m_subst));
+        t.push(insert_map(m_instances, e));        
+    }
+
+    void inst::collect_instantiations(expr* e) {
+        ptr_vector<func_decl> instances;
+        u.collect_poly_instances(e, instances);
+        add_instantiations(e, instances);
+    }
+
+    void inst::add_instantiations(expr* e, ptr_vector<func_decl> const& instances) {
+        for (auto* f : instances) {
+            if (m_in_decl_queue.is_marked(f))
+                continue;
+            m_in_decl_queue.mark(f, true);
+            m_decl_queue.push_back(f);
+            t.push(add_decl_queue(*this));
+        }
+    }
+    
+    void inst::instantiate(vector<instantiation>& instances) {
+        unsigned num_decls = m_decl_queue.size();
+        if (m_assertions_qhead < m_assertions.size()) {
+            t.push(value_trail(m_assertions_qhead));
+            for (; m_assertions_qhead < m_assertions.size(); ++m_assertions_qhead) {
+                expr* e = m_assertions.get(m_assertions_qhead);
+                for (unsigned i = 0; i < num_decls; ++i)
+                    instantiate(m_decl_queue.get(i), e, instances);
+            }
+        }       
+        if (m_decl_qhead < num_decls) {
+            t.push(value_trail(m_decl_qhead));
+            for (; m_decl_qhead < num_decls; ++m_decl_qhead) {
+                func_decl* p = m_decl_queue.get(m_decl_qhead);
+                for (expr* e : m_occurs[m.poly_root(p)])
+                    instantiate(p, e, instances);
+            }
+        }
+    }
+
+    void inst::instantiate(func_decl* f1, expr* e, vector<instantiation>& instances) {
+        auto const& [tv, fns, substs] = m_instances[e];
+                
+        for (auto* f2 : fns) {
+            substitution sub1(m), new_sub(m);
+            if (!u.unify(f1, f2, sub1))
+                continue;
+            if (substs->contains(&sub1))
+                continue;
+            substitutions new_substs;
+            for (auto* sub2 : *substs) {
+                if (!u.unify(sub1, *sub2, new_sub))
+                    continue;
+                if (substs->contains(&new_sub))
+                    continue;
+                if (new_substs.contains(&new_sub))
+                    continue;
+                expr_ref e_inst = new_sub(e);
+                if (!m_from_instantiation.contains(e_inst)) {
+                    collect_instantiations(e_inst);
+                    auto* new_sub1 = alloc(substitution, new_sub);
+                    instances.push_back(instantiation(e, e_inst, new_sub1));
+                    new_substs.insert(new_sub1);
+                    m_from_instantiation.insert(e_inst);
+                    m.inc_ref(e_inst);
+                    t.push(insert_ref_map(m, m_from_instantiation, e_inst));
+                }
+            }
+            for (auto* sub2 : new_substs) {
+                SASSERT(!substs->contains(sub2));
+                substs->insert(sub2);
+                t.push(new_obj_trail(sub2));
+                t.push(insert_map(*substs, sub2));
+            }
+        }        
+    }
+}

src/ast/polymorphism_inst.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    polymorphism_inst.h
+
+Abstract:
+
+    Utilities for instantiating polymorphic assertions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2023-7-8
+
+
+--*/
+#pragma once
+
+#include "util/trail.h"
+#include "ast/ast.h"
+#include "ast/polymorphism_util.h"
+
+namespace polymorphism {
+    
+    struct instantiation {
+        expr* orig;
+        expr_ref inst;
+        substitution* sub;
+        instantiation(expr* orig, expr_ref& inst, substitution* s):
+            orig(orig), inst(inst), sub(s) {}
+    };
+    
+    class inst {
+        ast_manager& m;
+        trail_stack& t;
+        util u;
+        
+        struct instances {
+            ptr_vector<sort>               m_tvs;
+            ptr_vector<func_decl>          m_poly_fns;
+            substitutions*                 m_subst = nullptr;
+        };
+        
+        func_decl_ref_vector m_poly_roots;
+        obj_map<func_decl, ptr_vector<expr>> m_occurs;
+        obj_map<expr, instances>      m_instances;
+        func_decl_ref_vector          m_decl_queue;
+        unsigned                      m_decl_qhead = 0;
+        ast_mark                      m_in_decl_queue;
+        expr_ref_vector               m_assertions;
+        unsigned                      m_assertions_qhead = 0;
+        obj_hashtable<expr>           m_from_instantiation;
+                
+        struct add_decl_queue : public trail {
+            inst& i;
+            add_decl_queue(inst& i): i(i) {}
+            void undo() override {
+                i.m_in_decl_queue.mark(i.m_decl_queue.back(), false);
+                i.m_decl_queue.pop_back();
+            };
+        };
+
+        struct remove_back : public trail {
+            obj_map<func_decl, ptr_vector<expr>>& occ;
+            func_decl* f;
+            remove_back(obj_map<func_decl, ptr_vector<expr>>& occ, func_decl* f):
+                occ(occ), f(f) {}
+            void undo() override {
+                occ.find(f).pop_back();
+            }
+        };
+
+        void instantiate(func_decl* p, expr* e, vector<instantiation>& instances);
+
+        void collect_instantiations(expr* e);
+
+        void add_instantiations(expr* e, ptr_vector<func_decl> const& insts);
+
+    public:
+        inst(ast_manager& m, trail_stack& t):
+            m(m), t(t), u(m), m_poly_roots(m), m_decl_queue(m), m_assertions(m) {}
+        
+        void add(expr* e);
+        
+        void instantiate(vector<instantiation>& instances);
+
+        bool pending() const { return m_decl_qhead < m_decl_queue.size() || m_assertions_qhead < m_assertions.size(); }
+        
+    };
+}

src/ast/polymorphism_util.cpp

@@ -0,0 +1,353 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    polymorphism_util.cpp
+
+Abstract:
+
+    Utilities for supporting polymorphic type signatures.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2023-7-8
+
+--*/
+
+#include "ast/polymorphism_util.h"
+#include "ast/for_each_ast.h"
+#include "ast/occurs.h"
+#include "ast/ast_pp.h"
+
+namespace polymorphism {
+
+    sort_ref_vector substitution::operator()(sort_ref_vector const& s) {
+        sort_ref_vector r(m);
+        for (auto* srt : s)
+            r.push_back((*this)(srt));
+        return r;
+    }
+    
+    sort_ref substitution::operator()(sort* s) {
+        if (!m.has_type_var(s))
+            return sort_ref(s, m);
+        if (s->is_type_var()) {
+            if (m_sub.find(s, s))
+                return (*this)(s);
+            return sort_ref(s, m);
+        }
+        unsigned n = s->get_num_parameters();
+        vector<parameter> ps;
+        for (unsigned i = 0; i < n; ++i) {
+            auto p = s->get_parameter(i);
+            if (p.is_ast() && is_sort(p.get_ast())) {
+                sort_ref s = (*this)(to_sort(p.get_ast()));
+                ps.push_back(parameter(s.get()));
+            }
+            else
+                ps.push_back(p);
+        }
+        sort_info si(s->get_family_id(), s->get_decl_kind(), n, ps.data(), s->private_parameters());
+        return sort_ref(m.mk_sort(s->get_name(), si), m);
+    }
+    
+    expr_ref substitution::operator()(expr* e) {
+        ptr_vector<expr> todo;
+        expr_ref_vector result(m);
+        todo.push_back(e);
+        auto in_cache = [&](expr* a) {
+            return result.size() > a->get_id() && result.get(a->get_id());
+        };
+        ptr_buffer<expr> args;
+        sort_ref_buffer domain(m);
+        while (!todo.empty()) {
+            expr* a = todo.back();
+            if (in_cache(a)) {
+                todo.pop_back();
+                continue;
+            }
+            if (is_var(a)) {
+                if (m.has_type_var(a->get_sort())) 
+                    result.setx(a->get_id(), m.mk_var(to_var(a)->get_idx(), (*this)(a->get_sort())));                
+                else
+                    result.setx(a->get_id(), a);                
+                todo.pop_back();
+            }
+            else if (is_quantifier(a)) {
+                quantifier* q = to_quantifier(a);
+                bool pending = false;
+                if (!in_cache(q->get_expr())) {
+                    todo.push_back(q->get_expr());
+                    pending = true;
+                }
+                ptr_buffer<expr> patterns, no_patterns;
+                unsigned np = q->get_num_patterns();
+                for (unsigned i = 0; i < np; ++i) {
+                    if (!in_cache(q->get_pattern(i))) {
+                        todo.push_back(q->get_pattern(i));
+                        pending = true;
+                    }
+                    else
+                        patterns.push_back(result.get(q->get_pattern(i)->get_id()));
+                }
+                np = q->get_num_no_patterns();
+                for (unsigned i = 0; i < np; ++i) {
+                    if (!in_cache(q->get_no_pattern(i))) {
+                        todo.push_back(q->get_no_pattern(i));
+                        pending = true;
+                    }
+                    else
+                        no_patterns.push_back(result.get(q->get_no_pattern(i)->get_id()));
+                }
+                if (pending)
+                    continue;
+                todo.pop_back();
+                domain.reset();
+                for (unsigned i = 0; i < q->get_num_decls(); ++i)
+                    domain.push_back((*this)(q->get_decl_sort(i)));
+                quantifier* q2 = 
+                    m.mk_quantifier(q->get_kind(), q->get_num_decls(), domain.data(), q->get_decl_names(), result.get(q->get_expr()->get_id()),
+                    q->get_weight(),
+                    q->get_qid(), q->get_skid(), 
+                    q->get_num_patterns(), patterns.data(), q->get_num_no_patterns(), no_patterns.data()
+                    );
+                result.setx(q->get_id(), q2);
+            }
+            else if (is_app(a)) {
+                args.reset();
+                unsigned n = todo.size();
+                for (expr* arg : *to_app(a)) {
+                    if (!in_cache(arg))
+                        todo.push_back(arg);
+                    else
+                        args.push_back(result.get(arg->get_id()));
+                }
+                if (n < todo.size())
+                    continue;
+                func_decl* f = to_app(a)->get_decl();
+                if (f->is_polymorphic()) {
+                    domain.reset();
+                    for (unsigned i = 0; i < f->get_arity(); ++i)
+                        domain.push_back((*this)(f->get_domain(i)));
+                    sort_ref range = (*this)(f->get_range());
+                    f = m.instantiate_polymorphic(f, f->get_arity(), domain.data(), range);
+                }
+                result.setx(a->get_id(), m.mk_app(f, args));
+                todo.pop_back();
+            }
+        }
+        return expr_ref(result.get(e->get_id()), m);
+    }
+    
+    bool substitution::unify(sort* s1, sort* s2) {
+        if (s1 == s2)
+            return true;
+        if (s1->is_type_var() && m_sub.find(s1, s1))
+            return unify(s1, s2);
+        if (s2->is_type_var() && m_sub.find(s2, s2))
+            return unify(s1, s2);
+        if (s2->is_type_var() && !s1->is_type_var())
+            std::swap(s1, s2);
+        if (s1->is_type_var()) {
+            auto s22 = (*this)(s2);
+            if (occurs(s1, s22))
+                return false;    
+            m_trail.push_back(s22);
+            m_trail.push_back(s1);
+            m_sub.insert(s1, s22);
+            return true;
+        }
+        if (s1->get_family_id() != s2->get_family_id())
+            return false;
+        if (s1->get_decl_kind() != s2->get_decl_kind())
+            return false;
+        if (s1->get_name() != s2->get_name())
+            return false;
+        if (s1->get_num_parameters() != s2->get_num_parameters())
+            return false;
+        for (unsigned i = s1->get_num_parameters(); i-- > 0;) {
+            auto p1 = s1->get_parameter(i);
+            auto p2 = s2->get_parameter(i);
+            if (p1.is_ast() && is_sort(p1.get_ast())) {
+                if (!p2.is_ast())
+                    return false;
+                if (!is_sort(p2.get_ast()))
+                    return false;
+                if (!unify(to_sort(p1.get_ast()), to_sort(p2.get_ast())))
+                    return false;
+                continue;
+            }
+            if (p1 != p2)
+                return false;
+        }
+        return true;
+    }    
+
+    bool substitution::match(sort* s1, sort* s2) {
+        if (s1 == s2)
+            return true;
+        if (s1->is_type_var() && m_sub.find(s1, s1))
+            return match(s1, s2);
+        if (s1->is_type_var()) {
+            m_trail.push_back(s2);
+            m_trail.push_back(s1);
+            m_sub.insert(s1, s2);
+            return true;
+        }
+        if (s1->get_family_id() != s2->get_family_id())
+            return false;
+        if (s1->get_decl_kind() != s2->get_decl_kind())
+            return false;
+        if (s1->get_name() != s2->get_name())
+            return false;
+        if (s1->get_num_parameters() != s2->get_num_parameters())
+            return false;
+        for (unsigned i = s1->get_num_parameters(); i-- > 0;) {
+            auto p1 = s1->get_parameter(i);
+            auto p2 = s2->get_parameter(i);
+            if (p1.is_ast() && is_sort(p1.get_ast())) {
+                if (!p2.is_ast())
+                    return false;
+                if (!is_sort(p2.get_ast()))
+                    return false;
+                if (!match(to_sort(p1.get_ast()), to_sort(p2.get_ast())))
+                    return false;
+                continue;
+            }
+            if (p1 != p2)
+                return false;
+        }
+        return true;
+    }     
+
+    // util        
+    bool util::unify(sort* s1, sort* s2, substitution& sub) {
+        return sub.unify(s1, s2);
+    }
+        
+    bool util::unify(func_decl* f1, func_decl* f2, substitution& sub) {
+        if (f1 == f2)
+            return true;
+        if (!f1->is_polymorphic() || !f2->is_polymorphic())
+            return false;
+        if (m.poly_root(f1) != m.poly_root(f2))
+            return false;
+        for (unsigned i = f1->get_arity(); i-- > 0; )
+            if (!sub.unify(fresh(f1->get_domain(i)), f2->get_domain(i)))
+                return false;
+        return sub.unify(fresh(f1->get_range()), f2->get_range());
+    }
+        
+    bool util::unify(substitution const& s1, substitution const& s2,
+                     substitution& sub) {
+        sort* v2;
+        for (auto const& [k, v] : s1)
+            sub.insert(k, v);
+        for (auto const& [k, v] : s2) {
+            if (sub.find(k, v2)) {
+                if (!sub.unify(sub(v), v2))
+                    return false;
+            }
+            else
+                sub.insert(k, sub(v));
+        }
+        return true;
+    }
+
+    bool util::match(substitution& sub, sort* s1, sort* s_ground) {
+        return sub.match(s1, s_ground);
+    }
+     
+    /**
+    * Create fresh variables, but with caching. 
+    * So "fresh" variables are not truly fresh globally.
+    * This can block some unifications and therefore block some instantiations of
+    * polymorphic assertions. A different caching scheme could be created to
+    * ensure that fresh variables are introduced at the right time, or use other
+    * tricks such as creating variable/offset pairs to distinguish name spaces without 
+    * incurring costs.
+    */
+    sort_ref util::fresh(sort* s) {
+        sort* s1;
+        if (m_fresh.find(s, s1))
+            return sort_ref(s1, m);
+
+        if (m.is_type_var(s)) {
+            s1 = m.mk_type_var(symbol("fresh!" + std::to_string(m_counter)));
+            m_trail.push_back(s1);
+            m_trail.push_back(s);
+            m_fresh.insert(s, s1);
+            return sort_ref(s1, m);
+        }
+        vector<parameter> params;
+        for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
+            parameter p = s->get_parameter(i);
+            if (p.is_ast() && is_sort(p.get_ast())) {
+                sort_ref fs = fresh(to_sort(p.get_ast()));
+                params.push_back(parameter(fs.get()));
+            }
+            else
+                params.push_back(p);
+        }
+        sort_info info(s->get_family_id(), s->get_decl_kind(), params.size(), params.data(), s->private_parameters());
+        s1 = m.mk_sort(s->get_name(), info);
+        m_trail.push_back(s1);
+        m_trail.push_back(s);
+        m_fresh.insert(s, s1);
+        return sort_ref(s1, m);
+    }
+        
+    sort_ref_vector util::fresh(unsigned n, sort* const* s) {
+        sort_ref_vector r(m);
+        for (unsigned i = 0; i < n; ++i)
+            r.push_back(fresh(s[i]));
+        return r;
+    }
+     
+    void util::collect_poly_instances(expr* e, ptr_vector<func_decl>& instances) {
+        struct proc {
+            ast_manager& m;
+            ptr_vector<func_decl>& instances;
+            proc(ast_manager& m, ptr_vector<func_decl>& instances) : m(m), instances(instances) {}
+            void operator()(func_decl* f) {
+                if (f->is_polymorphic() && !m.is_eq(f) && !is_decl_of(f, pattern_family_id, OP_PATTERN))
+                    instances.push_back(f);
+            }
+            void operator()(ast* a) {}
+        };
+        proc proc(m, instances);
+        for_each_ast(proc, e, false);        
+    }
+        
+    bool util::has_type_vars(expr* e) {
+        struct proc {
+            ast_manager& m;
+            bool found = false;
+            proc(ast_manager& m) : m(m) {}
+            void operator()(sort* f) {
+                if (m.has_type_var(f))
+                    found = true;
+            }
+            void operator()(ast* a) {}
+        };
+        proc proc(m);
+        for_each_ast(proc, e, false);
+        return proc.found;
+    }
+    
+    void util::collect_type_vars(expr* e, ptr_vector<sort>& tvs) {
+        struct proc {
+            ast_manager& m;
+            ptr_vector<sort>& tvs;
+            proc(ast_manager& m, ptr_vector<sort>& tvs) : m(m), tvs(tvs) {}
+            void operator()(sort* s) {
+                if (m.is_type_var(s))
+                    tvs.push_back(s);
+            }
+            void operator()(ast* a) {}
+        };
+        proc proc(m, tvs);
+        for_each_ast(proc, e, true);
+    }
+}

src/ast/polymorphism_util.h

@@ -0,0 +1,112 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    polymorphism_util.h
+
+Abstract:
+
+    Utilities for supporting polymorphic type signatures.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2023-7-8
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "util/hashtable.h"
+
+namespace polymorphism {
+
+    class substitution {
+        ast_manager& m;
+        obj_map<sort, sort*> m_sub;
+        sort_ref_vector m_trail;
+    public:
+        substitution(ast_manager& m): m(m), m_trail(m) {}
+    
+        sort_ref_vector operator()(sort_ref_vector const& s);
+        
+        sort_ref operator()(sort* s);
+
+        expr_ref operator()(expr* e);
+        
+        bool unify(sort* s1, sort* s2);       
+
+        bool match(sort* s1, sort* s_ground);
+
+        obj_map<sort, sort*>::iterator begin() const { return m_sub.begin(); }
+        obj_map<sort, sort*>::iterator end() const { return m_sub.end(); }
+
+        void insert(sort* v, sort* t) { m_trail.push_back(v).push_back(t); m_sub.insert(v, t); }
+
+        bool find(sort* v, sort*& t) const { return m_sub.find(v, t); }
+
+        unsigned size() const { return m_sub.size(); }
+
+        /**
+        * weak equality: strong equality considers applying substitutions recursively in range
+        * because substitutions may be in triangular form.
+        */
+        struct eq {
+            bool operator()(substitution const* s1, substitution const* s2) const {
+                if (s1->size() != s2->size())
+                    return false;
+                sort* v2;
+                for (auto const& [k, v] : *s1) {
+                    if (!s2->find(k, v2))
+                        return false;
+                    if (v != v2)
+                        return false;
+                }
+                return true;
+            }
+        };
+
+        struct hash {
+            unsigned operator()(substitution const* s) const {
+                unsigned hash = 0xfabc1234 + s->size();
+                for (auto const& [k, v] : *s) 
+                    hash ^= k->hash() + 2 * v->hash();                
+                return hash;
+            }
+        };
+    };
+
+    typedef hashtable<substitution*, substitution::hash, substitution::eq> substitutions;
+    
+    class util {
+        ast_manager&         m;
+        sort_ref_vector      m_trail;
+        obj_map<sort, sort*> m_fresh;
+        unsigned             m_counter = 0;
+
+        sort_ref fresh(sort* s);
+
+        sort_ref_vector fresh(unsigned n, sort* const* s);
+        
+    public:
+        util(ast_manager& m): m(m), m_trail(m) {}
+        
+        bool unify(sort* s1, sort* s2, substitution& sub);
+        
+        bool unify(func_decl* f1, func_decl* f2, substitution& sub);
+        
+        bool unify(substitution const& s1, substitution const& s2,
+                   substitution& sub);
+
+        bool match(substitution& sub, sort* s1, sort* s_ground);
+                        
+        // collect instantiations of polymorphic functions
+        void collect_poly_instances(expr* e, ptr_vector<func_decl>& instances);
+        
+        // test if expression contains polymorphic variable.
+        bool has_type_vars(expr* e);
+
+        void collect_type_vars(expr* e, ptr_vector<sort>& tvs);
+        
+    };
+}

src/ast/rewriter/CMakeLists.txt

@@ -23,7 +23,6 @@ z3_add_component(rewriter
     factor_rewriter.cpp
     fpa_rewriter.cpp
     func_decl_replace.cpp
-    hoist_rewriter.cpp
     inj_axiom.cpp
     label_rewriter.cpp
     macro_replacer.cpp

src/ast/rewriter/arith_rewriter.cpp

@@ -551,24 +551,9 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
 }
 
     if (m_anum_simp) {
-        if (is_numeral(arg1, a1) && m_util.is_irrational_algebraic_numeral(arg2)) {
+        auto& am = m_util.am();
-            anum_manager & am = m_util.am();
+        scoped_anum v1(am), v2(am);
-            scoped_anum v1(am);
+        if (is_algebraic_numeral(arg1, v1) && is_algebraic_numeral(arg2, v2)) {
-            am.set(v1, a1.to_mpq());
-            anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2);
-            ANUM_LE_GE_EQ();
-        }
-        if (m_util.is_irrational_algebraic_numeral(arg1) && is_numeral(arg2, a2)) {
-            anum_manager & am = m_util.am();
-            anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1);
-            scoped_anum v2(am);
-            am.set(v2, a2.to_mpq());
-            ANUM_LE_GE_EQ();
-        }
-        if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_irrational_algebraic_numeral(arg2)) {
-            anum_manager & am = m_util.am();
-            anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1);
-            anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2);
             ANUM_LE_GE_EQ();            
         }
     }
@@ -669,6 +654,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
     return BR_FAILED;
 }
 
+
 br_status arith_rewriter::mk_le_core(expr * arg1, expr * arg2, expr_ref & result) {
     return mk_le_ge_eq_core(arg1, arg2, LE, result);
 }
@@ -751,11 +737,19 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
     return false;
 }
 
-expr_ref arith_rewriter::neg_monomial(expr* e) const {
+expr_ref arith_rewriter::neg_monomial(expr* e) {
     expr_ref_vector args(m);
     rational a1;
     if (m_util.is_numeral(e, a1)) 
         args.push_back(m_util.mk_numeral(-a1, e->get_sort()));
+    else if (m_util.is_irrational_algebraic_numeral(e)) {
+        auto& n = m_util.to_irrational_algebraic_numeral(e);
+        auto& am = m_util.am();
+        scoped_anum new_n(am);
+        am.set(new_n, n);
+        am.neg(new_n);
+        args.push_back(m_util.mk_numeral(am, new_n, m_util.is_int(e)));
+    }
     else if (is_app(e) && m_util.is_mul(e)) {
         if (is_numeral(to_app(e)->get_arg(0), a1)) {
             if (!a1.is_minus_one()) {
@@ -780,7 +774,7 @@ expr_ref arith_rewriter::neg_monomial(expr* e) const {
     }
 }
 
-bool arith_rewriter::is_neg_poly(expr* t, expr_ref& neg) const {
+bool arith_rewriter::is_neg_poly(expr* t, expr_ref& neg) {
     rational r;
     if (m_util.is_mul(t) && is_numeral(to_app(t)->get_arg(0), r) && r.is_neg()) {
         neg = neg_monomial(t);
@@ -824,6 +818,36 @@ bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args)
     return false;
 }
 
+bool arith_rewriter::is_algebraic_numeral(expr* n, scoped_anum& a) {
+    auto& am = m_util.am();
+    expr* x, *y;
+    rational r;
+    if (m_util.is_mul(n, x, y)) {
+        scoped_anum ax(am), ay(am);
+        if (is_algebraic_numeral(x, ax) && is_algebraic_numeral(y, ay)) {
+            am.mul(ax, ay, a);
+            return true;
+        }
+    }
+    else if (m_util.is_add(n, x, y)) {
+        scoped_anum ax(am), ay(am);
+        if (is_algebraic_numeral(x, ax) && is_algebraic_numeral(y, ay)) {
+            am.add(ax, ay, a);
+            return true;
+        }
+    }
+    else if (m_util.is_numeral(n, r)) {
+        am.set(a, r.to_mpq());
+        return true;
+    }    
+    else if (m_util.is_irrational_algebraic_numeral(n)) {
+        am.set(a, m_util.to_irrational_algebraic_numeral(n));
+        return true;
+    }
+    return false;
+}
+
+
 br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
     if (is_anum_simp_target(num_args, args)) {
         expr_ref_buffer new_args(m);

src/ast/rewriter/arith_rewriter.h

@@ -21,6 +21,7 @@ Notes:
 #include "ast/rewriter/poly_rewriter.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
+#include "math/polynomial/algebraic_numbers.h"
 
 class arith_rewriter_core {
 protected:
@@ -80,6 +81,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     void updt_local_params(params_ref const & p);
 
     bool is_anum_simp_target(unsigned num_args, expr * const * args);
+    bool is_algebraic_numeral(expr* n, scoped_anum& a);
 
     br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result);
@@ -97,8 +99,8 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     bool is_2_pi_integer_offset(expr * t, expr * & m);
     bool is_pi_integer(expr * t);
     bool is_pi_integer_offset(expr * t, expr * & m);
-    bool is_neg_poly(expr* e, expr_ref& neg) const;
+    bool is_neg_poly(expr* e, expr_ref& neg);
-    expr_ref neg_monomial(expr * e) const;
+    expr_ref neg_monomial(expr * e);
     expr * mk_sin_value(rational const & k);
     app * mk_sqrt(rational const & k);
     bool divides(expr* d, expr* n, expr_ref& result);

src/ast/rewriter/array_rewriter.cpp

@@ -24,6 +24,7 @@ Notes:
 #include "ast/rewriter/var_subst.h"
 #include "params/array_rewriter_params.hpp"
 #include "util/util.h"
+#include "ast/array_peq.h"
 
 void array_rewriter::updt_params(params_ref const & _p) {
     array_rewriter_params p(_p);
@@ -40,8 +41,48 @@ void array_rewriter::get_param_descrs(param_descrs & r) {
 }
 
 br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    br_status st = BR_FAILED;
+
+    // BEGIN: rewrite rules for PEQs
+    if (is_partial_eq(f)) {
+        SASSERT(num_args >= 2);
+        expr *e0, *e1;
+        e0 = args[0];
+        e1 = args[1];
+
+        expr_ref a(m()), val(m());
+        expr_ref_vector vindex(m());
+
+        if (e0 == e1) {
+            // t peq t --> true
+            result = m().mk_true();
+            st = BR_DONE;
+        }
+        else if (m_util.is_store_ext(e0, a, vindex, val)) {
+            if (num_args == 2 && a == e1) {
+                // (a[i := x] peq_{\emptyset} a) ---> a[i] == x
+                mk_select(vindex.size(), vindex.data(), result);
+                result = m().mk_eq(result, val);
+                st = BR_REWRITE_FULL;
+            }
+            else if (a == e1 && vindex.size() == num_args + 2) {
+                // a [i: = x] peq_{i} a -- > true
+                bool all_eq = true;
+                for (unsigned i = 0, sz = vindex.size(); all_eq && i < sz;
+                     ++i) {
+                    all_eq &= vindex.get(i) == args[2+i];
+                }
+                if (all_eq) {
+                    result = m().mk_true();
+                    st = BR_DONE;
+                }
+            }
+        }
+        return st;
+    }
+    // END: rewrite rules for PEQs
+
     SASSERT(f->get_family_id() == get_fid());
-    br_status st;
     switch (f->get_decl_kind()) {
     case OP_SELECT:
         st = mk_select_core(num_args, args, result);

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "ast/rewriter/bit_blaster/bit_blaster_tpl_def.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "util/ref_util.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -552,7 +553,16 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             default:                
                 TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
+                {
+                    expr_ref r(m().mk_app(f, num, args), m());
+                    result = r;
+                    th_rewriter rw(m());
+                    rw(result);
+                    if (!is_app(result) || to_app(result)->get_decl() != f)
+                        return BR_REWRITE_FULL;                    
+                }
                 throw_unsupported(f);
+
             }
         }
 

src/ast/rewriter/bool_rewriter.cpp

@@ -34,7 +34,6 @@ void bool_rewriter::updt_params(params_ref const & _p) {
     m_blast_distinct       = p.blast_distinct();
     m_blast_distinct_threshold = p.blast_distinct_threshold();
     m_ite_extra_rules      = p.ite_extra_rules();
-    m_hoist.set_elim_and(m_elim_and);
 }
 
 void bool_rewriter::get_param_descrs(param_descrs & r) {
@@ -270,28 +269,6 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 return BR_DONE;
         }
 
-#if 1
-        br_status st;
-        expr_ref r(m());
-        st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
-        if (st != BR_FAILED) {
-            m_counts1.reserve(m().get_num_asts() + 1);
-            m_counts2.reserve(m().get_num_asts() + 1);
-            get_num_internal_exprs(m_counts1, m_todo1, r);
-            for (unsigned i = 0; i < num_args; ++i)
-                get_num_internal_exprs(m_counts2, m_todo2, args[i]);
-            unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
-            unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
-            if (count1 > count2)
-                st = BR_FAILED;
-        }
-        if (st != BR_FAILED)
-            result = r;
-        if (st == BR_DONE)
-            return BR_REWRITE1;
-        if (st != BR_FAILED)
-            return st;
-#endif
         if (s) {
             if (m_sort_disjunctions) {
                 ast_lt lt;

src/ast/rewriter/bool_rewriter.h

@@ -20,7 +20,6 @@ Notes:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/hoist_rewriter.h"
 #include "util/params.h"
 
 /**
@@ -51,7 +50,6 @@ Notes:
 */
 class bool_rewriter {
     ast_manager &  m_manager;
-    hoist_rewriter m_hoist;
     bool           m_flat_and_or = false;
     bool           m_sort_disjunctions = true;
     bool           m_local_ctx = false;
@@ -84,7 +82,7 @@ class bool_rewriter {
     void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
 
 public:
-    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { 
+    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { 
         updt_params(p); 
     }
     ast_manager & m() const { return m_manager; }

src/ast/rewriter/bv_rewriter.cpp

@@ -217,7 +217,7 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
     case OP_BUSUB_OVFL:
         return mk_bvusub_underflow(num_args, args, result);
     case OP_BSSUB_OVFL:
-        return mk_bvssub_overflow(num_args, args, result);
+        return mk_bvssub_under_overflow(num_args, args, result);
     default:
         return BR_FAILED;
     }
@@ -3085,19 +3085,29 @@ br_status bv_rewriter::mk_bvusub_underflow(unsigned num, expr * const * args, ex
     return status;
 }
 
-br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result) {
+//
+// no_overflow    := if t2 = min_int then t1 <s 0 else no_overflow(t1 + -t2)
+// no_underflow   := 0 <s -t2 => no_underflow(t1 + -t2)
+// over_underflow := 0 <s -t2 & under_overflow+(t1 + -t2) || t2 = min_int & t1 >=s 0 || t2 != min_int & under_overflow+(t1 + -t2)
+//                := if t2 == min_int then t1 >=s 0 else under_overflow+(t1 + -t2)
+// because when 0 <s min_int = false
+// 
+br_status bv_rewriter::mk_bvssub_under_overflow(unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
     SASSERT(get_bv_size(args[0]) == get_bv_size(args[1]));
     auto sz = get_bv_size(args[0]);
     auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz);
     expr_ref bvsaddo {m};
     expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) };
-    auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo);
+    auto bvsaddo_stat = mk_bvsadd_over_underflow(2, args2, bvsaddo);
     SASSERT(bvsaddo_stat != BR_FAILED); (void)bvsaddo_stat;
     auto first_arg_ge_zero = m_util.mk_sle(mk_zero(sz), args[0]);
     result = m.mk_ite(m.mk_eq(args[1], minSigned), first_arg_ge_zero, bvsaddo);
     return BR_REWRITE_FULL;
 }
+
+//br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result) {
+//}
 br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
     SASSERT(get_bv_size(args[0]) == get_bv_size(args[1]));

src/ast/rewriter/bv_rewriter.h

@@ -153,7 +153,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bvsadd_over_underflow(unsigned num, expr * const * args, expr_ref & result);
 
     br_status mk_bvusub_underflow(unsigned num, expr * const * args, expr_ref & result);
-    br_status mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result);
+    // br_status mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bvssub_under_overflow(unsigned num, expr * const * args, expr_ref & result);
 
     bool is_minus_one_times_t(expr * arg);
     void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result);

src/ast/rewriter/datatype_rewriter.cpp

@@ -21,7 +21,8 @@ Notes:
 br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
     switch(f->get_decl_kind()) {
-    case OP_DT_CONSTRUCTOR: return BR_FAILED;
+    case OP_DT_CONSTRUCTOR:
+        return BR_FAILED;
     case OP_DT_RECOGNISER:
         SASSERT(num_args == 1);
         result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);

src/ast/rewriter/elim_bounds.cpp

@@ -17,8 +17,6 @@ Revision History:
 
 --*/
 
-#ifndef ELIM_BOUNDS_H_
-#define ELIM_BOUNDS_H_
 
 #include "ast/used_vars.h"
 #include "util/obj_hashtable.h"
@@ -201,4 +199,3 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
     return true;
 }
 
-#endif /* ELIM_BOUNDS_H_ */

src/ast/rewriter/hoist_rewriter.cpp

@@ -1,248 +0,0 @@
-/*++
-Copyright (c) 2019 Microsoft Corporation
-
-Module Name:
-
-    hoist_rewriter.cpp
-
-Abstract:
-
-    Hoist predicates over disjunctions
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2019-2-4
-
---*/
-
-
-#include "ast/rewriter/hoist_rewriter.h"
-#include "ast/rewriter/bool_rewriter.h"
-#include "ast/ast_util.h"
-#include "ast/ast_pp.h"
-#include "ast/ast_ll_pp.h"
-
-hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
-    m(m), m_args1(m), m_args2(m), m_refs(m), m_subst(m) { 
-    updt_params(p); 
-}
-
-expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) {
-    if (m_elim_and) {
-        expr_ref_vector negs(m);
-        for (expr* a : args)
-            if (m.is_false(a))
-                return expr_ref(m.mk_false(), m);
-            else if (m.is_true(a))
-                continue;
-            else
-                negs.push_back(::mk_not(m, a));
-        return ::mk_not(mk_or(negs));
-    }
-    else
-        return ::mk_and(args);
-}
-
-expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) {
-    return ::mk_or(args);
-}
-
-br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
-    if (num_args < 2) 
-        return BR_FAILED;
-
-    for (unsigned i = 0; i < num_args; ++i) 
-        if (!is_and(es[i], nullptr)) 
-            return BR_FAILED;
-
-    bool turn = false;
-    m_preds1.reset(); 
-    m_preds2.reset();
-    m_uf1.reset(); 
-    m_uf2.reset();
-    m_expr2var.reset();
-    m_var2expr.reset();
-    basic_union_find* uf[2] = { &m_uf1, &m_uf2 };
-    obj_hashtable<expr>* preds[2] = { &m_preds1, &m_preds2 };
-    expr_ref_vector* args[2] = { &m_args1, &m_args2 };
-    VERIFY(is_and(es[0], args[turn]));
-    expr* e1, *e2;
-    for (expr* e : *(args[turn])) {
-        if (m.is_eq(e, e1, e2))             
-            (*uf)[turn].merge(mk_var(e1), mk_var(e2));
-        else 
-            (*preds)[turn].insert(e);
-    }
-    unsigned round = 0;
-    for (unsigned j = 1; j < num_args; ++j) {
-        ++round;
-        m_es.reset();
-        m_mark.reset();
-
-        bool last = turn;
-        turn = !turn;
-        (*preds)[turn].reset();
-        reset(m_uf0);
-        VERIFY(is_and(es[j], args[turn]));
-
-        for (expr* e : *args[turn]) {
-            if (m.is_eq(e, e1, e2)) {
-                m_es.push_back(e1);                
-                m_uf0.merge(mk_var(e1), mk_var(e2));
-            }    
-            else if ((*preds)[last].contains(e)) 
-                (*preds)[turn].insert(e);
-        }
-
-        if ((*preds)[turn].empty() && m_es.empty()) 
-            return BR_FAILED;
-
-        m_eqs.reset();
-        for (expr* e : m_es) {
-            if (m_mark.is_marked(e)) 
-                continue;
-            unsigned u = mk_var(e);
-            unsigned v = u;
-            m_roots.reset();
-            do {
-                m_mark.mark(e);
-                unsigned r = (*uf)[last].find(v);
-                if (m_roots.find(r, e2)) 
-                    m_eqs.push_back({e, e2});
-                else 
-                    m_roots.insert(r, e);
-                v = m_uf0.next(v);
-                e = mk_expr(v);
-            }
-            while (u != v);
-        }
-        reset((*uf)[turn]);
-        for (auto const& [e1, e2] : m_eqs) 
-            (*uf)[turn].merge(mk_var(e1), mk_var(e2));
-        if ((*preds)[turn].empty() && m_eqs.empty()) 
-            return BR_FAILED;
-    }
-    if (m_eqs.empty()) {
-        result = hoist_predicates((*preds)[turn], num_args, es);
-        return BR_DONE;
-    }
-    // p & eqs & (or fmls)
-    expr_ref_vector fmls(m);
-    m_subst.reset();
-    for (expr * p : (*preds)[turn]) {
-        expr* q = nullptr;
-        if (m.is_not(p, q)) 
-            m_subst.insert(q, m.mk_false());
-        else 
-            m_subst.insert(p, m.mk_true());
-        fmls.push_back(p);
-    }
-    for (auto& p : m_eqs) {
-        if (m.is_value(p.first))
-            std::swap(p.first, p.second);
-        m_subst.insert(p.first, p.second);
-        fmls.push_back(m.mk_eq(p.first, p.second));
-    }    
-    expr_ref ors(::mk_or(m, num_args, es), m);
-    m_subst(ors);
-    fmls.push_back(ors);
-    result = mk_and(fmls);
-    TRACE("hoist", tout << ors << " => " << result << "\n";);
-    return BR_DONE;
-}
-
-unsigned hoist_rewriter::mk_var(expr* e) {
-    unsigned v = 0;
-    if (m_expr2var.find(e, v)) 
-        return v;
-    m_uf1.mk_var();
-    v = m_uf2.mk_var();
-    SASSERT(v == m_var2expr.size());
-    m_expr2var.insert(e, v);
-    m_var2expr.push_back(e);
-    return v;
-}
-
-expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
-    expr_ref_vector args(m), args1(m), fmls(m);
-    for (unsigned i = 0; i < num_args; ++i) {
-        VERIFY(is_and(es[i], &args1));
-        fmls.reset();
-        for (expr* e : args1) 
-            if (!preds.contains(e))
-                fmls.push_back(e);
-        args.push_back(mk_and(fmls));
-    }
-    fmls.reset();
-    fmls.push_back(mk_or(args));
-    for (auto* p : preds) 
-        fmls.push_back(p);
-    return mk_and(fmls);
-}
-
-
-br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
-    switch (f->get_decl_kind()) {
-    case OP_OR:        
-        return mk_or(num_args, args, result);
-    default:
-        return BR_FAILED;
-    }
-}
-
-bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
-#if 0
-    if (!args) 
-        return m.is_and(e) || (m.is_not(e, e) && m.is_or(e));
-    expr_fast_mark1 visited;
-    args->reset();
-    args->push_back(e);
-    m_refs.reset();
-    for (unsigned i = 0; i < args->size(); ++i) {
-        e = args->get(i);
-        if (visited.is_marked(e)) 
-            goto drop;
-        m_refs.push_back(e);
-        visited.mark(e, true);
-        if (m.is_and(e)) 
-            args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
-        else if (m.is_not(e, e) && m.is_or(e)) 
-            for (expr* arg : *to_app(e)) 
-                args->push_back(::mk_not(m, arg));
-        else 
-            continue;
-    drop:
-        (*args)[i] = args->back();
-        args->pop_back();
-        --i;
-    }
-    return args->size() > 1;
-#else
-    if (m.is_and(e)) {
-        if (args) {
-            args->reset();
-            args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
-        }
-        return true;
-    }
-    if (m.is_not(e, e) && m.is_or(e)) {
-        if (args) {
-            args->reset();
-            for (expr* arg : *to_app(e)) 
-                args->push_back(::mk_not(m, arg));
-            TRACE("hoist", tout << args << " " <<  * args << "\n");
-        }
-        return true;
-    }
-#endif
-    return false;
-}
-
-
-void hoist_rewriter::reset(basic_union_find& uf) {
-    uf.reset();
-    for (expr* e : m_var2expr) {
-        (void)e;
-        uf.mk_var();
-    }
-}

src/ast/rewriter/hoist_rewriter.h

@@ -1,87 +0,0 @@
-/*++
-Copyright (c) 2019 Microsoft Corporation
-
-Module Name:
-
-    hoist_rewriter.h
-
-Abstract:
-
-    Hoist predicates over disjunctions
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2019-2-4
-
-Notes:
-
---*/
-#pragma once
-
-#include "ast/ast.h"
-#include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/expr_safe_replace.h"
-#include "util/params.h"
-#include "util/union_find.h"
-#include "util/obj_hashtable.h"
-
-class bool_rewriter;
-
-class hoist_rewriter {
-    ast_manager &                   m;
-    expr_ref_vector                 m_args1, m_args2, m_refs;
-    obj_hashtable<expr>             m_preds1, m_preds2;
-    basic_union_find                m_uf1, m_uf2, m_uf0;
-    ptr_vector<expr>                m_es;
-    svector<std::pair<expr*,expr*>> m_eqs;
-    u_map<expr*>                    m_roots;
-    expr_safe_replace               m_subst;
-    obj_map<expr, unsigned>         m_expr2var;
-    ptr_vector<expr>                m_var2expr;
-    expr_mark                       m_mark;
-    bool                            m_elim_and = false;
-
-    bool is_and(expr* e, expr_ref_vector* args);
-    expr_ref mk_and(expr_ref_vector const& args);
-    expr_ref mk_or(expr_ref_vector const& args);
-
-    bool is_var(expr* e) { return m_expr2var.contains(e); }
-    expr* mk_expr(unsigned v) { return m_var2expr[v]; }
-    unsigned mk_var(expr* e);
-
-    void reset(basic_union_find& uf);
-
-    expr_ref hoist_predicates(obj_hashtable<expr> const& p, unsigned num_args, expr* const* args);
-
-
-public:
-    hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
-    family_id get_fid() const { return m.get_basic_family_id(); }
-    bool is_eq(expr * t) const { return m.is_eq(t); }       
-    void updt_params(params_ref const & p) {}
-    static void get_param_descrs(param_descrs & r) {}
-    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);    
-    br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);    
-    void set_elim_and(bool b) { m_elim_and = b; }
-};
-
-struct hoist_rewriter_cfg : public default_rewriter_cfg {
-    hoist_rewriter m_r;
-    bool rewrite_patterns() const { return false; }
-    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        result_pr = nullptr;
-        if (f->get_family_id() != m_r.get_fid())
-            return BR_FAILED;
-        return m_r.mk_app_core(f, num, args, result);
-    }
-    hoist_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {}
-};
-
-class hoist_rewriter_star : public rewriter_tpl<hoist_rewriter_cfg> {
-    hoist_rewriter_cfg m_cfg;
-public:
-    hoist_rewriter_star(ast_manager & m, params_ref const & p = params_ref()):
-        rewriter_tpl<hoist_rewriter_cfg>(m, false, m_cfg),
-        m_cfg(m, p) {}
-};
-

src/ast/rewriter/rewriter.cpp

@@ -17,6 +17,8 @@ Notes:
 
 --*/
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/push_app_ite.h"
+#include "ast/rewriter/elim_bounds.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_smt2_pp.h"
@@ -417,3 +419,6 @@ void inv_var_shifter::process_var(var * v) {
 }
     
 template class rewriter_tpl<beta_reducer_cfg>;
+template class rewriter_tpl<ng_push_app_ite_cfg>;
+template class rewriter_tpl<push_app_ite_cfg>;
+template class rewriter_tpl<elim_bounds_cfg>;

src/ast/rewriter/rewriter_types.h

@@ -33,6 +33,18 @@ enum br_status {
     BR_FAILED                  // no builtin rewrite is available
 };
 
+inline std::ostream& operator<<(std::ostream& out, br_status st) {
+    switch (st) {
+    case BR_REWRITE1: return out << "rewrite1";
+    case BR_REWRITE2: return out << "rewrite2";
+    case BR_REWRITE3: return out << "rewrite3";
+    case BR_REWRITE_FULL: return out << "rewrite_full";
+    case BR_DONE: return out << "done";
+    case BR_FAILED: return out << "failed";
+    default: return out << "unknown";
+    }
+}
+
 #define RW_UNBOUNDED_DEPTH 3
 inline br_status unsigned2br_status(unsigned u) {
     br_status r = u >= RW_UNBOUNDED_DEPTH ? BR_REWRITE_FULL : static_cast<br_status>(u);

src/ast/rewriter/seq_axioms.cpp

@@ -538,6 +538,7 @@ namespace seq {
         expr_ref t_eq_empty = mk_eq_empty(t);
         expr_ref xsy        = mk_concat(x, s, y);
 
+        //        add_clause(~mk_eq(t, s), i_eq_0);
         add_clause(cnt, i_eq_m1);
         add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
         add_clause(~s_eq_empty, mk_eq(i, mk_len(t)));

src/ast/rewriter/seq_rewriter.cpp

@@ -828,6 +828,7 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
 
 br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     zstring b;
+    rational r;
     m_es.reset();
     str().get_concat(a, m_es);
     unsigned len = 0;
@@ -867,6 +868,16 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = str().mk_length(z);
         return BR_REWRITE1;
     } 
+    // len(extract(x, 0, z)) = min(z, len(x))
+    if (str().is_extract(a, x, y, z) && 
+        m_autil.is_numeral(y, r) && r.is_zero() &&
+        m_autil.is_numeral(z, r) && r >= 0) {
+        expr* len_x = str().mk_length(x);
+        result = m().mk_ite(m_autil.mk_le(len_x, z), len_x, z);
+        // expr* zero = m_autil.mk_int(0);
+        // result = m().mk_ite(m_autil.mk_le(z, zero), zero, result);
+        return BR_REWRITE_FULL;
+    }
 #if 0
     expr* s = nullptr, *offset = nullptr, *length = nullptr;
     if (str().is_extract(a, s, offset, length)) {
@@ -1209,6 +1220,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     constantPos &= pos.is_unsigned();
     constantLen &= len.is_unsigned();
 
+    if (constantPos && constantLen && len == 1) {
+        result = str().mk_at(a, b);
+        return BR_REWRITE1;
+    }
+
     if (constantPos && constantLen && constantBase) {
         unsigned _pos = pos.get_unsigned();
         unsigned _len = len.get_unsigned();
@@ -1245,6 +1261,15 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         result = str().mk_substr(a1, m_autil.mk_add(b1, b), m_autil.mk_sub(c1, b));
         return BR_REWRITE3;
     }
+    rational r1, r2;
+    if (str().is_extract(a, a1, b1, c1) &&
+        m_autil.is_numeral(b1, r1) && r1.is_unsigned() &&
+        m_autil.is_numeral(c1, r2) && r2.is_unsigned() &&
+        constantPos && constantLen &&
+        r1 == 0 && r2 >= pos + len) {        
+        result = str().mk_substr(a1, b, c);
+        return BR_REWRITE1;            
+    }
 
     if (str().is_extract(a, a1, b1, c1) && 
         is_prefix(a1, b1, c1) && is_prefix(a, b, c)) {
@@ -1539,9 +1564,17 @@ bool seq_rewriter::reduce_by_char(expr_ref& r, expr* ch, unsigned depth) {
  */
 br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     zstring c;
-    rational r;
+    rational r, offset_r, len_r;
+    expr* offset, *a1, *len;
     expr_ref_vector lens(m());
     sort* sort_a = a->get_sort();
+    if (str().is_extract(a, a1, offset, len) && 
+        m_autil.is_numeral(offset, offset_r) && offset_r.is_zero() && 
+        m_autil.is_numeral(len, len_r) && m_autil.is_numeral(b, r) && 
+        r < len_r) {
+        result = str().mk_at(a1, b);
+        return BR_REWRITE1;
+    }
     if (!get_lengths(b, lens, r)) {
         return BR_FAILED;
     }
@@ -1716,6 +1749,10 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
         result = m_autil.mk_numeral(rational(idx), true);
         return BR_DONE;
     }
+    if (a == b) {
+        result = m_autil.mk_int(0);
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 

src/ast/rewriter/th_rewriter.cpp

@@ -39,6 +39,7 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 #include "ast/for_each_expr.h"
+#include "ast/array_peq.h"
 
 namespace {
 struct th_rewriter_cfg : public default_rewriter_cfg {
@@ -75,6 +76,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     bool                m_ignore_patterns_on_ground_qbody = true;
     bool                m_rewrite_patterns = true;
     bool                m_enable_der = true;
+    bool                m_nested_der = false;
 
 
     ast_manager & m() const { return m_b_rw.m(); }
@@ -91,6 +93,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
         m_rewrite_patterns = p.rewrite_patterns();
         m_enable_der     = p.enable_der();
+        m_nested_der     = _p.get_bool("nested_der", false);
     }
 
     void updt_params(params_ref const & p) {
@@ -644,6 +647,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             else
                 st = pull_ite(result);
         }
+        if (st == BR_FAILED && f->get_family_id() == null_family_id && is_partial_eq(f)) {
+            st = m_ar_rw.mk_app_core(f,  num, args, result);
+        }
+
         CTRACE("th_rewriter_step", st != BR_FAILED,
                tout << f->get_name() << "\n";
                for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
@@ -838,8 +845,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             result = r;
         }
 
-        if (der_change) {
+        if (der_change && !m_nested_der) {
             th_rewriter rw(m());
+            params_ref p;
+            p.set_bool("nested_der", true);
+            rw.updt_params(p);
             rw(result, r, p2);
             if (m().proofs_enabled() && result.get() != r.get()) 
                 result_pr = m().mk_transitivity(result_pr, p2);

src/ast/simplifiers/bound_simplifier.h

@@ -37,6 +37,7 @@ class bound_simplifier : public dependent_expr_simplifier {
     unsynch_mpq_manager     nm;
     small_object_allocator  m_alloc;
     bound_propagator        bp;
+    u_dependency_manager    m_dep_manager;
     dep_intervals           m_interval;
     ptr_vector<expr>        m_var2expr;
     unsigned_vector         m_expr2var;
@@ -105,7 +106,7 @@ public:
         a(m),
         m_rewriter(m),
         bp(nm, m_alloc, p),
-        m_interval(m.limit()),
+        m_interval(m_dep_manager, m.limit()),
         m_trail(m),
         m_num_buffer(nm) {
         updt_params(p);