| java.lang.Object
 de.uka.ilkd.key.counterexample.MgtpWrapper
| MgtpWrapper | | public class MgtpWrapper (Code) | | This class calls the parser of Mgtp with the generated Calculus.
After the parser has processed the calculus, the theorem prover
is called and the returned model is then further processed
and written to the 'result' attribute. Most of the code is copied from
the Mgtp Class, so a new version of Mgtp might make changes necessary.
!!! I have not yet implemented any method to read the prove mgtp writes
to stdout!!!
author:
Sonja Pieper
version:
2.1
since:
August 2000 |
| Method Summary | |
| public boolean | foundModel()
| | public String | getProve()
| | public String | getStats()
Output of several mgtp statistics as number of models, branches, atoms
and of course if the problem is SAT or UNSAT. |
| MgtpWrapper | | MgtpWrapper(Calculus calc)(Code) | | Creates a new MgtpWrapper. All the initializations which are done in
the classbody of Mgtp are here done in the constructor.
Those parts of the code are mostly copied to make things easier to use.
Parameters:
calc - the constructor receives the previously generated calculus |
| foundModel | | public boolean foundModel()(Code) | | |
| getStats | | public String getStats()(Code) | | Output of several mgtp statistics as number of models, branches, atoms
and of course if the problem is SAT or UNSAT.
A string representation of the above statistics. |
|
|