PZ3

KO | EN

gitlite — search

#javascript #python #react #ai #machine-learning #deep-learning #docker #java #kubernetes #vue #pytorch #mcp #openai #open-source

(★ 8)

Parallelizing SMT Solving: Lazy Decomposition + Conciliation

PZ3 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

Download
--------
__Download PZ3 (Beta 2 updated in 2017-8-5)__: https://git.io/v7wN5

Introduction
-------------
PZ3 is a parallel SMT solver from the paper "Parallelizing SMT Solving: Lazy Decomposition + Conciliation". It is based on Z3 project(https://github.com/Z3Prover/z3) by Microsoft Research. Although PZ3 only supports QF_UF theory for now, we plan to extend PZ3 to support other popular theories such as QF_DL, QF_LRA.

Requirements
-------------
OS: Linux distributions

CPU: multi-core CPU with more than 4 cores

Memory: 8GB or higher

Building & Configuration
---------------------------
**1.** Download source code of Z3 from https://github.com/Z3Prover/z3. You can download Z3 4.3.2 from master branch or 4.3.3 from unstable branch. Please ensure that you are not using an older Z3 because old version has relatively poor support on interpolation. (UPDATE: If you use Z3 4.4.0 or higher, PZ3 would have segmentation fault due to some changes on interpolation API)

**2.** Build Z3 from source and install it using the following commands:

python scripts/mk_make.py
    cd build
    make
    sudo make install

**3.** Build PZ3 from source using the following commands:

make

Usage
------
The usage of PZ3 is

pz3 [Path of SMTLIB2 file] [Number of cores]

For example, if you want to solve `test.smt2` with 4 cores, you can execute

pz3 test.smt2 4

Note 
-----
1. it is not recommended to specify `Number of cores` larger than the number of physical cores because overall performance may degrade significantly.
2. when `Number of cores` is specified with 1, we are using sequential Z3 to solve the benchmark file.
3. PZ3 calls `Z3_interpolate_proof` but in some versions of Z3 this API is not available. If you have problem building or running the program, you should add the codes below into `src/api/z3_interp.h`.

```c
void Z3_API Z3_interpolate_proof(Z3_context ctx,
                                 Z3_ast proof,
                                 int num,
                                 Z3_ast *cnsts,
                                 unsigned *parents,
                                 Z3_params options,
                                 Z3_ast *interps,
                                 int num_theory,
                                 Z3_ast *theory);
```

PZ3

PZ3 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

PZ3

PZ3 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Download README