Fix tracker in SubstitutionMap (#7829)

This PR fixes a subtle issue in #7787 where the rhs (instead of the lhs) of the applied substitution was inserted into the tracker.
Fixes cvc5/cvc5-projects#388

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index e495630467681480f684734f48d07dfa2f337915..b56aa4f16265d282c2130e5c0bc92d39a35422b8 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -111,11 +111,11 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache, std::set<TNo
             internalSubstitute(rhs, cache, tracker);
             d_substitutions[result] = cache[rhs];
             cache[result] = cache[rhs];
-            result = cache[rhs];
             if (tracker != nullptr)
             {
               tracker->insert(result);
             }
+            result = cache[rhs];
           }
         }
       }

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index e99732ca4c2be50bd706a98eee26bf54ee95be8d..3e1330d6f592f35294c63d5fa7b2792037148fe7 100644 (file)
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -22,3 +22,4 @@ cvc5_add_unit_test_white(solver_white api)
 cvc5_add_unit_test_black(sort_black api)
 cvc5_add_unit_test_black(term_black api)
 cvc5_add_unit_test_white(term_white api)
+cvc5_add_unit_test_black(theory_arith_nl_black api)

diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp
new file mode 100644 (file)
index 0000000..91f260a
--- /dev/null
+++ b/test/unit/api/cpp/theory_arith_nl_black.cpp
@@ -0,0 +1,66 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Blackbox tests using the API targeting nonlinear arithmetic.
+ */
+
+#include "test_api.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestTheoryBlackArithNl : public TestApi
+{
+};
+
+TEST_F(TestTheoryBlackArithNl, cvc5Projects388)
+{
+  Solver slv;
+  slv.setLogic("QF_NRA");
+  Sort s = slv.getRealSort();
+  Term t1 = slv.mkConst(s, "a");
+  Term t2 = slv.mkConst(s, "b");
+  Term t3 = slv.mkConst(s, "c");
+  Term t4 = slv.mkTerm(Kind::DIVISION, {t1, t2});
+  Term t5 = slv.mkTerm(Kind::GT, {t4, t3});
+  Term t6 = slv.mkTerm(Kind::DIVISION, {t1, t3});
+  Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t6});
+  Term t8 = slv.mkTerm(Kind::AND, {t5, t7, t5});
+  Term t9 = slv.mkTerm(Kind::NOT, {t8});
+  slv.assertFormula(t9);
+  slv.checkSat();
+}
+
+TEST_F(TestTheoryBlackArithNl, cvc5Projects388Min)
+{
+  Solver slv;
+  slv.setOption("nl-cad", "true");
+  slv.setOption("nl-cad-var-elim", "true");
+  slv.setOption("nl-ext", "none");
+  slv.setLogic("QF_NIRA");
+  Sort s = slv.getRealSort();
+  Term t1 = slv.mkConst(s, "a");
+  Term t2 = slv.mkConst(s, "b");
+  Term t3 = slv.mkReal(0);
+  Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t1});
+  Term t4 = slv.mkTerm(Kind::DIVISION, {t2, t1});
+  Term t5 = slv.mkTerm(Kind::DISTINCT, {t3, t4});
+  Term t8 = slv.mkTerm(Kind::OR, {t7, t5});
+  slv.assertFormula(t8);
+  slv.checkSat();
+}
+
+}  // namespace test
+}  // namespace cvc5