search

SymbolicPathFinder / jpf-symbc

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

SPF changes to support path-merging (1 of 2) #31

Closed vaibhavbsharma closed 4 years ago

vaibhavbsharma commented 5 years ago

This pull request primarily captures changes to SPF needed for path-merging support. It consists of 4 changes, 3 of which are about solving queries in SPF.

  1. Allow logical-and, logical-or, and logical-not to be used as operators in the solver interface
  2. Allow the values for SymbolicInteger and IntVariable to be captured from the model returned by the solver, even with incremental solving
  3. Allow Green constraints and expressions to be used in SPF
  4. Allow a PCChoiceGenerator with a single choice to be created on encountering a method invocation with symbolic argument(s) because path-merging depends on having a prior PCChoiceGenerator to append the formula for a region's summary

Testing: These changes have been tested in combination with changes from the second pull request. Tests are described in the second pull request.

vaibhavbsharma commented 4 years ago

Closing this pull request because we came to an agreement that Java Ranger's changes should be maintained in a separate Java Ranger repository and Java Ranger's changes to SPF should be submitted to SPF. While this pull request does only contain Java Ranger's SPF changes, it is now over a year old.

I will re-examine Java Ranger's changes to SPF and resubmit these changes in a new pull request.