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    }