Skip to content

Adding STP solver @GSoC 2019#163

Open
refactormyself wants to merge 26 commits intomasterfrom
dev_add_stp
Open

Adding STP solver @GSoC 2019#163
refactormyself wants to merge 26 commits intomasterfrom
dev_add_stp

Conversation

@refactormyself
Copy link
Contributor

@refactormyself refactormyself commented Aug 26, 2019 •
edited
Loading

So far this is the progress made on adding STP solver to java-smt:

  • 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)

TODO: (I will like to continue with this after GSoC)

  • 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

@refactormyself
Add folders and scripts to clone and build STP and it's Java API
aa50f3c
@refactormyself
Edit .gitignore; Add STP package and a Test
97d113c 
I have added the build paths and STP repo to .gitignore
so I have to do less cleaning before commit

Now in the STP solver package the shared library is
detected - Test passing
@refactormyself
All required Types generated and limited functions add to the API
5dd1faf
@refactormyself
I think I did it, the Sample code, from repo is working
d343022 
Error Handling is not properly done
Tests not written, so fuctions are expected to fail
But it's working
@refactormyself
before rebuilding the API binding (for many reasons)
e467796
@refactormyself
API's package modified and few Classes.Rebuild done
fdb4dfc
@refactormyself
Update the new API and fixed reference errors
e23b5e9
@refactormyself
not working commit
00e03b2
@refactormyself
Add BasicSample and test run
5e13202
@refactormyself
Create Test and Fix error due to no UFManager
7440f28
@refactormyself
Create Test for Boolean Manager and Complete function immplementation
9dd07dc 
Test not passing yet, though
@refactormyself
DId few minor clean ups
c489a72 
unnecessary classes removed
calling functions adjusted

But now StpSolverTest gives a Segfault
@refactormyself
Test the native API
5619883 
The Segfault is a kind of false negative.
The pointers are mismatching i.e. not consistent as objects move around.
Still debugging this
@refactormyself
Add more test for STP the native API binding
94a13c5
@refactormyself
Fixed some bugs
788b0f1
@refactormyself
a bunch
57cedf9
@refactormyself
some adjustment and refactor to make a trivial test pass
b3119cf
@refactormyself
FormulaManagers
d2bfe1d
@refactormyself
Documentation and a few re-factoring
5f9025f
@refactormyself
Fixed bugs and rebuild the API
6be724b
@refactormyself
Confused !
7599622
@refactormyself
API Extension Documentation Before cleanup
0da75f1
@refactormyself
fix and test create variables and formulae. Also toString
c307159 
The Hashcode is done too
Multiple changes done here
@refactormyself
fix and test prover.unsat()
fb868a5
@refactormyself
Fix bug in StpTheoremProver
1a346c5
@refactormyself refactormyself self-assigned this Aug 26, 2019
@refactormyself
FINAL GSoC 2019: let ant include jars in classpath.Create Model class
63e7ed3 
STP only print the models to stdout, I will have to rewrite an
extension method to return the collection of models or an iterator.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@refactormyself refactormyself

Labels

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@refactormyself @kfriedberger