VIATRA-Generator icon indicating copy to clipboard operation
VIATRA-Generator copied to clipboard

Finally! a pull request for the Vampire-new branch

Open ArenBabikian opened this issue 4 years ago • 0 comments

After years of implementation, I am very happy to finally be able to say that the Vampire-New branch is ready to be merged into master.

In the current state of the branch, users can call any TPTP solver from a configuration file through server calls to the TPTP website, and may also call a local installation of Vampire. Outputs of the call are currently hard-coded to UndecideableResult instances (in other words, no .xmi model is output). A backwards mapping for the local Vampire calls is partially implemented, but not yet integrated. Statistics are also not yet fully handled (correctly) by the TPTP solver calls.

Future work to make the TPTP solver calls more user-friendly also involves refactoring the corresponding project to more general names (i.e., by replacing "Vampire" by "TPTP")

ArenBabikian avatar Jun 15 '20 00:06 ArenBabikian