search

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
130 stars 91 forks source link

Carson Smith - GSoC Submission PR #54

Open CarsSmith opened 4 years ago

CarsSmith commented 4 years ago

This PR is in reference to the Google Summer of Code 2020 Project 'A Restructuring of the Path Constraint Interface'

In total, this pull request compiles all of the progress I have made throughout the months I have worked on my Google Summer of Code 2020 project. What started off as a project that focused on restructuring Path Constraints ultimately ended up focusing on restructuring the system with how those constraints are parsed. The ultimate goal of the project was the same, however, in that it makes it easier for a prospective programmer to come along and add additional constraint types and solvers to SPF.

This pull request essentially includes a full redesign of the PCParser class in the Numeric package, breaking up the parsing of the various types of constraints into a much more dynamic object-oriented system. This is done through the implementation of a Visitor pattern, primarily centered around the new class ProblemGeneralVisitor.java, which uses the visitor pattern to parse the constraints (and the expressions included within those constraints) to a given ProblemGeneral object.

Everything included in this PR has been tested in full with all of the provided tests/examples provided with SPF with the mindset of maintaining existing functionality as best as possible.

This project ended up being a lot more than I expected given the size of the codebase and the amount of work I had to get done and testing I had to do. Eventually, I really felt like all the pieces of the puzzle were coming together in my head, and felt super satisfied with the work I've done. This project really reinforced my understanding of the concepts of Polymorphism and Inheritance on a much deeper level than anything I had learned in school, and the whole concept of the Visitor Pattern was a ton of fun to implement. Figuring out how the system would best work with SPF was probably the best part of all of it.

With all the changes made in the commits below, the code should work identically or nearly identically to the functionality it originally did. I am more than willing to stick around after the conclusion of GSoC to make additional changes and fix any bugs or issues that arise as a consequence of the changes made here.

I finished with most everything I intended to get done in this project with the exception of the ArrayConstraintVisitor and RealArrayContraintVisitor classes, which have some additional refactoring I'd like to do sometime sooner or later. Either way, the functionality should still be the same.

corinus commented 4 years ago

Thank you for your impressive work. I have been busy but hopefully I'll get to review soon.

corinus commented 4 years ago

Hi Carson: looking at your project it seems it is 16 commits ahead and 2 commits behind from main branch. can you please check wrt latest version? Also did you run ant test on your updates? Thanks

CarsSmith commented 4 years ago

Hello!

I can have my branch update to the latest version from master. There should be no problems there.

As for the testing aspect, I did run as many tests as possible with my changes. I ran most, if not all, of the tests provided along with SPF and made sure they all ran the same.

corinus commented 4 years ago

thanks. just to double check please run 'ant test' after you get the latest version of the master. this should run all the unit tests for spf. thanks. please let me know once you are done and i can merge.