From 52bab1414d41a4beb301f3c8a4165fa972f71a93 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 31 Aug 2020 21:59:39 +0200 Subject: [PATCH] Fix --ackermann in the presence on syntactically different but possibly equal selects (#4981) 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. --- src/preprocessing/passes/ackermann.cpp | 16 +++++++--------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/arrays/bug4957.smt2 | 6 ++++++ 3 files changed, 14 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress0/arrays/bug4957.smt2 diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 31c92a09f..ab9c2482b 100644 --- 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 0caeafb36..4de32a426 100644 --- 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 index 000000000..f82ae1932 --- /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) -- 2.30.2