From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 28 Jan 2022 16:56:27 +0000 (-0800)
Subject: [Rewrite Synthesis] Fix args for non-chaining ops (#7996)
X-Git-Tag: cvc5-1.0.0~497
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f25aa7f135b8f50dadc0252231943cf077a7ff9e;p=cvc5.git

[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.
---

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<TypeNode> argListTmp = argList;
-        argList.clear();
-        std::map<TypeNode, bool> 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<TypeNode> 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 <cassert>
+
+#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);
+}