Unit tests for fixed projects issues (#8229)

Fixes cvc5/cvc5-projects#421.
Fixes cvc5/cvc5-projects#361.

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index 3e1330d6f592f35294c63d5fa7b2792037148fe7..c10214803a47348b53fa1923bdd55b4b2d9b81d6 100644 (file)
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -23,3 +23,4 @@ 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)
+cvc5_add_unit_test_black(theory_uf_ho_black api)

diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp
index e72b7d7cd5933f8dbbbc42b3ea7ffe2f48f680ad..9fc19fb79529a26fa6cd3094c638f8371ad0a745 100644 (file)
--- a/test/unit/api/cpp/theory_arith_nl_black.cpp
+++ b/test/unit/api/cpp/theory_arith_nl_black.cpp
@@ -71,6 +71,23 @@ TEST_F(TestTheoryBlackArithNl, cvc5Projects388Min)
   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.checkEntailed({1, t128});
+}
+
 TEST_F(TestTheoryBlackArithNl, cvc5Projects455)
 {
   Solver slv;

diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/api/cpp/theory_uf_ho_black.cpp
new file mode 100644 (file)
index 0000000..03eb430
--- /dev/null
+++ b/test/unit/api/cpp/theory_uf_ho_black.cpp
@@ -0,0 +1,50 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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 UF + higher-order.
+ */
+
+#include "test_api.h"
+#include "base/configuration.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+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