From f25aa7f135b8f50dadc0252231943cf077a7ff9e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 28 Jan 2022 08:56:27 -0800 Subject: [PATCH] [Rewrite Synthesis] Fix args for non-chaining ops (#7996) Fixes https://github.com/cvc5/cvc5-projects/issues/445. Fixes https://github.com/cvc5/cvc5-projects/issues/446. The issue is related to the preprocessing pass for doing rewrite rule synthesis based on the input. It was removing duplicate arguments from both chaining operators and non-chaining operators when constructing the corresponding datatypes. In the case of non-chaining operators, it could happen that the constructor of the datatype did not have the correct number of arguments for a given kind if there was a term where multiple arguments were the same. This commit fixes the issue by doing the duplicate elimination only for chaining operators. --- src/preprocessing/passes/synth_rew_rules.cpp | 33 ++++++---------- test/api/cpp/CMakeLists.txt | 1 + test/api/cpp/proj-issue445.cpp | 41 ++++++++++++++++++++ 3 files changed, 53 insertions(+), 22 deletions(-) create mode 100644 test/api/cpp/proj-issue445.cpp diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 4adfa1fd6..6386e402a 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -311,28 +311,15 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( argList.push_back(cterm_to_utype[ctc]); } // check if we should chain - bool do_chain = false; - if (argList.size() > 2) - { - Kind k = NodeManager::operatorToKind(op); - do_chain = theory::quantifiers::TermUtil::isAssoc(k) - && theory::quantifiers::TermUtil::isComm(k); - // eliminate duplicate child types - std::vector argListTmp = argList; - argList.clear(); - std::map hasArgType; - for (unsigned j = 0, size = argListTmp.size(); j < size; j++) - { - TypeNode tn = argListTmp[j]; - if (hasArgType.find(tn) == hasArgType.end()) - { - hasArgType[tn] = true; - argList.push_back(tn); - } - } - } + Kind k = NodeManager::operatorToKind(op); + bool do_chain = argList.size() > 2 + && theory::quantifiers::TermUtil::isAssoc(k) + && theory::quantifiers::TermUtil::isComm(k); if (do_chain) { + // eliminate duplicate child types + std::set argSet(argList.begin(), argList.end()); + // we make one type per child // the operator of each constructor is a no-op Node tbv = nm->mkBoundVar(ctt); @@ -347,10 +334,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // Notice this construction allows to abstract subsets of the factors // of t1+t2+t3. This is particularly helpful for terms t1+...+tn for // large n, where we would like to consider binary applications of +. - for (unsigned j = 0, size = argList.size(); j < size; j++) + size_t j = 0; + for (const TypeNode& arg : argSet) { argListc.clear(); - argListc.push_back(argList[j]); + argListc.push_back(arg); std::stringstream sscs; sscs << "C_factor_" << i << "_" << j; // ID function is not printed and does not count towards weight @@ -358,6 +346,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( sscs.str(), argListc, 0); + j++; } // recursive apply TypeNode recType = cterm_to_utype[ct]; diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index 0c9bcc463..c82b8974c 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -58,3 +58,4 @@ cvc5_add_api_test(proj-issue344) cvc5_add_api_test(proj-issue345) cvc5_add_api_test(proj-issue395) cvc5_add_api_test(proj-issue399) +cvc5_add_api_test(proj-issue445) diff --git a/test/api/cpp/proj-issue445.cpp b/test/api/cpp/proj-issue445.cpp new file mode 100644 index 000000000..730151d07 --- /dev/null +++ b/test/api/cpp/proj-issue445.cpp @@ -0,0 +1,41 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for project issue #445 + * + */ + +#include + +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("sygus-rr-synth-input", "true"); + Sort s1 = slv.mkUninterpretedSort("_u0"); + Sort s5 = slv.mkUninterpretedSort("_u1"); + Sort s6 = slv.mkUninterpretedSort("_u2"); + Sort s7 = slv.mkFunctionSort({s1}, s6); + Term t7 = slv.mkConst(s7, "_x8"); + Term t13 = slv.mkConst(s5, "_x14"); + Term t15 = slv.mkTerm(Kind::SEQ_UNIT, {t13}); + Term t84 = slv.mkTerm(Kind::SEQ_REV, {t15}); + Term t141 = slv.mkTerm(Kind::SEQ_UNIT, {t84}); + Term t229 = slv.mkTerm(Kind::SEQ_UNIT, {t15}); + Term t279 = slv.mkTerm(Kind::SEQ_REPLACE_ALL, {t141, t229, t141}); + Term t289 = slv.mkTerm(Kind::SEQ_PREFIX, {t279, t229}); + slv.assertFormula({t289}); + (void)slv.simplify(t7); +} -- 2.30.2