summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2020-06-19 15:10:27 -0300
committerGitHub <noreply@github.com>2020-06-19 15:10:27 -0300
commit11c1fba70098cc72c59b2d335249332790287c20 (patch)
tree56ce77e7842403e82fddbfca0fc39a50ff497459
parent5247901077efbc7b9016ba35fded7a6ab459a379 (diff)
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 |```
Diffstat
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp96
1 files 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback