Merge branch 'poly' of https://github.com/z3prover/z3 into poly

.github/workflows/Windows.yml

@@ -0,0 +1,64 @@
+name: Windows
+
+on:
+  push:
+    branches: [ master ]
+
+jobs:               
+  build:
+    strategy:
+      matrix:
+        arch : [x86,x64,amd64_arm64]
+        include:
+         - arch : x86
+         - arch : amd64_arm64
+         - arch : x64
+           cmd1 : 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\"))"'
+           cmd2 : 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
+           cmd3 : 'set /P JlCxxDir=<tmp.env'
+           test : 1
+           bindings: -DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True 
+
+    runs-on: windows-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+      - name: Add msbuild to PATH
+        uses: microsoft/setup-msbuild@v2
+      - run: |
+          md build
+          cd build
+          ${{ matrix.cmd1 }}
+          ${{ matrix.cmd2 }}
+          ${{ matrix.cmd3 }}
+          call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" ${{ matrix.arch }}
+          cmake ${{ matrix.bindings }} -G "NMake Makefiles" ../
+          nmake    
+          cd ..
+        shell: cmd
+      - name: Run Regressions
+        if: ${{ matrix.test }}
+        run: |
+           git clone https://github.com/z3prover/z3test z3test
+           python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
+        shell: cmd      
+      - name: Run Tests
+        if: ${{ matrix.test }}
+        run: |
+           pushd build
+           call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" ${{ matrix.arch }}
+           pushd build\python
+           python z3test.py z3
+           python z3test.py z3num
+           popd
+           pushd build
+           nmake cpp_example
+           examples\cpp_example_build_dir\cpp_example.exe
+           nmake c_example
+           examples\c_example_build_dir\c_example.exe
+           nmake test-z3
+           test-z3.exe -a
+           popd
+        shell: cmd
+  
+

.github/workflows/android-build.yml

@@ -32,7 +32,7 @@ jobs:
         tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so
 
     - name: Archive production artifacts
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: android-build-${{ matrix.android-abi }}
         path: build/z3-build-${{ matrix.android-abi }}.tar

.github/workflows/coverage.yml

@@ -89,15 +89,15 @@ jobs:
 
     - name: Get date
       id: date
-      run: echo "::set-output name=date::$(date +'%Y-%m-%d')"
+      run: echo "date=$(date +'%Y-%m-%d')" >> $GITHUB_OUTPUT
 
-    - uses: actions/upload-artifact@v3
+    - uses: actions/upload-artifact@v4
       with:
         name: coverage-${{steps.date.outputs.date}}
         path: ${{github.workspace}}/coverage.html
         retention-days: 4
 
-    - uses: actions/upload-artifact@v3
+    - uses: actions/upload-artifact@v4
       with:
         name: coverage-details-${{steps.date.outputs.date}}
         path: ${{env.COV_DETAILS_PATH}}

.github/workflows/wasm-release.yml

@@ -36,7 +36,7 @@ jobs:
           cp ../../../LICENSE.txt .
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v13
+        uses: mymindstorm/setup-emsdk@v14
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

.github/workflows/wasm.yml

@@ -29,7 +29,7 @@ jobs:
           node-version: "lts/*"
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v13
+        uses: mymindstorm/setup-emsdk@v14
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

CMakeLists.txt

@@ -2,7 +2,7 @@
 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.5.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.6.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version

README.md

@@ -14,9 +14,9 @@ See the [release notes](RELEASE_NOTES.md) for notes on various stable releases o
 
 ## Build status
 
-| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | 
-| --------------- | --------------|-----------|---------------|------------|
-| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) |
+| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | Windows Build |
+| --------------- | --------------|-----------|---------------|------------|---------------|
+| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml)
 
 <a href="https://github.com/z3prover/z3/pkgs/container/z3">Docker image</a>.
 

RELEASE_NOTES.md

@@ -10,14 +10,25 @@ 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.6
+==============
+- remove expensive rewrite that coalesces adjacent stores
+- improved Java use of reference queues thanks to Thomas Haas #7131
+- fixes to conditional import of python library thanks to Cal Jacobson #7116
+- include universe for constants that get removed during pre-processing #7121
+- code improvements, Bruce Mitchener #7119
+- fix nested callback handling for user propagators
+- include ARM64 binaries in distribution
+- added Julia API, Thanks to Yisu Remy Yang #7108
+
 Version 4.12.5
 ==============
 - Fixes to pypi setup and build for MacOS distributions
 - A new theory solver "int-blast" enabled by using:
   - sat.smt=true smt.bv.solver=2
   - It solves a few bit-vector problems not handled by bit-blasting, especially if the bit-widths are large.
-  - It is based on encoding bit-vector constraints to non-linear integer arithemtic.
-
+  - It is based on encoding bit-vector constraints to non-linear integer arithmetic.
+- Optimizations to the arithmetic solver. Description: https://github.com/Z3Prover/doc/tree/master/arithmetic
 
 Version 4.12.4
 ==============

azure-pipelines.yml

@@ -183,63 +183,6 @@ jobs:
       - template: scripts/test-regressions.yml
          
 
-- job: "WindowsLatest"
-  displayName: "Windows"
-  pool: 
-    vmImage: "windows-latest"
-  strategy:
-    matrix:
-      x86:
-        arch: 'x86'
-        setupCmd1: ''
-        setupCmd2: ''
-        setupCmd3: ''
-        bindings: '$(cmakePy)'
-        runTests: 'False'
-      x64:
-        arch: 'x64'
-        setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\"))"'
-        setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
-        setupCmd3: 'set /P JlCxxDir=<tmp.env'
-        bindings:  '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx $(cmakeJava) $(cmakeNet) $(cmakePy) -DCMAKE_BUILD_TYPE=RelWithDebInfo'
-        runTests:  'False'
-      arm64:
-        arch: 'amd64_arm64'
-        setupCmd1: ''
-        setupCmd2: ''
-        setupCmd3: ''
-        bindings: ''
-        runTests: 'False'
-  steps:
-    - script: md build
-    - script: |
-         cd build
-         $(setupCmd1)
-         $(setupCmd2)
-         $(setupCmd3)
-         call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
-         cmake $(bindings) -G "NMake Makefiles" ../
-         nmake
-         cd ..
-    - script: |
-         call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
-         pushd build\python
-         python z3test.py z3
-         python z3test.py z3num
-         popd
-         pushd build
-         nmake cpp_example
-         examples\cpp_example_build_dir\cpp_example.exe
-         nmake c_example
-         examples\c_example_build_dir\c_example.exe
-         nmake test-z3
-         test-z3.exe -a
-         popd
-      condition: eq(variables['runTests'], 'True')
-    - script: |
-         git clone https://github.com/z3prover/z3test z3test
-         python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
-      condition: eq(variables['runTests'], 'True')
 
          
 - job: "MacOSPython"

cmake/compiler_warnings.cmake

@@ -30,6 +30,8 @@ set(MSVC_WARNINGS "/W3")
 set(GCC_AND_CLANG_WARNINGS_AS_ERRORS
   # https://clang.llvm.org/docs/DiagnosticsReference.html#wodr
   "-Werror=odr"
+  # https://clang.llvm.org/docs/DiagnosticsReference.html#wreturn-type
+  "-Werror=return-type"
 )
 set(GCC_WARNINGS_AS_ERRORS
   ""

examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2

@@ -50,7 +50,7 @@
     )
 )
 
-; Transition funcion
+; Transition function
 (define-fun body ((f_0 Int) (f Int) (i_0 Int) (i_1 Int)(_A (Array Int Int)) (_x Int)) Bool
     (and
         (= f (ite (= _x (select _A i_0)) 1 f_0))

examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2

@@ -52,7 +52,7 @@
     )
 )
 
