Hi Daniel, Sorry for the slow response.
On Thu, Apr 08, 2010 at 06:45:58PM -0700, Daniel Dunbar wrote: > Um, ignore this question, since you obviously attached a patch for > exactly this! :) > > It would be cool if we could tweak the patch to use the internal STP > if --with-stp isn't specified, then we could go ahead and put it in > trunk. I finally got round to doing this -- please see the attached patch. I'll commit this if OK. > > It should be possible for us to support both options, > > initially, which is nice for comparing the performance of them side by > > side. Do you have any hard numbers that show that the new STP is > > better, or by how much? On one particular benchmark, we experienced query runtimes of several hours with the old STP, and approx 12 minutes with the new STP (dual 2.0GHz machine, using CryptoMiniSat 2). I've attached a copy of the problematic query. If you would like a copy of the benchmark itself (it has a dependency on another library) I can try to do that. Thanks, -- Peter -------------- next part -------------- __tmpInt8 : BITVECTOR(8); __tmpInt16 : BITVECTOR(16); __tmpInt32 : BITVECTOR(32); __tmpInt64 : BITVECTOR(64); arr1_0x1b03690 : ARRAY BITVECTOR(32) OF BITVECTOR(8); %---------------------------------------------------- ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); ASSERT( TRUE ); %---------------------------------------------------- QUERY( (LET let_k_0 = (arr1_0x1b03690[0hex00000047] @ (arr1_0x1b03690[0hex00000046] @ (arr1_0x1b03690[0hex00000045] @ (arr1_0x1b03690[0hex00000044] @ (arr1_0x1b03690[0hex00000043] @ (arr1_0x1b03690[0hex00000042] @ (arr1_0x1b03690[0hex00000041] @ arr1_0x1b03690[0hex00000040]) ) ) ) ) ) ) , let_k_1 = SBVDIV(64, let_k_0, 0hex000000000000B665) , let_k_2 = BVSUB(64, let_k_0, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVSUB(64, BVPLUS(64, (let_k_1[48:0] @ 0bin000000000000000) , (let_k_1[49:0] @ 0bin00000000000000) ) , (let_k_1[52:0] @ 0bin00000000000) ) , (let_k_1[54:0] @ 0bin000000000) ) , (let_k_1[56:0] @ 0bin0000000) ) , (let_k_1[58:0] @ 0bin00000) ) , (let_k_1[61:0] @ 0bin00) ) , let_k_1) ) , let_k_3 = (let_k_1[48:0] @ 0bin000000000000000) , let_k_4 = (let_k_1[58:0] @ 0bin00000) , let_k_5 = (let_k_1[61:0] @ 0bin00) , let_k_6 = BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_2[48:0] @ 0bin000000000000000) , (let_k_2[49:0] @ 0bin00000000000000) ) , (let_k_2[51:0] @ 0hex000) ) , (let_k_2[53:0] @ 0bin0000000000) ) , (let_k_2[56:0] @ 0bin0000000) ) , (let_k_2[58:0] @ 0bin00000) ) , (let_k_2[60:0] @ 0bin000) ) , let_k_2) , BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, let_k_3, (let_k_1[50:0] @ 0bin0000000000000) ) , (let_k_1[53:0] @ 0bin0000000000) ) , (let_k_1[55:0] @ 0hex00) ) , let_k_4) , let_k_5) ) , let_k_7 = IF(SBVLT(let_k_6,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFFFF, let_k_6) ELSE let_k_6 ENDIF, let_k_8 = SBVDIV(64, let_k_7, 0hex000000000000B665) , let_k_9 = BVSUB(64, let_k_7, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVSUB(64, BVPLUS(64, (let_k_8[48:0] @ 0bin000000000000000) , (let_k_8[49:0] @ 0bin00000000000000) ) , (let_k_8[52:0] @ 0bin00000000000) ) , (let_k_8[54:0] @ 0bin000000000) ) , (let_k_8[56:0] @ 0bin0000000) ) , (let_k_8[58:0] @ 0bin00000) ) , (let_k_8[61:0] @ 0bin00) ) , let_k_8) ) , let_k_10 = (let_k_8[48:0] @ 0bin000000000000000) , let_k_11 = (let_k_8[58:0] @ 0bin00000) , let_k_12 = (let_k_8[61:0] @ 0bin00) , let_k_13 = BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_9[48:0] @ 0bin000000000000000) , (let_k_9[49:0] @ 0bin00000000000000) ) , (let_k_9[51:0] @ 0hex000) ) , (let_k_9[53:0] @ 0bin0000000000) ) , (let_k_9[56:0] @ 0bin0000000) ) , (let_k_9[58:0] @ 0bin00000) ) , (let_k_9[60:0] @ 0bin000) ) , let_k_9) , BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, let_k_10, (let_k_8[50:0] @ 0bin0000000000000) ) , (let_k_8[53:0] @ 0bin0000000000) ) , (let_k_8[55:0] @ 0hex00) ) , let_k_11) , let_k_12) ) , let_k_14 = IF(SBVLT(let_k_13,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFFFF, let_k_13) ELSE let_k_13 ENDIF, let_k_15 = (arr1_0x1b03690[0hex0000004F] @ (arr1_0x1b03690[0hex0000004E] @ (arr1_0x1b03690[0hex0000004D] @ (arr1_0x1b03690[0hex0000004C] @ (arr1_0x1b03690[0hex0000004B] @ (arr1_0x1b03690[0hex0000004A] @ (arr1_0x1b03690[0hex00000049] @ arr1_0x1b03690[0hex00000048]) ) ) ) ) ) ) , let_k_16 = SBVDIV(64, let_k_15, 0hex0000000000002863) , let_k_17 = BVSUB(64, let_k_15, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, (let_k_16[50:0] @ 0bin0000000000000) , (let_k_16[52:0] @ 0bin00000000000) ) , (let_k_16[56:0] @ 0bin0000000) ) , (let_k_16[58:0] @ 0bin00000) ) , (let_k_16[61:0] @ 0bin00) ) , let_k_16) ) , let_k_18 = (let_k_16[56:0] @ 0bin0000000) , let_k_19 = (let_k_16[58:0] @ 0bin00000) , let_k_20 = BVSUB(64, BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_17[45:0] @ 0bin000000000000000000) , (let_k_17[47:0] @ 0hex0000) ) , (let_k_17[50:0] @ 0bin0000000000000) ) , (let_k_17[52:0] @ 0bin00000000000) ) , (let_k_17[53:0] @ 0bin0000000000) ) , (let_k_17[55:0] @ 0hex00) ) , (let_k_17[57:0] @ 0bin000000) ) , (let_k_17[58:0] @ 0bin00000) ) , (let_k_17[61:0] @ 0bin00) ) , let_k_17) , BVSUB(64, BVPLUS(64, BVSUB(64, BVSUB(64, (let_k_16[53:0] @ 0bin0000000000) , let_k_18) , let_k_19) , (let_k_16[60:0] @ 0bin000) ) , (let_k_16[62:0] @ 0bin0) ) ) , let_k_21 = IF(SBVLT(let_k_20,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFF97, let_k_20) ELSE let_k_20 ENDIF, let_k_22 = SBVDIV(64, let_k_21, 0hex0000000000002863) , let_k_23 = BVSUB(64, let_k_21, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, (let_k_22[50:0] @ 0bin0000000000000) , (let_k_22[52:0] @ 0bin00000000000) ) , (let_k_22[56:0] @ 0bin0000000) ) , (let_k_22[58:0] @ 0bin00000) ) , (let_k_22[61:0] @ 0bin00) ) , let_k_22) ) , let_k_24 = (let_k_22[56:0] @ 0bin0000000) , let_k_25 = (let_k_22[58:0] @ 0bin00000) , let_k_26 = BVSUB(64, BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_23[45:0] @ 0bin000000000000000000) , (let_k_23[47:0] @ 0hex0000) ) , (let_k_23[50:0] @ 0bin0000000000000) ) , (let_k_23[52:0] @ 0bin00000000000) ) , (let_k_23[53:0] @ 0bin0000000000) ) , (let_k_23[55:0] @ 0hex00) ) , (let_k_23[57:0] @ 0bin000000) ) , (let_k_23[58:0] @ 0bin00000) ) , (let_k_23[61:0] @ 0bin00) ) , let_k_23) , BVSUB(64, BVPLUS(64, BVSUB(64, BVSUB(64, (let_k_22[53:0] @ 0bin0000000000) , let_k_24) , let_k_25) , (let_k_22[60:0] @ 0bin000) ) , (let_k_22[62:0] @ 0bin0) ) ) , let_k_27 = IF(SBVLT(let_k_26,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFF97, let_k_26) ELSE let_k_26 ENDIF, let_k_28 = (arr1_0x1b03690[0hex00000057] @ (arr1_0x1b03690[0hex00000056] @ (arr1_0x1b03690[0hex00000055] @ (arr1_0x1b03690[0hex00000054] @ (arr1_0x1b03690[0hex00000053] @ (arr1_0x1b03690[0hex00000052] @ (arr1_0x1b03690[0hex00000051] @ arr1_0x1b03690[0hex00000050]) ) ) ) ) ) ) , let_k_29 = SBVDIV(64, let_k_28, 0hex0000000000003C8B) , let_k_30 = BVSUB(64, let_k_28, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_29[49:0] @ 0bin00000000000000) , (let_k_29[53:0] @ 0bin0000000000) ) , (let_k_29[56:0] @ 0bin0000000) ) , (let_k_29[60:0] @ 0bin000) ) , (let_k_29[61:0] @ 0bin00) ) , let_k_29) ) , let_k_31 = (let_k_29[56:0] @ 0bin0000000) , let_k_32 = (let_k_29[60:0] @ 0bin000) , let_k_33 = (let_k_29[61:0] @ 0bin00) , let_k_34 = BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_30[46:0] @ 0bin00000000000000000) , (let_k_30[50:0] @ 0bin0000000000000) ) , (let_k_30[53:0] @ 0bin0000000000) ) , (let_k_30[55:0] @ 0hex00) ) , (let_k_30[57:0] @ 0bin000000) ) , (let_k_30[61:0] @ 0bin00) ) , BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_29[51:0] @ 0hex000) , let_k_31) , let_k_32) , let_k_33) , let_k_29) ) , let_k_35 = SBVDIV(64, let_k_34, 0hex0000000000003C8B) , let_k_36 = BVSUB(64, let_k_34, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_35[49:0] @ 0bin00000000000000) , (let_k_35[53:0] @ 0bin0000000000) ) , (let_k_35[56:0] @ 0bin0000000) ) , (let_k_35[60:0] @ 0bin000) ) , (let_k_35[61:0] @ 0bin00) ) , let_k_35) ) , let_k_37 = (let_k_35[56:0] @ 0bin0000000) , let_k_38 = (let_k_35[60:0] @ 0bin000) , let_k_39 = (let_k_35[61:0] @ 0bin00) , let_k_40 = BVSUB(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_36[46:0] @ 0bin00000000000000000) , (let_k_36[50:0] @ 0bin0000000000000) ) , (let_k_36[53:0] @ 0bin0000000000) ) , (let_k_36[55:0] @ 0hex00) ) , (let_k_36[57:0] @ 0bin000000) ) , (let_k_36[61:0] @ 0bin00) ) , BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_35[51:0] @ 0hex000) , let_k_37) , let_k_38) , let_k_39) , let_k_35) ) , let_k_41 = (arr1_0x1b03690[0hex0000005F] @ (arr1_0x1b03690[0hex0000005E] @ (arr1_0x1b03690[0hex0000005D] @ (arr1_0x1b03690[0hex0000005C] @ (arr1_0x1b03690[0hex0000005B] @ (arr1_0x1b03690[0hex0000005A] @ (arr1_0x1b03690[0hex00000059] @ arr1_0x1b03690[0hex00000058]) ) ) ) ) ) ) , let_k_42 = SBVDIV(64, let_k_41, 0hex000000000000A8D2) , let_k_43 = BVSUB(64, let_k_41, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, (let_k_42[48:0] @ 0bin000000000000000) , (let_k_42[50:0] @ 0bin0000000000000) ) , (let_k_42[52:0] @ 0bin00000000000) ) , (let_k_42[55:0] @ 0hex00) ) , (let_k_42[57:0] @ 0bin000000) ) , (let_k_42[59:0] @ 0hex0) ) , (let_k_42[62:0] @ 0bin0) ) ) , let_k_44 = (let_k_42[50:0] @ 0bin0000000000000) , let_k_45 = (let_k_42[57:0] @ 0bin000000) , let_k_46 = BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_43[47:0] @ 0hex0000) , (let_k_43[49:0] @ 0bin00000000000000) ) , (let_k_43[54:0] @ 0bin000000000) ) , (let_k_43[58:0] @ 0bin00000) ) , (let_k_43[60:0] @ 0bin000) ) , let_k_43) , BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_42[49:0] @ 0bin00000000000000) , let_k_44) , (let_k_42[54:0] @ 0bin000000000) ) , let_k_45) , (let_k_42[60:0] @ 0bin000) ) , let_k_42) ) , let_k_47 = IF(SBVLT(let_k_46,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFEBB, let_k_46) ELSE let_k_46 ENDIF, let_k_48 = SBVDIV(64, let_k_47, 0hex000000000000A8D2) , let_k_49 = BVSUB(64, let_k_47, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, (let_k_48[48:0] @ 0bin000000000000000) , (let_k_48[50:0] @ 0bin0000000000000) ) , (let_k_48[52:0] @ 0bin00000000000) ) , (let_k_48[55:0] @ 0hex00) ) , (let_k_48[57:0] @ 0bin000000) ) , (let_k_48[59:0] @ 0hex0) ) , (let_k_48[62:0] @ 0bin0) ) ) , let_k_50 = (let_k_48[50:0] @ 0bin0000000000000) , let_k_51 = (let_k_48[57:0] @ 0bin000000) , let_k_52 = BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, (let_k_49[47:0] @ 0hex0000) , (let_k_49[49:0] @ 0bin00000000000000) ) , (let_k_49[54:0] @ 0bin000000000) ) , (let_k_49[58:0] @ 0bin00000) ) , (let_k_49[60:0] @ 0bin000) ) , let_k_49) , BVPLUS(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_48[49:0] @ 0bin00000000000000) , let_k_50) , (let_k_48[54:0] @ 0bin000000000) ) , let_k_51) , (let_k_48[60:0] @ 0bin000) ) , let_k_48) ) , let_k_53 = IF(SBVLT(let_k_52,0hex0000000000000000) ) THEN BVPLUS(64, 0hex000000007FFFFEBB, let_k_52) ELSE let_k_52 ENDIF IN (((let_k_7 = SBVMOD(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, (let_k_14[33:0] @ 0bin000000000000000000000000000000) , (let_k_14[35:0] @ 0hex0000000) ) , (let_k_14[37:0] @ 0bin00000000000000000000000000) ) , (let_k_14[38:0] @ 0bin0000000000000000000000000) ) , (let_k_14[42:0] @ 0bin000000000000000000000) ) , (let_k_14[44:0] @ 0bin0000000000000000000) ) , (let_k_14[47:0] @ 0hex0000) ) , (let_k_14[50:0] @ 0bin0000000000000) ) , (let_k_14[52:0] @ 0bin00000000000) ) , (let_k_14[53:0] @ 0bin0000000000) ) , (let_k_14[55:0] @ 0hex00) ) , (let_k_14[59:0] @ 0hex0) ) , 0hex000000007FFFFFFF) AND let_k_21 = SBVMOD(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVSUB(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, (let_k_27[33:0] @ 0bin000000000000000000000000000000) , (let_k_27[35:0] @ 0hex0000000) ) , (let_k_27[36:0] @ 0bin000000000000000000000000000) ) , (let_k_27[39:0] @ 0hex000000) ) , (let_k_27[41:0] @ 0bin0000000000000000000000) ) , (let_k_27[47:0] @ 0hex0000) ) , (let_k_27[52:0] @ 0bin00000000000) ) , (let_k_27[60:0] @ 0bin000) ) , (let_k_27[62:0] @ 0bin0) ) , 0hex000000007FFFFF97) ) AND let_k_34 = SBVMOD(64, BVPLUS(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVSUB(64, (let_k_40[34:0] @ 0bin00000000000000000000000000000) , (let_k_40[38:0] @ 0bin0000000000000000000000000) ) , (let_k_40[41:0] @ 0bin0000000000000000000000) ) , (let_k_40[44:0] @ 0bin0000000000000000000) ) , (let_k_40[46:0] @ 0bin00000000000000000) ) , (let_k_40[49:0] @ 0bin00000000000000) ) , (let_k_40[51:0] @ 0hex000) ) , (let_k_40[53:0] @ 0bin0000000000) ) , (let_k_40[56:0] @ 0bin0000000) ) , (let_k_40[58:0] @ 0bin00000) ) , (let_k_40[61:0] @ 0bin00) ) , let_k_40) , 0hex000000007FFFFF1F) ) AND let_k_47 = SBVMOD(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, BVPLUS(64, BVSUB(64, BVPLUS(64, (let_k_53[34:0] @ 0bin00000000000000000000000000000) , (let_k_53[36:0] @ 0bin000000000000000000000000000) ) , (let_k_53[39:0] @ 0hex000000) ) , (let_k_53[41:0] @ 0bin0000000000000000000000) ) , (let_k_53[42:0] @ 0bin000000000000000000000) ) , (let_k_53[45:0] @ 0bin000000000000000000) ) , (let_k_53[47:0] @ 0hex0000) ) , (let_k_53[49:0] @ 0bin00000000000000) ) , (let_k_53[53:0] @ 0bin0000000000) ) , (let_k_53[58:0] @ 0bin00000) ) , (let_k_53[59:0] @ 0hex0) ) , (let_k_53[61:0] @ 0bin00) ) , 0hex000000007FFFFEBB) )) ); -------------- next part -------------- A non-text attachment was scrubbed... Name: 0001-Add-option-to-use-an-external-version-of-STP.patch Type: text/x-diff Size: 0 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100709/c6f8c2db/attachment-0001.bin
