mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
c1f8d64f3b
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.
57 lines
1.6 KiB
Java
57 lines
1.6 KiB
Java
/********************* */
|
|
/*! \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());
|
|
}
|
|
}
|
|
}
|