From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Feb 2022 21:07:33 +0000 (-0600)
Subject: Fix for lambda-to-array constant conversion for unused arguments (#8082)
X-Git-Tag: cvc5-1.0.0~426
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6137c76753b0e1043c2ea30deceafaa66e0ddc3;p=cvc5.git

Fix for lambda-to-array constant conversion for unused arguments (#8082)

Fixes #4434.
---

diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp
index 85fec7cb2..ef19a65d2 100644
--- a/src/theory/uf/function_const.cpp
+++ b/src/theory/uf/function_const.cpp
@@ -189,7 +189,7 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n,
       // thus requiring the rest of the disjunction to be further processed in
       // the then-branch as the current value.
       bool pol = curr[0].getKind() != kind::NOT;
-      bool inverted = (pol && ck == kind::AND) || (!pol && ck == kind::OR);
+      bool inverted = (pol == (ck == kind::AND));
       index_eq = pol ? curr[0] : curr[0][0];
       // processed : the value that is determined by the first child of curr
       // remainder : the remaining children of curr
@@ -236,7 +236,7 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n,
           << "  process base : " << curr << std::endl;
       // Simple Boolean return cases, in which
       //  (1) lambda x. (= x v) becomes lambda x. (ite (= x v) true false)
-      //  (2) lambda x. v becomes lambda x. (ite (= x v) true false)
+      //  (2) lambda x. x becomes lambda x. (ite (= x true) true false)
       // Note the negateg cases of the bodies above are also handled.
       bool pol = ck != kind::NOT;
       index_eq = pol ? curr : curr[0];
@@ -309,7 +309,12 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n,
     {
       Trace("builtin-rewrite-debug2")
           << "  ...could not infer index value." << std::endl;
-      return Node::null();
+      // it could correspond to the default value that does not involve the
+      // current argument, hence we break and take curr as the default value
+      // below. For example, if we are processing lambda xy. (not y) for x,
+      // we have index_eq is (= y true), which does not match for x, hence
+      // (not y) is taken as the default value below.
+      break;
     }
 
     // [4] Recurse to ensure that "curr_val" has been normalized w.r.t. the
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c812d364e..8d9af1db5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -661,6 +661,7 @@ set(regress_0_tests
   regress0/ho/ho-matching-nested-app.smt2
   regress0/ho/ho-std-fmf.smt2
   regress0/ho/hoa0008.smt2
+  regress0/ho/issue4434-const-preserve.smt2
   regress0/ho/issue4477.smt2
   regress0/ho/issue4990-care-graph.smt2
   regress0/ho/issue5233-part1-usort-owner.smt2
diff --git a/test/regress/regress0/ho/issue4434-const-preserve.smt2 b/test/regress/regress0/ho/issue4434-const-preserve.smt2
new file mode 100644
index 000000000..59f3fd96a
--- /dev/null
+++ b/test/regress/regress0/ho/issue4434-const-preserve.smt2
@@ -0,0 +1,8 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-datatype a ((b)))
+(declare-datatype c ((i (j a))))
+(declare-datatype e ((f)))
+(declare-fun h (c e Bool) Bool)
+(assert (h (i b) f false))
+(check-sat)