Language bindings: Enable catching of exceptions (#2813)

Fixes #2810. SWIG relies on throw specifiers to determine which
exceptions a method can throw. The wrappers generated by SWIG catch
those C++ exceptions and turn them into exceptions for the target
language. However, we have removed throw specifiers because they have
been deprecated in C++11, so SWIG did not know about any of our
exceptions. This commit fixes the issue using the %catches directive,
declaring that all methods may throw a CVC4::Exception or a general
exception. Note: This means that users of the language bindings will
just receive a general CVC4::Exception instead of more specific
exceptions like TypeExceptions. Given that we are planning to have a
single exception type for the new CVC4 API, this seemed like a natural
choice.
Additionally, the commit (significantly) simplifies the mapping of C++
to Java exceptions and fixes an issue with Python exceptions not
inheriting from BaseException. Finally, the commit adds API examples
for Java and Python, which demonstrate catching exceptions, and adds
Python examples as tests in our build system.

6 files changed, 149 insertions, 5 deletions

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 893ea5c95..6168a8e22 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -86,3 +86,8 @@ if(TARGET CVC4::cvc4jar)
 
   add_subdirectory(api/java)
 endif()
+
+if(CVC4_BINDINGS_PYTHON)
+  # If legacy Python API has been built
+  add_subdirectory(api/python)
+endif()
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 5550974c9..50c52868b 100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -16,11 +16,9 @@
 ### A simple demonstration of the Python interface.  Compare to the
 ### C++ interface in simple_vc_cxx.cpp; they are quite similar.
 ###
-### To run, use something like:
+### To run from a build directory, use something like:
 ###
-###   ln -s ../builds/src/bindings/python/CVC4.py CVC4.py
-###   ln -s ../builds/src/bindings/python/.libs/CVC4.so _CVC4.so
-###   ./SimpleVC.py
+###   PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py
 ####
 
 import CVC4
@@ -61,4 +59,3 @@ def main():
 
 if __name__ == '__main__':
   sys.exit(main())
-
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 108ae3cd3..31f62db56 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -5,6 +5,7 @@ set(EXAMPLES_API_JAVA
   #CVC4Streams
   Combination
   Datatypes
+  Exceptions
   FloatingPointArith
   HelloWorld
   LinearArith
diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java
new file mode 100644
index 000000000..d3ddb85cc
--- /dev/null
+++ b/examples/api/java/Exceptions.java
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file Exceptions.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Catching CVC4 exceptions via the Java API.
+ **
+ ** A simple demonstration of catching CVC4 execptions via the Java API.
+ **/
+
+import edu.stanford.CVC4.*;
+
+public class Exceptions {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    smt.setOption("produce-models", new SExpr(true));
+
+    // Setting an invalid option
+    try {
+      smt.setOption("non-existing", new SExpr(true));
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Creating a term with an invalid type
+    try {
+      Type integer = em.integerType();
+      Expr x = em.mkVar("x", integer);
+      Expr invalidExpr = em.mkExpr(Kind.AND, x, x);
+      smt.checkSat(invalidExpr);
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Asking for a model after unsat result
+    try {
+      smt.checkSat(em.mkConst(false));
+      smt.getModel();
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+  }
+}
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
new file mode 100644
index 000000000..6e255c5b1
--- /dev/null
+++ b/examples/api/python/CMakeLists.txt
@@ -0,0 +1,27 @@
+set(EXAMPLES_API_PYTHON
+  exceptions
+)
+
+find_package(PythonInterp REQUIRED)
+
+# Find Python bindings in the corresponding python-*/site-packages directory.
+# Lookup Python module directory and store path in PYTHON_MODULE_PATH.
+execute_process(COMMAND
+                  ${PYTHON_EXECUTABLE} -c
+                    "from distutils.sysconfig import get_python_lib;\
+                     print(get_python_lib(plat_specific=True,\
+                             prefix='${CMAKE_PREFIX_PATH}/../..'))"
+                OUTPUT_VARIABLE PYTHON_MODULE_PATH
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+foreach(example ${EXAMPLES_API_PYTHON})
+  set(example_test example/api/python/${example})
+  add_test(
+    NAME ${example_test}
+    COMMAND
+      "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/api/python/${example}.py"
+  )
+  set_tests_properties(${example_test} PROPERTIES
+    LABELS "example"
+    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH})
+endforeach()
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
new file mode 100644
index 000000000..780f75bf7
--- /dev/null
+++ b/examples/api/python/exceptions.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python
+
+#####################
+## \file exceptions.py
+## \verbatim
+## Top contributors (to current version):
+##   Andres Noetzli
+## 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 Catching CVC4 exceptions with the legacy Python API.
+##
+## A simple demonstration of catching CVC4 execptions with the legacy Python
+## API.
+
+import CVC4
+import sys
+
+
+def main():
+    em = CVC4.ExprManager()
+    smt = CVC4.SmtEngine(em)
+
+    smt.setOption("produce-models", CVC4.SExpr("true"))
+
+    # Setting an invalid option
+    try:
+        smt.setOption("non-existing", CVC4.SExpr("true"))
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Creating a term with an invalid type
+    try:
+        integer = em.integerType()
+        x = em.mkVar("x", integer)
+        invalidExpr = em.mkExpr(CVC4.AND, x, x)
+        smt.checkSat(invalidExpr)
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Asking for a model after unsat result
+    try:
+        smt.checkSat(em.mkBoolConst(False))
+        smt.getModel()
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    return 0
+
+
+if __name__ == '__main__':
+    sys.exit(main())