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 }