From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 11 Feb 2019 17:04:54 +0000 (-0800)
Subject: New C++ API: Unit tests for declare* functions. (#2831)
X-Git-Tag: cvc5-1.0.0~4263
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c86e0178bfaa662b6586d866c953a56f81cefe51;p=cvc5.git

New C++ API: Unit tests for declare* functions. (#2831)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ddb17c3a7..ea70fc056 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1373,6 +1373,13 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out,
+                         const std::vector<DatatypeConstructorDecl>& vector)
+{
+  container_to_stream(out, vector);
+  return out;
+}
+
 /* DatatypeDecl ------------------------------------------------------------- */
 
 DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype)
@@ -2980,7 +2987,17 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
  */
 Term Solver::declareConst(const std::string& symbol, Sort sort) const
 {
-  return d_exprMgr->mkVar(symbol, *sort.d_type);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (const CVC4::TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 /**
@@ -2990,12 +3007,14 @@ Sort Solver::declareDatatype(
     const std::string& symbol,
     const std::vector<DatatypeConstructorDecl>& ctors) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
+      << "a datatype declaration with at least one constructor";
   DatatypeDecl dtdecl(symbol);
   for (const DatatypeConstructorDecl& ctor : ctors)
   {
     dtdecl.addConstructor(ctor);
   }
-  return mkDatatypeSort(dtdecl);
+  return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
 }
 
 /**
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index b8da070fc..955aff21a 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1455,6 +1455,16 @@ std::ostream& operator<<(std::ostream& out,
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeConstructorDecl& ctordecl) CVC4_PUBLIC;
 
+/**
+ * Serialize a vector of datatype constructor declarations to given stream.
+ * @param out the output stream
+ * @param vector the vector of datatype constructor declarations to be
+ * serialized to the given stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out,
+                         const std::vector<DatatypeConstructorDecl>& vector);
+
 /**
  * Serialize a datatype selector declaration to given stream.
  * @param out the output stream
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index fcc68d981..169a9948d 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -76,7 +76,11 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkUniverseSet();
   void testMkVar();
 
+  void testDeclareConst();
+  void testDeclareDatatype();
   void testDeclareFun();
+  void testDeclareSort();
+
   void testDefineFun();
   void testDefineFunRec();
   void testDefineFunsRec();
@@ -733,6 +737,34 @@ void SolverBlack::testMkVar()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort));
 }
 
+void SolverBlack::testDeclareConst()
+{
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort));
+  TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&);
+}
+
+void SolverBlack::testDeclareDatatype()
+{
+  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl nil("nil");
+  std::vector<DatatypeConstructorDecl> ctors1 = {nil};
+  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil};
+  std::vector<DatatypeConstructorDecl> ctors3;
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2));
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3),
+                   CVC4ApiException&);
+}
+
 void SolverBlack::testDeclareFun()
 {
   Sort bvSort = d_solver->mkBitVectorSort(32);
@@ -748,6 +780,13 @@ void SolverBlack::testDeclareFun()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testDeclareSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 0));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("", 2));
+}
+
 void SolverBlack::testDefineFun()
 {
   Sort bvSort = d_solver->mkBitVectorSort(32);