Rename system tests to api tests and remove obsolete Java test. (#5066)

13 files changed, 62 insertions, 134 deletions

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 8c11acf3b..5138d79b5 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -31,8 +31,8 @@ add_dependencies(main cvc4 cvc4parser gen-tokens)
 get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES)
 target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
 
-# main-test library is only used for linking against system and unit tests so
-# that we don't have to include all object files of main into each unit/system
+# main-test library is only used for linking against api and unit tests so
+# that we don't have to include all object files of main into each api/unit
 # test. Do not link against main-test in any other case.
 add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>)
 target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER)
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index cc05aff43..4c8b9d156 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -2,11 +2,11 @@
 # Add target 'check', builds and runs
 # > unit tests
 # > regression tests of levels 0 and 1
-# > system tests
+# > api tests
 
 add_custom_target(build-tests)
 
-# Note: Do not add custom targets for running tests (regress, systemtests,
+# Note: Do not add custom targets for running tests (regress, apitests,
 # units) as dependencies to other run targets. This will result in executing
 # tests multiple times. For example, if check would depend on regress it would
 # first run the command of the regress target (i.e., run all regression tests)
@@ -24,7 +24,7 @@ add_custom_target(check
 if (NOT BUILD_LIB_ONLY)
   add_subdirectory(regress)
 endif()
-add_subdirectory(system EXCLUDE_FROM_ALL)
+add_subdirectory(api EXCLUDE_FROM_ALL)
 
 if(ENABLE_UNIT_TESTING)
   add_subdirectory(unit EXCLUDE_FROM_ALL)
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
new file mode 100644
index 000000000..8d9110e9f
--- /dev/null
+++ b/test/api/CMakeLists.txt
@@ -0,0 +1,57 @@
+include_directories(.)
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+#-----------------------------------------------------------------------------#
+# Add target 'apitests', builds and runs
+# > api tests
+
+add_custom_target(build-apitests)
+add_dependencies(build-tests build-apitests)
+
+add_custom_target(apitests
+  COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS
+  DEPENDS build-apitests)
+
+set(CVC4_API_TEST_FLAGS
+  -D__BUILDING_CVC4_API_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
+
+macro(cvc4_add_api_test name)
+  add_executable(${name} ${name}.cpp)
+  target_link_libraries(${name} main-test)
+  target_compile_definitions(${name} PRIVATE ${CVC4_API_TEST_FLAGS})
+  add_test(api/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
+  set_tests_properties(api/${name} PROPERTIES LABELS "api")
+  add_dependencies(build-apitests ${name})
+endmacro()
+
+cvc4_add_api_test(boilerplate)
+cvc4_add_api_test(ouroborous)
+cvc4_add_api_test(reset_assertions)
+cvc4_add_api_test(sep_log_api)
+cvc4_add_api_test(smt2_compliance)
+# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API
+# cvc4_add_api_test(statistics)
+cvc4_add_api_test(two_solvers)
+
+# if we've built using libedit, then we want the interactive shell tests
+if (USE_EDITLINE)
+
+  # Check for pexpect -- zero return code is success
+  execute_process(
+    COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect"
+    RESULT_VARIABLE PEXPECT_RC
+    ERROR_QUIET
+  )
+
+  # Add the test if we have pexpect
+  if(PEXPECT_RC EQUAL 0)
+    add_test(
+      NAME interactive_shell
+      COMMAND
+      "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/api/interactive_shell.py"
+      WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
+    )
+  endif()
+endif()
diff --git a/test/system/boilerplate.cpp b/test/api/boilerplate.cpp
index 315cec7bf..315cec7bf 100644
--- a/test/system/boilerplate.cpp
+++ b/test/api/boilerplate.cpp
diff --git a/test/system/interactive_shell.py b/test/api/interactive_shell.py
index 3cc9953ee..3cc9953ee 100755
--- a/test/system/interactive_shell.py
+++ b/test/api/interactive_shell.py
diff --git a/test/system/ouroborous.cpp b/test/api/ouroborous.cpp
index ef360628a..ef360628a 100644
--- a/test/system/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
diff --git a/test/system/reset_assertions.cpp b/test/api/reset_assertions.cpp
index dc9bd24f6..dc9bd24f6 100644
--- a/test/system/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
diff --git a/test/system/sep_log_api.cpp b/test/api/sep_log_api.cpp
index 9341310a3..9341310a3 100644
--- a/test/system/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
diff --git a/test/system/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 340326e40..340326e40 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
diff --git a/test/system/statistics.cpp b/test/api/statistics.cpp
index 234246112..234246112 100644
--- a/test/system/statistics.cpp
+++ b/test/api/statistics.cpp
diff --git a/test/system/two_solvers.cpp b/test/api/two_solvers.cpp
index c5bea4860..c5bea4860 100644
--- a/test/system/two_solvers.cpp
+++ b/test/api/two_solvers.cpp
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
deleted file mode 100644
index a9c1a80db..000000000
--- a/test/system/CMakeLists.txt
+++ /dev/null
@@ -1,59 +0,0 @@
-include_directories(.)
-include_directories(${PROJECT_SOURCE_DIR}/src)
-include_directories(${PROJECT_SOURCE_DIR}/src/include)
-include_directories(${CMAKE_BINARY_DIR}/src)
-
-#-----------------------------------------------------------------------------#
-# Add target 'systemtests', builds and runs
-# > system tests
-
-add_custom_target(build-systemtests)
-add_dependencies(build-tests build-systemtests)
-
-add_custom_target(systemtests
-  COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $$ARGS
-  DEPENDS build-systemtests)
-
-set(CVC4_SYSTEM_TEST_FLAGS
-  -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
-
-macro(cvc4_add_system_test name)
-  add_executable(${name} ${name}.cpp)
-  target_link_libraries(${name} main-test)
-  target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS})
-  add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
-  set_tests_properties(system/${name} PROPERTIES LABELS "system")
-  add_dependencies(build-systemtests ${name})
-endmacro()
-
-cvc4_add_system_test(boilerplate)
-cvc4_add_system_test(ouroborous)
-cvc4_add_system_test(reset_assertions)
-cvc4_add_system_test(sep_log_api)
-cvc4_add_system_test(smt2_compliance)
-# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API
-# cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_solvers)
-
-# if we've built using libedit, then we want the interactive shell tests
-if (USE_EDITLINE)
-
-  # Check for pexpect -- zero return code is success
-  execute_process(
-    COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect"
-    RESULT_VARIABLE PEXPECT_RC
-    ERROR_QUIET
-  )
-
-  # Add the test if we have pexpect
-  if(PEXPECT_RC EQUAL 0)
-    add_test(
-      NAME interactive_shell
-      COMMAND
-      "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/system/interactive_shell.py"
-      WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
-    )
-  endif()
-endif()
-
-# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java
deleted file mode 100644
index c38cfab3d..000000000
--- a/test/system/CVC4JavaTest.java
+++ /dev/null
@@ -1,70 +0,0 @@
-/*********************                                                        */
-/*! \file CVC4JavaTest.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-import edu.nyu.acsys.CVC4.CVC4;
-
-import edu.nyu.acsys.CVC4.SmtEngine;
-import edu.nyu.acsys.CVC4.ExprManager;
-import edu.nyu.acsys.CVC4.Expr;
-import edu.nyu.acsys.CVC4.Type;
-import edu.nyu.acsys.CVC4.Kind;
-import edu.nyu.acsys.CVC4.Result;
-import edu.nyu.acsys.CVC4.Configuration;
-
-//import edu.nyu.acsys.CVC4.Exception;
-
-import edu.nyu.acsys.CVC4.Parser;
-import edu.nyu.acsys.CVC4.ParserBuilder;
-
-public class CVC4JavaTest {
-  public static void main(String[] args) {
-    try {
-      System.loadLibrary("cvc4jni");
-
-      //CVC4.getDebugChannel().on("current");
-
-      System.out.println(Configuration.about());
-
-      String[] tags = Configuration.getDebugTags();
-      System.out.print("available debug tags:");
-      for(int i = 0; i < tags.length; ++i) {
-        System.out.print(" " + tags[i]);
-      }
-      System.out.println();
-
-      ExprManager em = new ExprManager();
-      SmtEngine smt = new SmtEngine(em);
-
-      Type t = em.booleanType();
-      Expr a = em.mkVar("a", em.booleanType());
-      Expr b = em.mkVar("b", em.booleanType());
-      Expr e = new Expr(em.mkExpr(Kind.AND, a, b, new Expr(a).notExpr()));
-      System.out.println("==> " + e);
-
-      Result r = smt.checkSat(e);
-      boolean correct = r.isSat() == Result.Sat.UNSAT;
-
-      System.out.println(smt.getStatistics());
-
-      System.exit(correct ? 0 : 1);
-    } catch(Exception e) {
-      System.err.println(e);
-      System.exit(1);
-    }
-  }
-}
-