A report of my activities in GSoC 2019 Program

GSoC2019report.md

Google Summer of Code 2019 Report

BY BOLARINWA OLAYEMI SAHEED

PROJECT: Integrate more SMT solvers into JavaSMT

ORGANISATION: Software and Computational Systems Lab at LMU Munich

MENTOR: Karlheinz Friedberger

ABSTRACT:

This goal of this project is integrate more SMT Solver into the JavaSMT library. I have chosen to integrate STP and OpenSMT solver libraries. Both are written in C++ and provide a C language interface which what I creating Java bindings to. I will also be written code to glue the integrated solvers to the JavaSMT library.

ACTIVITES:

OpenSMT All here in one Pull Request

• Create a basic sample (simpler than the more elaborate existing ones) to use the java-smt library
• Create a Build Script which can automatically:
  • Clone and Build opensmt2,
  • Generate the java bindings and compile if a Jar (so we a Jar and .so)
  • Copy the Jar and .so files to appropriate folder inside the java-smt
• Fixed some of the bugs in the initial attempt,
• Create SolverContext class (not fully implemented)
• Create FormulaManager class (not fully implemented)
• Create FormulaCreator class (not fully implemented)
• Create classes for supported Formulae/Thoeries and their Managers (not fully implemented)
• Create classes for the Theorem Prover (not fully implemented)
• Contacted JavaCpp team for help
• Research and Switched to SWIG - tested examples
• Research CMake + SWIG and Reimplement some examples.
• Used SWIG + Cmake to create Java Binding for OpenSMT2.

STP All here in one Pull Request

• Create a Build Script which can automatically:
  • Clone and Build STP,
  • Generate the java bindings and compile if a Jar (so we a Jar and .so)
  • Copy the Jar and .so files to appropriate folder inside the java-smt
• Extend the STP's C interface, to support some needed functions like (UNSAT, GetModel, etc)
• Create SolverContext class
• Create FormulaManager class
• Create FormulaCreator class
• Create classes for supported Formulae/Thoeries and their Managers
• Create classes for the Theorem Prover (not fully implemented)
• Create Model class (not fully implemented)

PROJECT STATUS:

OpenSMT2 (incomplete)

TODO: towards completion -

• Fix the Java Binding build
  • Write a custom interface for OpenSMT2 which will be useful in this purpose
  • Figure out how to get an array of Models out of OpenSMT and not string
  • Write a SWIG interface for the custom interface
  • Adjust the build script if needed
• Fully implement the glue code for Formula creation
• Fully implement the glue code for proving SAT/UNSAT
• Create and Implement the Model Class
• Documentation

STP (incomplete)

TODO: towards completion -

• Complete the extension of STP api to support needed functions
  • UNSAT (the current implementation is a hack)
  • Figure out how to get an array of Models out of STP and not string
  • Maybe a better way to fully merge the C++ interface into the C interface
  • A better error handling
• Test Array Formula creation
• Fully implement the glue code for proving SAT/UNSAT
• Fully Implement the Model Class
• Documentation

SKILLS ACQUIRED/PERFECTED:

• Languages: C, C++, Java, BASH,
• Build tools: Cmake, Ant, Apache Ivy,
• Other tools: SWIG, git, Vagrant, Eclipse IDE, Github
• Linux and Debugging

CHALLENGES:

• Communication, clearly I have to work more on this.
• Unfamiliarity with SMT Solver libraries, it is my first experience with these libraries. I had to read the code to understand what's going on. (I could have asked my mentor)
• Reading other people's code.
• The libraries I chose were poorly documented and I couldn't get any help from the team either.
• I wasted time with JavaCPP before settling on SWIG
• Constantly Switching languages C, C++, Java, Bash
• I also have challenges with my laptop, which make my development environment complicated.