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 /*@non_null*/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 /*@non_null*/ProverResponse set_prover_resource_flags(/*@non_null*/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 /*@non_null*/ProverResponse signature(/*@non_null*/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 /*@non_null*/ProverResponse declare_axiom(/*@non_null*/Formula formula) {
184
185 /*
186 * Is an axiom a declaration of a predicate ?
187 */
188
189 return null;
190 }
191
192 public /*@non_null*/ProverResponse make_assumption(/*@non_null*/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 /*@non_null*/ProverResponse retract_assumption(int count) {
203
204 /*
205 * == 'backtrack' in sammy's interface ?
206 */
207
208 return null;
209 }
210
211 public /*@non_null*/ProverResponse is_valid(/*@non_null*/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 /*@non_null*/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 }