Fix --ackermann in the presence on syntactically different but possibly equal selects...

The implementation of --ackermann mishandled selects in a subtle way:
If select is applied to two syntactically different arrays (that may be semantically equal), the ackermann preprocessing failed to generate the "all arguments equal implies terms equal" lemmas.
The problem is that we used the first argument (that is: the array) as lookup to identify terms that need to be considered for these lemmas. Instead we now use their operator (select) just like for uninterpreted function applications.

Fixes #4957 . Also adds a regression.

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 31c92a09f81e847ca9f302147bcafd23a76006a5..ab9c2482baa8b323b61f343b0880ea9f78cb1ec0 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -70,11 +70,14 @@ void addLemmaForPair(TNode args1,
   }
   else
   {
-    Assert(args1.getKind() == kind::SELECT && args1[0] == func);
-    Assert(args2.getKind() == kind::SELECT && args2[0] == func);
+    Assert(args1.getKind() == kind::SELECT && args1.getOperator() == func);
+    Assert(args2.getKind() == kind::SELECT && args2.getOperator() == func);
     Assert(args1.getNumChildren() == 2);
     Assert(args2.getNumChildren() == 2);
-    args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
+    args_eq = nm->mkNode(Kind::AND,
+      nm->mkNode(kind::EQUAL, args1[0], args2[0]),
+      nm->mkNode(kind::EQUAL, args1[1], args2[1])
+    );
   }
   Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
   Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
@@ -153,7 +156,7 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
     if (seen.find(term) == seen.end())
     {
       TNode func;
-      if (term.getKind() == kind::APPLY_UF)
+      if (term.getKind() == kind::APPLY_UF || term.getKind() == kind::SELECT)
       {
         storeFunctionAndAddLemmas(term.getOperator(),
                                   term,
@@ -163,11 +166,6 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
                                   nm,
                                   vec);
       }
-      else if (term.getKind() == kind::SELECT)
-      {
-        storeFunctionAndAddLemmas(
-            term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec);
-      }
       else
       {
         AlwaysAssert(term.getKind() != kind::STORE)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0caeafb36120c38f830bc7d1a5a70eb98618b791..4de32a426638556c568cfcce00ec65942465e9c9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -59,6 +59,7 @@ set(regress_0_tests
   regress0/arrays/bug272.minimized.smtv1.smt2
   regress0/arrays/bug272.smtv1.smt2
   regress0/arrays/bug3020.smt2
+  regress0/arrays/bug4957.smt2
   regress0/arrays/bug637.delta.smt2
   regress0/arrays/constarr.cvc
   regress0/arrays/constarr.smt2

diff --git a/test/regress/regress0/arrays/bug4957.smt2 b/test/regress/regress0/arrays/bug4957.smt2
new file mode 100644 (file)
index 0000000..f82ae19
--- /dev/null
+++ b/test/regress/regress0/arrays/bug4957.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_ALIA)
+(declare-fun a () (Array Int Int))
+(assert (distinct (select a 0) (select (ite false a a) 0)))
+(check-sat)