From 11c1fba70098cc72c59b2d335249332790287c20 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 19 Jun 2020 15:10:27 -0300 Subject: [PATCH] Always rewrite boolean ITEs with constant then/else-branches (#4619) Also adds better tracing and rewrites for binary AND/OR to account for reductions from constant ITEs. An evaluation of master vs this commit, with 600s, no options, shows the impact of this commit to be negligible and mostly restricted to QF_LIA. Below there is a summary and a list of the unique solves. ``` Benchmark | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | QF_ALIA | ok 125 126 1 0 0 2382.6 5410.8 0 | ok 125 126 1 0 0 2322.1 5211.8 0 | QF_AX | ok 549 551 2 0 0 2381.4 2533.1 0 | ok 549 551 2 0 0 2400.8 2676.4 0 | QF_IDL | ok 1682 2193 511 0 0 399395.4 491490.3 3 | ok 1682 2193 511 0 0 400813.9 491129.9 3 | QF_LIA | ok 4419 6947 2521 7 0 1774140.9 2782838.1 27 | ok 4409 6947 2531 7 0 1775886.7 2785165.7 17 | QF_LIRA | ok 5 7 2 0 0 1209.9 3626.9 0 | ok 5 7 2 0 0 1209.5 3707.2 0 | QF_LRA | ok 1517 1648 131 0 0 134215.1 170443.1 3 | ok 1516 1648 132 0 0 134819.6 169942.7 2 | QF_RDL | ok 210 255 45 0 0 32896.0 23261.0 0 | ok 210 255 45 0 0 32902.7 23312.5 0 | QF_UF | ok 7444 7457 13 0 0 16156.4 74432.9 0 | ok 7444 7457 13 0 0 16043.8 75067.6 0 | __totals | ok 15951 19184 3226 7 0 2362777.7 3554036.2 33 | ok 15940 19184 3237 7 0 2366399.2 3556213.8 22 |``` ``` DIRECTORY | master | branch | Benchmark | Stat RES Exit Cpu[s] Mem[MB] | Stat RES Exit Cpu[s] Mem[MB] | non_incremental_QF_IDL/asp-GraphPartitioning-rand_21_150_1235870252_0_k=3_v=10_e=20_unsat.gph.smt2 | to - 2 600.1 246.4 | ok 20 0 596.71 245.9 | non_incremental_QF_IDL/asp-SchurNumbers-15.13.schur.lp.smt2 | ok 10 0 533.64 243.8 | to - 2 600.07 246.8 | non_incremental_QF_IDL/job_shop-jobshop38-2-19-19-4-4-12.smt2 | ok 10 0 586.13 221.5 | to - 2 600.09 216.8 | non_incremental_QF_IDL/queens_bench-n_queen-queen82-1.smt2 | to - 2 600.01 197.8 | ok 10 0 570.36 198.9 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_3_mkspan871.smt2 | to - 2 600.1 128.0 | ok 10 0 586.8 127.8 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_9_mkspan930.smt2 | ok 10 0 575.55 124.4 | to - 2 600.07 122.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1007795.smt2 | ok 10 0 334.96 386.7 | to - 2 600.02 335.5 | non_incremental_QF_LIA/arctic-matrix-constraint-1008025.smt2 | ok 10 0 180.57 384.6 | to - 2 600.02 338.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1107622.smt2 | ok 10 0 310.68 349.2 | to - 2 600.01 341.3 | non_incremental_QF_LIA/arctic-matrix-constraint-1275621.smt2 | ok 10 0 5.59 232.0 | to - 2 600.04 407.4 | non_incremental_QF_LIA/arctic-matrix-constraint-1360077.smt2 | ok 10 0 422.4 667.7 | to - 11 591.94 663.2 | non_incremental_QF_LIA/arctic-matrix-constraint-1765766.smt2 | to - 11 598.02 656.8 | ok 10 0 62.5 669.8 | non_incremental_QF_LIA/arctic-matrix-constraint-391798.smt2 | ok 10 0 9.0 119.3 | to - 2 600.08 131.8 | non_incremental_QF_LIA/arctic-matrix-constraint-481231.smt2 | ok 10 0 402.37 220.9 | to - 2 600.09 199.6 | non_incremental_QF_LIA/arctic-matrix-constraint-689472.smt2 | ok 10 0 28.51 155.9 | to - 2 600.06 215.1 | non_incremental_QF_LIA/arctic-matrix-constraint-864173.smt2 | ok 10 0 125.59 326.3 | to - 11 597.87 348.8 | non_incremental_QF_LIA/arctic-matrix-constraint-901628.smt2 | to - 2 600.04 225.5 | ok 10 0 391.31 228.3 | non_incremental_QF_LIA/arctic-matrix-constraint-916576.smt2 | to - 2 600.01 244.4 | ok 10 0 432.4 246.9 | non_incremental_QF_LIA/arctic-matrix-constraint-928134.smt2 | ok 10 0 447.55 222.7 | to - 2 600.06 264.7 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-42.smt2 | ok 10 0 579.39 414.9 | to - 2 600.07 417.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-47.smt2 | to - 2 600.02 604.2 | ok 10 0 594.54 603.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-45-43.smt2 | to - 2 600.05 628.1 | ok 10 0 588.25 627.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-46-47.smt2 | ok 10 0 589.88 570.0 | to - 2 600.09 566.9 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-47.smt2 | ok 20 0 590.89 599.9 | to - 2 600.01 598.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-50.smt2 | ok 10 0 594.72 804.7 | to - 11 593.13 843.5 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-17-47.smt2 | ok 20 0 593.29 524.2 | to - 2 600.08 522.8 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-20-48.smt2 | to - 2 600.02 562.5 | ok 10 0 594.33 560.3 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-5-46.smt2 | to - 2 600.09 492.9 | ok 10 0 576.02 491.9 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-52-47.smt2 | to - 2 600.02 532.2 | ok 20 0 592.3 533.4 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-53-48.smt2 | ok 20 0 599.82 729.4 | to - 2 600.02 742.1 | non_incremental_QF_LIA/nec-smt-large-getoption_user-prp-41-47.smt2 | to - 11 589.46 1377.2 | ok 20 0 580.82 1380.1 | non_incremental_QF_LIA/nec-smt-large-user_is_in_group-prp-23-46.smt2 | to - 2 600.08 633.5 | ok 10 0 576.07 634.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1015084.smt2 | ok 10 0 408.08 374.5 | to - 2 600.01 336.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1206577.smt2 | ok 10 0 361.82 375.4 | to - 11 593.45 288.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1268455.smt2 | ok 10 0 270.87 654.3 | to - 2 600.08 670.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1270163.smt2 | to - 2 600.02 410.4 | ok 10 0 425.02 420.6 | non_incremental_QF_LIA/tropical-matrix-constraint-1270998.smt2 | ok 10 0 349.91 384.6 | to - 2 600.01 417.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1290859.smt2 | to - 2 600.1 365.9 | ok 10 0 117.77 270.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1361831.smt2 | to - 2 600.07 431.0 | ok 10 0 421.55 686.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1452366.smt2 | to - 2 600.04 439.4 | ok 10 0 87.42 451.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1791895.smt2 | to - 2 600.1 480.3 | ok 10 0 102.16 459.7 | non_incremental_QF_LIA/tropical-matrix-constraint-1908553.smt2 | to - 2 600.01 713.8 | ok 10 0 22.22 394.9 | non_incremental_QF_LIA/tropical-matrix-constraint-2061672.smt2 | ok 10 0 51.6 521.2 | to - 2 600.04 545.8 | non_incremental_QF_LIA/tropical-matrix-constraint-244431.smt2 | ok 10 0 292.95 88.2 | to - 2 600.01 97.7 | non_incremental_QF_LIA/tropical-matrix-constraint-368069.smt2 | to - 2 600.05 135.3 | ok 10 0 445.93 134.2 | non_incremental_QF_LIA/tropical-matrix-constraint-369883.smt2 | ok 10 0 510.59 134.2 | to - 2 600.01 127.7 | non_incremental_QF_LIA/tropical-matrix-constraint-527358.smt2 | ok 10 0 243.33 135.0 | to - 2 600.05 140.7 | non_incremental_QF_LIA/tropical-matrix-constraint-614657.smt2 | ok 10 0 515.89 209.6 | to - 2 600.07 166.6 | non_incremental_QF_LIA/tropical-matrix-constraint-645054.smt2 | ok 10 0 41.34 185.3 | to - 2 600.08 205.1 | non_incremental_QF_LIA/tropical-matrix-constraint-794687.smt2 | ok 10 0 502.03 235.3 | to - 2 600.07 242.0 | non_incremental_QF_LRA/LassoRanker-CooperatingT2-sas2.t2.c_Iteration7_Loop_7-phaseTemplate.smt2 | ok 20 0 593.7 591.3 | to - 2 600.03 614.7 | non_incremental_QF_LRA/LassoRanker-SV-COMP-aviad_true-termination.c_Iteration1_Loop_4-phaseTemplate.smt2 | ok 10 0 594.16 738.5 | to - 2 600.03 701.6 | non_incremental_QF_LRA/LassoRanker-Ultimate-Collatz.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | to - 2 600.09 711.5 | ok 20 0 593.46 711.2 | non_incremental_QF_LRA/tropical-matrix-constraint-199552.smt2 | ok 10 0 268.04 71.2 | to - 2 600.05 81.6 | non_incremental_QF_LRA/tropical-matrix-constraint-223827.smt2 | to - 2 600.06 91.9 | ok 10 0 505.07 95.9 |``` --- src/theory/booleans/theory_bool_rewriter.cpp | 96 +++++++++++++++----- 1 file changed, 71 insertions(+), 25 deletions(-) diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index e63526806..ca2ac13ea 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -157,6 +157,19 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (!done) { return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff); } + // x v ... v x --> x + unsigned ind, size; + for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind) + { + if (n[ind] != n[ind+1]) + { + break; + } + } + if (ind == size - 1) + { + return RewriteResponse(REWRITE_AGAIN, n[0]); + } break; } case kind::AND: { @@ -172,6 +185,19 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { Debug("bool-flatten") << n << ": " << ret.d_node << std::endl; return ret; } + // x ^ ... ^ x --> x + unsigned ind, size; + for (ind = 0, size = n.getNumChildren(); ind < size - 1; ++ind) + { + if (n[ind] != n[ind+1]) + { + break; + } + } + if (ind == size - 1) + { + return RewriteResponse(REWRITE_AGAIN, n[0]); + } break; } case kind::IMPLIES: { @@ -293,28 +319,39 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0].isConst()) { if (n[0] == tt) { // ITE true x y - - Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl; + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==tt " + << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[1]); } else { Assert(n[0] == ff); // ITE false x y - Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl; + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[0] ==ff " + << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[2]); } } else if (n[1].isConst()) { if (n[1] == tt && n[2] == ff) { - Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==tt && n[2] == ff " + << n << ": " << n[0] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[0]); } else if (n[1] == ff && n[2] == tt) { - Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite_ITE: n[1] ==ff && n[2] == tt " + << n << ": " << n[0].notNode() << std::endl; return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } - // else if(n[1] == ff){ - // Node resp = (n[0].notNode()).andNode(n[2]); - // return RewriteResponse(REWRITE_AGAIN, resp); - // } + if (n[1] == tt || n[1] == ff) + { + // ITE C true y --> C v y + // ITE C false y --> ~C ^ y + Node resp = + n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } } if (n[0].getKind() == kind::NOT) @@ -324,18 +361,23 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1])); } - // else if (n[2].isConst()) { - // if(n[2] == ff){ - // Node resp = (n[0]).andNode(n[1]); - // return RewriteResponse(REWRITE_AGAIN, resp); - // } - // } + if (n[2].isConst() && (n[2] == tt || n[2] == ff)) + { + // ITE C x true --> ~C v x + // ITE C x false --> C ^ x + Node resp = + n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } int parityTmp; if ((parityTmp = equalityParity(n[1], n[2])) != 0) { Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); - Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp - << " " << n << ": " << resp << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[1], n[2] " + << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now // } else if (n[0].getKind() == kind::NOT) { @@ -346,15 +388,17 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // if n[1] is constant this can loop, this is possible in prewrite Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]); - Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp - << " " << n << ": " << resp << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[1] " + << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){ // (parityTmp == 1) if n[0] == n[2] // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2] Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt); - Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp - << " " << n << ": " << resp << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite_ITE: equalityParity n[0], n[2] " + << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } else if(n[1].getKind() == kind::ITE && (parityTmp = equalityParity(n[0], n[1][0])) != 0){ @@ -362,8 +406,9 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // (parityTmp > 1) then n : (ite c (ite (not c) x y) z) or // n: (ite (not c) (ite c x y) z) Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]); - Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp - << " " << n << ": " << resp << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[1][0] " + << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } else if(n[2].getKind() == kind::ITE && (parityTmp = equalityParity(n[0], n[2][0])) != 0){ @@ -371,8 +416,9 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // (parityTmp > 1) then n : (ite c x (ite (not c) y z)) or // n: (ite (not c) x (ite c y z)) Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]); - Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp - << " " << n << ": " << resp << std::endl; + Debug("bool-ite") + << "TheoryBoolRewriter::preRewrite: equalityParity n[0], n[2][0] " + << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } break; -- 2.30.2