001 package escjava.prover;
002
003 import java.util.Properties;
004 import java.util.Vector;
005 import java.util.Enumeration;
006
007 import java.io.*;
008
009 import java.lang.Process;
010
011 public class Harvey extends NewProver {
012
013 SubProcess P; // connection to rv
014
015 static boolean debug = false;
016
017 // special constructor for debugging
018 public Harvey(boolean debug){
019 Harvey.debug = debug;
020 }
021
022 public /*@non_null*/ProverResponse start_prover() {
023
024 //++
025 if(debug) System.out.println("Harvey::start_prover");
026 //++
027
028 started = true;
029
030 return HarveyResponse.factory(1);
031
032 }
033
034 public /*@non_null*/ProverResponse set_prover_resource_flags(/*@non_null*/Properties properties) {
035
036 //++
037 if(debug) System.out.println("Harvey::set_prover_resource_flags");
038 //++
039
040 return null;
041 }
042
043 public /*@non_null*/ProverResponse signature(/*@non_null*/Signature signature) {
044
045 //++
046 if(debug)
047 System.out.print("Harvey::signature");
048 //++
049
050 return null;
051 }
052
053 public /*@non_null*/ProverResponse declare_axiom(/*@non_null*/Formula formula) {
054
055 return null;
056 }
057
058 public /*@non_null*/ProverResponse make_assumption(/*@non_null*/Formula formula) {
059
060 return null;
061 }
062
063 public /*@non_null*/ProverResponse retract_assumption(int count) {
064
065 return null;
066 }
067
068 /*
069 * Everything here is just for demo,
070 * but it's ultra lame even compared to interacting with simplify
071 */
072 public /*@non_null*/ProverResponse is_valid(/*@non_null*/Formula formula,
073 Properties properties) {
074
075 PrintWriter file = null;
076
077 Runtime r = Runtime.getRuntime();
078
079 /* save formula on disk */
080 try {
081
082 file = new PrintWriter(new BufferedWriter
083 (new FileWriter("temp-rv.rv")));
084
085 file.println(formula.toString());
086 }
087 catch (Exception e) { System.out.println(e.toString()); }
088
089 file.close();
090
091 /* execute rvc */
092 try {
093 r.exec("rvc temp-rv.rv");
094 }
095 catch (Exception e) { System.out.println(e.toString());}
096
097 /* result is written to "temp-rv.baf"
098 * such interaction with the prover!!!
099 */
100
101 /* exec rv on the file generated */
102 //P = new SubProcess("Harvey",
103 //new String[] {"/usr/local/bin/rv","temp-rv.baf"},null);
104
105 Process Q = null;
106
107 try {
108 Q = r.exec(new String[]{"/usr/local/bin/rv","temp-rv.baf"});
109
110 Q.waitFor();
111
112 /* check validity */
113 InputStream i = Q.getInputStream();
114
115 while( i.available() > 0 ){
116 int next = i.read();
117 char c = (char)next;
118 System.out.print(c);
119 }
120
121 }
122 catch (Exception e) { System.out.println(e.toString());}
123
124 return null;
125 }
126
127 public /*@non_null*/ProverResponse stop_prover() {
128
129 //++
130 if(debug) System.out.println("Harvey::stop_prover");
131 //++
132
133 if(P!=null)
134 P.close();
135
136 return HarveyResponse.factory(1);
137 }
138
139 public static void main(String[] argv){
140
141
142 Harvey harvey = new Harvey(true);
143
144 harvey.start_prover();
145
146 LineNumberReader lNR = null;
147 String formulaString = null;
148 StringBuffer formulaStringB = new StringBuffer();
149
150 try {
151
152 lNR = new LineNumberReader(new FileReader("test-rv.rv"));
153 formulaString = new String();
154
155 while( lNR.ready() ){
156
157 formulaStringB.append("\n").append(lNR.readLine());
158
159 }
160
161 formulaString = formulaStringB.toString();
162
163 harvey.is_valid(new Formula(formulaString),null);
164
165 }
166 catch (Exception e) {
167
168 System.err.println(e);
169 System.err.println("You seems to be trying to launch the harvey demo...");
170 System.err.println("In order to be able to do that, you need to have harvey in /usr/local/bin/ under the name rv");
171 System.err.println("And you need a proof example in a file called 'test-rv.rv' in ESCTools/Escjava/.");
172 System.err.println("I know that's crappy..");
173 }
174
175 harvey.stop_prover();
176
177 System.exit(0);
178
179 }
180
181 }