VIATRA-Generator
VIATRA-Generator copied to clipboard
Finally! a pull request for the Vampire-new branch
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")