    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    }