From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 12 Dec 2018 23:19:30 +0000 (+0000)
Subject: API: Add simple empty/sigma regexp unit tests (#2746)
X-Git-Tag: cvc5-1.0.0~4325
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12f88ad664c24ee522643073dcddf144854ca1ef;p=cvc5.git

API: Add simple empty/sigma regexp unit tests (#2746)
---

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 538899a0f..7527a5c55 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -36,6 +36,8 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFun();
   void testDefineFunRec();
   void testDefineFunsRec();
+  void testMkRegexpEmpty();
+  void testMkRegexpSigma();
 
  private:
   Solver d_solver;
@@ -228,3 +230,19 @@ void SolverBlack::testDefineFunsRec()
       d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
       CVC4ApiException&);
 }
+
+void SolverBlack::testMkRegexpEmpty()
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkVar("s", strSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+}
+
+void SolverBlack::testMkRegexpSigma()
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkVar("s", strSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+}