projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 5247901)
Always rewrite boolean ITEs with constant then/else-branches (#4619)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 19 Jun 2020 18:10:27 +0000 (15:10 -0300)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 18:10:27 +0000 (15:10 -0300)
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 patch | blob | history

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index e635268061af3a174f7a24752387257e747ef6d5..ca2ac13ea7be7c6463f63ff54e736abd35cf1674 100644 (file)
--- 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;