-; Transition funcion
+; Transition function
 (define-fun body ((f_0 IntValue) (f IntValue) (i_0 IntValue) (i_1 IntValue)(_A (Array IntValue IntValue)) (_x IntValue)) Bool
     (and
         (= f (ite (= _x (select _A i_0)) #x00000001 f_0))

examples/java/JavaGenericExample.java

@@ -1366,10 +1366,10 @@ class JavaGenericExample
         System.out.println("EnumExample");
         Log.append("EnumExample");
 
-        Symbol name = ctx.mkSymbol("fruit");
+        Symbol name = ctx.mkSymbol("fruit2");
 
-        EnumSort<Object> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple"),
-                ctx.mkSymbol("banana"), ctx.mkSymbol("orange"));
+        EnumSort<Object> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple2"),
+                ctx.mkSymbol("banana2"), ctx.mkSymbol("orange2"));
 
         System.out.println((fruit.getConsts()[0]));
         System.out.println((fruit.getConsts()[1]));

examples/ml/ml_example.ml

@@ -308,6 +308,7 @@ let fpa_example ( ctx : context ) =
   (
     let solver = (mk_solver ctx None) in
 	(Solver.add solver [ c5 ]) ;
+    Printf.printf "Memory in use before `check`: %Lu bytes\n" (Statistics.get_estimated_alloc_size());
     if (check solver []) != SATISFIABLE then
 	  raise (TestFailedException "")
     else

examples/python/bincover.py

@@ -0,0 +1,382 @@
+from z3 import *
+import math
+
+# Rudimentary bin cover solver using the UserPropagator feature.
+# It supports the most basic propagation for bin covering.
+# - each bin has a propositional variable set to true if the bin is covered
+# - each item has a bit-vector recording the assigned bin
+# It searches for a locally optimal solution.
+
+class Bin:
+    """
+    Each bin carries values:
+    - min_bound  - the lower bound required to be added to bin
+    - weight     - the sum of weight of items currently added to bin
+    - slack      - the difference between the maximal possible assignment and the assignments to other bin2bound.
+    - var        - is propagated to true/false if the bin gets filled/cannot be filled.
+    """
+    def __init__(self, min_bound, index):
+        assert min_bound > 0
+        assert index >= 0
+        self.index = index
+        self.min_bound = min_bound
+        self.weight = 0
+        self.slack = 0
+        self.added = []
+        self.var = Bool(f"bin-{index}")
+
+    def set_slack(self, slack):
+        self.slack = slack
+
+    def set_fill(self, fill):
+        self.weight = fill
+
+    def __repr__(self):
+        return f"{self.var}:bound-{self.min_bound}"
+
+
+class Item:
+    def __init__(self, weight, index):
+        self.weight = weight
+        self.index = index
+        self.var = None
+
+    def set_var(self, num_bits):
+        self.var = BitVec(f"binof-{self.index}", num_bits)
+
+    def __repr__(self):
+        return f"binof-{self.index}:weight-{self.weight}"
+
+class BranchAndBound:
+    """Branch and Bound solver.
+    It keeps track of a current best score and a slack that tracks bins that are set unfilled.
+    It blocks branches that are worse than the current best score.
+    In Final check it blocks the current assignment.
+    """
+    def __init__(self, user_propagator):
+        self.up = user_propagator
+
+    def init(self, soft_literals):
+        self.value = 0
+        self.best = 0
+        self.slack = 0
+        self.id2weight = {}
+        self.assigned_to_false = []
+        for p, weight in soft_literals:
+            self.slack += weight
+            self.id2weight[p.get_id()] = weight
+
+    def fixed(self, p, value):
+        weight = self.id2weight[p.get_id()]
+        if is_true(value):
+            old_value = self.value
+            self.up.trail += [lambda : self._undo_value(old_value)]
+            self.value += weight
+        elif self.best > self.slack - weight:
+            self.assigned_to_false += [ p ]
+            self.up.conflict(self.assigned_to_false)
+            self.assigned_to_false.pop(-1)
+        else:
+            old_slack = self.slack
+            self.up.trail += [lambda : self._undo_slack(old_slack)]
+            self.slack -= weight
+            self.assigned_to_false += [p]
+
+    def final(self):
+        if self.value > self.best:
+            self.best = self.value
+        print("Number of bins filled", self.value)
+        for bin in self.up.bins:
+            print(bin.var, bin.added)
+        self.up.conflict(self.assigned_to_false)
+
+    def _undo_value(self, old_value):
+        self.value = old_value
+
+    def _undo_slack(self, old_slack):
+        self.slack = old_slack
+        self.assigned_to_false.pop(-1)
+        
+class BinCoverSolver(UserPropagateBase):
+    """Represent a bin-covering problem by associating each bin with a variable
+       For each item i associate a bit-vector
+       - bin-of-i that carries the bin identifier where an item is assigned.
+
+    """
+
+    def __init__(self, s=None, ctx=None):
+        UserPropagateBase.__init__(self, s, ctx)
+        self.bins = []
+        self.items = []
+        self.item2index = {}
+        self.trail = []  # Undo stack
+        self.lim = []
+        self.solver = s
+        self.initialized = False
+        self.add_fixed(lambda x, v : self._fixed(x, v))
+        self.branch_and_bound = None
+
+
+    # Initialize bit-vector variables for items.
+    # Register the bit-vector variables with the user propagator to get callbacks
+    # Ensure the bit-vector variables are assigned to a valid bin.
+    # Initialize the slack of each bin.
+    def init(self):
+        print(self.bins, len(self.bins))
+        print(self.items)
+        assert not self.initialized
+        self.initialized = True
+        powerof2, num_bits = self._num_bits()
+        for item in self.items:
+            item.set_var(num_bits)
+            self.item2index[item.var.get_id()] = item.index
+            self.add(item.var)
+            if not powerof2:
+                bound = BitVecVal(len(self.bins), num_bits)
+                ineq = ULT(item.var, bound)
+                self.solver.add(ineq)
+        total_weight = sum(item.weight for item in self.items)
+        for bin in self.bins:
+            bin.slack = total_weight
+
+    #
+    # Register optional branch and bound weighted solver.
+    # If it is registered, it 
+    def init_branch_and_bound(self):
+        soft = [(bin.var, 1) for bin in self.bins]
+        self.branch_and_bound = BranchAndBound(self)
+        self.branch_and_bound.init(soft)
+        for bin in self.bins:
+            self.add(bin.var)
+        self.add_final(lambda : self.branch_and_bound.final())
+        
+    def add_bin(self, min_bound):
+        assert not self.initialized
+        index = len(self.bins)
+        bin = Bin(min_bound, index)
+        self.bins += [bin]
+        return bin
+        
+    def add_item(self, weight):
+        assert not self.initialized
+        assert weight > 0
+        index = len(self.items)
+        item = Item(weight, index)
+        self.items += [item]
+        return item
+        
+    def num_items(self):
+        return len(self.items)
+
+    def num_bins(self):
+        return len(self.bins)
+    
+    def _num_bits(self):
+        log = math.log2(self.num_bins())
+        if log.is_integer():
+            return True, int(log)
+        else:
+            return False, int(log) + 1
+
+    def _set_slack(self, bin, slack_value):
+        bin.slack = slack_value
+        
+    def _set_fill(self, bin, fill_value):
+        bin.weight = fill_value
+        bin.added.pop()
+
+    def _itemvar2item(self, v):
+        index  = self.item2index[v.get_id()]
+        if index >= len(self.items):
+            return None
+        return self.items[index]
+
+    def _value2bin(self, value):
+        assert isinstance(value, BitVecNumRef)
+        bin_index = value.as_long()
+        if bin_index >= len(self.bins):
+            return NOne
+        return self.bins[bin_index]
+
+    def _add_item2bin(self, item, bin):
+        # print("add", item, "to", bin)
+        old_weight = bin.weight
+        bin.weight += item.weight
+        bin.added += [item]
+        self.trail += [lambda : self._set_fill(bin, old_weight)]
+        if old_weight < bin.min_bound and old_weight + item.weight >= bin.min_bound:
+            self._propagate_filled(bin)
+
+    # This item can never go into bin
+    def _exclude_item2bin(self, item, bin):
+        # print("exclude", item, "from", bin)
+        # Check if bin has already been blocked
+        if bin.slack < bin.min_bound:
+            return
+        if bin.weight >= bin.min_bound:
+            return
+        old_slack = bin.slack
+        new_slack = old_slack - item.weight
+        bin.slack = new_slack
+        self.trail += [lambda : self._set_slack(bin, old_slack)]
+        # If the new slack does not permit the bin to be filled, propagate
+        if new_slack < bin.min_bound:
+            self._propagate_slack(bin)
+        
+
+    # Callback from Z3 when an item gets fixed.
+    def _fixed(self, _item, value):
+        if self.branch_and_bound and is_bool(value):
+            self.branch_and_bound.fixed(_item, value)
+            return 
+        item = self._itemvar2item(_item)
+        if item is None:
+            print("no item for ", _item)
+            return
+        bin  = self._value2bin(value)
+        if bin is None:
+            print("no bin for ", value)
+            return
+        self._add_item2bin(item, bin)
+        for idx in range(len(self.bins)):
+            if idx == bin.index:
+                continue
+            other_bin = self.bins[idx]
+            self._exclude_item2bin(item, other_bin)
+
+    def _propagate_filled(self, bin):
+        """Propagate that bin_index is filled justified by the set of
+        items that have been added
+        """
+        justification = [i.var for i in bin.added]
+        self.propagate(bin.var, justification)
+
+    def _propagate_slack(self, bin):
+        """Propagate that bin_index cannot be filled"""
+        justification = []
+        for other_bin in self.bins:
+            if other_bin.index == bin.index:
+                continue
+            justification += other_bin.added
+        justification = [item.var for item in justification]
+        self.propagate(Not(bin.var), justification)
+
+    def push(self):
+        self.lim += [len(self.trail)]
+
+    def pop(self, n):
+        head = self.lim[len(self.lim) - n]
+        while len(self.trail) > head:
+            self.trail[-1]()
+            self.trail.pop(-1)
+        self.lim = self.lim[0:len(self.lim)-n]                
+
+# Find a first maximally satisfying subset
+class MaximalSatisfyingSubset:
+    def __init__(self, s):
+        self.s = s
+        self.model = None
+
+    def tt(self, f): 
+        return is_true(self.model.eval(f))
+
+    def get_mss(self, ps):
+        s = self.s
+        if sat != s.check():
+            return []
+        self.model = s.model()
+        mss = { q for q in ps if self.tt(q) }
+        return self._get_mss(mss, ps)
+
+    def _get_mss(self, mss, ps):
+        ps = set(ps) - mss
+        backbones = set([])
+        s = self.s
+        while len(ps) > 0:
+            p = ps.pop()
+            if sat == s.check(mss | backbones | { p }):
+                self.model = s.model()
+                mss = mss | { p } | { q for q in ps if self.tt(q) }
+                ps  = ps - mss
+            else:
+                backbones = backbones | { Not(p) }
+        return mss
+    
+
+class OptimizeBinCoverSolver:
+    def __init__(self):
+        self.solver = Solver()
+        self.bin_solver = BinCoverSolver(self.solver)
+        self.mss_solver = MaximalSatisfyingSubset(self.solver)
+
+    #
+    # Facilities to set up solver
+    # First add items and bins.
+    # Keep references to the returned objects.
+    # Then call init
+    # Then add any other custom constraints to the "solver" object.
+    #
+    def init(self):
+        self.bin_solver.init()
+
+    def add_item(self, weight):
+        return self.bin_solver.add_item(weight)
+
+    def add_bin(self, min_bound):
+        return self.bin_solver.add_bin(min_bound)
+
+    def optimize(self):
+        self.init()
+        mss = self.mss_solver.get_mss([bin.var for bin in self.bin_solver.bins])
+        print(self.mss_solver.model)
+        print("filled bins", mss)
+        print("bin contents")
+        for bin in self.bin_solver.bins:
+            print(bin, bin.added)
+
+
+def example1():
+    s = OptimizeBinCoverSolver()
+    i1 = s.add_item(2)
+    i2 = s.add_item(4)
+    i3 = s.add_item(5)
+    i4 = s.add_item(2)
+    b1 = s.add_bin(3)
+    b2 = s.add_bin(6)
+    b3 = s.add_bin(1)
+    s.optimize()
+
+#example1()
+
+
+class BranchAndBoundCoverSolver:
+    def __init__(self):
+        self.solver = Solver()
+        self.bin_solver = BinCoverSolver(self.solver)
+
+    def init(self):
+        self.bin_solver.init()
+        self.bin_solver.init_branch_and_bound()
+
+    def add_item(self, weight):
+        return self.bin_solver.add_item(weight)
+
+    def add_bin(self, min_bound):
+        return self.bin_solver.add_bin(min_bound)
+
+    def optimize(self):
+        self.init()
+        self.solver.check()
+
+def example2():
+    s = BranchAndBoundCoverSolver()
+    i1 = s.add_item(2)
+    i2 = s.add_item(4)
+    i3 = s.add_item(5)
+    i4 = s.add_item(2)
+    b1 = s.add_bin(3)
+    b2 = s.add_bin(6)
+    b3 = s.add_bin(1)
+    s.optimize()
+
+example2()

examples/python/proofreplay.py

@@ -86,7 +86,7 @@ if __name__ == "__main__":
     # The pair -inst 2 indicates that two quantifier instantiations were not self-validated
     # They were instead validated using a call to SMT solving. A log for an smt invocation
     # is exemplified in the next line.
-    # Note that the pair +inst 6 indicates that 6 quantifier instantations were validated
+    # Note that the pair +inst 6 indicates that 6 quantifier instantiations were validated
     # using a syntactic (cheap) check. Some quantifier instantiations based on quantifier elimination
     # are not simple substitutions and therefore a simple syntactic check does not suffice.
     set_param("solver.proof.check", True)

scripts/build-win-signed-cmake.yml

@@ -0,0 +1,99 @@
+parameters:
+  ReleaseVersion: ''
+  BuildArchitecture: ''
+  VCArchitecture: ''
+
+jobs:
+- job: WindowsBuild${{parameters.BuildArchitecture}}
+  displayName: "Windows build (${{parameters.BuildArchitecture}})"
+  pool:
+    vmImage: "windows-latest"
+  steps:
+  - powershell: write-host $(System.TeamProjectId)
+    displayName: 'System.TeamProjectId'
+  - powershell: write-host $(System.DefinitionId)
+    displayName: 'System.DefinitionId'
+  - powershell: write-host $(Build.BuildId)
+    displayName: 'Build.BuildId'
+  - task: CmdLine@2
+    displayName: Build
+    inputs:
+      script:
+        call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" ${{parameters.VCArchitecture}} &
+        python scripts\mk_win_dist_cmake.py
+            --${{parameters.BuildArchitecture}}-only
+            --assembly-version=${{parameters.ReleaseVersion}}
+            --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+  - task: CopyFiles@2
+    displayName: 'Collect Symbols'
+    inputs:
+      sourceFolder: build-dist/${{parameters.BuildArchitecture}}/
+      contents: '*.pdb'
+      targetFolder: '$(Build.ArtifactStagingDirectory)/symbols'
+  # Publish symbol archive to match nuget package
+  # Index your source code and publish symbols to a file share or Azure Artifacts symbol server
+  - task: PublishSymbols@2
+    inputs:
+      symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols'
+      searchPattern: '**/*.pdb' 
+      indexSources: false # Github sources not supported
+      publishSymbols: true
+      symbolServerType: TeamServices
+      detailedLog: true
+  - task: EsrpCodeSigning@2
+    displayName: Sign
+    inputs:
+      ConnectedServiceName: 'z3-esrp-signing-2'
+      FolderPath: 'build-dist/${{parameters.BuildArchitecture}}/dist/z3-${{parameters.ReleaseVersion}}-${{parameters.BuildArchitecture}}-win/bin'
+      Pattern: 'Microsoft.Z3.dll,libz3.dll,libz3java.dll,z3.exe'
+      signConfigType: 'inlineSignParams'
+      inlineOperation: |
+        [
+          {
+            "keyCode": "CP-230012",
+            "operationSetCode": "SigntoolSign",
+            "parameters": [
+              {
+                "parameterName": "OpusName",
+                "parameterValue": "Microsoft"
+              },
+              {
+                "parameterName": "OpusInfo",
+                "parameterValue": "http://www.microsoft.com"
+              },
+              {
+                "parameterName": "PageHash",
+                "parameterValue": "/NPH"
+              },
+              {
+                "parameterName": "FileDigest",
+                "parameterValue": "/fd sha256"
+              },
+              {
+                "parameterName": "TimeStamp",
+                "parameterValue": "/tr \"http://rfc3161.gtm.corp.microsoft.com/TSS/HttpTspServer\" /td sha256"
+              }
+            ],
+            "toolName": "signtool.exe",
+            "toolVersion": "6.2.9304.0"
+          }
+        ]
+      SessionTimeout: '60'
+      MaxConcurrency: '50'
+      MaxRetryAttempts: '5'
+  - task: DeleteFiles@1
+    displayName: Cleanup
+    inputs:
+      SourceFolder: 'build-dist/${{parameters.BuildArchitecture}}/dist/z3-${{parameters.ReleaseVersion}}-${{parameters.BuildArchitecture}}-win/bin'
+      Contents: 'CodeSignSummary*'
+  - task: ArchiveFiles@2
+    displayName: Zip
+    inputs:
+      rootFolderOrFile: 'build-dist/${{parameters.BuildArchitecture}}/dist/z3-${{parameters.ReleaseVersion}}-${{parameters.BuildArchitecture}}-win'
+      includeRootFolder: true
+      archiveType: 'zip'
+      archiveFile: '$(Build.ArtifactStagingDirectory)/z3-${{parameters.ReleaseVersion}}-${{parameters.BuildArchitecture}}-win.zip'
+  - task: PublishPipelineArtifact@1
+    inputs:
+      targetPath: '$(Build.ArtifactStagingDirectory)/z3-${{parameters.ReleaseVersion}}-${{parameters.BuildArchitecture}}-win.zip'
+      artifactName: 'WindowsBuild-${{parameters.BuildArchitecture}}'

scripts/mk_nuget_task.py

@@ -21,9 +21,10 @@ def mk_dir(d):
     if not os.path.exists(d):
         os.makedirs(d)
 
-os_info = {  'ubuntu-latest' : ('so', 'linux-x64'),
-             'ubuntu-18' : ('so', 'linux-x64'),
-             'ubuntu-20' : ('so', 'linux-x64'),
+os_info = {  'x64-ubuntu-latest' : ('so', 'linux-x64'),
+             'x64-ubuntu-18' : ('so', 'linux-x64'),
+             'x64-ubuntu-20' : ('so', 'linux-x64'),
+             'x64-ubuntu-22' : ('so', 'linux-x64'),
              'x64-glibc-2.35' : ('so', 'linux-x64'),
              'x64-win' : ('dll', 'win-x64'),
              'x86-win' : ('dll', 'win-x86'),
@@ -78,8 +79,15 @@ def unpack(packages, symbols, arch):
                 if symbols:
                     files += ["Microsoft.Z3.pdb", "Microsoft.Z3.xml"]
                 for b in files:
-                    zip_ref.extract(f"{package_dir}/bin/{b}", f"{tmp}")
-                    replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard2.0/{b}")
+                    file = f"{package_dir}/bin/{b}"
+                    if os.path.exists(file):
+                        zip_ref.extract(file, f"{tmp}")
+                        replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard2.0/{b}")
+                    file = os.path.join(file,"netstandard2.0")
+                    if os.path.exists(file):
+                        zip_ref.extract(file, f"{tmp}")
+                        replace(f"{tmp}/{package_dir}/bin/netstandard2.0/{b}", f"out/lib/netstandard2.0/{b}")
+
 
 def mk_targets(source_root):
     mk_dir("out/build")
@@ -88,11 +96,7 @@ def mk_targets(source_root):
 def mk_icon(source_root):
     mk_dir("out/content")
     shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
-<<<<<<< HEAD
 #   shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
-=======
-    shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
->>>>>>> bdc40b1f5f83cca22dc1d6c5808e935a3b50176c
 
 
     
@@ -113,7 +117,6 @@ Linux Dependencies:
         <copyright>&#169; Microsoft Corporation. All rights reserved.</copyright>
         <tags>smt constraint solver theorem prover</tags>
         <icon>content/icon.jpg</icon>
-        <readme>content/README.md</readme>
         <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
         <license type="expression">MIT</license>
         <repository type="git" url="{1}" branch="{2}" commit="{3}" />
@@ -123,10 +126,6 @@ Linux Dependencies:
             <group targetFramework=".netstandard2.0" />
         </dependencies>
     </metadata>
-    <files>
-      <file src="content/README.md" target="content/README.md"/>
-      <file src="content/icon.jpg" target="content/icon.jpg"/>
-    </files>
 </package>""".format(version, repo, branch, commit, arch)
     print(contents)
     sym = "sym." if symbols else ""

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 12, 5, 0) # express a default build version or pick up ci build version
+    set_version(4, 12, 6, 0) # express a default build version or pick up ci build version
     
 # Z3 Project definition
 def init_project_def():
@@ -40,6 +40,7 @@ def init_project_def():
     add_lib('model',  ['macros'])
     add_lib('converters', ['model'], 'ast/converters')
     add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
+    add_lib('ast_sls', ['ast','normal_forms','converters'], 'ast/sls')
     add_lib('tactic', ['simplifiers'])
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
@@ -65,7 +66,7 @@ def init_project_def():
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
-    add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
+    add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics', 'ast_sls'], 'tactic/sls')
     add_lib('qe', ['smt', 'mbp', 'qe_lite', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe')
     add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
     add_lib('fd_solver', ['core_tactics', 'arith_tactics', 'sat_solver', 'smt'], 'tactic/fd_solver') 

scripts/mk_unix_dist_cmake.py

@@ -0,0 +1,268 @@
+############################################
+# Copyright (c) 2013 Microsoft Corporation
+#
+# Scripts for automatically generating
+# Linux/OSX/BSD distribution zip files.
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+
+import os
+import subprocess
+import zipfile
+import re
+import getopt
+import sys
+import shutil
+from mk_exception import *
+from fnmatch import fnmatch
+
+def getenv(name, default):
+    try:
+        return os.environ[name].strip(' "\'')
+    except:
+        return default
+
+BUILD_DIR = 'build-dist'
+DIST_DIR = 'dist'
+VERBOSE = True
+FORCE_MK = False
+ASSEMBLY_VERSION = None
+DOTNET_CORE_ENABLED = True
+DOTNET_KEY_FILE = None
+JAVA_ENABLED = True
+JULIA_ENABLED = False
+GIT_HASH = False
+PYTHON_ENABLED = True
+ARM64 = False
+MAKEJOBS = getenv("MAKEJOBS", "24")
+
+def set_verbose(flag):
+    global VERBOSE
+    VERBOSE = flag
+
+def is_verbose():
+    return VERBOSE
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        if is_verbose():
+            print("Make directory", d)
+        os.makedirs(d)
+
+def get_z3_name():
+    version = "4"
+    if ASSEMBLY_VERSION:
+        version = ASSEMBLY_VERSION
+    print("Assembly version:", version)
+    if GIT_HASH:
+        return 'z3-%s.%s' % (version, get_git_hash())
+    else:
+        return 'z3-%s' % (version)
+
+def get_build_dir():
+    return BUILD_DIR
+
+def get_build_dist():
+    return os.path.join(get_build_dir(), DIST_DIR)
+
+def get_build_dist_path():
+    return os.path.join(get_build_dist(), get_z3_name())
+
+def set_build_dir(path):
+    global BUILD_DIR
+    BUILD_DIR = os.path.expanduser(os.path.normpath(path))
+    mk_dir(BUILD_DIR)
+
+def display_help():
+    print("mk_unix_dist_cmake.py: Z3 Unix distribution generator\n")
+    print("This script generates the zip files containing executables, shared objects, header files for Unix.")
+    print("It must be executed from the Z3 root directory.")
+    print("\nOptions:")
+    print("  -h, --help                    display this message.")
+    print("  -s, --silent                  do not print verbose messages.")
+    print("  -b <subdir>, --build=<subdir> subdirectory where Z3 will be built (default: build-dist).")
+    print("  -f, --force                   force script to regenerate Makefiles.")
+    print("  --version=<version>           release version.")
+    print("  --assembly-version            assembly version for dll")
+    print("  --nodotnet                    do not include .NET bindings in the binary distribution files.")
+    print("  --dotnet-key=<file>           strongname sign the .NET assembly with the private key in <file>.")
+    print("  --nojava                      do not include Java bindings in the binary distribution files.")
+    print("  --nopython                    do not include Python bindings in the binary distribution files.")
+    print("  --julia                       build Julia bindings.")
+    print("  --githash                     include git hash in the Zip file.")
+    print("  --arm64                       build for ARM64 architecture.")
+    exit(0)
+
+# Parse configuration option for mk_make script
+def parse_options():
+    global FORCE_MK, JAVA_ENABLED, JULIA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, PYTHON_ENABLED, ARM64
+    path = BUILD_DIR
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
+                                                                   'help',
+                                                                   'silent',
+                                                                   'force',
+                                                                   'nojava',
+                                                                   'nodotnet',
+                                                                   'dotnet-key=',
+                                                                   'assembly-version=',
+                                                                   'githash',
+                                                                   'nopython',
+                                                                   'julia',
+                                                                   'arm64'
+                                                                   ])
+    for opt, arg in options:
+        if opt in ('-b', '--build'):
+            if arg == 'src':
+                raise MKException('The src directory should not be used to host the Makefile')
+            path = arg
+        elif opt in ('-s', '--silent'):
+            set_verbose(False)
+        elif opt in ('-h', '--help'):
+            display_help()
+        elif opt in ('-f', '--force'):
+            FORCE_MK = True
+        elif opt == '--nodotnet':
+            DOTNET_CORE_ENABLED = False
+        elif opt == '--assembly-version':
+            ASSEMBLY_VERSION = arg
+        elif opt == '--nopython':
+            PYTHON_ENABLED = False
+        elif opt == '--dotnet-key':
+            DOTNET_KEY_FILE = arg
+        elif opt == '--nojava':
+            JAVA_ENABLED = False
+        elif opt == '--julia':
+            JULIA_ENABLED = True
+        elif opt == '--githash':
+            GIT_HASH = True
+        elif opt == '--arm64':
+            ARM64 = True
+        else:
+            raise MKException("Invalid command line option '%s'" % opt)
+    set_build_dir(path)
+
+def check_output(cmd):
+    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
+    if out != None:
+        enc = sys.getdefaultencoding()
+        if enc != None: return out.decode(enc).rstrip('\r\n')
+        else: return out.rstrip('\r\n')
+    else:
+        return ""
+
+def get_git_hash():
+    try:
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
+        r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
+    except:
+        raise MKException("Failed to retrieve git hash")
+    ls = r.split(' ')
+    if len(ls) != 2:
+        raise MKException("Unexpected git output " + r)
+    return ls[0]
+
+# Create a build directory using CMake
+def mk_build_dir():
+    build_path = get_build_dir()
+    if not os.path.exists(build_path) or FORCE_MK:
+        mk_dir(build_path)
+        cmds = []
+        cmds.append(f"cd {build_path}")
+        cmd = []
+        cmd.append("cmake -S .")
+        if DOTNET_CORE_ENABLED:
+            cmd.append(' -DZ3_BUILD_DOTNET_BINDINGS=ON')
+        if JAVA_ENABLED:
+            cmd.append(' -DZ3_BUILD_JAVA_BINDINGS=ON')
+            cmd.append(' -DZ3_INSTALL_JAVA_BINDINGS=ON')
+            cmd.append(' -DZ3_JAVA_JAR_INSTALLDIR=java')
+            cmd.append(' -DZ3_JAVA_JNI_LIB_INSTALLDIR=bin/java')
+        if PYTHON_ENABLED:
+            cmd.append(' -DZ3_BUILD_PYTHON_BINDINGS=ON')
+            cmd.append(' -DZ3_INSTALL_PYTHON_BINDINGS=ON')
+            cmd.append(' -DCMAKE_INSTALL_PYTHON_PKG_DIR=bin/python')
+        if JULIA_ENABLED:
+            cmd.append(' -DZ3_BUILD_JULIA_BINDINGS=ON')
+            cmd.append(' -DZ3_INSTALL_JULIA_BINDINGS=ON')
+        if GIT_HASH:
+            git_hash = get_git_hash()
+            cmd.append(' -DGIT_HASH=' + git_hash)
+        cmd.append(' -DZ3_USE_LIB_GMP=OFF')
+        cmd.append(' -DZ3_BUILD_LIBZ3_SHARED=ON')
+        cmd.append(' -DCMAKE_BUILD_TYPE=RelWithDebInfo')
+        cmd.append(' -DCMAKE_INSTALL_PREFIX=' + get_build_dist_path())
+        cmd.append(' -G "Ninja"')
+        cmd.append(' ..\n')
+        cmds.append("".join(cmd))
+        print("CMAKE commands:", cmds)
+        sys.stdout.flush()
+        if exec_cmds(cmds) != 0:
+            raise MKException("failed to run commands")
+
+def exec_cmds(cmds):
+    cmd_file = 'z3_tmp.sh'
+    f = open(cmd_file, 'w')
+    for cmd in cmds:
+        f.write(cmd)
+        f.write('\n')
+    f.close()
+    res = 0
+    try:
+        res = subprocess.call(['sh', cmd_file])
+    except:
+        res = 1
+    try:
+        os.remove(cmd_file)
+    except:
+        pass
+    return res
+
+def build_z3():
+    if is_verbose():
+        print("build z3")
+    build_dir = get_build_dir()
+    cmds = []
+    cmds.append('cd %s' % build_dir)
+    cmds.append('ninja install')
+    if exec_cmds(cmds) != 0:
+        raise MKException("Failed to make z3")
+
+def mk_zip():
+    build_dist = get_build_dist_path()
+    dist_name = get_z3_name()
+    old = os.getcwd()
+    try:
+        if is_verbose():
+            print("dist path", build_dist)
+        mk_dir(build_dist)
+        zfname = '%s.zip' % dist_name
+        zipout = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
+        os.chdir(get_build_dist())
+        for root, dirs, files in os.walk("."):
+            for f in files:
+                if is_verbose():
+                    print("adding ", os.path.join(root, f))
+                zipout.write(os.path.join(root, f))
+        if is_verbose():
+            print("Generated '%s'" % zfname)
+    except:
+        pass
+    os.chdir(old)
+
+def cp_license():
+    if is_verbose():
+        print("copy licence")
+    path = get_build_dist_path()
+    mk_dir(path)
+    shutil.copy("LICENSE.txt", path)
+
+# Entry point
+def main():
+    parse_options()
+    mk_build_dir()
+    build_z3()
+    cp_license()
+    mk_zip()
+
+main()

scripts/mk_win_dist_cmake.py

@@ -0,0 +1,423 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+#
+# Scripts for automatically generating
+# Window distribution zip files.
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+
+import os
+import subprocess
+import zipfile
+import re
+import getopt
+import sys
+import shutil
+from mk_exception import *
+from fnmatch import fnmatch
+
+def getenv(name, default):
+    try:
+        return os.environ[name].strip(' "\'')
+    except:
+        return default
+
+BUILD_DIR = 'build-dist'
+DIST_DIR = 'dist'
+BUILD_X64_DIR = os.path.join(BUILD_DIR, 'x64')
+BUILD_X86_DIR = os.path.join(BUILD_DIR, 'x86')
+BUILD_ARM64_DIR = os.path.join(BUILD_DIR, 'arm64')
+VERBOSE = True
+FORCE_MK = False
+ASSEMBLY_VERSION = None
+DOTNET_CORE_ENABLED = True
+DOTNET_KEY_FILE = None
+JAVA_ENABLED = True
+ZIP_BUILD_OUTPUTS = False
+GIT_HASH = False
+PYTHON_ENABLED = True
+X86ONLY = False
+X64ONLY = False
+ARM64ONLY = False  
+ARCHITECTURES = []
+
+def set_verbose(flag):
+    global VERBOSE
+    VERBOSE = flag
+
+def is_verbose():
+    return VERBOSE
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        if is_verbose():
+            print("Make directory", d)
+        os.makedirs(d)
+
+def get_z3_name(arch):
+    version = "4"
+    if ASSEMBLY_VERSION:
+        version = ASSEMBLY_VERSION
+    print("Assembly version:", version)
+    if GIT_HASH:
+        return 'z3-%s.%s-%s-win' % (version, get_git_hash(), arch)
+    else:
+        return 'z3-%s-%s-win' % (version, arch)
+
+def get_build_dir(arch):
+    return ARCHITECTURES[arch]
+
+def get_build_dist(arch):
+    return os.path.join(get_build_dir(arch), DIST_DIR)
+
+def get_build_dist_path(arch):
+    return os.path.join(get_build_dir(arch), DIST_DIR, get_z3_name(arch))
+
+def get_bin_dist_path(arch):
+    return os.path.join(get_build_dist_path(arch), "bin")
+
+def get_lib_dist_path(arch):
+    return os.path.join(get_build_dist_path(arch), "lib")
+
+def get_java_dist_path(arch):
+    return os.path.join(get_build_dist_path(arch), "java")
+
+def get_dist_path(arch):
+    return os.path.join(DIST_DIR, arch)
+
+def set_build_dir(path):
+    global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR, BUILD_ARM64_DIR, ARCHITECTURES
+    BUILD_DIR = os.path.expanduser(os.path.normpath(path))
+    BUILD_X86_DIR = os.path.join(path, 'x86')
+    BUILD_X64_DIR = os.path.join(path, 'x64')
+    BUILD_ARM64_DIR = os.path.join(path, 'arm64')  # Set ARM64 build directory
+    ARCHITECTURES = {'x64': BUILD_X64_DIR, 'x86':BUILD_X86_DIR, 'arm64':BUILD_ARM64_DIR}
+
+def display_help():
+    print("mk_win_dist.py: Z3 Windows distribution generator\n")
+    print("This script generates the zip files containing executables, dlls, header files for Windows.")
+    print("It must be executed from the Z3 root directory.")
+    print("\nOptions:")    
+    print("  -h, --help                    display this message.")
+    print("  -s, --silent                  do not print verbose messages.")
+    print("  -b <sudir>, --build=<subdir>  subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).")
+    print("  -f, --force                   force script to regenerate Makefiles.")
+    print("  --version=<version>           release version.")
+    print("  --assembly-version            assembly version for dll")
+    print("  --nodotnet                    do not include .NET bindings in the binary distribution files.")
+    print("  --dotnet-key=<file>           strongname sign the .NET assembly with the private key in <file>.")
+    print("  --nojava                      do not include Java bindings in the binary distribution files.")
+    print("  --nopython                    do not include Python bindings in the binary distribution files.")
+    print("  --zip                         package build outputs in zip file.")
+    print("  --githash                     include git hash in the Zip file.")
+    print("  --x86-only                    x86 dist only.")
+    print("  --x64-only                    x64 dist only.")
+    print("  --arm64-only                  arm64 dist only.")
+    exit(0)
+
+# Parse configuration option for mk_make script
+def parse_options():
+    global FORCE_MK, JAVA_ENABLED, ZIP_BUILD_OUTPUTS, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, PYTHON_ENABLED, X86ONLY, X64ONLY, ARM64ONLY
+    path = BUILD_DIR
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
+                                                                   'help',
+                                                                   'silent',
+                                                                   'force',
+                                                                   'nojava',
+                                                                   'nodotnet',
+                                                                   'dotnet-key=',
+                                                                   'assembly-version=',
+                                                                   'zip',
+                                                                   'githash',
+                                                                   'nopython',
+                                                                   'x86-only',
+                                                                   'x64-only',
+                                                                   'arm64-only'
+                                                                   ])
+    for opt, arg in options:
+        if opt in ('-b', '--build'):
+            if arg == 'src':
+                raise MKException('The src directory should not be used to host the Makefile')
+            path = arg
+        elif opt in ('-s', '--silent'):
+            set_verbose(False)
+        elif opt in ('-h', '--help'):
+            display_help()
+        elif opt in ('-f', '--force'):
+            FORCE_MK = True
+        elif opt == '--nodotnet':
+            DOTNET_CORE_ENABLED = False
+        elif opt == '--assembly-version':
+            ASSEMBLY_VERSION = arg
+        elif opt == '--nopython':
+            PYTHON_ENABLED = False
+        elif opt == '--dotnet-key':
+            DOTNET_KEY_FILE = arg
+        elif opt == '--nojava':
+            JAVA_ENABLED = False
+        elif opt == '--zip':
+            ZIP_BUILD_OUTPUTS = True
+        elif opt == '--githash':
+            GIT_HASH = True
+        elif opt == '--x86-only' and not X64ONLY:
+            X86ONLY = True
+        elif opt == '--arm64-only' and not X86ONLY and not X64ONLY: 
+            ARM64ONLY = True
+        elif opt == '--x64-only' and not X86ONLY:
+            X64ONLY = True
+        else:
+            raise MKException("Invalid command line option '%s'" % opt)
+    set_build_dir(path)
+
+# Check whether build directory already exists or not
+def check_build_dir(path):
+    return os.path.exists(path) and os.path.exists(os.path.join(path, 'Makefile'))
+
+def check_output(cmd):
+    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
+    if out != None:
+        enc = sys.getdefaultencoding()
+        if enc != None: return out.decode(enc).rstrip('\r\n')
+        else: return out.rstrip('\r\n')
+    else:
+        return ""
+
+def get_git_hash():
+    try:
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
+        r = check_output(['git', 'show-ref', '--abbrev=12', 'refs/heads/%s' % branch])
+    except:
+        raise MKException("Failed to retrieve git hash")
+    ls = r.split(' ')
+    if len(ls) != 2:
+        raise MKException("Unexpected git output " + r)
+    return ls[0]
+
+
+
+# Create a build directory using mk_make.py
+def mk_build_dir(arch):
+    build_path = get_build_dir(arch)
+    if not check_build_dir(build_path) or FORCE_MK:
+        mk_dir(build_path)
+        vsarch = arch
+        if arch == "arm64":
+            vsarch = "amd64_arm64"
+
+        cmds = []
+        cmds.append(f"cd {build_path}")
+        cmds.append('call "%VCINSTALLDIR%Auxiliary\\build\\vcvarsall.bat" ' + vsarch)
+        cmd = []
+        cmd.append("cmake -S .")
+        if DOTNET_CORE_ENABLED:
+            cmd.append(' -DZ3_BUILD_DOTNET_BINDINGS=ON')
+#           cmd.append(' -DZ3_INSTALL_DOTNET_BINDINGS=ON')
+        if JAVA_ENABLED:
+            cmd.append(' -DZ3_BUILD_JAVA_BINDINGS=ON')
+            cmd.append(' -DZ3_INSTALL_JAVA_BINDINGS=ON')
+            cmd.append(' -DZ3_JAVA_JAR_INSTALLDIR=java')
+            cmd.append(' -DZ3_JAVA_JNI_LIB_INSTALLDIR=bin/java')
+        if PYTHON_ENABLED:
+            cmd.append(' -DZ3_BUILD_PYTHON_BINDINGS=ON')
+            cmd.append(' -DZ3_INSTALL_PYTHON_BINDINGS=ON')
+            cmd.append(' -DCMAKE_INSTALL_PYTHON_PKG_DIR=bin/python')
+
+        if GIT_HASH:
+            git_hash = get_git_hash()
+            cmd.append(' -DGIT_HASH=' + git_hash)
+        cmd.append(' -DZ3_USE_LIB_GMP=OFF')
+        cmd.append(' -DZ3_BUILD_LIBZ3_SHARED=ON')
+        cmd.append(' -DCMAKE_BUILD_TYPE=RelWithDebInfo')
+        cmd.append(' -DCMAKE_INSTALL_PREFIX=' + os.path.join(DIST_DIR, get_z3_name(arch)))
+        cmd.append(' -G "Ninja"')
+        cmd.append(' ../..\n')
+        cmds.append("".join(cmd))
+        print("CMAKE commands:", cmds)
+        sys.stdout.flush()
+        if exec_cmds(cmds) != 0:
+            raise MKException("failed to run commands")
+
+
+    
+# Check if on Visual Studio command prompt
+def check_vc_cmd_prompt():
+    try:
+        DEVNULL = open(os.devnull, 'wb')
+        subprocess.call(['cl'], stdout=DEVNULL, stderr=DEVNULL)
+    except:
+        raise MKException("You must execute the mk_win_dist.py script on a Visual Studio Command Prompt")
+
+def exec_cmds(cmds):
+    cmd_file = 'z3_tmp.cmd'
+    f = open(cmd_file, 'w')
+    for cmd in cmds:
+        f.write(cmd)
+        f.write('\n')
+    f.close()
+    res = 0
+    try:
+        res = subprocess.call(cmd_file, shell=True)
+    except:
+        res = 1
+    try:
+        os.erase(cmd_file)
+    except:
+        pass
+    return res
+
+
+
+def build_z3(arch):
+    if is_verbose():
+        print("build z3")
+    build_dir = get_build_dir(arch)
+    if arch == "arm64":
+        arch = "amd64_arm64"
+    cmds = []
+    cmds.append('call "%VCINSTALLDIR%Auxiliary\\build\\vcvarsall.bat" ' + arch)
+    cmds.append('cd %s' % build_dir)
+    cmds.append('ninja install')
+    if exec_cmds(cmds) != 0:
+        raise MKException("Failed to make z3")
+
+
+
+def mk_zip(arch):
+    if not ZIP_BUILD_OUTPUTS:
+        return
+    build_dist = get_build_dist_path(arch)
+    dist_name = get_z3_name(arch)
+    dist_path = get_dist_path(arch)
+    build_dir = get_build_dir(arch)
+    old = os.getcwd()
+    try:
+        if is_verbose():
+            print("dist path", dist_path)
+        mk_dir(dist_path)
+        zfname = os.path.join(dist_path, '%s.zip' % dist_name)
+        zipout = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
+        os.chdir(get_build_dist(arch))
+        for root, dirs, files in os.walk("."):
+            for f in files:
+                if is_verbose():
+                    print("adding ", os.path.join(root, f))
+                zipout.write(os.path.join(root, f))
+        if is_verbose():
+            print("Generated '%s'" % zfname)
+    except:
+        pass
+    os.chdir(old)
+
+
+
+VS_RUNTIME_PATS = [re.compile(r'vcomp.*\.dll'),
+                   re.compile(r'msvcp.*\.dll'),
+                   re.compile(r'msvcr.*\.dll'),
+                   re.compile(r'vcrun.*\.dll')]
+
+# Copy Visual Studio Runtime libraries
+def cp_vs_runtime(arch):
+    platform = arch
+    vcdir = os.environ['VCINSTALLDIR']
+    path  = '%sredist' % vcdir
+    vs_runtime_files = []
+    print("Walking %s" % path)
+    # Everything changes with every release of VS
+    # Prior versions of VS had DLLs under "redist\x64"
+    # There are now several variants of redistributables
+    # The naming convention defies my understanding so 
+    # we use a "check_root" filter to find some hopefully suitable
+    # redistributable.
+    def check_root(root):
+        return platform in root and ("CRT" in root or "MP" in root) and "onecore" not in root and "debug" not in root
+    for root, dirs, files in os.walk(path):
+        for filename in files:
+            if fnmatch(filename, '*.dll') and check_root(root):
+                print("Checking %s %s" % (root, filename))
+                for pat in VS_RUNTIME_PATS:
+                    if pat.match(filename):
+                        fname = os.path.join(root, filename)
+                        if not os.path.isdir(fname):
+                            vs_runtime_files.append(fname)
+    if not vs_runtime_files:
+        raise MKException("Did not find any runtime files to include")
+    bin_dist_path = get_bin_dist_path(arch)
+    for f in vs_runtime_files:
+        shutil.copy(f, bin_dist_path)
+        if is_verbose():
+            print("Copied '%s' to '%s'" % (f, bin_dist_path))
+        
+def cp_license(arch):
+    if is_verbose():
+        print("copy licence")
+    path = get_build_dist_path(arch)
+    mk_dir(path)
+    shutil.copy("LICENSE.txt", path)
+
+def cp_dotnet(arch):
+    if not DOTNET_CORE_ENABLED:
+        return
+    if is_verbose():
+        print("copy dotnet")
+    build_dir = get_build_dir(arch)
+    dist_dir = get_bin_dist_path(arch)
+    shutil.copytree(os.path.join(build_dir, "Microsoft.Z3"),
+                    dist_dir,
+                    dirs_exist_ok=True)
+
+def cp_into_bin(arch):
+    if is_verbose():
+        print("copy lib")
+    lib_dir = get_lib_dist_path(arch)
+    bin_dir = get_bin_dist_path(arch)
+    shutil.copyfile(os.path.join(lib_dir, "libz3.lib"),
+                os.path.join(bin_dir, "libz3.lib"))
+    shutil.rmtree(lib_dir)
+    if JAVA_ENABLED:
+        java_dir = get_java_dist_path(arch)
+        shutil.copytree(java_dir,
+                        bin_dir,
+                        dirs_exist_ok=True)
+        shutil.rmtree(java_dir)
+                
+def cp_pdb(arch):
+    if is_verbose():
+        print("copy pdb")
+    build_dir = get_build_dir(arch)
+    bin_path = get_bin_dist_path(arch)
+    mk_dir(bin_path)
+    for f in os.listdir(build_dir):
+        if f.endswith("libz3.pdb"):
+            shutil.copy(os.path.join(build_dir, f), bin_path)
+
+def build_for_arch(arch):
+    mk_build_dir(arch)
+    build_z3(arch)
+    cp_license(arch)
+    cp_pdb(arch)
+    cp_dotnet(arch)
+    cp_vs_runtime(arch)
+    cp_into_bin(arch)
+    mk_zip(arch)
+    
+# Entry point
+def main():
+    if os.name != 'nt':
+        raise MKException("This script is for Windows only")
+
+    parse_options()
+    check_vc_cmd_prompt()
+
+    if X86ONLY:
+        build_for_arch("x86")
+    elif X64ONLY:
+        build_for_arch("x64")
+    elif ARM64ONLY: 
+        build_for_arch("arm64")
+    else:
+        for arch in ARCHITECTURES:
+            build_for_arch(arch)
+
+main()
+

scripts/nightly.yaml

@@ -1,28 +1,44 @@
 variables:
   Major: '4'
   Minor: '12'
-  Patch: '5'
+  Patch: '6'
+  ReleaseVersion: $(Major).$(Minor).$(Patch)
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
-  NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
+  NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
 
 stages:
 - stage: Build
   jobs:
-  - job: Mac
-    displayName: "Mac Build"
+  - job: MacBuild
+    displayName: "macOS Build"
     pool:
       vmImage: "macOS-11"
     steps:
-    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
-    - 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@1
+    - task: PythonScript@0
+      displayName: Build
       inputs:
-        artifactName: 'Mac'
+        scriptSource: 'filepath'
+        scriptPath: scripts/mk_unix_dist.py
+        arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+    - script: git clone https://github.com/z3prover/z3test z3test
+      displayName: 'Clone z3test'
+    - task: PythonScript@0
+      displayName: Test
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: z3test/scripts/test_benchmarks.py
+        arguments: build-dist/z3 z3test/regressions/smt2
+    - task: CopyFiles@2
+      inputs:
+        sourceFolder: dist
+        contents: '*.zip'
+        targetFolder: $(Build.ArtifactStagingDirectory)
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'macOSBuild'
         targetPath: $(Build.ArtifactStagingDirectory)
 
-  - job: MacArm64
+  - job: MacBuildArm64
     displayName: "Mac ARM64 Build"
     pool:
       vmImage: "macOS-11"
@@ -35,32 +51,62 @@ stages:
         artifactName: 'MacArm64'
         targetPath: $(Build.ArtifactStagingDirectory)
 
-  - job: Ubuntu20
-    displayName: "Ubuntu20 build"
-    pool:
-      vmImage: "ubuntu-20.04"
-    steps:
-    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
-    - 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: 'Ubuntu-20.04'
-        targetPath: $(Build.ArtifactStagingDirectory)
-
-  - job: Ubuntu
+  - job: UbuntuBuild
     displayName: "Ubuntu build"
     pool:
       vmImage: "ubuntu-latest"
     steps:
-    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+    - task: PythonScript@0
+      displayName: Build
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: scripts/mk_unix_dist.py
+        arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
     - 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)/.
+      displayName: 'Clone z3test'
+    - task: PythonScript@0
+      displayName: Test
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: z3test/scripts/test_benchmarks.py
+        arguments: build-dist/z3 z3test/regressions/smt2
+    - task: CopyFiles@2
+      inputs:
+        sourceFolder: dist
+        contents: '*.zip'
+        targetFolder: $(Build.ArtifactStagingDirectory)
     - task: PublishPipelineArtifact@0
       inputs:
-        artifactName: 'Ubuntu'
+        artifactName: 'UbuntuBuild'
+        targetPath: $(Build.ArtifactStagingDirectory)
+
+  - job: UbuntuBuild20
+    displayName: "Ubuntu build 20"
+    pool:
+      vmImage: "ubuntu-20.04"
+    steps:
+    - task: PythonScript@0
+      displayName: Build
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: scripts/mk_unix_dist.py
+        arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+    - script: git clone https://github.com/z3prover/z3test z3test
+      displayName: 'Clone z3test'
+    - task: PythonScript@0
+      displayName: Test
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: z3test/scripts/test_benchmarks.py
+        arguments: build-dist/z3 z3test/regressions/smt2
+    - task: CopyFiles@2
+      inputs:
+        sourceFolder: dist
+        contents: '*.zip'
+        targetFolder: $(Build.ArtifactStagingDirectory)
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'UbuntuBuild20'
         targetPath: $(Build.ArtifactStagingDirectory)
 
   - job: UbuntuArm64
@@ -68,12 +114,9 @@ stages:
     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: 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:
@@ -115,165 +158,57 @@ stages:
       inputs:
         artifactName: 'UbuntuDoc'
         targetPath: $(Build.ArtifactStagingDirectory)
-
-  - job: ManyLinuxBuild
-    variables:
-      python: "/opt/python/cp37-cp37m/bin/python"
-      name: ManyLinux
+    
+  - job: LinuxBuilds
     displayName: "ManyLinux build"
+    variables:
+      name: ManyLinux
+      python: "/opt/python/cp37-cp37m/bin/python"
     pool:
       vmImage: "ubuntu-latest"
     container: "quay.io/pypa/manylinux2014_x86_64:latest"
     steps:
-    - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
+    - task: PythonScript@0
+      displayName: Build
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: scripts/mk_unix_dist.py
+        arguments: --nodotnet --nojava
+        pythonInterpreter: $(python)
     - 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)/
+      displayName: 'Clone z3test'
+    - task: PythonScript@0
+      displayName: Test
+      inputs:
+        scriptSource: 'filepath'
+        scriptPath: z3test/scripts/test_benchmarks.py
+        arguments: build-dist/z3 z3test/regressions/smt2
+        pythonInterpreter: $(python)
+    - task: CopyFiles@2
+      inputs:
+        sourceFolder: dist
+        contents: '*.zip'
+        targetFolder: $(Build.ArtifactStagingDirectory)
     - task: PublishPipelineArtifact@0
       inputs:
-        artifactName: '$(name)Build'
+        artifactName: 'ManyLinuxBuild'
         targetPath: $(Build.ArtifactStagingDirectory)
+  
+  - template: build-win-signed.yml
+    parameters:
+      ReleaseVersion: $(ReleaseVersion)
+      BuildArchitecture: 'x64'
 
-#  - job: MuslLinuxBuild
-#    condition: eq(0,1)
-#    variables:
-#      python: "/opt/python/cp310-cp310/bin/python"
-#      name: MuslLinux
-#    displayName: "MuslLinux build"
-#    pool:
-#      vmImage: "ubuntu-latest"
-#    container: "quay.io/pypa/musllinux_1_1_x86_64:latest"
-#    steps:
-#    - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
-#    - 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: '$(name)Build'
-#        targetPath: $(Build.ArtifactStagingDirectory)
-
-  - job: Windows32
-    displayName: "Windows 32-bit build"
-    pool:
-      vmImage: "windows-latest"
-    steps:
-    - task: CmdLine@2
-      inputs:
-        script:
-          call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x86 &
-          python scripts\mk_win_dist.py
-            --assembly-version=$(AssemblyVersion)
-            --x86-only
-            --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
-            --zip
-    - task: CopyFiles@2
-      inputs:
-        sourceFolder: dist
-        contents: '*.zip'
-        targetFolder: $(Build.ArtifactStagingDirectory)
-    - task: PublishPipelineArtifact@1
-      inputs:
-        targetPath: $(Build.ArtifactStagingDirectory)
-        artifactName: 'Windows32'
-    - task: CopyFiles@2
-      displayName: 'Collect Symbols'
-      inputs:
-        sourceFolder: dist
-        contents: '**/*.pdb'
-        targetFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-    # Publish symbol archive to match nuget package
-    # Index your source code and publish symbols to a file share or Azure Artifacts symbol server
-    - task: PublishSymbols@2
-      inputs:
-        symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-        searchPattern: '**/*.pdb' 
-        indexSources: false # Github not supported
-        publishSymbols: true
-        symbolServerType: TeamServices
-        detailedLog: true
-
-  - job: Windows64
-    displayName: "Windows 64-bit build"
-    pool:
-      vmImage: "windows-latest"
-    steps:
-    - task: CmdLine@2
-      inputs:
-        script:
-          call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x64 &
-          python scripts\mk_win_dist.py
-            --assembly-version=$(AssemblyVersion)
-            --x64-only
-            --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
-            --zip
-    - task: CopyFiles@2
-      inputs:
-        sourceFolder: dist
-        contents: '*.zip'
-        targetFolder: $(Build.ArtifactStagingDirectory)
-    - task: PublishPipelineArtifact@1
-      inputs:
-        targetPath: $(Build.ArtifactStagingDirectory)
-        artifactName: 'Windows64'
-    - task: CopyFiles@2
-      displayName: 'Collect Symbols'
-      inputs:
-        sourceFolder: dist
-        contents: '**/*.pdb'
-        targetFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-    # Publish symbol archive to match nuget package
-    # Index your source code and publish symbols to a file share or Azure Artifacts symbol server
-    - task: PublishSymbols@2
-      inputs:
-        symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-        searchPattern: '**/*.pdb' 
-        indexSources: false # Github not supported
-        publishSymbols: true
-        symbolServerType: TeamServices
-        detailedLog: true
-
-  - job: "WindowsArm64"
-    displayName: "WindowsArm64"
-    pool: 
-      vmImage: "windows-latest"
-    variables:
-       arch: "amd64_arm64"
-       bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo"
-    steps:
-    - script: md build
-    - script: |
-         cd build
-         call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
-         cmake $(bindings) -G "NMake Makefiles" ../
-         nmake
-         cd ..
-    - task: CopyFiles@2
-      inputs:
-        sourceFolder: build
-        contents: '*z3*.*'
-        targetFolder: $(Build.ArtifactStagingDirectory)
-    - task: PublishPipelineArtifact@1
-      inputs:
-        targetPath: $(Build.ArtifactStagingDirectory)
-        artifactName: 'WindowsArm64'
-    - task: CopyFiles@2
-      displayName: 'Collect Symbols'
-      inputs:
-        sourceFolder: build
-        contents: '**/*.pdb'
-        targetFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-    # Publish symbol archive to match nuget package
-    # Index your source code and publish symbols to a file share or Azure Artifacts symbol server
-    - task: PublishSymbols@2
-      inputs:
-        symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols'
-        searchPattern: '**/*.pdb' 
-        indexSources: false # Github not supported
-        publishSymbols: true
-        symbolServerType: TeamServices
-        detailedLog: true
+  - template: build-win-signed.yml
+    parameters:
+      ReleaseVersion: $(ReleaseVersion)
+      BuildArchitecture: 'x86'
 
+  - template: build-win-signed-cmake.yml
+    parameters:
+      ReleaseVersion: $(ReleaseVersion)
+      BuildArchitecture: 'arm64'
+      VCArchitecture: 'amd64_arm64'
 
 - stage: Package
   jobs:
@@ -291,27 +226,22 @@ stages:
     - task: DownloadPipelineArtifact@2
       displayName: 'Download Win64 Build'
       inputs:
-        artifact: 'Windows64'
-        path: $(Agent.TempDirectory)\package
-    - task: DownloadPipelineArtifact@2
-      displayName: 'Download Ubuntu Build'
-      inputs:
-        artifact: 'Ubuntu'
+        artifact: 'WindowsBuild-x64'
         path: $(Agent.TempDirectory)\package
     - task: DownloadPipelineArtifact@2
       displayName: 'Download Ubuntu 20.04 Build'
       inputs:
-        artifact: 'Ubuntu-20.04'
+        artifact: 'UbuntuBuild20'
         path: $(Agent.TempDirectory)\package
     - task: DownloadPipelineArtifact@2
       displayName: 'Download Ubuntu ARM64 Build'
       inputs:
         artifact: 'UbuntuArm64'
-        path: $(Agent.TempDirectory)\package
+        path: $(Agent.TempDirectory)\package    
     - task: DownloadPipelineArtifact@2
       displayName: 'Download macOS Build'
       inputs:
-        artifact: 'Mac'
+        artifact: 'macOsBuild'
         path: $(Agent.TempDirectory)\package
     - task: DownloadPipelineArtifact@2
       displayName: 'Download macOS Arm64 Build'
@@ -420,7 +350,7 @@ stages:
     - task: DownloadPipelineArtifact@2
       displayName: 'Download Win32 Build'
       inputs:
-        artifact: 'Windows32'
+        artifact: 'WindowsBuild-x86'
         path: $(Agent.TempDirectory)\package
     - task: NuGetToolInstaller@0
       inputs:
@@ -519,24 +449,19 @@ stages:
     steps:
     - task: DownloadPipelineArtifact@2
       inputs:
-        artifactName: 'Windows32'
+        artifactName: 'WindowsBuild-x86'
         targetPath: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       inputs:
-        artifactName: 'Windows64'
+        artifactName: 'WindowsBuild-x64'
         targetPath: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       inputs:
         artifactName: 'ManyLinuxBuild'
         targetPath: $(Agent.TempDirectory)
-#    - task: DownloadPipelineArtifact@2
-#      displayName: 'Download MuslLinux Build'
-#      inputs:
-#        artifact: 'MuslLinuxBuild'
-#        path: $(Agent.TempDirectory)	
     - task: DownloadPipelineArtifact@2
       inputs:
-        artifactName: 'Mac'
+        artifactName: 'macOsBuild'
         targetPath: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       inputs:
@@ -574,22 +499,22 @@ stages:
     - task: DownloadPipelineArtifact@2
       displayName: "Download windows32"
       inputs:
-        artifactName: 'Windows32'
-        targetPath: tmp
-    - task: DownloadPipelineArtifact@2
-      displayName: "Download windowsArm64"
-      inputs:
-        artifactName: 'WindowsArm64'
+        artifactName: 'WindowsBuild-x86'
         targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download windows64"
       inputs:
-        artifactName: 'Windows64'
+        artifactName: 'WindowsBuild-x64'
+        targetPath: tmp
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download windowsARM64"
+      inputs:
+        artifactName: 'WindowsBuild-arm64'
         targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download Mac"
       inputs:
-        artifactName: 'Mac'
+        artifactName: 'macOsBuild'
         targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download MacArm64"
@@ -601,15 +526,10 @@ stages:
       inputs:
         artifactName: 'UbuntuArm64'
         targetPath: tmp
-    - task: DownloadPipelineArtifact@2
-      displayName: "Download Ubuntu"
-      inputs:
-        artifactName: 'Ubuntu'
-        targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download Ubuntu-20.04"
       inputs:
-        artifactName: 'Ubuntu-20.04'
+        artifactName: 'UbuntuBuild20'
         targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download Doc"

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.12.5'
+  ReleaseVersion: '4.12.6'
 
 stages:
 
@@ -209,6 +209,12 @@ stages:
       ReleaseVersion: $(ReleaseVersion)
       BuildArchitecture: 'x86'
 
+  - template: build-win-signed-cmake.yml
+    parameters:
+      ReleaseVersion: $(ReleaseVersion)
+      BuildArchitecture: 'arm64'
+      VCArchitecture: 'amd64_arm64'
+
 
 # Creates Z3 packages in various formats
 - stage: Package
@@ -525,16 +531,21 @@ stages:
       inputs:
         artifact: 'WindowsBuild-x86'
         path: $(Agent.TempDirectory)
-    - task: DownloadPipelineArtifact@2
-      displayName: "Download Python"
-      inputs:
-        artifactName: 'PythonPackage'
-        path: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       displayName: 'Download Win64 Build'
       inputs:
         artifact: 'WindowsBuild-x64'
         path: $(Agent.TempDirectory)
+    - task: DownloadPipelineArtifact@2
+      displayName: 'Download Arm64 Build'
+      inputs:
+        artifact: 'WindowsBuild-arm64'
+        path: $(Agent.TempDirectory)	
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download Python"
+      inputs:
+        artifactName: 'PythonPackage'
+        path: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       displayName: 'Download NuGet64 Package'
       inputs:

scripts/update_api.py

@@ -641,8 +641,8 @@ def mk_java(java_src, java_dir, package_name):
   public static native void propagateRegisterEq(Object o, long ctx, long solver);
   public static native void propagateRegisterDecide(Object o, long ctx, long solver);
   public static native void propagateRegisterFinal(Object o, long ctx, long solver);
-  public static native void propagateConflict(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq);
   public static native void propagateAdd(Object o, long ctx, long solver, long javainfo, long e);
+  public static native boolean propagateConsequence(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq);
   public static native boolean propagateNextSplit(Object o, long ctx, long solver, long javainfo, long e, long idx, int phase);
   public static native void propagateDestroy(Object o, long ctx, long solver, long javainfo);
 
@@ -698,6 +698,8 @@ def mk_java(java_src, java_dir, package_name):
     protected abstract void createdWrapper(long le);
 
     protected abstract void fixedWrapper(long lvar, long lvalue);
+
+    protected abstract void decideWrapper(long lvar, int bit, boolean is_pos);
   }
     """)
     java_native.write('\n')

src/CMakeLists.txt

@@ -54,6 +54,7 @@ add_subdirectory(ast/euf)
 add_subdirectory(ast/converters)
 add_subdirectory(ast/substitution)
 add_subdirectory(ast/simplifiers)
+add_subdirectory(ast/sls)
 add_subdirectory(tactic)
 add_subdirectory(qe/mbp)
 add_subdirectory(qe/lite)

src/api/api_ast.cpp

@@ -146,8 +146,7 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
         if (!p.has_def(d)) {
-            std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
-            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl");
             return;
         }
         expr_ref abs_body(m);
@@ -168,8 +167,7 @@ extern "C" {
             return;
         }
         if (!pd.get_def()->get_cases().empty()) {
-            std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
-            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " has already been given a definition");
             return;            
         }
                 
@@ -377,9 +375,7 @@ extern "C" {
         RESET_ERROR_CODE();
         symbol _s = to_symbol(s);
         if (_s.is_numerical()) {
-            std::ostringstream buffer;
-            buffer << _s.get_num();
-            return mk_c(c)->mk_external_string(buffer.str());
+            return mk_c(c)->mk_external_string(std::to_string(_s.get_num()));
         }
         else {
             return mk_c(c)->mk_external_string(_s.str());
@@ -823,7 +819,7 @@ extern "C" {
         param_descrs descrs;
         th_rewriter::get_param_descrs(descrs);
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -1031,7 +1027,7 @@ extern "C" {
         default:
             UNREACHABLE();
         }
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN(nullptr);
     }
 
@@ -1066,7 +1062,7 @@ extern "C" {
             pp.add_assumption(to_expr(assumptions[i]));
         }
         pp.display_smt2(buffer, to_expr(formula));
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

src/api/api_ast_map.cpp

@@ -160,8 +160,8 @@ extern "C" {
         for (; it != end; ++it) {
             buffer << "\n  (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n   " << mk_ismt2_pp(it->m_value, mng, 3) << ")";
         }
-        buffer << ")";
-        return mk_c(c)->mk_external_string(buffer.str());
+        buffer << ')';
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN(nullptr);
     }
 

src/api/api_config_params.cpp

@@ -98,7 +98,10 @@ extern "C" {
         LOG_Z3_set_param_value(c, param_id, param_value);
         try {
             ast_context_params * p = reinterpret_cast<ast_context_params*>(c);
-            p->set(param_id, param_value);
+            if (p->is_shell_only_parameter(param_id)) 
+                warning_msg("parameter %s can only be set for the shell, not binary API", param_id);
+            else
+                p->set(param_id, param_value);
         }
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
@@ -111,7 +114,10 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_update_param_value(c, param_id, param_value);
         RESET_ERROR_CODE();
-        mk_c(c)->params().set(param_id, param_value);
+        if (mk_c(c)->params().is_shell_only_parameter(param_id))
+            warning_msg("parameter %s can only be set for the shell, not binary API", param_id);
+        else
+            mk_c(c)->params().set(param_id, param_value);
         Z3_CATCH;
     }
 

src/api/api_context.cpp

@@ -338,12 +338,12 @@ namespace api {
                 std::ostringstream buffer;
                 app * a = to_app(n);
                 buffer << mk_pp(a->get_decl(), m()) << " applied to: ";
-                if (a->get_num_args() > 1) buffer << "\n";
+                if (a->get_num_args() > 1) buffer << '\n';
                 for (unsigned i = 0; i < a->get_num_args(); ++i) {
                     buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort ";
-                    buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << "\n";
+                    buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << '\n';
                 }
-                auto str = buffer.str();
+                auto str = std::move(buffer).str();
                 warning_msg("%s", str.c_str());
                 break;
             }

src/api/api_fpa.cpp

@@ -1022,7 +1022,7 @@ extern "C" {
         if (mpfm.is_inf(val)) mpqm.set(q, 0);
         std::stringstream ss;
         mpqm.display_decimal(ss, q, sbits);
-        return mk_c(c)->mk_external_string(ss.str());
+        return mk_c(c)->mk_external_string(std::move(ss).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -1100,7 +1100,7 @@ extern "C" {
         }
         std::stringstream ss;
         ss << exp;
-        return mk_c(c)->mk_external_string(ss.str());
+        return mk_c(c)->mk_external_string(std::move(ss).str());
         Z3_CATCH_RETURN("");
     }
 

src/api/api_goal.cpp

@@ -185,7 +185,7 @@ extern "C" {
         std::ostringstream buffer;
         to_goal_ref(g)->display(buffer);
         // Hack for removing the trailing '\n'
-        std::string result = buffer.str();
+        std::string result = std::move(buffer).str();
         SASSERT(result.size() > 0);
         result.resize(result.size()-1);
         return mk_c(c)->mk_external_string(std::move(result));
@@ -203,7 +203,7 @@ extern "C" {
         }
         to_goal_ref(g)->display_dimacs(buffer, include_names);
         // Hack for removing the trailing '\n'
-        std::string result = buffer.str();
+        std::string result = std::move(buffer).str();
         SASSERT(result.size() > 0);
         result.resize(result.size()-1);
         return mk_c(c)->mk_external_string(std::move(result));

src/api/api_model.cpp

@@ -432,14 +432,14 @@ extern "C" {
         if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
             model_smt2_pp(buffer, mk_c(c)->m(), *(to_model_ref(m)), 0);
             // Hack for removing the trailing '\n'
-            result = buffer.str();
+            result = std::move(buffer).str();
             if (!result.empty())
                 result.resize(result.size()-1);
         }
         else {
             model_params p;
             model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
-            result = buffer.str();
+            result = std::move(buffer).str();
         }
         return mk_c(c)->mk_external_string(std::move(result));
         Z3_CATCH_RETURN(nullptr);

src/api/api_numeral.cpp

@@ -188,8 +188,8 @@ extern "C" {
         bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok && r.is_int() && !r.is_neg()) {
             std::stringstream strm;
-            r.display_bin(strm, r.get_num_bits());
-            return mk_c(c)->mk_external_string(strm.str());
+            strm << r.as_bin(r.get_num_bits());
+            return mk_c(c)->mk_external_string(std::move(strm).str());
         }
         else {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -237,7 +237,7 @@ extern "C" {
             else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
                 std::ostringstream buffer;
                 fu.fm().display_smt2(buffer, tmp, false);
-                return mk_c(c)->mk_external_string(buffer.str());
+                return mk_c(c)->mk_external_string(std::move(buffer).str());
             }
             else {
                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -288,21 +288,21 @@ extern "C" {
         if (u.is_numeral(e, r) && !r.is_int()) {
             std::ostringstream buffer;
             r.display_decimal(buffer, precision);
-            return mk_c(c)->mk_external_string(buffer.str());
+            return mk_c(c)->mk_external_string(std::move(buffer).str());
         }
         if (u.is_irrational_algebraic_numeral(e)) {
             algebraic_numbers::anum const & n = u.to_irrational_algebraic_numeral(e);
             algebraic_numbers::manager & am   = u.am();
             std::ostringstream buffer;
             am.display_decimal(buffer, n, precision);
-            return mk_c(c)->mk_external_string(buffer.str());
+            return mk_c(c)->mk_external_string(std::move(buffer).str());
         }
         else if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm))
             return Z3_get_numeral_string(c, a);
         else if (mk_c(c)->fpautil().is_numeral(to_expr(a), ftmp)) {
             std::ostringstream buffer;
             fu.fm().display_decimal(buffer, ftmp, 12);
-            return mk_c(c)->mk_external_string(buffer.str());
+            return mk_c(c)->mk_external_string(std::move(buffer).str());
         }
         else if (Z3_get_numeral_rational(c, a, r)) {
             return mk_c(c)->mk_external_string(r.to_string());

src/api/api_solver.cpp

@@ -170,8 +170,8 @@ extern "C" {
             if (g_is_threaded || g_thread_id != std::this_thread::get_id()) {
                 g_is_threaded = true;
                 std::ostringstream strm;
-                strm << smt2log << "-" << std::this_thread::get_id();
-                smt2log = symbol(strm.str());                
+                strm << smt2log << '-' << std::this_thread::get_id();
+                smt2log = symbol(std::move(strm).str());
             }
             to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str());
         }
@@ -208,7 +208,7 @@ extern "C" {
         if (!smt_logics::supported_logic(to_symbol(logic))) {
             std::ostringstream strm;
             strm << "logic '" << to_symbol(logic) << "' is not recognized";
-            SET_ERROR_CODE(Z3_INVALID_ARG, strm.str());
+            SET_ERROR_CODE(Z3_INVALID_ARG, std::move(strm).str());
             RETURN_Z3(nullptr);
         }
         else {
@@ -306,7 +306,7 @@ extern "C" {
 
         if (!parse_smt2_commands(*ctx.get(), is)) {
             ctx = nullptr;
-            SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
+            SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(errstrm).str());
             return;
         }
 
@@ -333,7 +333,7 @@ extern "C" {
         std::stringstream err;
         sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
         if (!parse_dimacs(is, err, solver)) {
-            SET_ERROR_CODE(Z3_PARSER_ERROR, err.str());
+            SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(err).str());
             return;
         }
         sat2goal s2g;
@@ -400,7 +400,7 @@ extern "C" {
         if (!initialized)
             to_solver(s)->m_solver = nullptr;
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -799,7 +799,7 @@ extern "C" {
         init_solver(c, s);
         std::ostringstream buffer;
         to_solver_ref(s)->display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -810,7 +810,7 @@ extern "C" {
         init_solver(c, s);
         std::ostringstream buffer;
         to_solver_ref(s)->display_dimacs(buffer, include_names);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

src/api/java/AST.java

@@ -19,6 +19,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_ast_kind;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * The abstract syntax tree (AST) class.
  **/
@@ -196,7 +198,7 @@ public class AST extends Z3Object implements Comparable<AST>
 
     @Override
     void addToReferenceQueue() {
-        getContext().getASTDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ASTRef::new);
     }
 
     static AST create(Context ctx, long obj)
@@ -217,4 +219,16 @@ public class AST extends Z3Object implements Comparable<AST>
             throw new Z3Exception("Unknown AST kind");
         }
     }
+
+    private static class ASTRef extends Z3ReferenceQueue.Reference<AST> {
+
+        private ASTRef(AST referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.decRef(ctx.nCtx(), z3Obj);
+        }
+    }
 }

src/api/java/ASTDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ASTDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-class ASTDecRefQueue extends IDecRefQueue<AST>
-{
-    public ASTDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.decRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/ASTMap.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Map from AST to AST
  **/
@@ -123,6 +125,18 @@ class ASTMap extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getASTMapDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ASTMapRef::new);
+    }
+
+    private static class ASTMapRef extends Z3ReferenceQueue.Reference<ASTMap> {
+
+        private ASTMapRef(ASTMap referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.astMapDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ASTVector.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Vectors of ASTs.
  **/
@@ -101,16 +103,6 @@ public class ASTVector extends Z3Object {
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }
 
-    @Override
-    void incRef() {
-        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
-    }
-
-    @Override
-    void addToReferenceQueue() {
-        getContext().getASTVectorDRQ().storeReference(getContext(), this);
-    }
-
     /**
      * Translates the AST vector into an AST[]
      * */
@@ -241,4 +233,26 @@ public class ASTVector extends Z3Object {
             res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
+
+    @Override
+    void incRef() {
+        Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
+    }
+
+    @Override
+    void addToReferenceQueue() {
+        getContext().getReferenceQueue().storeReference(this, ASTVectorRef::new);
+    }
+
+    private static class ASTVectorRef extends Z3ReferenceQueue.Reference<ASTVector> {
+
+        private ASTVectorRef(ASTVector referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.astVectorDecRef(ctx.nCtx(), z3Obj);
+        }
+    }
 }

src/api/java/ApplyResult.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * ApplyResult objects represent the result of an application of a tactic to a
  * goal. It contains the subgoals that were produced.
@@ -66,6 +68,18 @@ public class ApplyResult extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getApplyResultDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ApplyResultRef::new);
+    }
+
+    private static class ApplyResultRef extends Z3ReferenceQueue.Reference<ApplyResult> {
+
+        private ApplyResultRef(ApplyResult referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.applyResultDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ApplyResultDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ApplyResultDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
-{
-    public ApplyResultDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.applyResultDecRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/AstMapDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    AstMapDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
-    public ASTMapDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.astMapDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/AstVectorDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    AstVectorDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
-    public ASTVectorDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.astVectorDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/CMakeLists.txt

@@ -91,17 +91,13 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
 
 set(Z3_JAVA_JAR_SOURCE_FILES
   AlgebraicNum.java
-  ApplyResultDecRefQueue.java
   ApplyResult.java
   ArithExpr.java
   ArithSort.java
   ArrayExpr.java
   ArraySort.java
-  ASTDecRefQueue.java
   AST.java
-  AstMapDecRefQueue.java
   ASTMap.java
-  AstVectorDecRefQueue.java
   ASTVector.java
   BitVecExpr.java
   BitVecNum.java
@@ -109,9 +105,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   BoolExpr.java
   BoolSort.java
   CharSort.java
-  ConstructorDecRefQueue.java
   Constructor.java
-  ConstructorListDecRefQueue.java
   ConstructorList.java
   Context.java
   DatatypeExpr.java
@@ -121,7 +115,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   FiniteDomainExpr.java
   FiniteDomainNum.java
   FiniteDomainSort.java
-  FixedpointDecRefQueue.java
   Fixedpoint.java
   FPExpr.java
   FPNum.java
@@ -130,13 +123,9 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   FPRMSort.java
   FPSort.java
   FuncDecl.java
-  FuncInterpDecRefQueue.java
-  FuncInterpEntryDecRefQueue.java
   FuncInterp.java
   Global.java
-  GoalDecRefQueue.java
   Goal.java
-  IDecRefQueue.java
   IntExpr.java
   IntNum.java
   IntSort.java
@@ -144,16 +133,11 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   Lambda.java
   ListSort.java
   Log.java
-  ModelDecRefQueue.java
   Model.java
-  OptimizeDecRefQueue.java
   Optimize.java
-  ParamDescrsDecRefQueue.java
   ParamDescrs.java
-  ParamsDecRefQueue.java
   Params.java
   Pattern.java
-  ProbeDecRefQueue.java
   Probe.java
   Quantifier.java
   RatNum.java
@@ -166,16 +150,12 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   SeqSort.java
   SetSort.java
   Simplifier.java
-  SimplifierDecRefQueue.java
-  SolverDecRefQueue.java
   Solver.java
   Sort.java
-  StatisticsDecRefQueue.java
   Statistics.java
   Status.java
   StringSymbol.java
   Symbol.java
-  TacticDecRefQueue.java
   Tactic.java
   TupleSort.java
   UninterpretedSort.java
@@ -183,6 +163,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   Version.java
   Z3Exception.java
   Z3Object.java
+  Z3ReferenceQueue.java
 )
 set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
 foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
@@ -204,11 +185,13 @@ add_custom_target(build_z3_java_bindings
 
 # Rule to build ``com.microsoft.z3.jar``
 # TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
+# REMARK: removed VERSION to fix issue with using this to create installations.
+
 add_jar(z3JavaJar
   SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
   OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
   OUTPUT_DIR "${PROJECT_BINARY_DIR}"
-  VERSION "${Z3_VERSION}"
+# VERSION "${Z3_VERSION}"
 )
 
 ###############################################################################
@@ -219,21 +202,22 @@ if (Z3_INSTALL_JAVA_BINDINGS)
   # Provide cache variables for the install locations that the user can change.
   # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
   # files on Linux distributions
-  set(Z3_JAVA_JAR_INSTALLDIR
-    "${CMAKE_INSTALL_DATAROOTDIR}/java"
-    CACHE
-    PATH
-    "Directory to install Z3 Java jar file relative to install prefix"
-  )
-  # FIXME: I don't think this the right installation location
-  set(Z3_JAVA_JNI_LIB_INSTALLDIR
-    "${CMAKE_INSTALL_LIBDIR}"
-    CACHE
-    PATH
-    "Directory to install Z3 Java JNI bridge library relative to install prefix"
-  )
+  if (NOT Z3_JAVA_JAR_INSTALLDIR)
+     set(Z3_JAVA_JAR_INSTALLDIR
+       "${CMAKE_INSTALL_DATAROOTDIR}/java"
+       CACHE
+       PATH
+       "Directory to install Z3 Java jar file relative to install prefix"
+     )
+  endif()
+  if (NOT Z3_JAVA_JNI_LIB_INSTALLDIR)
+    set(Z3_JAVA_JNI_LIB_INSTALLDIR
+       "${CMAKE_INSTALL_LIBDIR}"
+       CACHE
+       PATH
+       "Directory to install Z3 Java JNI bridge library relative to install prefix"
+     )
+  endif()
   install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
-  # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
-  # with CMake 2.8.12.2 handles that incorrectly.
   install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
 endif()

src/api/java/Constructor.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Constructors are used for datatype sorts.
  **/
@@ -91,7 +93,7 @@ public class Constructor<R> extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getConstructorDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ConstructorRef::new);
     }
 
     static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
@@ -114,4 +116,16 @@ public class Constructor<R> extends Z3Object {
         return new Constructor<>(ctx, n, nativeObj);
 
     }
+
+    private static class ConstructorRef extends Z3ReferenceQueue.Reference<Constructor<?>> {
+
+        private ConstructorRef(Constructor<?> referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.delConstructor(ctx.nCtx(), z3Obj);
+        }
+    }
 }

src/api/java/ConstructorDecRefQueue.java

@@ -1,12 +0,0 @@
-package com.microsoft.z3;
-
-public class ConstructorDecRefQueue extends IDecRefQueue<Constructor<?>> {
-    public ConstructorDecRefQueue() {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.delConstructor(ctx.nCtx(), obj);
-    }
-}

src/api/java/ConstructorList.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Lists of constructors
  **/
@@ -34,7 +36,7 @@ public class ConstructorList<R> extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getConstructorListDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ConstructorListRef::new);
     }
 
     ConstructorList(Context ctx, Constructor<R>[] constructors)
@@ -43,4 +45,16 @@ public class ConstructorList<R> extends Z3Object {
                 constructors.length,
                 Constructor.arrayToNative(constructors)));
     }
+
+    private static class ConstructorListRef extends Z3ReferenceQueue.Reference<ConstructorList<?>> {
+
+        private ConstructorListRef(ConstructorList<?> referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.delConstructorList(ctx.nCtx(), z3Obj);
+        }
+    }
 }

src/api/java/ConstructorListDecRefQueue.java

@@ -1,12 +0,0 @@
-package com.microsoft.z3;
-
-public class ConstructorListDecRefQueue extends IDecRefQueue<ConstructorList<?>> {
-    public ConstructorListDecRefQueue() {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.delConstructorList(ctx.nCtx(), obj);
-    }
-}

src/api/java/Context.java

@@ -4319,119 +4319,9 @@ public class Context implements AutoCloseable {
                 checkContextMatch(a);
     }
 
-    private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
-    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
-    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
-    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
-    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
-    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
-    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
-    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
-    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
-    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
-    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
-    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
-    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
-    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
-    private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
-    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
-    private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
-    private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
-    private ConstructorListDecRefQueue m_ConstructorList_DRQ =
-            new ConstructorListDecRefQueue();
+    private Z3ReferenceQueue m_RefQueue = new Z3ReferenceQueue(this);
 
-    public IDecRefQueue<Constructor<?>> getConstructorDRQ() {
-        return m_Constructor_DRQ;
-    }
-
-    public IDecRefQueue<ConstructorList<?>> getConstructorListDRQ() {
-        return m_ConstructorList_DRQ;
-    }
-
-    public IDecRefQueue<AST> getASTDRQ()
-    {
-        return m_AST_DRQ;
-    }
-
-    public IDecRefQueue<ASTMap> getASTMapDRQ()
-    {
-        return m_ASTMap_DRQ;
-    }
-
-    public IDecRefQueue<ASTVector> getASTVectorDRQ()
-    {
-        return m_ASTVector_DRQ;
-    }
-
-    public IDecRefQueue<ApplyResult> getApplyResultDRQ()
-    {
-        return m_ApplyResult_DRQ;
-    }
-
-    public IDecRefQueue<FuncInterp.Entry<?>> getFuncEntryDRQ()
-    {
-        return m_FuncEntry_DRQ;
-    }
-
-    public IDecRefQueue<FuncInterp<?>> getFuncInterpDRQ()
-    {
-        return m_FuncInterp_DRQ;
-    }
-
-    public IDecRefQueue<Goal> getGoalDRQ()
-    {
-        return m_Goal_DRQ;
-    }
-
-    public IDecRefQueue<Model> getModelDRQ()
-    {
-        return m_Model_DRQ;
-    }
-
-    public IDecRefQueue<Params> getParamsDRQ()
-    {
-        return m_Params_DRQ;
-    }
-
-    public IDecRefQueue<ParamDescrs> getParamDescrsDRQ()
-    {
-        return m_ParamDescrs_DRQ;
-    }
-
-    public IDecRefQueue<Probe> getProbeDRQ()
-    {
-        return m_Probe_DRQ;
-    }
-
-    public IDecRefQueue<Solver> getSolverDRQ()
-    {
-        return m_Solver_DRQ;
-    }
-
-    public IDecRefQueue<Statistics> getStatisticsDRQ()
-    {
-        return m_Statistics_DRQ;
-    }
-
-    public IDecRefQueue<Tactic> getTacticDRQ()
-    {
-        return m_Tactic_DRQ;
-    }
-
-    public IDecRefQueue<Simplifier> getSimplifierDRQ()
-    {
-        return m_Simplifier_DRQ;
-    }
-
-    public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
-    {
-        return m_Fixedpoint_DRQ;
-    }
-
-    public IDecRefQueue<Optimize> getOptimizeDRQ()
-    {
-        return m_Optimize_DRQ;
-    }
+    Z3ReferenceQueue getReferenceQueue() { return m_RefQueue; }
 
     /**
      * Disposes of the context.
@@ -4439,27 +4329,16 @@ public class Context implements AutoCloseable {
     @Override
     public void close()
     {
-        m_AST_DRQ.forceClear(this);
-        m_ASTMap_DRQ.forceClear(this);
-        m_ASTVector_DRQ.forceClear(this);
-        m_ApplyResult_DRQ.forceClear(this);
-        m_FuncEntry_DRQ.forceClear(this);
-        m_FuncInterp_DRQ.forceClear(this);
-        m_Goal_DRQ.forceClear(this);
-        m_Model_DRQ.forceClear(this);
-        m_Params_DRQ.forceClear(this);
-        m_Probe_DRQ.forceClear(this);
-        m_Solver_DRQ.forceClear(this);
-        m_Optimize_DRQ.forceClear(this);
-        m_Statistics_DRQ.forceClear(this);
-        m_Tactic_DRQ.forceClear(this);
-        m_Simplifier_DRQ.forceClear(this);
-        m_Fixedpoint_DRQ.forceClear(this);
+        if (m_ctx == 0)
+            return;
+
+        m_RefQueue.forceClear();
 
         m_boolSort = null;
         m_intSort = null;
         m_realSort = null;
         m_stringSort = null;
+        m_RefQueue = null;
 
         synchronized (creation_lock) {
             Native.delContext(m_ctx);

src/api/java/Fixedpoint.java

@@ -19,6 +19,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_lbool;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Object for managing fixedpoints
  **/
@@ -327,9 +329,18 @@ public class Fixedpoint extends Z3Object
 
     @Override
     void addToReferenceQueue() {
-        getContext().getFixedpointDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, FixedpointRef::new);
     }
 
-    @Override
-    void checkNativeObject(long obj) { }
+    private static class FixedpointRef extends Z3ReferenceQueue.Reference<Fixedpoint> {
+
+        private FixedpointRef(Fixedpoint referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.fixedpointDecRef(ctx.nCtx(), z3Obj);
+        }
+    }
 }

src/api/java/FixedpointDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    FixedpointDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
-    public FixedpointDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        Native.fixedpointDecRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/FuncInterp.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * A function interpretation is represented as a finite map and an 'else' value.
  * Each entry in the finite map represents the value of a function given a set
@@ -93,7 +95,19 @@ public class FuncInterp<R extends Sort> extends Z3Object {
 
         @Override
         void addToReferenceQueue() {
-            getContext().getFuncEntryDRQ().storeReference(getContext(), this);
+            getContext().getReferenceQueue().storeReference(this, FuncEntryRef::new);
+        }
+
+        private static class FuncEntryRef extends Z3ReferenceQueue.Reference<Entry<?>> {
+
+            private FuncEntryRef(Entry<?> referent, ReferenceQueue<Z3Object> q) {
+                super(referent, q);
+            }
+
+            @Override
+            void decRef(Context ctx, long z3Obj) {
+                Native.funcEntryDecRef(ctx.nCtx(), z3Obj);
+            }
         }
     }
 
@@ -186,6 +200,18 @@ public class FuncInterp<R extends Sort> extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getFuncInterpDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, FuncInterpRef::new);
+    }
+
+    private static class FuncInterpRef extends Z3ReferenceQueue.Reference<FuncInterp<?>> {
+
+        private FuncInterpRef(FuncInterp<?> referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.funcInterpDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/FuncInterpDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    FuncInterpDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp<?>>
-{
-    public FuncInterpDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.funcInterpDecRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/FuncInterpEntryDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    FuncInterpEntryDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry<?>> {
-    public FuncInterpEntryDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.funcEntryDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Goal.java

@@ -19,6 +19,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_goal_prec;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * A goal (aka problem). A goal is essentially a set of formulas, that can be
  * solved and/or transformed using tactics and solvers.
@@ -262,6 +264,18 @@ public class Goal extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getGoalDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, GoalRef::new);
+    }
+
+    private static class GoalRef extends Z3ReferenceQueue.Reference<Goal> {
+
+        private GoalRef(Goal referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.goalDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/GoalDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    GoalDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class GoalDecRefQueue extends IDecRefQueue<Goal> {
-    public GoalDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-            Native.goalDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/IDecRefQueue.java

@@ -1,83 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    IDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/
-
-package com.microsoft.z3;
-
-import java.lang.ref.PhantomReference;
-import java.lang.ref.Reference;
-import java.lang.ref.ReferenceQueue;
-import java.util.IdentityHashMap;
-import java.util.Map;
-
-/**
- * A queue to handle management of native memory.
- *
- * <p><b>Mechanics: </b>once an object is created, a metadata is stored for it in
- * {@code referenceMap}, and a {@link PhantomReference} is created with a
- * reference to {@code referenceQueue}.
- * Once the object becomes strongly unreachable, the phantom reference gets
- * added by JVM to the {@code referenceQueue}.
- * After each object creation, we iterate through the available objects in
- * {@code referenceQueue} and decrement references for them.
- *
- * @param <T> Type of object stored in queue.
- */
-public abstract class IDecRefQueue<T extends Z3Object> {
-    private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
-    private final Map<PhantomReference<T>, Long> referenceMap =
-            new IdentityHashMap<>();
-
-    protected IDecRefQueue() {}
-
-    /**
-     * An implementation of this method should decrement the reference on a
-     * given native object.
-     * This function should always be called on the {@code ctx} thread.
-     *
-     * @param ctx Z3 context.
-     * @param obj Pointer to a Z3 object.
-     */
-    protected abstract void decRef(Context ctx, long obj);
-
-    public void storeReference(Context ctx, T obj) {
-        PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
-        referenceMap.put(ref, obj.getNativeObject());
-        clear(ctx);
-    }
-
-    /**
-     * Clean all references currently in {@code referenceQueue}.
-     */
-    protected void clear(Context ctx)
-    {
-        Reference<? extends T> ref;
-        while ((ref = referenceQueue.poll()) != null) {
-            long z3ast = referenceMap.remove(ref);
-            decRef(ctx, z3ast);
-        }
-    }
-
-    /**
-     * Clean all references stored in {@code referenceMap},
-     * <b>regardless</b> of whether they are in {@code referenceMap} or not.
-     */
-    public void forceClear(Context ctx) {
-        for (long ref : referenceMap.values()) {
-            decRef(ctx, ref);
-        }
-    }
-}

src/api/java/Model.java

@@ -19,6 +19,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * A Model contains interpretations (assignments) of constants and functions.
  **/
@@ -296,6 +298,18 @@ public class Model extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getModelDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ModelRef::new);
+    }
+
+    private static class ModelRef extends Z3ReferenceQueue.Reference<Model> {
+
+        private ModelRef(Model referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.modelDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ModelDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ModelDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class ModelDecRefQueue extends IDecRefQueue<Model> {
-    public ModelDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.modelDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/NativeStatic.txt

@@ -150,7 +150,7 @@ static void final_eh(void* _p, Z3_solver_callback cb) {
 static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit, bool is_pos) {
   JavaInfo *info = static_cast<JavaInfo*>(_p);
   ScopedCB scoped(info, cb);
-  info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val);
+  info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos);
 }
 
 DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
@@ -166,7 +166,7 @@ DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEn
   info->fixed = jenv->GetMethodID(jcls, "fixedWrapper", "(JJ)V");
   info->eq = jenv->GetMethodID(jcls, "eqWrapper", "(JJ)V");
   info->final = jenv->GetMethodID(jcls, "finWrapper", "()V");
-  info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JII)V");
+  info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JIZ)V");
 
   if (!info->push || !info->pop || !info->fresh || !info->created || !info->fixed || !info->eq || !info->final || !info->decide) {
     assert(false);
@@ -203,15 +203,16 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateRegisterDec
   Z3_solver_propagate_decide((Z3_context)ctx, (Z3_solver)solver, decide_eh);
 }
 
-DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateConflict(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long num_fixed, jlongArray fixed, long num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) {
+DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_propagateConsequence(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long num_fixed, jlongArray fixed, long num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) {
   JavaInfo *info = (JavaInfo*)javainfo;
   GETLONGAELEMS(Z3_ast, fixed, _fixed);
   GETLONGAELEMS(Z3_ast, eq_lhs, _eq_lhs);
   GETLONGAELEMS(Z3_ast, eq_rhs, _eq_rhs);
-  Z3_solver_propagate_consequence((Z3_context)ctx, info->cb, num_fixed, _fixed, num_eqs, _eq_lhs, _eq_rhs, (Z3_ast)conseq);
+  bool retval = Z3_solver_propagate_consequence((Z3_context)ctx, info->cb, num_fixed, _fixed, num_eqs, _eq_lhs, _eq_rhs, (Z3_ast)conseq);
   RELEASELONGAELEMS(fixed, _fixed);
   RELEASELONGAELEMS(eq_lhs, _eq_lhs);
   RELEASELONGAELEMS(eq_rhs, _eq_rhs);
+  return (jboolean) retval;
 }
 
 DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateAdd(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e) {
@@ -227,8 +228,8 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateAdd(JNIEnv
 }
 
 
-DLL_VIS JNIEXPORT bool JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e, long idx, int phase) {
+DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e, long idx, int phase) {
   JavaInfo *info = (JavaInfo*)javainfo;
   Z3_solver_callback cb = info->cb;
-  return Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));
+  return (jboolean) Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));
 }

