    001    package escjava.prover;
    002
    003    import java.util.Properties;
    004    import org.apache.xmlrpc.*;
    005    import java.util.Vector;
    006    import java.util.Enumeration;
    007    import java.util.Iterator;
    008    import java.lang.Thread;
    009
    010    public class Sammy extends NewProver {
    011
    012      /*
    013       * README
    014       * This class and the new other ones like NewProver, ProverResponse
    015       * have been specified with jml. Even if we cannot use jmlc and jmlrac for
    016       * the whole escjava2 program, these new classes have been tested
    017       * apart from the rest of the program. Using jmlrac on a few test seems
    018       * to show that these classes are respecting there specification.
    019       * Anyway nothing has been done with escjava2.
    020       */
    021
    022      //@ public invariant started ==> serverInstance != null;
    023
    024      private static /*@ spec_public @*/ XmlRpcClientLite serverInstance;
    025
    026      /**
    027       * Vector representing the parameters that are given to sammy
    028       * Notice that it's cleared after each call to execute()
    029       */
    030
    031      private /*@ spec_public non_null @*/ static Vector parameters = new Vector();
    032
    033      static boolean debug = false;
    034
    035      // special constructor for debugging
    036      public Sammy(boolean debug){
    037        Sammy.debug = debug;
    038      }
    039
    040      /*@
    041       @ also
    042       @ assignable serverInstance, parameters;
    043       @*/
    044      public ProverResponse start_prover() {
    045
    046        //++
    047        if(debug) System.out.println("Sammy::start_prover");
    048        //++
    049
    050        killAnySammyAndStartNewOne();
    051
    052        try { serverInstance = new XmlRpcClientLite("localhost",8000); }
    053        catch (Exception e) {
    054          System.err.println("Sammy::Failed to init XmlRpc");
    055          System.exit(0);
    056        }
    057
    058        // parameters can't be empty (rpc stuff)
    059        parameters.add("");
    060
    061        ProverResponse res = execute("start_solver");
    062
    063        //++
    064        if(debug)
    065          if( res != ProverResponse.OK )
    066            System.out.println("Failed to init sammy");
    067          //++
    068
    069        started = true;
    070
    071        return res;
    072
    073      }
    074
    075      public ProverResponse set_prover_resource_flags(Properties properties) {
    076
    077        //++
    078        if(debug) System.out.println("Sammy::set_prover_resource_flags");
    079        //++
    080
    081        /* we have to create a big string containing
    082         * all the flags ( = key in the hashtable of Properties)
    083         * and their values ( = value)
    084         */
    085        Enumeration flags = properties.keys();
    086
    087        String value = null;
    088        String currentFlag = null;
    089
    090        for (  ; flags.hasMoreElements() ;) {
    091
    092          try {
    093            currentFlag = (String)flags.nextElement();
    094            value = properties.getProperty( currentFlag );
    095          }
    096
    097          catch (Exception e) {
    098            System.err.println("Sammy::Failed to inspect properties");
    099            System.exit(0);
    100          }
    101
    102          parameters.add(currentFlag);
    103
    104          /* flags can be without value, I guess it means that
    105           * value = ""
    106           */
    107          if( value != null )
    108            parameters.add(value);
    109
    110        }
    111
    112        ProverResponse res = execute("set_flags");
    113
    114        //++
    115        if(debug)
    116          if( res!= ProverResponse.OK )
    117            System.out.println("Failed to set flags");
    118          //++
    119
    120        return res;
    121      }
    122
    123      public ProverResponse signature(Signature signature) {
    124
    125        //++
    126        if(debug)
    127          System.out.print("Sammy::signature");
    128        //++
    129
    130        /*
    131         * Calls for every decomposition of the signature
    132         * Notice that it returns the last response code, not the
    133         * worst one of all calls.
    134         */
    135
    136        //  /*
    137        //   * Types
    138        //   */
    139        //  parameters.add(signature.type());
    140
    141        //  ProverResponse res = execute("type_declaration");
    142
    143        //  //++
    144        //  if(debug)
    145        //      if( res!= ProverResponse.OK )
    146        //          System.out.println("Failed to set types");
    147        //  //++
    148
    149        //  /*
    150        //   * Variables = 0 unary function in smt lib so there is no
    151        //   * need to declare them apart from functions.
    152        //   */
    153
    154        //  /*
    155        //   * Functions
    156        //   */
    157        //  parameters.add(signature.function());
    158
    159        //  res = execute("func_declaration");
    160
    161        //  if(debug)
    162        //      if( res!= ProverResponse.OK )
    163        //          System.out.println("Sammy::Failed to set functions");
    164
    165        //  /*
    166        //   * Predicates
    167        //   */
    168        //  parameters.add(signature.predicate());
    169
    170        //  res = execute("pred_declaration");
    171
    172        //  //++
    173        //  if(debug)
    174        //      if( res!= ProverResponse.OK )
    175        //          System.out.println("Failed to set predicates");
    176        //  //++
    177
    178        //  signature_defined = true;
    179
    180        return null;
    181      }
    182
    183      public ProverResponse declare_axiom(Formula formula) {
    184
    185        /*
    186         * Is an axiom a declaration of a predicate ?
    187         */
    188
    189        return null;
    190      }
    191
    192      public ProverResponse make_assumption(Formula formula) {
    193
    194        /*
    195         * Does it correspond to 'add_assertion' in sammy's interface ?
    196         */
    197
    198
    199        return null;
    200      }
    201
    202      public ProverResponse retract_assumption(int count) {
    203
    204        /*
    205         * == 'backtrack' in sammy's interface ?
    206         */
    207
    208        return null;
    209      }
    210
    211      public ProverResponse is_valid(Formula formula,
    212          Properties properties) {
    213
    214        /*
    215         * I guess it corresponds to the 'query' function of
    216         * sammy's interface ?
    217         */
    218
    219        return null;
    220      }
    221
    222        //@ also
    223        //@ assignable parameters, signature_defined, started;
    224      public ProverResponse stop_prover() {
    225
    226        //++
    227        if(debug) System.out.println("Sammy::stop_prover");
    228        //++
    229
    230        int result;
    231
    232        // parameters can't be empty (rpc stuff)
    233        parameters.add("");
    234
    235        ProverResponse res = execute("stop_solver");
    236
    237        if(debug)
    238          if( res != ProverResponse.OK )
    239            System.out.println("Sammy::Failed to stop");
    240
    241        started = false;
    242        signature_defined = false;
    243
    244        return res;
    245      }
    246
    247      /**
    248       * call to sammy using xml rpc
    249       * commands available :
    250       * start_solver
    251       * set_flags
    252       * type_declaration
    253       * func_declaration
    254       * add_assertion
    255       * query
    256       * backtrack
    257       * stop_solver
    258       * See sammy's cvcl/smt/README.TXT for further informations
    259       */
    260
    261      /*@   requires serverInstance != null;
    262       @   requires !parameters.isEmpty();
    263       @   ensures \result == ProverResponse.OK ||
    264       @   \result == ProverResponse.FAIL ||
    265       @   \result == ProverResponse.YES ||
    266       @   \result == ProverResponse.NO ||
    267       @   \result == ProverResponse.COUNTER_EXAMPLE ||
    268       @   \result == ProverResponse.SYNTAX_ERROR ||
    269       @   \result == ProverResponse.PROGRESS_INFORMATION ||
    270       @   \result == ProverResponse.TIMEOUT ||
    271       @   \result == ProverResponse.INCONSISTENCY_WARNING;
    272       @   assignable parameters;
    273       @*/
    274      private ProverResponse execute(/*@ non_null @*/ String cmd ){
    275
    276        // TODO : improve that
    277        if( parameters.size() > 1)
    278          flatParameters();
    279
    280        //++
    281        System.out.println("Sammy::execute   "+cmd+parameters.toString());
    282        //++
    283
    284        Integer res = new Integer(-1); // negative attitude
    285
    286        try { res = (Integer)serverInstance.execute("sammy."+cmd,parameters); }
    287        catch (Exception e) {
    288          System.err.println("Sammy::Error during rpc call\n"+e);
    289          System.exit(0);
    290        }
    291
    292        //++
    293        if(debug)
    294          System.out.println("=> return value = "+res.intValue());
    295        //++
    296
    297        // clean the parameters before next call
    298        parameters.clear();
    299
    300        return SammyResponse.factory(res.intValue());
    301      }
    302
    303      /*
    304       * Temporary ?
    305       */
    306      /*@
    307       @ assignable parameters;
    308       @*/
    309      private void flatParameters() {
    310
    311        Iterator i = parameters.iterator();
    312        StringBuffer res = new StringBuffer() ;
    313        String temp = null ;
    314
    315        for( ; i.hasNext();) {
    316
    317          try { temp = (String)i.next(); }
    318          catch (Exception e) {
    319            System.err.println("Sammy::Error during flattening parameters\n"+e);
    320            System.exit(0);
    321          }
    322
    323          // without the first space, it fails
    324          // (sammy parsing issue I guess)
    325          res.append(" ").append(temp);
    326
    327        }
    328
    329        parameters.clear();
    330        parameters.add(res.toString());
    331
    332        //++
    333        if(debug)
    334          System.out.println("Sammy::flatParameters   "+res);
    335        //++
    336
    337      }
    338
    339      /*
    340       * Isn't it a good name ?
    341       */
    342      private /*@ pure @*/ int killAnySammyAndStartNewOne(){
    343
    344        //++
    345        if(debug)
    346          System.out.println("Sammy::killAnySammyAndStartNewOne");
    347        //++
    348
    349        /*
    350         * TODO : Is it the right way to do that, and what about Windows ?
    351         */
    352
    353        if( System.getProperty("os.name").startsWith("Linux") ||  System.getProperty("os.name").startsWith("Mac") ){
    354          Runtime r = Runtime.getRuntime();
    355
    356          /*
    357           * TODO : improve that
    358           * for the moment the sleep is required, otherwise there is some issues
    359           * I guess that sammy needs a little time to get ready to accept rpc calls
    360           */
    361          try{
    362            r.exec("killall sammy");
    363            r.exec("sammy");
    364            Thread.sleep(1000);
    365          }
    366          catch(Exception e){
    367            System.out.println(e);
    368            System.out.println("Sammy::Failed to kill existing sammy and starting a new one");
    369            System.exit(0);
    370          }
    371        }
    372
    373
    374        return 0;
    375
    376      }
    377
    378      /*
    379       * Test
    380       */
    381
    382      static public void main(String[] argv){
    383
    384        long startTime = java.lang.System.currentTimeMillis();
    385        Sammy sammy = new Sammy(true);
    386
    387        /* Test 1 */
    388        //  sammy.start_prover();
    389
    390        //  parameters.add("(exp real real real)");
    391        //  parameters.add("(pc real)");
    392        //  sammy.execute("func_declaration");
    393
    394        //  parameters.add("(greater_than real real)");
    395        //  sammy.execute("pred_declaration");
    396
    397        //  parameters.add("(or (not true) (= (+ 1 1) 2))");
    398        //  sammy.execute("add_assertion");
    399
    400        //  parameters.add("(= 1 2)");
    401        //  sammy.execute("add_assertion");
    402
    403        //  sammy.stop_prover();
    404
    405        /* Test 2, given by Cesare */
    406        sammy.start_prover();
    407
    408        parameters.add("(x_0) (x_1)  (x_2)  (x_3)  (x_4)  (x_5)  (x_11)  (x_12)  (x_14)  (x_15)  (x_16)  (x_17)  (x_25)  (x_26)  (x_28)  (x_29)  (x_30)  (x_31)  (x_39)  (x_40)  (x_42)  (x_43)  (x_44)  (x_45)");
    409        sammy.execute("pred_declaration");
    410
    411        parameters.add("(cvclZero Real)  (x_6 Real)  (x_7 Real)  (x_8 Real)  (x_9 Real)  (x_10 Real)  (x_13 Real)  (x_18 Real)  (x_19 Real)  (x_20 Real)  (x_21 Real)  (x_22 Real)  (x_23 Real)  (x_24 Real)  (x_27 Real)  (x_32 Real)  (x_33 Real)  (x_34 Real)  (x_35 Real)  (x_36 Real)  (x_37 Real)  (x_38 Real)  (x_41 Real)  (x_46 Real)  (x_47 Real)  (x_48 Real)  (x_49 Real)  (x_50 Real)  (x_51 Real)");
    412        sammy.execute("func_declaration");
    413
    414        parameters.add("(flet ($cvcl_12 (not x_39)) (flet ($cvcl_13 (not x_40)) (flet ($cvcl_14 (and $cvcl_12 $cvcl_13)) (flet ($cvcl_45 (not x_42)) (flet ($cvcl_46 (not x_43)) (flet ($cvcl_47 (and $cvcl_45 $cvcl_46)) (flet ($cvcl_32 (not x_44)) (flet ($cvcl_33 (not x_45)) (flet ($cvcl_35 (and $cvcl_32 $cvcl_33)) (flet ($cvcl_17 (and (iff x_42 x_28) (iff x_43 x_29))) (flet ($cvcl_42 (not x_28)) (flet ($cvcl_41 (not x_29)) (flet ($cvcl_38 (and $cvcl_42 $cvcl_41)) (flet ($cvcl_7 (and (iff x_39 x_25) (iff x_40 x_26))) (flet ($cvcl_28 (not x_30)) (flet ($cvcl_26 (not x_31)) (flet ($cvcl_21 (and $cvcl_28 $cvcl_26)) (flet ($cvcl_43 (and $cvcl_42 x_29)) (flet ($cvcl_15 (and (iff x_44 x_30) (iff x_45 x_31))) (flet ($cvcl_30 (and $cvcl_28 x_31)) (flet ($cvcl_9 (not x_25)) (flet ($cvcl_8 (not x_26)) (flet ($cvcl_3 (and $cvcl_9 $cvcl_8)) (flet ($cvcl_10 (and $cvcl_9 x_26)) (flet ($cvcl_62 (and (iff x_28 x_14) (iff x_29 x_15))) (flet ($cvcl_83 (not x_14)) (flet ($cvcl_82 (not x_15)) (flet ($cvcl_79 (and $cvcl_83 $cvcl_82)) (flet ($cvcl_55 (and (iff x_25 x_11) (iff x_26 x_12))) (flet ($cvcl_73 (not x_16)) (flet ($cvcl_71 (not x_17)) (flet ($cvcl_66 (and $cvcl_73 $cvcl_71)) (flet ($cvcl_84 (and $cvcl_83 x_15)) (flet ($cvcl_60 (and (iff x_30 x_16) (iff x_31 x_17))) (flet ($cvcl_75 (and $cvcl_73 x_17)) (flet ($cvcl_57 (not x_11)) (flet ($cvcl_56 (not x_12)) (flet ($cvcl_51 (and $cvcl_57 $cvcl_56)) (flet ($cvcl_58 (and $cvcl_57 x_12)) (flet ($cvcl_103 (and (iff x_14 x_4) (iff x_15 x_5))) (flet ($cvcl_124 (not x_4)) (flet ($cvcl_123 (not x_5)) (flet ($cvcl_120 (and $cvcl_124 $cvcl_123)) (flet ($cvcl_96 (and (iff x_11 x_0) (iff x_12 x_1))) (flet ($cvcl_114 (not x_2)) (flet ($cvcl_112 (not x_3)) (flet ($cvcl_106 (and $cvcl_114 $cvcl_112)) (flet ($cvcl_125 (and $cvcl_124 x_5)) (flet ($cvcl_101 (and (iff x_16 x_2) (iff x_17 x_3))) (flet ($cvcl_116 (and $cvcl_114 x_3)) (flet ($cvcl_98 (not x_0)) (flet ($cvcl_97 (not x_1)) (flet ($cvcl_91 (and $cvcl_98 $cvcl_97)) (flet ($cvcl_99 (and $cvcl_98 x_1)) (flet ($cvcl_89 (< (- cvclZero x_6) 0)) (flet ($cvcl_88 (< (- cvclZero x_7) 0)) (flet ($cvcl_87 (< (- cvclZero x_8) 0)) (flet ($cvcl_92 (= (- x_9 cvclZero) 0)) (flet ($cvcl_0 (< (- x_32 x_33) 0)) (flet ($cvcl_1 (if_then_else $cvcl_0 (< (- x_32 x_34) 0) (< (- x_33 x_34) 0))) (flet ($cvcl_37 (= (- x_48 x_34) 0)) (flet ($cvcl_16 (= (- x_47 x_33) 0)) (flet ($cvcl_18 (= (- x_46 x_32) 0)) (flet ($cvcl_2 (= (- x_41 x_27) 0)) (flet ($cvcl_19 (= (- x_38 cvclZero) 0)) (flet ($cvcl_4 (= (- x_36 x_34) 0)) (flet ($cvcl_5 (= (- x_27 cvclZero) 0)) (flet ($cvcl_6 (< (- x_36 x_48) 0)) (flet ($cvcl_20 (= (- x_38 cvclZero) 1)) (flet ($cvcl_23 (not $cvcl_5)) (flet ($cvcl_25 (= (- x_38 cvclZero) 2)) (flet ($cvcl_127 (= (- x_41 cvclZero) 1)) (flet ($cvcl_27 (= (- x_38 cvclZero) 3)) (flet ($cvcl_11 (= (- x_27 cvclZero) 1)) (flet ($cvcl_29 (= (- x_38 cvclZero) 4)) (flet ($cvcl_130 (not $cvcl_11)) (flet ($cvcl_34 (= (- x_38 cvclZero) 5)) (flet ($cvcl_36 (= (- x_41 cvclZero) 0)) (flet ($cvcl_22 (= (- x_36 x_33) 0)) (flet ($cvcl_24 (< (- x_36 x_47) 0)) (flet ($cvcl_128 (= (- x_41 cvclZero) 2)) (flet ($cvcl_31 (= (- x_27 cvclZero) 2)) (flet ($cvcl_131 (not $cvcl_31)) (flet ($cvcl_39 (= (- x_36 x_32) 0)) (flet ($cvcl_40 (< (- x_36 x_46) 0)) (flet ($cvcl_129 (= (- x_41 cvclZero) 3)) (flet ($cvcl_44 (= (- x_27 cvclZero) 3)) (flet ($cvcl_132 (not $cvcl_44)) (flet ($cvcl_48 (< (- x_18 x_19) 0)) (flet ($cvcl_49 (if_then_else $cvcl_48 (< (- x_18 x_20) 0) (< (- x_19 x_20) 0))) (flet ($cvcl_78 (= (- x_34 x_20) 0)) (flet ($cvcl_61 (= (- x_33 x_19) 0)) (flet ($cvcl_63 (= (- x_32 x_18) 0)) (flet ($cvcl_50 (= (- x_27 x_13) 0)) (flet ($cvcl_64 (= (- x_24 cvclZero) 0)) (flet ($cvcl_52 (= (- x_22 x_20) 0)) (flet ($cvcl_53 (= (- x_13 cvclZero) 0)) (flet ($cvcl_54 (< (- x_22 x_34) 0)) (flet ($cvcl_65 (= (- x_24 cvclZero) 1)) (flet ($cvcl_68 (not $cvcl_53)) (flet ($cvcl_70 (= (- x_24 cvclZero) 2)) (flet ($cvcl_72 (= (- x_24 cvclZero) 3)) (flet ($cvcl_59 (= (- x_13 cvclZero) 1)) (flet ($cvcl_74 (= (- x_24 cvclZero) 4)) (flet ($cvcl_133 (not $cvcl_59)) (flet ($cvcl_77 (= (- x_24 cvclZero) 5)) (flet ($cvcl_67 (= (- x_22 x_19) 0)) (flet ($cvcl_69 (< (- x_22 x_33) 0)) (flet ($cvcl_76 (= (- x_13 cvclZero) 2)) (flet ($cvcl_134 (not $cvcl_76)) (flet ($cvcl_80 (= (- x_22 x_18) 0)) (flet ($cvcl_81 (< (- x_22 x_32) 0)) (flet ($cvcl_85 (= (- x_13 cvclZero) 3)) (flet ($cvcl_135 (not $cvcl_85)) (flet ($cvcl_86 (< (- x_8 x_7) 0)) (flet ($cvcl_90 (if_then_else $cvcl_86 (< (- x_8 x_6) 0) (< (- x_7 x_6) 0))) (flet ($cvcl_119 (= (- x_20 x_6) 0)) (flet ($cvcl_102 (= (- x_19 x_7) 0)) (flet ($cvcl_104 (= (- x_18 x_8) 0)) (flet ($cvcl_93 (= (- x_13 x_9) 0)) (flet ($cvcl_105 (= (- x_10 cvclZero) 0)) (flet ($cvcl_94 (= (- cvclZero x_6) 0)) (flet ($cvcl_95 (< (- cvclZero x_20) 0)) (flet ($cvcl_107 (= (- x_10 cvclZero) 1)) (flet ($cvcl_109 (not $cvcl_92)) (flet ($cvcl_111 (= (- x_10 cvclZero) 2)) (flet ($cvcl_113 (= (- x_10 cvclZero) 3)) (flet ($cvcl_100 (= (- x_9 cvclZero) 1)) (flet ($cvcl_115 (= (- x_10 cvclZero) 4)) (flet ($cvcl_136 (not $cvcl_100)) (flet ($cvcl_118 (= (- x_10 cvclZero) 5)) (flet ($cvcl_108 (= (- cvclZero x_7) 0)) (flet ($cvcl_110 (< (- cvclZero x_19) 0)) (flet ($cvcl_117 (= (- x_9 cvclZero) 2)) (flet ($cvcl_137 (not $cvcl_117)) (flet ($cvcl_121 (= (- cvclZero x_8) 0)) (flet ($cvcl_122 (< (- cvclZero x_18) 0)) (flet ($cvcl_126 (= (- x_9 cvclZero) 3)) (flet ($cvcl_138 (not $cvcl_126)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (< (- x_9 cvclZero) 0)) (<= (- x_9 cvclZero) 3)) (not (< (- x_13 cvclZero) 0))) (<= (- x_13 cvclZero) 3)) (not (< (- x_27 cvclZero) 0))) (<= (- x_27 cvclZero) 3)) (not (< (- x_41 cvclZero) 0))) (<= (- x_41 cvclZero) 3)) $cvcl_91) $cvcl_106) $cvcl_120) $cvcl_89) $cvcl_88) $cvcl_87) $cvcl_92) (or (and (and (and (and (and (and (and (and (and (= (- x_49 cvclZero) 0) (if_then_else $cvcl_1 (if_then_else $cvcl_0 (< (- x_36 x_32) 0) (< (- x_36 x_33) 0)) (< (- x_36 x_34) 0))) (if_then_else $cvcl_1 (if_then_else $cvcl_0 (= (- x_50 x_32) 0) (= (- x_50 x_33) 0)) (= (- x_50 x_34) 0))) $cvcl_7) $cvcl_15) $cvcl_17) $cvcl_37) $cvcl_16) $cvcl_18) $cvcl_2)  (and (and (= (- x_49 cvclZero) 1) (or (or (and (and (and (and (and (= (- x_51 cvclZero) 1) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_19 $cvcl_3) $cvcl_4) $cvcl_5) x_39) $cvcl_13) $cvcl_6) (<= (- x_48 x_36) 2)) $cvcl_2)  (and (and (and (and (and (and $cvcl_20 $cvcl_3) $cvcl_4) $cvcl_23) $cvcl_6) $cvcl_2) $cvcl_7) )  (and (and (and (and (and (and (and $cvcl_25 x_25) $cvcl_8) $cvcl_4) $cvcl_12) x_40) $cvcl_127) (<= (- x_36 x_48) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_27 $cvcl_10) $cvcl_4) $cvcl_11) x_39) x_40) $cvcl_6) $cvcl_2) )  (and (and (and (and (and (and $cvcl_29 $cvcl_10) $cvcl_4) $cvcl_130) $cvcl_14) $cvcl_6) $cvcl_2) )  (and (and (and (and (and (and $cvcl_34 x_25) x_26) $cvcl_4) $cvcl_14) $cvcl_36) $cvcl_6) )) $cvcl_15) $cvcl_16) $cvcl_17) $cvcl_18)  (and (and (and (and (and (= (- x_51 cvclZero) 2) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_19 $cvcl_21) $cvcl_22) $cvcl_5) x_44) $cvcl_33) $cvcl_24) (<= (- x_47 x_36) 2)) $cvcl_2)  (and (and (and (and (and (and $cvcl_20 $cvcl_21) $cvcl_22) $cvcl_23) $cvcl_24) $cvcl_2) $cvcl_15) )  (and (and (and (and (and (and (and $cvcl_25 x_30) $cvcl_26) $cvcl_22) $cvcl_32) x_45) $cvcl_128) (<= (- x_36 x_47) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_27 $cvcl_30) $cvcl_22) $cvcl_31) x_44) x_45) $cvcl_24) $cvcl_2) )  (and (and (and (and (and (and $cvcl_29 $cvcl_30) $cvcl_22) $cvcl_131) $cvcl_35) $cvcl_24) $cvcl_2) )  (and (and (and (and (and (and $cvcl_34 x_30) x_31) $cvcl_22) $cvcl_35) $cvcl_36) $cvcl_24) )) $cvcl_7) $cvcl_37) $cvcl_17) $cvcl_18) )  (and (and (and (and (and (= (- x_51 cvclZero) 3) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_19 $cvcl_38) $cvcl_39) $cvcl_5) x_42) $cvcl_46) $cvcl_40) (<= (- x_46 x_36) 2)) $cvcl_2)  (and (and (and (and (and (and $cvcl_20 $cvcl_38) $cvcl_39) $cvcl_23) $cvcl_40) $cvcl_2) $cvcl_17) )  (and (and (and (and (and (and (and $cvcl_25 x_28) $cvcl_41) $cvcl_39) $cvcl_45) x_43) $cvcl_129) (<= (- x_36 x_46) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_27 $cvcl_43) $cvcl_39) $cvcl_44) x_42) x_43) $cvcl_40) $cvcl_2) )  (and (and (and (and (and (and $cvcl_29 $cvcl_43) $cvcl_39) $cvcl_132) $cvcl_47) $cvcl_40) $cvcl_2) )  (and (and (and (and (and (and $cvcl_34 x_28) x_29) $cvcl_39) $cvcl_47) $cvcl_36) $cvcl_40) )) $cvcl_7) $cvcl_37) $cvcl_15) $cvcl_16) )) (= (- x_50 x_36) 0)) )) (or (and (and (and (and (and (and (and (and (and (= (- x_35 cvclZero) 0) (if_then_else $cvcl_49 (if_then_else $cvcl_48 (< (- x_22 x_18) 0) (< (- x_22 x_19) 0)) (< (- x_22 x_20) 0))) (if_then_else $cvcl_49 (if_then_else $cvcl_48 (= (- x_36 x_18) 0) (= (- x_36 x_19) 0)) (= (- x_36 x_20) 0))) $cvcl_55) $cvcl_60) $cvcl_62) $cvcl_78) $cvcl_61) $cvcl_63) $cvcl_50)  (and (and (= (- x_35 cvclZero) 1) (or (or (and (and (and (and (and (= (- x_37 cvclZero) 1) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_64 $cvcl_51) $cvcl_52) $cvcl_53) x_25) $cvcl_8) $cvcl_54) (<= (- x_34 x_22) 2)) $cvcl_50)  (and (and (and (and (and (and $cvcl_65 $cvcl_51) $cvcl_52) $cvcl_68) $cvcl_54) $cvcl_50) $cvcl_55) )  (and (and (and (and (and (and (and $cvcl_70 x_11) $cvcl_56) $cvcl_52) $cvcl_9) x_26) $cvcl_11) (<= (- x_22 x_34) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_72 $cvcl_58) $cvcl_52) $cvcl_59) x_25) x_26) $cvcl_54) $cvcl_50) )  (and (and (and (and (and (and $cvcl_74 $cvcl_58) $cvcl_52) $cvcl_133) $cvcl_3) $cvcl_54) $cvcl_50) )  (and (and (and (and (and (and $cvcl_77 x_11) x_12) $cvcl_52) $cvcl_3) $cvcl_5) $cvcl_54) )) $cvcl_60) $cvcl_61) $cvcl_62) $cvcl_63)  (and (and (and (and (and (= (- x_37 cvclZero) 2) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_64 $cvcl_66) $cvcl_67) $cvcl_53) x_30) $cvcl_26) $cvcl_69) (<= (- x_33 x_22) 2)) $cvcl_50)  (and (and (and (and (and (and $cvcl_65 $cvcl_66) $cvcl_67) $cvcl_68) $cvcl_69) $cvcl_50) $cvcl_60) )  (and (and (and (and (and (and (and $cvcl_70 x_16) $cvcl_71) $cvcl_67) $cvcl_28) x_31) $cvcl_31) (<= (- x_22 x_33) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_72 $cvcl_75) $cvcl_67) $cvcl_76) x_30) x_31) $cvcl_69) $cvcl_50) )  (and (and (and (and (and (and $cvcl_74 $cvcl_75) $cvcl_67) $cvcl_134) $cvcl_21) $cvcl_69) $cvcl_50) )  (and (and (and (and (and (and $cvcl_77 x_16) x_17) $cvcl_67) $cvcl_21) $cvcl_5) $cvcl_69) )) $cvcl_55) $cvcl_78) $cvcl_62) $cvcl_63) )  (and (and (and (and (and (= (- x_37 cvclZero) 3) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_64 $cvcl_79) $cvcl_80) $cvcl_53) x_28) $cvcl_41) $cvcl_81) (<= (- x_32 x_22) 2)) $cvcl_50)  (and (and (and (and (and (and $cvcl_65 $cvcl_79) $cvcl_80) $cvcl_68) $cvcl_81) $cvcl_50) $cvcl_62) )  (and (and (and (and (and (and (and $cvcl_70 x_14) $cvcl_82) $cvcl_80) $cvcl_42) x_29) $cvcl_44) (<= (- x_22 x_32) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_72 $cvcl_84) $cvcl_80) $cvcl_85) x_28) x_29) $cvcl_81) $cvcl_50) )  (and (and (and (and (and (and $cvcl_74 $cvcl_84) $cvcl_80) $cvcl_135) $cvcl_38) $cvcl_81) $cvcl_50) )  (and (and (and (and (and (and $cvcl_77 x_14) x_15) $cvcl_80) $cvcl_38) $cvcl_5) $cvcl_81) )) $cvcl_55) $cvcl_78) $cvcl_60) $cvcl_61) )) (= (- x_36 x_22) 0)) )) (or (and (and (and (and (and (and (and (and (and (= (- x_21 cvclZero) 0) (if_then_else $cvcl_90 (if_then_else $cvcl_86 $cvcl_87 $cvcl_88) $cvcl_89)) (if_then_else $cvcl_90 (if_then_else $cvcl_86 (= (- x_22 x_8) 0) (= (- x_22 x_7) 0)) (= (- x_22 x_6) 0))) $cvcl_96) $cvcl_101) $cvcl_103) $cvcl_119) $cvcl_102) $cvcl_104) $cvcl_93)  (and (and (= (- x_21 cvclZero) 1) (or (or (and (and (and (and (and (= (- x_23 cvclZero) 1) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_105 $cvcl_91) $cvcl_94) $cvcl_92) x_11) $cvcl_56) $cvcl_95) (<= (- x_20 cvclZero) 2)) $cvcl_93)  (and (and (and (and (and (and $cvcl_107 $cvcl_91) $cvcl_94) $cvcl_109) $cvcl_95) $cvcl_93) $cvcl_96) )  (and (and (and (and (and (and (and $cvcl_111 x_0) $cvcl_97) $cvcl_94) $cvcl_57) x_12) $cvcl_59) (<= (- cvclZero x_20) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_113 $cvcl_99) $cvcl_94) $cvcl_100) x_11) x_12) $cvcl_95) $cvcl_93) )  (and (and (and (and (and (and $cvcl_115 $cvcl_99) $cvcl_94) $cvcl_136) $cvcl_51) $cvcl_95) $cvcl_93) )  (and (and (and (and (and (and $cvcl_118 x_0) x_1) $cvcl_94) $cvcl_51) $cvcl_53) $cvcl_95) )) $cvcl_101) $cvcl_102) $cvcl_103) $cvcl_104)  (and (and (and (and (and (= (- x_23 cvclZero) 2) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_105 $cvcl_106) $cvcl_108) $cvcl_92) x_16) $cvcl_71) $cvcl_110) (<= (- x_19 cvclZero) 2)) $cvcl_93)  (and (and (and (and (and (and $cvcl_107 $cvcl_106) $cvcl_108) $cvcl_109) $cvcl_110) $cvcl_93) $cvcl_101) )  (and (and (and (and (and (and (and $cvcl_111 x_2) $cvcl_112) $cvcl_108) $cvcl_73) x_17) $cvcl_76) (<= (- cvclZero x_19) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_113 $cvcl_116) $cvcl_108) $cvcl_117) x_16) x_17) $cvcl_110) $cvcl_93) )  (and (and (and (and (and (and $cvcl_115 $cvcl_116) $cvcl_108) $cvcl_137) $cvcl_66) $cvcl_110) $cvcl_93) )  (and (and (and (and (and (and $cvcl_118 x_2) x_3) $cvcl_108) $cvcl_66) $cvcl_53) $cvcl_110) )) $cvcl_96) $cvcl_119) $cvcl_103) $cvcl_104) )  (and (and (and (and (and (= (- x_23 cvclZero) 3) (or (or (or (or (or (and (and (and (and (and (and (and (and $cvcl_105 $cvcl_120) $cvcl_121) $cvcl_92) x_14) $cvcl_82) $cvcl_122) (<= (- x_18 cvclZero) 2)) $cvcl_93)  (and (and (and (and (and (and $cvcl_107 $cvcl_120) $cvcl_121) $cvcl_109) $cvcl_122) $cvcl_93) $cvcl_103) )  (and (and (and (and (and (and (and $cvcl_111 x_4) $cvcl_123) $cvcl_121) $cvcl_83) x_15) $cvcl_85) (<= (- cvclZero x_18) (~ 4))) )  (and (and (and (and (and (and (and $cvcl_113 $cvcl_125) $cvcl_121) $cvcl_126) x_14) x_15) $cvcl_122) $cvcl_93) )  (and (and (and (and (and (and $cvcl_115 $cvcl_125) $cvcl_121) $cvcl_138) $cvcl_79) $cvcl_122) $cvcl_93) )  (and (and (and (and (and (and $cvcl_118 x_4) x_5) $cvcl_121) $cvcl_79) $cvcl_53) $cvcl_122) )) $cvcl_96) $cvcl_119) $cvcl_101) $cvcl_102) )) (= (- x_22 cvclZero) 0)) )) (or (or (or (or (or (or (or (or (or (or (or (and (and x_39 x_40) (not $cvcl_127))  (and (and x_44 x_45) (not $cvcl_128)) )  (and (and x_42 x_43) (not $cvcl_129)) )  (and (and x_25 x_26) $cvcl_130) )  (and (and x_30 x_31) $cvcl_131) )  (and (and x_28 x_29) $cvcl_132) )  (and (and x_11 x_12) $cvcl_133) )  (and (and x_16 x_17) $cvcl_134) )  (and (and x_14 x_15) $cvcl_135) )  (and (and x_0 x_1) $cvcl_136) )  (and (and x_2 x_3) $cvcl_137) )  (and (and x_4 x_5) $cvcl_138) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))");
    415        sammy.execute("add_assertion");
    416
    417        sammy.stop_prover();
    418        long endTime = java.lang.System.currentTimeMillis();
    419
    420        long totalTime = endTime - startTime;
    421
    422        System.out.println("Time spend : "+totalTime+" milliseconds");
    423
    424      }
    425
    426    }