z3/azure-pipelines.yml

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')
# Need to install jupyter-nbconvert
#    - 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
#        jupyter-nbconvert --to notebook --execute --output out.txt examples/python/tutorial/jupyter/advanced.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