Skip to content

Commit

Permalink
Merge pull request #100 from VeriFIT/update_z3
Browse files Browse the repository at this point in the history
Update z3
  • Loading branch information
jurajsic authored Sep 27, 2023
2 parents 39f78f5 + 1ba1904 commit f211b89
Show file tree
Hide file tree
Showing 766 changed files with 26,435 additions and 30,122 deletions.
3 changes: 2 additions & 1 deletion .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,9 +56,10 @@ jobs:
./test-z3 -a
cd -
# Disabled: ${{github.workspace}}/build/examples/c_example_build_dir/c_example

- name: Run examples
run: |
${{github.workspace}}/build/examples/c_example_build_dir/c_example
${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example
${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help
${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/docker-image.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ jobs:
type=edge
type=sha,prefix=ubuntu-20.04-bare-z3-sha-
- name: Build and push Bare Z3 Docker Image
uses: docker/build-push-action@v3.2.0
uses: docker/build-push-action@v4.0.0
with:
context: .
push: true
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/wasm-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ jobs:
cp ../../../LICENSE.txt .
- name: Setup emscripten
uses: mymindstorm/setup-emsdk@v11
uses: mymindstorm/setup-emsdk@v12
with:
no-install: true
version: ${{env.EM_VERSION}}
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/wasm.yml
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ jobs:
node-version: "lts/*"

- name: Setup emscripten
uses: mymindstorm/setup-emsdk@v11
uses: mymindstorm/setup-emsdk@v12
with:
no-install: true
version: ${{env.EM_VERSION}}
Expand Down
11 changes: 5 additions & 6 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,12 @@ callgrind.out.*
.z3-trace
# OCaml generated files
*.a
*.o
*.cma
*.cmo
*.cmi
*.cmx
*.byte
*.cmxa
ocamlz3
# Java generated files
Expand All @@ -22,6 +25,7 @@ ocamlz3
# Directories with generated code and documentation
release/*
build/*
trace/*
build-dist/*
dist/*
src/out/*
Expand Down Expand Up @@ -95,9 +99,4 @@ CMakeSettings.json
*.swp
.DS_Store
dbg/**
.idea
CMakeFiles
cli/CTestTestfile.cmake
cli/cmake_install.cmake
cli/version.cc
cli/Makefile
*.wsp
2 changes: 1 addition & 1 deletion CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.4)

set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
project(Z3 VERSION 4.12.2.0 LANGUAGES CXX)

################################################################################
# Project version
Expand Down
605 changes: 0 additions & 605 deletions Parameters.md

This file was deleted.

31 changes: 31 additions & 0 deletions README-CMake.md
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,37 @@ CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../
Note like with the ``CC`` and ``CXX`` flags this must be done on the very first invocation
to CMake in the build directory.

### Adding Z3 as a dependency to a CMAKE Project

CMake's [FetchContent](https://cmake.org/cmake/help/latest/module/FetchContent.html) allows
the fetching and populating of an external project. This is useful when a certain version
of z3 is required that may not match with the system version. With the following code in the
cmake file of your project, z3 version 4.12.1 is downloaded to the build directory and the
cmake targets are added to the project:

```
FetchContent_Declare(z3
GIT_REPOSITORY https://github.com/Z3Prover/z3
GIT_TAG z3-4.12.1
)
FetchContent_MakeAvailable(z3)
```

The header files can be added to the included directories as follows:

```
include_directories( ${z3_SOURCE_DIR}/src/api )
```

Finally, the z3 library can be linked to a `yourTarget` using

```
target_link_libraries(yourTarget libz3)
```
Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`).



### Ninja

[Ninja](https://ninja-build.org/) is a simple build system that is built for speed.
Expand Down
28 changes: 28 additions & 0 deletions RELEASE_NOTES.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,32 @@ 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.2
==============
- remove MSF (Microsoft Solver Foundation) plugin
- updated propagate-ineqs tactic and implementing it as a simplifier, bound_simplifier.
It now eliminates occurrences of "mod" operators when bounds information
implies that the modulus is redundant. This tactic is useful for
benchmarks created by converting bit-vector semantics to integer
reasoning.
- add API function Z3_mk_real_int64 to take two int64 as arguments. The Z3_mk_real function takes integers.
- Add _simplifiers_ as optional incremental pre-processing to solvers.
They are exposed over the SMTLIB API using the command [`set-simplifier`](https://microsoft.github.io/z3guide/docs/strategies/simplifiers).
Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated.
The exposed simplifiers cover all the pre-processing techniques used internally with some additional simplifiers, such as `solve-eqs`
and `elim-predicates` that go beyond incremental pre-processing used internally. The advantage of using `solve-eqs` during pre-processing
can be significant. Incremental pre-processing simplification using `solve-eqs` and other simplifiers that change interpretations
was not possible before.
- Optimize added to JS API, thanks to gbagan
- SMTLIB2 proposal for bit-vector overflow predicates added, thanks to aehyvari
- bug fixes, thanks to Clemens Eisenhofer, hgvk94, Lev Nachmanson, and others


Version 4.12.1
==============
- change macos build to use explicit reference to Macos version 11. Hosted builds are migrating to macos-12 and it broke a user Issue #6539.

Version 4.12.0
==============
- add clause logging API.
Expand Down Expand Up @@ -112,6 +138,8 @@ Version 4.12.0
theory clauses.
- integration of pre-processing proofs with logging proofs. There is
currently no supported bridge to create a end-to-end proof objects.
- experimental API for accessing E-graphs. Exposed over Python. This API should be considered temporary
and subject to be changed depending on use cases or removed. The functions are `Z3_solver_congruence_root`, `Z3_solver_congruence_next`.


Version 4.11.2
Expand Down
2 changes: 1 addition & 1 deletion azure-pipelines.yml
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ jobs:
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: 'True'
runTests: 'False'
arm64:
arch: 'amd64_arm64'
setupCmd1: ''
Expand Down
2 changes: 1 addition & 1 deletion contrib/qprofdiff/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ int parse(string const & filename, map<string, map_entry> & data) {
inx != string::npos;
inx = line.find(" : ", from)) {
tokens[ti] = trim(line.substr(from, inx-from));
from = inx+1;
from = inx+3; //3 is the length of " : "
ti++;
}
if (from != line.length() && ti < 4)
Expand Down
4 changes: 2 additions & 2 deletions doc/mk_params_doc.py
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ def help(ous):
out = subprocess.Popen([z3_exe, "-pm"],stdout=subprocess.PIPE).communicate()[0]
modules = ["global"]
if out != None:
out = out.decode(sys.stdout.encoding)
out = out.decode(sys.getdefaultencoding())
module_re = re.compile(r"\[module\] (.*)\,")
lines = out.split("\n")
for line in lines:
Expand All @@ -48,7 +48,7 @@ def help(ous):
out = subprocess.Popen([z3_exe, "-pmmd:%s" % module],stdout=subprocess.PIPE).communicate()[0]
if out == None:
continue
out = out.decode(sys.stdout.encoding)
out = out.decode(sys.getdefaultencoding())
out = out.replace("\r","")
ous.write(out)

Expand Down
129 changes: 129 additions & 0 deletions doc/mk_tactic_doc.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
# Copyright (c) Microsoft Corporation 2015
"""
Tactic documentation generator script
"""

import os
import re
import sys
import subprocess

BUILD_DIR='../build'
SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
OUTPUT_DIRECTORY = os.path.join(os.getcwd(), 'api')

def doc_path(path):
return os.path.join(SCRIPT_DIR, path)

is_doc = re.compile("Tactic Documentation")
is_doc_end = re.compile("\-\-\*\/")
is_tac_name = re.compile("## Tactic (.*)")
is_simplifier = re.compile("ADD_SIMPLIFIER\(.*\"([^\"]*)\".*,.*\"([^\"]*)\".*,.*\"([^\"]*)\"\.*\)")

def is_ws(s):
return all([0 for ch in s if ch != ' ' and ch != '\n'])

def extract_params(ous, tac):
z3_exe = BUILD_DIR + "/z3"
out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
if not out:
return
out = out.decode(sys.getdefaultencoding())
if is_ws(out):
return
ous.write("### Parameters\n\n")
for line in out:
ous.write(line.replace("\r",""))
ous.write("\n")

def generate_tactic_doc(ous, f, ins):
tac_name = None
for line in ins:
m = is_tac_name.search(line)
if m:
tac_name = m.group(1)
if is_doc_end.search(line):
if tac_name:
extract_params(ous, tac_name)
break
ous.write(line)

def extract_tactic_doc(ous, f):
with open(f) as ins:
for line in ins:
if is_doc.search(line):
generate_tactic_doc(ous, f, ins)

def generate_simplifier_doc(ous, name, desc):
ous.write("## Simplifier [" + name + "](https://microsoft.github.io/z3guide/docs/strategies/summary/#tactic-" + name + ")\n")
ous.write("### Description\n" + desc + "\n")


def extract_simplifier_doc(ous, f):
with open(f) as ins:
for line in ins:
m = is_simplifier.search(line)
if m:
generate_simplifier_doc(ous, m.group(1), m.group(2))

def find_tactic_name(path):
with open(path) as ins:
for line in ins:
m = is_tac_name.search(line)
if m:
return m.group(1)
print(f"no tactic in {path}")
return ""

def find_simplifier_name(path):
with open(path) as ins:
for line in ins:
m = is_simplifier.search(line)
if m:
return m.group(1)
print(f"no simplifier in {path}")
return ""

def presort_files(find_fn):
tac_files = []
for root, dirs, files in os.walk(doc_path("../src")):
for f in files:
if f.endswith("~"):
continue
if f.endswith("tactic.h") or "simplifiers" in root:
tac_files += [(f, os.path.join(root, f))]
tac_files = sorted(tac_files, key = lambda x: find_fn(x[1]))
return tac_files


def help(ous):
ous.write("---\n")
ous.write("title: Tactics Summary\n")
ous.write("sidebar_position: 6\n")
ous.write("---\n")
tac_files = presort_files(find_tactic_name)
for file, path in tac_files:
extract_tactic_doc(ous, path)



def help_simplifier(ous):
ous.write("---\n")
ous.write("title: Simplifiers Summary\n")
ous.write("sidebar_position: 7\n")
ous.write("---\n")
tac_files = presort_files(find_simplifier_name)
for file, path in tac_files:
extract_simplifier_doc(ous, path)

def mk_dir(d):
if not os.path.exists(d):
os.makedirs(d)

mk_dir(os.path.join(OUTPUT_DIRECTORY, 'md'))

with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous:
help(ous)

with open(OUTPUT_DIRECTORY + "/md/simplifier-summary.md",'w') as ous:
help_simplifier(ous)
21 changes: 21 additions & 0 deletions examples/java/JavaExample.java
Original file line number Diff line number Diff line change
Expand Up @@ -2259,6 +2259,24 @@ public void translationExample() {
System.out.println(e1.equals(e3));
}

public void stringExample() {
System.out.println("String example");
Context ctx = new Context();
Expr a = ctx.mkToRe(ctx.mkString("abcd"));
Expr b = ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort()));
System.out.println(a);
System.out.println(b);
System.out.println(a.getSort());
System.out.println(b.getSort());
Expr c = ctx.mkConcat(ctx.mkToRe(ctx.mkString("abc")),
ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort())),
ctx.mkEmptyRe(ctx.mkReSort(ctx.mkStringSort())),
ctx.mkAllcharRe(ctx.mkReSort(ctx.mkStringSort())),
ctx.mkToRe(ctx.mkString("d")));
System.out.println(c);

}

public static void main(String[] args)
{
JavaExample p = new JavaExample();
Expand All @@ -2274,12 +2292,15 @@ public static void main(String[] args)
System.out.print("Z3 Full Version String: ");
System.out.println(Version.getFullVersion());

p.stringExample();

p.simpleExample();

{ // These examples need model generation turned on.
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);


p.optimizeExample(ctx);
p.basicTests(ctx);
Expand Down
20 changes: 0 additions & 20 deletions examples/msf/README

This file was deleted.

Loading

0 comments on commit f211b89

Please sign in to comment.