3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
z3/maxsat
Leonardo de Moura 97d365c11c removed redundant compilation modes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-10 23:11:44 -07:00
..
build-external.cmd other components 2012-10-02 11:48:48 -07:00
build.sh Cleaned maxsat example 2012-10-09 07:32:29 -07:00
ex.smt other components 2012-10-02 11:48:48 -07:00
exec-external.cmd other components 2012-10-02 11:48:48 -07:00
maxsat.c other components 2012-10-02 11:48:48 -07:00
maxsat.vcxproj removed redundant compilation modes 2012-10-10 23:11:44 -07:00
README-external.txt Cleaned maxsat example 2012-10-09 07:32:29 -07:00
README.txt removed redundant compilation modes 2012-10-10 23:11:44 -07:00

WARNING: this example still uses the old Z3 (version 3.x) C API. 
The current version is backward compatible. 

This directory contains scripts to build the MaxSAT application using
Microsoft C compiler, or gcc.

1) Using Visual Studio (with Z3 source code release)

The maxsat example application is automatically built when the z3-prover.sln is processed. The following command should be used to compile z3-prover.sln in the Z3 root directory

        msbuild /p:configuration=external

The maxsat executable is located at
    
        ..\external\maxsat

To process ex.smt, use

        ..\external\maxsat ex.smt

2) Using gcc (on Linux or OSX)

Use 'build.sh' to build the MaxSAT application using gcc. 

You must install Z3 before running this example.
To install Z3, execute the following command in the Z3 root directory.

  sudo make install

Use 'build.sh' to build the test application using gcc. 
It generates the executable 'maxsat'.