src/api/java/Optimize.java

@@ -20,6 +20,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_lbool;
 
+import java.lang.ref.ReferenceQueue;
+
 
 /**
  * Object for managing optimization context
@@ -421,6 +423,18 @@ public class Optimize extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getOptimizeDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, OptimizeRef::new);
+    }
+
+    private static class OptimizeRef extends Z3ReferenceQueue.Reference<Optimize> {
+
+        private OptimizeRef(Optimize referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.optimizeDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/OptimizeDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2015 Microsoft Corporation
-   
-Module Name:
-
-    OptimizeDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class OptimizeDecRefQueue extends IDecRefQueue<Optimize> {
-    public OptimizeDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.optimizeDecRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/ParamDescrs.java

@@ -19,6 +19,8 @@ package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_param_kind;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * A ParamDescrs describes a set of parameters.
  **/
@@ -97,6 +99,18 @@ public class ParamDescrs extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getParamDescrsDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ParamDescrsRef::new);
+    }
+
+    private static class ParamDescrsRef extends Z3ReferenceQueue.Reference<ParamDescrs> {
+
+        private ParamDescrsRef(ParamDescrs referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.paramDescrsDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ParamDescrsDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ParamDescrsDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs> {
-    public ParamDescrsDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        Native.paramDescrsDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Params.java

@@ -18,6 +18,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * A ParameterSet represents a configuration in the form of Symbol/value pairs.
  **/
@@ -130,6 +132,18 @@ public class Params extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getParamsDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ParamsRef::new);
+    }
+
+    private static class ParamsRef extends Z3ReferenceQueue.Reference<Params> {
+
+        private ParamsRef(Params referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.paramsDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ParamsDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ParamDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class ParamsDecRefQueue extends IDecRefQueue<Params> {
-    public ParamsDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.paramsDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Probe.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Probes are used to inspect a goal (aka problem) and collect information that
  * may be used to decide which solver and/or preprocessing step will be used.
@@ -56,6 +58,18 @@ public class Probe extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getProbeDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, ProbeRef::new);
+    }
+
+    private static class ProbeRef extends Z3ReferenceQueue.Reference<Probe> {
+
+        private ProbeRef(Probe referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.probeDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/ProbeDecRefQueue.java

@@ -1,32 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    ProbeDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class ProbeDecRefQueue extends IDecRefQueue<Probe>
-{
-    public ProbeDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        Native.probeDecRef(ctx.nCtx(), obj);
-    }
-};

src/api/java/Simplifier.java

@@ -18,6 +18,8 @@ Author:
 package com.microsoft.z3;
 
 
+import java.lang.ref.ReferenceQueue;
+
 public class Simplifier extends Z3Object {
     /*
      * A string containing a description of parameters accepted by the simplifier.
@@ -32,7 +34,7 @@ public class Simplifier extends Z3Object {
      * Retrieves parameter descriptions for Simplifiers.
      */
     public ParamDescrs getParameterDescriptions() {
-	return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject())); 
+        return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject()));
     }
 
     Simplifier(Context ctx, long obj)
