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    }