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 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 ProverResponse set_prover_resource_flags(Properties properties) { 035 036 //++ 037 if(debug) System.out.println("Harvey::set_prover_resource_flags"); 038 //++ 039 040 return null; 041 } 042 043 public ProverResponse signature(Signature signature) { 044 045 //++ 046 if(debug) 047 System.out.print("Harvey::signature"); 048 //++ 049 050 return null; 051 } 052 053 public ProverResponse declare_axiom(Formula formula) { 054 055 return null; 056 } 057 058 public ProverResponse make_assumption(Formula formula) { 059 060 return null; 061 } 062 063 public 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 ProverResponse is_valid(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 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 }