variables: cmakeStdArgs: '-DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "Ninja" ../' asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"' ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"' jobs: - job: "LinuxPythonDebug" displayName: "Ubuntu build - python make - debug" pool: vmImage: "Ubuntu-16.04" steps: - script: python scripts/mk_make.py -d --java --dotnet - script: | cd build make make examples ls ./cpp_example ./c_example make test-z3 ./test-z3 -a cd .. - script: git clone https://github.com/z3prover/z3test z3test - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 # TBD: # test python bindings # build documentation # Asan, ubsan, msan - job: "LinuxCMake" displayName: "Ubuntu build - cmake" pool: vmImage: "Ubuntu-16.04" strategy: matrix: debugClang: cmdLine: 'CC=clang CXX=clang++ cmake $(cmakeStdArgs)' runUnitTest: 'True' releaseClang: cmdLine: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release $(cmakeStdArgs)' runUnitTest: 'True' debugGcc: cmdLine: 'CC=gcc CXX=g++ cmake $(cmakeStdArgs)' runUnitTest: 'True' # gccX86: # cmdLine: 'CXXFLAGS="${CXXFLAGS} -m32" CFLAGS="${CFLAGS} -m32" CC=gcc-5 CXX=g++-5 cmake -DCMAKE_BUILD_TYPE=RelWithDebInfo $(cmakeStdArgs)' # runUnitTest: 'True' # asan: # cmdLine: '$(asanEnv) cmake $(cmakeStdArgs)' # runUnitTest: 'False' steps: - script: sudo apt-get install ninja-build - script: | mkdir build cd build $(cmdLine) ninja ninja test-z3 ninja c_example ninja cpp_example ninja z3_tptp5 ninja c_maxsat_example examples/c_example_build_dir/c_example examples/cpp_example_build_dir/cpp_example examples/tptp_build_dir/z3_tptp5 -help examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt mkdir -p examples/java cp ../examples/java/JavaExample.java examples/java/ javac examples/java/Javaexamplejava -classpath com.microsoft.z3.jar export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} java -cp .:examples/java:com.microsoft.z3.jar JavaExample ./test-z3 -a cd .. - script: | cd build ./test-z3 -a cd .. condition: eq(variables['runUnitTest'], 'True') - script: | jupyter-nbconvert --to notebook --execute --output out.txt examples/python/tutorial/jupyter/guide.ipynb jupyter-nbconvert --to notebook --execute --output out.txt examples/python/tutorial/jupyter/strategies.ipynb - script: git clone https://github.com/z3prover/z3test z3test - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 - job: "Windows2017" displayName: "Windows 2017 build" pool: vmImage: "vs2017-win2016" steps: - script: scripts\vsts-vs2017.cmd x64 - job: "MacOS" displayName: "MacOS build" pool: vmImage: "macOS-10.14" steps: - script: python scripts/mk_make.py -d --java --dotnet - script: | cd build make make examples ls ./cpp_example ./c_example make test-z3 ./test-z3 -a cd .. - script: git clone https://github.com/z3prover/z3test z3test - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 - job: "MacOSCMake" displayName: "MacOS build with CMake" pool: vmImage: "macOS-10.14" steps: - script: brew install ninja - script: | mkdir build cd build CC=clang CXX=clang++ cmake $(cmakeStdArgs) ninja ninja test-z3 ninja c_example ninja cpp_example ninja z3_tptp5 ninja c_maxsat_example examples/c_example_build_dir/c_example examples/cpp_example_build_dir/cpp_example examples/tptp_build_dir/z3_tptp5 -help examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt mkdir -p examples/java cp ../examples/java/JavaExample.java examples/java/ javac examples/java/Javaexamplejava -classpath com.microsoft.z3.jar export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} java -cp .:examples/java:com.microsoft.z3.jar JavaExample ./test-z3 -a cd .. - script: git clone https://github.com/z3prover/z3test z3test - script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2