From 425a28b996286c4eea66a96bad075fc342a9fed7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 5 Mar 2022 14:50:25 -0600
Subject: [PATCH] Unit tests for fixed projects issues (#8229)

Fixes cvc5/cvc5-projects#421.
Fixes cvc5/cvc5-projects#361.
---
 test/unit/api/cpp/CMakeLists.txt            |  1 +
 test/unit/api/cpp/theory_arith_nl_black.cpp | 17 +++++++
 test/unit/api/cpp/theory_uf_ho_black.cpp    | 50 +++++++++++++++++++++
 3 files changed, 68 insertions(+)
 create mode 100644 test/unit/api/cpp/theory_uf_ho_black.cpp

diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index 3e1330d6f..c10214803 100644
--- 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 e72b7d7cd..9fc19fb79 100644
--- 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
index 000000000..03eb4304a
--- /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
-- 
2.30.2