001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.counterexample;
012:
013: //import mgtp.*;
014:
015: /**
016: * This class calls the parser of Mgtp with the generated Calculus.
017: * After the parser has processed the calculus, the theorem prover
018: * is called and the returned model is then further processed
019: * and written to the 'result' attribute. Most of the code is copied from
020: * the Mgtp Class, so a new version of Mgtp might make changes necessary.
021: *
022: * !!! I have not yet implemented any method to read the prove mgtp writes
023: * to stdout!!!
024: *
025: * @author Sonja Pieper
026: * @version 2.1
027: * @since August 2000
028: */
029:
030: public class MgtpWrapper {//extends MGTP {
031:
032: private String parserInput;
033: private String result;
034:
035: /**
036: * Creates a new MgtpWrapper. All the initializations which are done in
037: * the classbody of Mgtp are here done in the constructor.
038: * Those parts of the code are mostly copied to make things easier to use.
039: *
040: * @param calc the constructor receives the previously generated calculus
041: */
042:
043: MgtpWrapper(Calculus calc) {
044:
045: parserInput = calc.toString();
046:
047: // MGTP.mgtp = this;
048: //setupOptions(mgtp.args);
049: //------------------begin copied mgtp code--------------------------
050: /* @@@ achtung mgtp code ist derzeit auskommentiert!
051: this.ac = new ACell();
052:
053: this.pModel=false;
054: this.nModel=false;
055: this.pdlF=DList.NIL; this.pdlL=DList.NIL; this.pdlnF=DList.NIL;
056: this.ndlF=DList.NIL; this.ndlL=DList.NIL; this.ndlnF=DList.NIL;
057: this.mdlF=DList.NIL; this.mdlL=DList.NIL; this.mdlnF=DList.NIL;
058:
059: this.closed=false; // R.H. 98.08.15
060: this.rll=RDlList.NIL;
061: this.rjl=RDjList.NIL;
062: */
063: //------------------end copied mgtp code--------------------------
064: }
065:
066: /**
067: * This function first calls the parser of MGTP with the generated calculus
068: * and afterwards the prover is started. The MGTP output is written to the
069: * attribute <code>result</code>.
070: */
071: private void runMgtp() {
072:
073: //------------------begin copied mgtp code--------------------------
074: /* @@@ achtung mgtp code ist auskommentiert!
075: //mgtp copyright notice:
076: System.out.println("JavaCMGTP Version 32gR99.04.09 9-Apr-1999");
077: System.out.println("Copyright (c) 1997-1999 Kyushu University");
078:
079: mgtp=(selectMin ? new MGTPpickupMin() : mgtp );
080:
081: java.io.StringReader fis = new java.io.StringReader(generatedCalculus);
082: probName = "natstack";
083: parser=new MGTPParser(fis);
084: parser.mgtp = this;
085: time=System.currentTimeMillis();
086: if (!parser.parse(mgtp)) return;
087: time=System.currentTimeMillis()-time;
088: System.out.println("Parsing time: "+time+" msec");
089:
090: if (verbose) {
091: System.out.println("\n"
092: +"Positive clause(s):\n"+mgtp.posCls
093: +"Negative clause(s):\n"+mgtp.negCls
094: +"Cont. clause(s):\n"+mgtp.cntCls
095: +"Mixed clause(s):\n"+mgtp.mixCls);
096: }
097:
098: System.out.println("Proving . . .");
099: time=System.currentTimeMillis();
100: mgtp.init();
101: mgtp.posCls.first.cjmCL(null);
102: mgtp.prove(); //@@@ missing some kind of stdout readout to process info!
103: time=System.currentTimeMillis()-time;
104: */
105: //------------------end copied mgtp code--------------------------
106: }
107:
108: public String getProve() {
109: this .runMgtp();
110: return result; //@@@ see runMgtp() not yet done need stdout readout!
111: }
112:
113: public boolean foundModel() {
114: //@@@ not really useful now!!!
115: return true; //mgtp.sat;
116: }
117:
118: /**
119: * Output of several mgtp statistics as number of models, branches, atoms
120: * and of course if the problem is SAT or UNSAT.
121: * @return A string representation of the above statistics.
122: */
123: public String getStats() {
124: return "No Stats available right now!";
125: /* @@@ auskommentierter mgtp code
126: return "Number of models: "+mgtp.models+"\n"+
127: "Number of failed branches: "+mgtp.failedBranches+"\n"+
128: "Number of total branches: "+mgtp.branches+"\n"+
129: "Number of total atoms: "+mgtp.atoms+"\n"+
130: (mgtp.sat? "SAT": "UNSAT")+
131: "\nProving time: "+time+" msec\n";
132: */
133: }
134:
135: }
|