@@ -53,6 +55,18 @@ public class Simplifier extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getSimplifierDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, SimplifierRef::new);
     }
-}	
+
+    private static class SimplifierRef extends Z3ReferenceQueue.Reference<Simplifier> {
+
+        private SimplifierRef(Simplifier referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.simplifierDecRef(ctx.nCtx(), z3Obj);
+        }
+    }
+}

src/api/java/SimplifierDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    SimplifierDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class SimplifierDecRefQueue extends IDecRefQueue<Simplifier> {
-    public SimplifierDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        Native.simplifierDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Solver.java

@@ -19,6 +19,8 @@ Notes:
 package com.microsoft.z3;
 
 import com.microsoft.z3.enumerations.Z3_lbool;
+
+import java.lang.ref.ReferenceQueue;
 import java.util.*;
 
 /**
@@ -403,6 +405,18 @@ public class Solver extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getSolverDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, SolverRef::new);
+    }
+
+    private static class SolverRef extends Z3ReferenceQueue.Reference<Solver> {
+
+        private SolverRef(Solver referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.solverDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/SolverDecRefQueue.java

@@ -1,27 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    SolverDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class SolverDecRefQueue extends IDecRefQueue<Solver> {
-    public SolverDecRefQueue() { super(); }
-    
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.solverDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Statistics.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Objects of this class track statistical information about solvers.
  **/
@@ -25,7 +27,7 @@ public class Statistics extends Z3Object {
      * Statistical data is organized into pairs of [Key, Entry], where every
      * Entry is either a {@code DoubleEntry} or a {@code UIntEntry}
      **/
-    public class Entry
+    public static class Entry
     {
         /**
          * The key of the entry.
@@ -191,11 +193,23 @@ public class Statistics extends Z3Object {
 
     @Override
     void incRef() {
-        getContext().getStatisticsDRQ().storeReference(getContext(), this);
+        Native.statsIncRef(getContext().nCtx(), getNativeObject());
     }
 
     @Override
     void addToReferenceQueue() {
-        Native.statsIncRef(getContext().nCtx(), getNativeObject());
+        getContext().getReferenceQueue().storeReference(this, StatisticsRef::new);
+    }
+
+    private static class StatisticsRef extends Z3ReferenceQueue.Reference<Statistics> {
+
+        private StatisticsRef(Statistics referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.statsDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/StatisticsDecRefQueue.java

@@ -1,30 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    StatisticsDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class StatisticsDecRefQueue extends IDecRefQueue<Statistics> {
-    public StatisticsDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj) {
-        Native.statsDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/Tactic.java

@@ -17,6 +17,8 @@ Notes:
 
 package com.microsoft.z3;
 
+import java.lang.ref.ReferenceQueue;
+
 /**
  * Tactics are the basic building block for creating custom solvers for specific
  * problem domains. The complete list of tactics may be obtained using
@@ -98,6 +100,19 @@ public class Tactic extends Z3Object {
 
     @Override
     void addToReferenceQueue() {
-        getContext().getTacticDRQ().storeReference(getContext(), this);
+        //getContext().getTacticDRQ().storeReference(getContext(), this);
+        getContext().getReferenceQueue().storeReference(this, TacticRef::new);
+    }
+
+    private static class TacticRef extends Z3ReferenceQueue.Reference<Tactic> {
+
+        private TacticRef(Tactic referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            Native.tacticDecRef(ctx.nCtx(), z3Obj);
+        }
     }
 }

src/api/java/TacticDecRefQueue.java

@@ -1,31 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-   
-Module Name:
-
-    TacticDecRefQueue.java
-
-Abstract:
-
-Author:
-
-    @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
-**/ 
-
-package com.microsoft.z3;
-
-class TacticDecRefQueue extends IDecRefQueue<Tactic> {
-    public TacticDecRefQueue() 
-    {
-        super();
-    }
-
-    @Override
-    protected void decRef(Context ctx, long obj)
-    {
-        Native.tacticDecRef(ctx.nCtx(), obj);
-    }
-}

src/api/java/UserPropagatorBase.java

@@ -60,36 +60,47 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase {
         fixed(var, value);
     }
 
+    @Override
+    protected final void decideWrapper(long lvar, int bit, boolean is_pos) {
+        Expr var = new Expr(ctx, lvar);
+        decide(var, bit, is_pos);
+    }
+
     public abstract void push();
 
     public abstract void pop(int number);
 
     public abstract UserPropagatorBase fresh(Context ctx);
 
-    public <R extends Sort> void created(Expr<R> ast) {}
+    public void created(Expr<?> ast) {}
 
-    public <R extends Sort> void fixed(Expr<R> var, Expr<R> value) {}
+    public void fixed(Expr<?> var, Expr<?> value) {}
 
-    public <R extends Sort> void eq(Expr<R> x, Expr<R> y) {}
+    public void eq(Expr<?> x, Expr<?> y) {}
+
+    public void decide(Expr<?> var, int bit, boolean is_pos) {}
 
     public void fin() {}
 
-    public final <R extends Sort> void add(Expr<R> expr) {
+    public final void add(Expr<?> expr) {
         Native.propagateAdd(this, ctx.nCtx(), solver.getNativeObject(), javainfo, expr.getNativeObject());
     }
 
-    public final <R extends Sort> void conflict(Expr<R>[] fixed) {
-        conflict(fixed, new Expr[0], new Expr[0]);
+    public final boolean conflict(Expr<?>[] fixed) {
+        return conflict(fixed, new Expr[0], new Expr[0]);
     }
 
-    public final <R extends Sort> void conflict(Expr<R>[] fixed, Expr<R>[] lhs, Expr<R>[] rhs) {
-        AST conseq = ctx.mkBool(false);
-        Native.propagateConflict(
+    public final boolean conflict(Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs) {
+        return consequence(fixed, lhs, rhs, ctx.mkBool(false));
+    }
+
+    public final boolean consequence(Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs, Expr<?> conseq) {
+        return Native.propagateConsequence(
             this, ctx.nCtx(), solver.getNativeObject(), javainfo,
             fixed.length, AST.arrayToNative(fixed), lhs.length, AST.arrayToNative(lhs), AST.arrayToNative(rhs), conseq.getNativeObject());
     }
 
-    public final <R extends Sort> boolean nextSplit(Expr<R> e, long idx, Z3_lbool phase) {
+    public final boolean nextSplit(Expr<?> e, long idx, Z3_lbool phase) {
         return Native.propagateNextSplit(
             this, ctx.nCtx(), solver.getNativeObject(), javainfo,
             e.getNativeObject(), idx, phase.toInt());

src/api/java/Z3ReferenceQueue.java

@@ -0,0 +1,144 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
+
+package com.microsoft.z3;
+
+import java.lang.ref.PhantomReference;
+import java.lang.ref.ReferenceQueue;
+
+/**
+ * A queue to handle management of native memory.
+ *
+ * <p><b>Mechanics: </b>When an object is created, a so-called {@link PhantomReference}
+ * is constructed that is associated with the created object and the reference queue {@code referenceQueue}.
+ * Once the object becomes strongly unreachable, the phantom reference gets
+ * added by JVM to the {@code referenceQueue}.
+ * After each object creation, we iterate through the available objects in
+ * {@code referenceQueue} and decrement references for them.
+ * <p>
+ * In order for this to work, we need to (i) associate to each phantom reference the underlying
+ * native object (and its type) that it references and (ii) keep the phantom references themselves alive, so they are not
+ * garbage collected before the object they reference.
+ * We use a doubly-linked list of custom phantom references, subclasses of {@link Reference}, to achieve this.
+ *
+ */
+class Z3ReferenceQueue {
+    private final Context ctx;
+    private final ReferenceQueue<Z3Object> referenceQueue = new ReferenceQueue<>();
+    private final Reference<?> referenceList = emptyList();
+
+    Z3ReferenceQueue(Context ctx) {
+        this.ctx = ctx;
+    }
+
+    /**
+     * Create and store a new phantom reference.
+     */
+    <T extends Z3Object> void storeReference(T z3Object, ReferenceConstructor<T> refConstructor) {
+        referenceList.insert(refConstructor.construct(z3Object, referenceQueue));
+        clear();
+    }
+
+    /**
+     * Clean all references currently in {@code referenceQueue}.
+     */
+    private void clear() {
+        Reference<?> ref;
+        while ((ref = (Reference<?>)referenceQueue.poll()) != null) {
+            ref.cleanup(ctx);
+        }
+    }
+
+    /**
+     * Clean all references stored in {@code referenceList},
+     * <b>regardless</b> of whether they are in {@code referenceQueue} or not.
+     */
+    @SuppressWarnings("StatementWithEmptyBody")
+    public void forceClear() {
+        // Decrement all reference counters
+        Reference<?> cur = referenceList.next;
+        while (cur.next != null) {
+            cur.decRef(ctx, cur.nativePtr);
+            cur = cur.next;
+        }
+
+        // Bulk-delete the reference list's entries
+        referenceList.next = cur;
+        cur.prev = referenceList;
+
+        // Empty the reference queue so that there are no living phantom references anymore.
+        // This makes sure that all stored phantom references can be GC'd now.
+        while (referenceQueue.poll() != null) {}
+    }
+
+    private static Reference<?> emptyList() {
+        Reference<?> head = new DummyReference();
+        Reference<?> tail = new DummyReference();
+        head.next = tail;
+        tail.prev = head;
+        return head;
+    }
+
+    // ================================================================================================================
+
+    @FunctionalInterface
+    interface ReferenceConstructor<T extends Z3Object> {
+        Reference<T> construct(T reference, ReferenceQueue<Z3Object> queue);
+    }
+
+    abstract static class Reference<T extends Z3Object> extends PhantomReference<T> {
+
+        private Reference<?> prev;
+        private Reference<?> next;
+        private final long nativePtr;
+
+        Reference(T referent, ReferenceQueue<Z3Object> q) {
+            super(referent, q);
+            this.nativePtr = referent != null ? referent.getNativeObject() : 0;
+        }
+
+        private void cleanup(Context ctx) {
+            decRef(ctx, nativePtr);
+            assert (prev != null && next != null);
+            prev.next = next;
+            next.prev = prev;
+        }
+
+        private void insert(Reference<?> ref) {
+            assert next != null;
+            ref.prev = this;
+            ref.next = this.next;
+            ref.next.prev = ref;
+            next = ref;
+        }
+
+        abstract void decRef(Context ctx, long z3Obj);
+    }
+
+    private static class DummyReference extends Reference<Z3Object> {
+
+        public DummyReference() {
+            super(null, null);
+        }
+
+        @Override
+        void decRef(Context ctx, long z3Obj) {
+            // Should never be called.
+            assert false;
+        }
+    }
+}

src/api/julia/README.md

@@ -14,7 +14,10 @@ make
 
 ## Julia part
 
-The Z3 binaries are provided to [Z3.jl](https://github.com/ahumenberger/Z3.jl) via [z3_jll.jl](https://github.com/JuliaBinaryWrappers/z3_jll.jl). That is, in order to release a new Z3 version one has to update the corresponding [build script](https://github.com/JuliaPackaging/Yggdrasil/tree/master/Z/z3) which triggers a new version of z3_jll.jl.
+The Z3 binaries are provided to [Z3.jl](https://github.com/ahumenberger/Z3.jl) via [z3_jll.jl](https://github.com/JuliaBinaryWrappers/z3_jll.jl). 
+That is, in order to propagate any C++ changes to the Julia side, one has to:
+1. Release a new version of Z3. 
+2. Update the corresponding [build script](https://github.com/JuliaPackaging/Yggdrasil/tree/master/Z/z3) to use the new Z3 release. 
 
 ### Using the compiled version of Z3
 

src/api/julia/z3jl.cpp

@@ -303,6 +303,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
     m.method("xnor", &xnor);
     m.method("min", &min);
     m.method("max", &max);
+    m.method("exists", static_cast<expr (*)(expr_vector const &, expr const &)>(&exists));
+    m.method("forall", static_cast<expr (*)(expr_vector const &, expr const &)>(&forall));
     m.method("abs", static_cast<expr (*)(expr const &)>(&abs));
     m.method("sqrt", static_cast<expr (*)(expr const &, expr const &)>(&sqrt));
     m.method("fma", static_cast<expr (*)(expr const &, expr const &, expr const &, expr const &)>(&fma));

src/api/ml/z3.ml

@@ -1832,6 +1832,9 @@ struct
   let get (x:statistics) (key:string) =
     try Some(List.find (fun c -> Entry.get_key c = key) (get_entries x)) with
     | Not_found -> None
+
+  let get_estimated_alloc_size =
+    Z3native.get_estimated_alloc_size
 end
 
 

src/api/ml/z3.mli

@@ -3224,6 +3224,9 @@ sig
 
   (** The value of a particular statistical counter. *)
   val get : statistics -> string -> Entry.statistics_entry option
+
+  (** The estimated allocated memory in bytes. *)
+  val get_estimated_alloc_size : unit -> int64
 end
 
 (** Solvers *)

src/api/python/setup.py

@@ -313,11 +313,12 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
             osver = RELEASE_METADATA[3]
             if osver.count('.') > 1:
                 osver = '.'.join(osver.split('.')[:2])
-            osver = osver.replace('.','_')
+            if osver.startswith("11"):
+                osver = "11_0"
             if arch == 'x64':
-                plat_name ='macosx_%s_x86_64' % re.sub(r'\A(1[1-9])(_[\d]+)*\Z', r'\1_0', osver)
+                plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
             elif arch == 'arm64':
-                plat_name ='macosx_%s_arm64' % osver
+                plat_name ='macosx_%s_arm64' % osver.replace('.', '_')
             else:
                 raise Exception(f"idk how os {distos} {osver} works. what goes here?")
         else:
@@ -340,7 +341,7 @@ setup(
     license='MIT License',
     keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
     packages=['z3'],
-    install_requires = ['importlib-resources'],
+    install_requires = ["importlib-resources; python_version < '3.9'"],
     include_package_data=True,
     package_data={
         'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]

src/api/python/z3/z3.py

@@ -8984,7 +8984,7 @@ def substitute_funs(t, *m):
             m = m1
     if z3_debug():
         _z3_assert(is_expr(t), "Z3 expression expected")
-        _z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, funcion pairs expected.")
+        _z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, function pairs expected.")
     num = len(m)
     _from = (FuncDecl * num)()
     _to = (Ast * num)()
@@ -9069,7 +9069,7 @@ def AtMost(*args):
 
 
 def AtLeast(*args):
-    """Create an at-most Pseudo-Boolean k constraint.
+    """Create an at-least Pseudo-Boolean k constraint.
 
     >>> a, b, c = Bools('a b c')
     >>> f = AtLeast(a, b, c, 2)
@@ -10969,10 +10969,10 @@ def CharVal(ch, ctx=None):
         raise Z3Exception("character value should be an ordinal")
     return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
     
-def CharFromBv(ch, ctx=None):
-    if not is_expr(ch):
-        raise Z3Expression("Bit-vector expression needed")
-    return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx)
+def CharFromBv(bv):
+    if not is_expr(bv):
+        raise Z3Exception("Bit-vector expression needed")
+    return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx)
 
 def CharToBv(ch, ctx=None):
     ch = _coerce_char(ch, ctx)
@@ -11570,47 +11570,54 @@ def user_prop_fresh(ctx, _new_ctx):
 
 def user_prop_fixed(ctx, cb, id, value):
     prop = _prop_closures.get(ctx)
-    prop.cb = cb
+    old_cb = prop.cb
+    prop.cb = cb    
     id = _to_expr_ref(to_Ast(id), prop.ctx())
     value = _to_expr_ref(to_Ast(value), prop.ctx())
     prop.fixed(id, value)
-    prop.cb = None
+    prop.cb = old_cb
 
 def user_prop_created(ctx, cb, id):
     prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
     prop.cb = cb
     id = _to_expr_ref(to_Ast(id), prop.ctx())
     prop.created(id)
-    prop.cb = None
+    prop.cb = old_cb
+    
     
 def user_prop_final(ctx, cb):
     prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
     prop.cb = cb
     prop.final()
-    prop.cb = None
+    prop.cb = old_cb
 
 def user_prop_eq(ctx, cb, x, y):
     prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
     prop.cb = cb
     x = _to_expr_ref(to_Ast(x), prop.ctx())
     y = _to_expr_ref(to_Ast(y), prop.ctx())
     prop.eq(x, y)
-    prop.cb = None
+    prop.cb = old_cb
 
 def user_prop_diseq(ctx, cb, x, y):
     prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
     prop.cb = cb
     x = _to_expr_ref(to_Ast(x), prop.ctx())
     y = _to_expr_ref(to_Ast(y), prop.ctx())
     prop.diseq(x, y)
-    prop.cb = None
+    prop.cb = old_cb
 
 def user_prop_decide(ctx, cb, t, idx, phase):
     prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
     prop.cb = cb
     t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
     prop.decide(t, idx, phase)
-    prop.cb = None
+    prop.cb = old_cb
     
 
 _user_prop_push = Z3_push_eh(user_prop_push)
@@ -11651,7 +11658,7 @@ class UserPropagateBase:
 
     #
     # Either solver is set or ctx is set.
-    # Propagators that are created throuh callbacks
+    # Propagators that are created through callbacks
     # to "fresh" inherit the context of that is supplied
     # as argument to the callback.
     # This context should not be deleted. It is owned by the solver.

src/api/python/z3/z3printer.py

@@ -99,6 +99,7 @@ _z3_op_to_str = {
     Z3_OP_ARRAY_EXT: "Ext",
 
     Z3_OP_PB_AT_MOST: "AtMost",
+    Z3_OP_PB_AT_LEAST: "AtLeast",
     Z3_OP_PB_LE: "PbLe",
     Z3_OP_PB_GE: "PbGe",
     Z3_OP_PB_EQ: "PbEq",
@@ -252,11 +253,11 @@ def _is_html_left_assoc(k):
 
 
 def _is_add(k):
-    return k == Z3_OP_ADD or k == Z3_OP_BADD
+    return k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_FPA_ADD
 
 
 def _is_sub(k):
-    return k == Z3_OP_SUB or k == Z3_OP_BSUB
+    return k == Z3_OP_SUB or k == Z3_OP_BSUB or k == Z3_OP_FPA_SUB
 
 
 if sys.version_info.major < 3:
@@ -890,9 +891,21 @@ class Formatter:
             if self.is_infix(k) and n >= 3:
                 rm = a.arg(0)
                 if z3.is_fprm_value(rm) and z3.get_default_rounding_mode(a.ctx).eq(rm):
-                    arg1 = to_format(self.pp_expr(a.arg(1), d + 1, xs))
-                    arg2 = to_format(self.pp_expr(a.arg(2), d + 1, xs))
+                    p = self.get_precedence(k)
                     r = []
+                    x = a.arg(1)
+                    y = a.arg(2)
+                    arg1 = to_format(self.pp_expr(x, d + 1, xs))
+                    arg2 = to_format(self.pp_expr(y, d + 1, xs))
+                    if z3.is_app(x):
+                        child_k = x.decl().kind()
+                        if child_k != k and self.is_infix(child_k) and self.get_precedence(child_k) > p:
+                            arg1 = self.add_paren(arg1)
+                    if z3.is_app(y):
+                        child_k = y.decl().kind()
+                        if child_k != k and self.is_infix(child_k) and self.get_precedence(child_k) > p:
+                            arg2 = self.add_paren(arg2)
+                            
                     r.append(arg1)
                     r.append(to_format(" "))
                     r.append(to_format(op))
@@ -1099,6 +1112,10 @@ class Formatter:
         k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
         return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
 
+    def pp_atleast(self, a, d, f, xs):
+        k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+        return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
+
     def pp_pbcmp(self, a, d, f, xs):
         chs = a.children()
         rchs = range(len(chs))
@@ -1151,6 +1168,8 @@ class Formatter:
                 return self.pp_K(a, d, xs)
             elif k == Z3_OP_PB_AT_MOST:
                 return self.pp_atmost(a, d, f, xs)
+            elif k == Z3_OP_PB_AT_LEAST:
+                return self.pp_atleast(a, d, f, xs)
             elif k == Z3_OP_PB_LE:
                 return self.pp_pbcmp(a, d, f, xs)
             elif k == Z3_OP_PB_GE:

src/api/z3_api.h

@@ -1363,7 +1363,7 @@ typedef enum {
    - Z3_NO_PARSER:     Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
    - Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
    - Z3_MEMOUT_FAIL:   A memory allocation failure was encountered.
-   - Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
+   - Z3_FILE_ACCESS_ERROR: A file could not be accessed.
    - Z3_INVALID_USAGE:   API call is invalid in the current state.
    - Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
    - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with #Z3_inc_ref.
@@ -7184,15 +7184,25 @@ extern "C" {
     void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e);
 
     /**
-       \brief propagate a consequence based on fixed values.
-       This is a callback a client may invoke during the fixed_eh callback.
-       The callback adds a propagation consequence based on the fixed values of the
-       \c ids.
+       \brief propagate a consequence based on fixed values and equalities.       
+       A client may invoke it during the \c propagate_fixed, \c propagate_eq, \c propagate_diseq, and \c propagate_final callbacks.
+       The callback adds a propagation consequence based on the fixed values passed \c ids and equalities \c eqs based on parameters \c lhs, \c rhs.
+       
        The solver might discard the propagation in case it is true in the current state.
        The function returns false in this case; otw. the function returns true.
        At least one propagation in the final callback has to return true in order to
        prevent the solver from finishing.
 
+       Assume the callback has the signature: \c propagate_consequence_eh(context, solver_cb, num_ids, ids, num_eqs, lhs, rhs, consequence).
+       \param c - context
+       \param solver_cb - solver callback
+       \param num_ids - number of fixed terms used as premise to propagation
+       \param ids - array of length \c num_ids containing terms that are fixed in the current scope
+       \param num_eqs - number of equalities used as premise to propagation
+       \param lhs - left side of equalities
+       \param rhs - right side of equalities
+       \param consequence - consequence to propagate. It is typically an atomic formula, but it can be an arbitrary formula. 
+
        def_API('Z3_solver_propagate_consequence', BOOL, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, AST), _in(UINT), _in_array(4, AST), _in_array(4, AST), _in(AST)))
     */
 

src/ast/arith_decl_plugin.cpp

@@ -984,7 +984,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
             return true;
         }
         return false;
-    } while (false);
+    } 
+    while (true);
     return false;
 }
 

src/ast/array_decl_plugin.cpp

@@ -49,7 +49,7 @@ sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
             m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
             return nullptr;
         }
-        parameter params[2] = { parameters[0], parameter(m_manager->mk_bool_sort()) };
+        parameter params[2] = { parameter(parameters[0]), parameter(m_manager->mk_bool_sort()) };
         return mk_sort(ARRAY_SORT, 2, params);
     }
     SASSERT(k == ARRAY_SORT);

src/ast/ast.cpp

@@ -48,21 +48,13 @@ parameter::~parameter() {
     }
 }
 
-parameter& parameter::operator=(parameter const& other) {
-    if (this == &other) {
-        return *this;
-    }
-
-    this->~parameter();
-    m_val = other.m_val;
-
+parameter::parameter(parameter const& other) : m_val(other.m_val) {
     if (auto p = std::get_if<rational*>(&m_val)) {
         m_val = alloc(rational, **p);
     }
     if (auto p = std::get_if<zstring*>(&m_val)) {
         m_val = alloc(zstring, **p);
     }
-    return *this;
 }
 
 void parameter::init_eh(ast_manager & m) {
@@ -319,26 +311,6 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain,
 //
 // -----------------------------------
 
-static app_flags mk_const_flags() {
-    app_flags r;
-    r.m_depth           = 1;
-    r.m_ground          = true;
-    r.m_has_quantifiers = false;
-    r.m_has_labels      = false;
-    return r;
-}
-
-static app_flags mk_default_app_flags() {
-    app_flags r;
-    r.m_depth           = 1;
-    r.m_ground          = true;
-    r.m_has_quantifiers = false;
-    r.m_has_labels      = false;
-    return r;
-}
-
-app_flags app::g_constant_flags = mk_const_flags();
-
 app::app(func_decl * decl, unsigned num_args, expr * const * args):
     expr(AST_APP),
     m_decl(decl),
@@ -1762,8 +1734,7 @@ ast * ast_manager::register_node_core(ast * n) {
         inc_ref(t->get_decl());
         unsigned num_args = t->get_num_args();
         if (num_args > 0) {
-            app_flags * f     = t->flags();
-            *f = mk_default_app_flags();
+            app_flags * f = &t->m_flags;
             SASSERT(t->is_ground());
             SASSERT(!t->has_quantifiers());
             SASSERT(!t->has_labels());
@@ -1776,13 +1747,13 @@ ast * ast_manager::register_node_core(ast * n) {
                 unsigned arg_depth = 0;
                 switch (arg->get_kind()) {
                 case AST_APP: {
-                    app_flags * arg_flags = to_app(arg)->flags();
-                    arg_depth = arg_flags->m_depth;
-                    if (arg_flags->m_has_quantifiers)
+                    app *app = to_app(arg);
+                    arg_depth = app->get_depth();
+                    if (app->has_quantifiers())
                         f->m_has_quantifiers = true;
-                    if (arg_flags->m_has_labels)
+                    if (app->has_labels())
                         f->m_has_labels = true;
-                    if (!arg_flags->m_ground)
+                    if (!app->is_ground())
                         f->m_ground = false;
                     break;
                 }

src/ast/ast.h

@@ -142,7 +142,7 @@ public:
     explicit parameter(const char *s): m_val(symbol(s)) {}
     explicit parameter(const std::string &s): m_val(symbol(s)) {}
     explicit parameter(unsigned ext_id, bool): m_val(ext_id) {}
-    parameter(parameter const& other) { *this = other; }
+    explicit parameter(parameter const& other);
 
     parameter(parameter && other) noexcept : m_val(std::move(other.m_val)) {
         other.m_val = 0;
@@ -150,7 +150,10 @@ public:
 
     ~parameter();
 
-    parameter& operator=(parameter const& other);
+    parameter& operator=(parameter && other) {
+        std::swap(other.m_val, m_val);
+        return *this;
+    }
 
     kind_t get_kind() const { return static_cast<kind_t>(m_val.index()); }
     bool is_int() const { return get_kind() == PARAM_INT; }
@@ -704,6 +707,7 @@ struct app_flags {
     unsigned     m_ground:1;   // application does not have free variables or nested quantifiers.
     unsigned     m_has_quantifiers:1; // application has nested quantifiers.
     unsigned     m_has_labels:1; // application has nested labels.
+    app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {}
 };
 
 class app : public expr {
@@ -711,19 +715,15 @@ class app : public expr {
 
     func_decl *  m_decl;
     unsigned     m_num_args;
+    app_flags    m_flags;
     expr *       m_args[0];
 
-    static app_flags g_constant_flags;
-
-    // remark: store term depth in the end of the app. the depth is only stored if the num_args > 0
     static unsigned get_obj_size(unsigned num_args) {
-        return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags);
+        return sizeof(app) + num_args * sizeof(expr *);
     }
 
     friend class tmp_app;
 
-    app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast<app_flags*>(const_cast<expr**>(m_args + m_num_args)); }
-
     app(func_decl * decl, unsigned num_args, expr * const * args);
 public:
     func_decl * get_decl() const { return m_decl; }
@@ -744,10 +744,10 @@ public:
     expr * const * end() const { return m_args + m_num_args; }
     sort * _get_sort() const { return get_decl()->get_range(); }
 
-    unsigned get_depth() const { return flags()->m_depth; }
-    bool is_ground() const { return flags()->m_ground; }
-    bool has_quantifiers() const { return flags()->m_has_quantifiers; }
-    bool has_labels() const { return flags()->m_has_labels; }
+    unsigned get_depth() const { return m_flags.m_depth; }
+    bool is_ground() const { return m_flags.m_ground; }
+    bool has_quantifiers() const { return m_flags.m_has_quantifiers; }
+    bool has_labels() const { return m_flags.m_has_labels; }
 };
 
 // -----------------------------------
@@ -1102,7 +1102,7 @@ public:
 
     // Event handlers for deleting/translating PARAM_EXTERNAL
     virtual void del(parameter const & p) {}
-    virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
+    virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return {}; }
 
     virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
 };

src/ast/ast_lt.cpp

@@ -68,8 +68,8 @@ bool lt(ast * n1, ast * n2) {
         num = to_sort(n1)->get_num_parameters();
         SASSERT(num > 0);
         for (unsigned i = 0; i < num; i++) {
-            parameter p1 = to_sort(n1)->get_parameter(i);
-            parameter p2 = to_sort(n2)->get_parameter(i);
+            const parameter &p1 = to_sort(n1)->get_parameter(i);
+            const parameter &p2 = to_sort(n2)->get_parameter(i);
             check_parameter(p1, p2);
         }
         UNREACHABLE();
@@ -80,8 +80,8 @@ bool lt(ast * n1, ast * n2) {
         check_value(to_func_decl(n1)->get_num_parameters(), to_func_decl(n2)->get_num_parameters());
         num = to_func_decl(n1)->get_num_parameters();
         for (unsigned i = 0; i < num; i++) {
-            parameter p1 = to_func_decl(n1)->get_parameter(i);
-            parameter p2 = to_func_decl(n2)->get_parameter(i);
+            const parameter &p1 = to_func_decl(n1)->get_parameter(i);
+            const parameter &p2 = to_func_decl(n2)->get_parameter(i);
             check_parameter(p1, p2);
         }
         num = to_func_decl(n1)->get_arity();

src/ast/ast_pp.h

@@ -58,13 +58,13 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
 inline std::string operator+(char const* s, mk_pp const& pp) {
     std::ostringstream strm;
     strm << s << pp;
-    return strm.str();
+    return std::move(strm).str();
 }
 
 inline std::string operator+(std::string const& s, mk_pp const& pp) {
     std::ostringstream strm;
     strm << s << pp;
-    return strm.str();
+    return std::move(strm).str();
 }
 
 inline std::string& operator+=(std::string& s, mk_pp const& pp) {

src/ast/bv_decl_plugin.cpp

@@ -454,9 +454,8 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
-    rational v = parameters[0].get_rational();
-    parameter p0(mod2k(v, bv_size));
-    parameter ps[2] = { std::move(p0), parameters[1] };
+    const rational &v = parameters[0].get_rational();
+    parameter ps[2] = { parameter(mod2k(v, bv_size)), parameter(parameters[1]) };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
 }
@@ -913,13 +912,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
 
     if (m_plugin->log_constant_meaning_prelude(r)) {
         if (bv_size % 4 == 0) {
-            m_manager.trace_stream() << "#x";
-            val.display_hex(m_manager.trace_stream(), bv_size);
-            m_manager.trace_stream() << "\n";
+            m_manager.trace_stream() << "#x" << val.as_hex(bv_size) << "\n";
         } else {
-            m_manager.trace_stream() << "#b";
-            val.display_bin(m_manager.trace_stream(), bv_size);
-            m_manager.trace_stream() << "\n";
+            m_manager.trace_stream() << "#b" << val.as_bin(bv_size) << "\n";
         }
     }
 

src/ast/converters/expr_inverter.cpp

@@ -400,6 +400,7 @@ class bv_expr_inverter : public iexpr_inverter {
     }
 
     bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+//        return false;
         if (num == 0)
             return false;
         if (!uncnstr(num, args))

src/ast/converters/generic_model_converter.cpp

@@ -43,6 +43,7 @@ void generic_model_converter::operator()(model_ref & md) {
     expr_ref val(m);
     unsigned arity;
     bool reset_ev = false;
+    obj_map<sort, ptr_vector<expr>> uninterpreted;
     for (unsigned i = m_entries.size(); i-- > 0; ) {
         entry const& e = m_entries[i];
         switch (e.m_instruction) {
@@ -63,6 +64,13 @@ void generic_model_converter::operator()(model_ref & md) {
                     reset_ev = old_val != nullptr;
                     md->register_decl(e.m_f, val);
                 }
+                // corner case when uninterpreted constants are eliminated
+                sort* s = e.m_f->get_range();
+                if (m.is_uninterp(s) && !md->has_uninterpreted_sort(s)) {
+                    uninterpreted.insert_if_not_there(s, {});
+                    if (!uninterpreted[s].contains(val))
+                        uninterpreted[s].push_back(val);
+                }
             }
             else {
                 func_interp * old_val = md->get_func_interp(e.m_f);
@@ -84,6 +92,9 @@ void generic_model_converter::operator()(model_ref & md) {
             break;
         }
     }
+    for (auto const& [s, u] : uninterpreted) {
+        md->register_usort(s, u.size(), u.data());
+    }
     TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md););
 }
 

src/ast/converters/generic_model_converter.h

@@ -68,6 +68,8 @@ public:
     void get_units(obj_map<expr, bool>& units) override;
 
     vector<entry> const& entries() const { return m_entries; }
+
+    void reset() { m_entries.reset(); }
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;

src/ast/euf/euf_ac_plugin.cpp

@@ -59,9 +59,9 @@ TODOs:
   - The shared terms hash table is not incremental. 
     It could be made incremental by updating it on every merge similar to how the egraph handles it.
 - V2 using multiplicities instead of repeated values in monomials.
-- Squash trail updates when equations or monomials are modified within the same epoque. 
-  - by an epoque counter that can be updated by the egraph class whenever there is a push/pop.
-  - store the epoque as a tick on equations and possibly when updating monomials on equations.
+- Squash trail updates when equations or monomials are modified within the same epoch.
+  - by an epoch counter that can be updated by the egraph class whenever there is a push/pop.
+  - store the epoch as a tick on equations and possibly when updating monomials on equations.
 
 --*/
 
@@ -80,7 +80,7 @@ namespace euf {
     }
 
     ac_plugin::ac_plugin(egraph& g, func_decl* f) :
-        plugin(g), m_fid(f->get_family_id()), m_decl(f), 
+        plugin(g), m_fid(f->get_family_id()), m_decl(f),
         m_dep_manager(get_region()),
         m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq)
     {

src/ast/euf/euf_arith_plugin.cpp

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    plugin structure for arithetic
+    plugin structure for arithmetic
 
 Author:
 

src/ast/euf/euf_arith_plugin.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    plugin structure for arithetic
+    plugin structure for arithmetic
 Author:
 
     Nikolaj Bjorner (nbjorner) 2023-11-11

src/ast/fpa/bv2fpa_converter.cpp

@@ -319,7 +319,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
 
         if (m_fpa_util.is_to_sbv(f) || m_fpa_util.is_to_ubv(f)) {
             auto k = m_fpa_util.is_to_sbv(f) ? OP_FPA_TO_SBV_I : OP_FPA_TO_UBV_I;
-            parameter param = f->get_parameter(0);
+            const parameter &param = f->get_parameter(0);
             func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, &param, dom.size(), dom.data()), m);
             expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m);
             result->set_else(else_value);

src/ast/fpa_decl_plugin.cpp

@@ -208,8 +208,7 @@ sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
     if (ebits > 63)
         m_manager->raise_exception("maximum number of exponent bits is 63");
 
-    parameter p1(ebits), p2(sbits);
-    parameter ps[2] = { p1, p2 };
+    parameter ps[2] = { parameter(ebits), parameter(sbits) };
     sort_size sz;
     sz = sort_size::mk_very_big(); // TODO: refine
     return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOATING_POINT_SORT, sz, 2, ps));