From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Thu, 28 Apr 2022 18:30:46 +0000 (-0700)
Subject: Move tests around (#8670)
X-Git-Tag: cvc5-1.0.1~207
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9dc2d55ce20f4b69b651ac75e28d3de0704b3520;p=cvc5.git

Move tests around (#8670)

This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/.
---

diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index fffb93ce3..bea15a3a0 100644
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -57,7 +57,10 @@ cvc5_add_api_test(proj-issue334)
 cvc5_add_api_test(proj-issue344)
 cvc5_add_api_test(proj-issue345)
 cvc5_add_api_test(proj-issue377)
+cvc5_add_api_test(proj-issue388)
 cvc5_add_api_test(proj-issue395)
 cvc5_add_api_test(proj-issue399)
+cvc5_add_api_test(proj-issue421)
 cvc5_add_api_test(proj-issue445)
+cvc5_add_api_test(proj-issue455)
 cvc5_add_api_test(proj-issue484)
diff --git a/test/api/cpp/proj-issue388.cpp b/test/api/cpp/proj-issue388.cpp
new file mode 100644
index 000000000..87638147b
--- /dev/null
+++ b/test/api/cpp/proj-issue388.cpp
@@ -0,0 +1,62 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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 #388
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+#include "base/configuration.h"
+#include <cassert>
+
+using namespace cvc5;
+
+int main(void)
+{
+  if (!internal::Configuration::isBuiltWithPoly())
+  {
+    return 0;
+  }
+  { // Original
+    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();
+  }
+  { // Minimized
+    Solver slv;
+    slv.setOption("nl-cov", "true");
+    slv.setOption("nl-cov-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();
+  }
+}
diff --git a/test/api/cpp/proj-issue421.cpp b/test/api/cpp/proj-issue421.cpp
new file mode 100644
index 000000000..3a152673e
--- /dev/null
+++ b/test/api/cpp/proj-issue421.cpp
@@ -0,0 +1,37 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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 #421
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+#include <cassert>
+
+using namespace cvc5;
+
+int main(void)
+{
+  Solver slv;
+  slv.setLogic("QF_ALL");
+  Sort s1 = slv.mkBitVectorSort(4);
+  Sort s4 = slv.getRealSort();
+  Sort s5 = slv.mkSequenceSort(s1);
+  Term t8 = slv.mkConst(s5, "_x49");
+  Term t10 = slv.mkConst(s4, "_x51");
+  Term t65 = slv.mkTerm(Kind::SEQ_REV, {t8});
+  Term t69 = slv.mkTerm(Kind::TANGENT, {t10});
+  Term t77 = slv.mkTerm(Kind::LEQ, {t69, t10});
+  Term t128 = slv.mkTerm(Kind::SEQ_PREFIX, {t65, t8});
+  slv.assertFormula({t77});
+  slv.checkSatAssuming(t128.notTerm());
+}
diff --git a/test/api/cpp/proj-issue455.cpp b/test/api/cpp/proj-issue455.cpp
new file mode 100644
index 000000000..c47247db9
--- /dev/null
+++ b/test/api/cpp/proj-issue455.cpp
@@ -0,0 +1,75 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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 #455
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+#include "base/configuration.h"
+#include <cassert>
+
+using namespace cvc5;
+
+int main(void)
+{
+  if (!internal::Configuration::isBuiltWithPoly())
+  {
+    return 0;
+  }
+  Solver slv;
+  slv.setLogic("QF_UFNRA");
+  slv.setOption("produce-unsat-assumptions", "true");
+  slv.setOption("incremental", "false");
+  slv.setOption("produce-models", "true");
+  Sort s1 = slv.mkUninterpretedSort("_u0");
+  Sort s2 = slv.getRealSort();
+  Term t1 = slv.mkConst(s2, "_x4");
+  Term t2 = slv.mkConst(s1, "_x5");
+  Term t3 = slv.mkConst(s2, "_x7");
+  Term t4 = slv.mkReal("2");
+  Term t5 = slv.mkConst(s2, "_x10");
+  Term t6 = slv.mkConst(s2, "_x11");
+  Term t7 = slv.mkReal("3615783917");
+  Term t8 = slv.mkConst(s2, "_x14");
+  Term t9 = slv.mkConst(s2, "_x15");
+  Term t10 = slv.mkTerm(Kind::ADD, {t5, t9});
+  Term t11 = slv.mkTerm(Kind::ADD, {t10, t7, t8, t6});
+  Term t12 = slv.mkTerm(Kind::LEQ, {t4, t11});
+  Term t13 = slv.mkTerm(Kind::SUB, {t11, t6});
+  Term t14 = slv.mkTerm(Kind::SUB, {t6, t13});
+  Term t15 = slv.mkTerm(Kind::MULT, {t4, t4});
+  Term t16 = slv.mkTerm(Kind::GT, {t15, t11});
+  Term t17 = slv.mkTerm(Kind::SUB, {t11, t3});
+  Term t18 = slv.mkTerm(Kind::LEQ, {t17, t7});
+  Term t19 = slv.mkTerm(Kind::IMPLIES, {t18, t12});
+  Term t20 = slv.mkTerm(Kind::GEQ, {t1, t3});
+  Term t21 = slv.mkTerm(Kind::MULT, {t7, t13});
+  Term t22 = slv.mkTerm(Kind::MULT, {t21, t14});
+  Term t23 = slv.mkTerm(Kind::SUB, {t14, t3});
+  Term t24 = slv.mkVar(s2, "_f19_0");
+  Term t25 = slv.mkVar(s2, "_f19_1");
+  Term t26 = slv.mkVar(s1, "_f19_2");
+  Term t27 = slv.mkVar(s2, "_f19_3");
+  Term t28 = slv.mkVar(s1, "_f19_4");
+  Term t29 = slv.defineFun("_f19", {t24, t25, t26, t27, t28}, t24.getSort(), t24);
+  Term t30 = slv.mkTerm(Kind::DISTINCT, {t19, t20, t16});
+  Term t31 = slv.mkTerm(Kind::ITE, {t30, t9, t22});
+  Term t32 = slv.mkTerm(Kind::DIVISION, {t11, t6, t10});
+  Term t33 = slv.mkTerm(Kind::GEQ, {t32, t3});
+  Term t34 = slv.mkTerm(Kind::APPLY_UF, {t29, t31, t3, t2, t3, t2});
+  Term t35 = slv.mkTerm(Kind::GEQ, {t34, t23});
+  Term t36 = slv.mkTerm(Kind::NOT, {t35});
+  slv.assertFormula({t36});
+  slv.assertFormula({t33});
+  slv.checkSatAssuming({t18.notTerm()});
+}
diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index 7d2657ea1..ca6fce4c3 100644
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -21,8 +21,6 @@ cvc5_add_unit_test_black(result_black api/cpp)
 cvc5_add_unit_test_black(solver_black api/cpp)
 cvc5_add_unit_test_black(sort_black api/cpp)
 cvc5_add_unit_test_black(term_black api/cpp)
-cvc5_add_unit_test_black(theory_arith_nl_black api/cpp)
-cvc5_add_unit_test_black(theory_uf_ho_black api/cpp)
 cvc5_add_unit_test_white(op_white api/cpp)
 cvc5_add_unit_test_white(solver_white api/cpp)
 cvc5_add_unit_test_black(synth_result_black api/cpp)
diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp
deleted file mode 100644
index bf461ef66..000000000
--- a/test/unit/api/cpp/theory_arith_nl_black.cpp
+++ /dev/null
@@ -1,144 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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"
-#include "base/configuration.h"
-
-namespace cvc5::internal {
-
-namespace test {
-
-class TestTheoryBlackArithNl : public TestApi
-{
-};
-
-TEST_F(TestTheoryBlackArithNl, cvc5Projects388)
-{
-  if (!Configuration::isBuiltWithPoly())
-  {
-    return;
-  }
-  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)
-{
-  if (!Configuration::isBuiltWithPoly())
-  {
-    return;
-  }
-  Solver slv;
-  slv.setOption("nl-cov", "true");
-  slv.setOption("nl-cov-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();
-}
-
-TEST_F(TestTheoryBlackArithNl, proj_issue421)
-{
-  Solver slv;
-  slv.setLogic("QF_ALL");
-  Sort s1 = slv.mkBitVectorSort(4);
-  Sort s4 = slv.getRealSort();
-  Sort s5 = slv.mkSequenceSort(s1);
-  Term t8 = slv.mkConst(s5, "_x49");
-  Term t10 = slv.mkConst(s4, "_x51");
-  Term t65 = slv.mkTerm(Kind::SEQ_REV, {t8});
-  Term t69 = slv.mkTerm(Kind::TANGENT, {t10});
-  Term t77 = slv.mkTerm(Kind::LEQ, {t69, t10});
-  Term t128 = slv.mkTerm(Kind::SEQ_PREFIX, {t65, t8});
-  slv.assertFormula({t77});
-  slv.checkSatAssuming(t128.notTerm());
-}
-
-TEST_F(TestTheoryBlackArithNl, cvc5Projects455)
-{
-  if (!Configuration::isBuiltWithPoly())
-  {
-    return;
-  }
-  Solver slv;
-  slv.setLogic("QF_UFNRA");
-  slv.setOption("produce-unsat-assumptions", "true");
-  slv.setOption("incremental", "false");
-  slv.setOption("produce-models", "true");
-  Sort s1 = slv.mkUninterpretedSort("_u0");
-  Sort s2 = slv.getRealSort();
-  Term t1 = slv.mkConst(s2, "_x4");
-  Term t2 = slv.mkConst(s1, "_x5");
-  Term t3 = slv.mkConst(s2, "_x7");
-  Term t4 = slv.mkReal("2");
-  Term t5 = slv.mkConst(s2, "_x10");
-  Term t6 = slv.mkConst(s2, "_x11");
-  Term t7 = slv.mkReal("3615783917");
-  Term t8 = slv.mkConst(s2, "_x14");
-  Term t9 = slv.mkConst(s2, "_x15");
-  Term t10 = slv.mkTerm(Kind::ADD, {t5, t9});
-  Term t11 = slv.mkTerm(Kind::ADD, {t10, t7, t8, t6});
-  Term t12 = slv.mkTerm(Kind::LEQ, {t4, t11});
-  Term t13 = slv.mkTerm(Kind::SUB, {t11, t6});
-  Term t14 = slv.mkTerm(Kind::SUB, {t6, t13});
-  Term t15 = slv.mkTerm(Kind::MULT, {t4, t4});
-  Term t16 = slv.mkTerm(Kind::GT, {t15, t11});
-  Term t17 = slv.mkTerm(Kind::SUB, {t11, t3});
-  Term t18 = slv.mkTerm(Kind::LEQ, {t17, t7});
-  Term t19 = slv.mkTerm(Kind::IMPLIES, {t18, t12});
-  Term t20 = slv.mkTerm(Kind::GEQ, {t1, t3});
-  Term t21 = slv.mkTerm(Kind::MULT, {t7, t13});
-  Term t22 = slv.mkTerm(Kind::MULT, {t21, t14});
-  Term t23 = slv.mkTerm(Kind::SUB, {t14, t3});
-  Term t24 = slv.mkVar(s2, "_f19_0");
-  Term t25 = slv.mkVar(s2, "_f19_1");
-  Term t26 = slv.mkVar(s1, "_f19_2");
-  Term t27 = slv.mkVar(s2, "_f19_3");
-  Term t28 = slv.mkVar(s1, "_f19_4");
-  Term t29 = slv.defineFun("_f19", {t24, t25, t26, t27, t28}, t24.getSort(), t24);
-  Term t30 = slv.mkTerm(Kind::DISTINCT, {t19, t20, t16});
-  Term t31 = slv.mkTerm(Kind::ITE, {t30, t9, t22});
-  Term t32 = slv.mkTerm(Kind::DIVISION, {t11, t6, t10});
-  Term t33 = slv.mkTerm(Kind::GEQ, {t32, t3});
-  Term t34 = slv.mkTerm(Kind::APPLY_UF, {t29, t31, t3, t2, t3, t2});
-  Term t35 = slv.mkTerm(Kind::GEQ, {t34, t23});
-  Term t36 = slv.mkTerm(Kind::NOT, {t35});
-  slv.assertFormula({t36});
-  slv.assertFormula({t33});
-  slv.checkSatAssuming({t18.notTerm()});
-}
-
-}  // namespace test
-}  // namespace cvc5::internal
diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/api/cpp/theory_uf_ho_black.cpp
deleted file mode 100644
index 0de0af4a1..000000000
--- a/test/unit/api/cpp/theory_uf_ho_black.cpp
+++ /dev/null
@@ -1,48 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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 UF + higher-order.
- */
-
-#include "base/configuration.h"
-#include "test_api.h"
-
-namespace cvc5::internal {
-
-namespace test {
-
-class TestTheoryBlackUfHo : public TestApi
-{
-};
-
-TEST_F(TestTheoryBlackUfHo, proj_issue361)
-{
-  d_solver.setLogic("HO_ALL");
-  d_solver.setOption("produce-models", "true");
-  Sort s1 = d_solver.getBooleanSort();
-  Term t1 = d_solver.mkConst(s1, "_x0");
-  Term t145 = d_solver.mkTerm(NOT, {t1});
-  Term t169 = d_solver.mkTerm(AND, {t145, t1});
-  Sort s4 = d_solver.mkFunctionSort({s1, s1, s1}, s1);
-  Sort s6 = d_solver.mkBagSort(s1);
-  Term t189 = d_solver.mkConst(s4, "_x32");
-  Term t200 = d_solver.mkConst(s6, "_x43");
-  Term t250 = d_solver.mkTerm(BAG_COUNT, {t145, t200});
-  Term t367 = d_solver.mkTerm(APPLY_UF, {t189, t1, t169, t1});
-  d_solver.checkSatAssuming({t145, t367, t145, t145, t145});
-  Term v = d_solver.getValue(t250);
-  ASSERT_TRUE(
-      d_solver.checkSatAssuming(d_solver.mkTerm(EQUAL, {t250, v})).isSat());
-}
-
-}  // namespace test
-}  // namespace cvc5::internal
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index ea6730179..7381cab55 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -14,6 +14,7 @@
 ##
 
 # Add unit tests.
+cvc5_add_unit_test_black(theory_uf_ho_black theory)
 cvc5_add_unit_test_black(regexp_operation_black theory)
 cvc5_add_unit_test_black(theory_black theory)
 cvc5_add_unit_test_white(evaluator_white theory)
diff --git a/test/unit/theory/theory_uf_ho_black.cpp b/test/unit/theory/theory_uf_ho_black.cpp
new file mode 100644
index 000000000..0de0af4a1
--- /dev/null
+++ b/test/unit/theory/theory_uf_ho_black.cpp
@@ -0,0 +1,48 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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 UF + higher-order.
+ */
+
+#include "base/configuration.h"
+#include "test_api.h"
+
+namespace cvc5::internal {
+
+namespace test {
+
+class TestTheoryBlackUfHo : public TestApi
+{
+};
+
+TEST_F(TestTheoryBlackUfHo, proj_issue361)
+{
+  d_solver.setLogic("HO_ALL");
+  d_solver.setOption("produce-models", "true");
+  Sort s1 = d_solver.getBooleanSort();
+  Term t1 = d_solver.mkConst(s1, "_x0");
+  Term t145 = d_solver.mkTerm(NOT, {t1});
+  Term t169 = d_solver.mkTerm(AND, {t145, t1});
+  Sort s4 = d_solver.mkFunctionSort({s1, s1, s1}, s1);
+  Sort s6 = d_solver.mkBagSort(s1);
+  Term t189 = d_solver.mkConst(s4, "_x32");
+  Term t200 = d_solver.mkConst(s6, "_x43");
+  Term t250 = d_solver.mkTerm(BAG_COUNT, {t145, t200});
+  Term t367 = d_solver.mkTerm(APPLY_UF, {t189, t1, t169, t1});
+  d_solver.checkSatAssuming({t145, t367, t145, t145, t145});
+  Term v = d_solver.getValue(t250);
+  ASSERT_TRUE(
+      d_solver.checkSatAssuming(d_solver.mkTerm(EQUAL, {t250, v})).isSat());
+}
+
+}  // namespace test
+}  // namespace cvc5::internal