mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
update release version
This commit is contained in:
parent
1d622a678e
commit
8ae24e2b38
62
.github/workflows/docker-image.yml
vendored
62
.github/workflows/docker-image.yml
vendored
|
@ -1,62 +0,0 @@
|
||||||
name: Publish Docker image
|
|
||||||
|
|
||||||
on:
|
|
||||||
workflow_dispatch: # on button click
|
|
||||||
|
|
||||||
permissions:
|
|
||||||
contents: read
|
|
||||||
|
|
||||||
jobs:
|
|
||||||
push_to_registry:
|
|
||||||
name: Push Docker image to GitHub Docker registry
|
|
||||||
runs-on: ubuntu-latest
|
|
||||||
|
|
||||||
steps:
|
|
||||||
- name: Check out the repo
|
|
||||||
uses: actions/checkout@v4
|
|
||||||
|
|
||||||
- name: Log in to GitHub Docker registry
|
|
||||||
uses: docker/login-action@v3
|
|
||||||
with:
|
|
||||||
registry: ghcr.io
|
|
||||||
username: ${{ secrets.DOCKER_USERNAME }}
|
|
||||||
password: ${{ secrets.DOCKER_PASSWORD }}
|
|
||||||
|
|
||||||
# -------
|
|
||||||
# BARE Z3
|
|
||||||
# -------
|
|
||||||
- name: Extract metadata (tags, labels) for Bare Z3 Docker Image
|
|
||||||
id: meta
|
|
||||||
uses: docker/metadata-action@v5
|
|
||||||
with:
|
|
||||||
images: ghcr.io/z3prover/z3
|
|
||||||
flavor: |
|
|
||||||
latest=auto
|
|
||||||
prefix=ubuntu-20.04-bare-z3-
|
|
||||||
tags: |
|
|
||||||
type=schedule,pattern={{date 'YYYYMMDD'}}
|
|
||||||
type=ref,event=tag
|
|
||||||
type=edge
|
|
||||||
type=sha,prefix=ubuntu-20.04-bare-z3-sha-
|
|
||||||
- name: Build and push Bare Z3 Docker Image
|
|
||||||
uses: docker/build-push-action@v6.13.0
|
|
||||||
with:
|
|
||||||
context: .
|
|
||||||
push: true
|
|
||||||
target: bare-z3
|
|
||||||
file: ./docker/ubuntu-20-04.Dockerfile
|
|
||||||
tags: ${{ steps.meta.outputs.tags }}
|
|
||||||
labels: ${{ steps.meta.outputs.labels }}
|
|
||||||
|
|
||||||
# ------------------------------
|
|
||||||
# Repo description on GHCR
|
|
||||||
# ------------------------------
|
|
||||||
# - name: Update repo description
|
|
||||||
# uses: peter-evans/dockerhub-description@v2
|
|
||||||
# with:
|
|
||||||
# registry: ghcr.io
|
|
||||||
# repository: z3prover/z3
|
|
||||||
# username: ${{ secrets.DOCKER_USERNAME }}
|
|
||||||
# password: ${{ secrets.DOCKER_PASSWORD }}
|
|
||||||
# short-description: ${{ github.event.repository.description }}
|
|
||||||
# readme-filepath: ./docker/README.md
|
|
|
@ -2,7 +2,7 @@
|
||||||
cmake_minimum_required(VERSION 3.16)
|
cmake_minimum_required(VERSION 3.16)
|
||||||
|
|
||||||
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
||||||
project(Z3 VERSION 4.13.4.0 LANGUAGES CXX)
|
project(Z3 VERSION 4.14.0.0 LANGUAGES CXX)
|
||||||
|
|
||||||
################################################################################
|
################################################################################
|
||||||
# Project version
|
# Project version
|
||||||
|
|
|
@ -10,6 +10,13 @@ Version 4.next
|
||||||
- native word level bit-vector solving.
|
- native word level bit-vector solving.
|
||||||
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
|
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
|
||||||
|
|
||||||
|
Versoin 4.14.0
|
||||||
|
==============
|
||||||
|
- [SLS modulo theories](https://microsoft.github.io/z3guide/programming/Local%20Search/) engine v1 release.
|
||||||
|
- API for accessing term [depth and groundness](https://github.com/Z3Prover/z3/pull/7479).
|
||||||
|
- A new API for solving LRA variables modulo constraints.
|
||||||
|
- Performance and bug fixes.
|
||||||
|
|
||||||
Version 4.13.4
|
Version 4.13.4
|
||||||
==============
|
==============
|
||||||
- several updates to emscripten including #7473
|
- several updates to emscripten including #7473
|
||||||
|
|
|
@ -8,7 +8,7 @@
|
||||||
from mk_util import *
|
from mk_util import *
|
||||||
|
|
||||||
def init_version():
|
def init_version():
|
||||||
set_version(4, 13, 4, 0) # express a default build version or pick up ci build version
|
set_version(4, 14, 0, 0) # express a default build version or pick up ci build version
|
||||||
|
|
||||||
# Z3 Project definition
|
# Z3 Project definition
|
||||||
def init_project_def():
|
def init_project_def():
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
variables:
|
variables:
|
||||||
Major: '4'
|
Major: '4'
|
||||||
Minor: '13'
|
Minor: '14'
|
||||||
Patch: '4'
|
Patch: '0'
|
||||||
ReleaseVersion: $(Major).$(Minor).$(Patch)
|
ReleaseVersion: $(Major).$(Minor).$(Patch)
|
||||||
AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
|
AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
|
||||||
NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
|
NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
|
||||||
|
|
|
@ -6,7 +6,7 @@
|
||||||
trigger: none
|
trigger: none
|
||||||
|
|
||||||
variables:
|
variables:
|
||||||
ReleaseVersion: '4.13.4'
|
ReleaseVersion: '4.14.0'
|
||||||
|
|
||||||
stages:
|
stages:
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
def_module_params('sls',
|
def_module_params('sls',
|
||||||
export=True,
|
export=True,
|
||||||
description='Experimental Stochastic Local Search Solver (for QFBV only).',
|
description='Stochastic Local Search Solver (invoked by sls-qfbv and sls-smt tactics or enabled by smt.sls.enable=true)',
|
||||||
params=(max_memory_param(),
|
params=(max_memory_param(),
|
||||||
('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
|
('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
|
||||||
('max_repairs', UINT, 1000, 'maximum number of repairs before restart'),
|
('max_repairs', UINT, 1000, 'maximum number of repairs before restart'),
|
||||||
|
|
Loading…
Reference in a new issue