Make lambda rewriter more robust (#3806)

The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.

2 files changed, 12 insertions, 3 deletions

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index c53610efa..1c5eab364 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -316,6 +316,14 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       //   return RewriteResponse(REWRITE_AGAIN, resp);
       // }
     }
+
+    if (n[0].getKind() == kind::NOT)
+    {
+      // ite(not(c), x, y) ---> ite(c, y, x)
+      return RewriteResponse(
+          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]);
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 15c312080..82952f9fd 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -224,9 +224,10 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n,
           << "  process base : " << curr << std::endl;
       // Boolean return case, e.g. lambda x. (= x v) becomes
       // lambda x. (ite (= x v) true false)
-      index_eq = curr;
-      curr_val = nm->mkConst(true);
-      next = nm->mkConst(false);
+      bool pol = curr.getKind() != kind::NOT;
+      index_eq = pol ? curr : curr[0];
+      curr_val = nm->mkConst(pol);
+      next = nm->mkConst(!pol);
     }
 
     // [2] We ensure that "index_eq" is an equality, if possible.