From 62d361071ea54c9b7cba882313ab4dedef6f1286 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 16 May 2019 00:18:48 +0000 Subject: [PATCH] Fix iterators in Java API (#3000) Fixes #2989. SWIG 3 seems to have an issue properly resolving `T::const_iterator::value_type` if that type itself is a `typedef`. This is for example the case in the `UnsatCore` class, which `typedef`s `const_iterator` to `std::vector::const_iterator`. As a workaround, this commit changes the `JavaIteratorAdapter` class to take two template parameters, one of which is the `value_type`. The commit also adds a compile-time assertion that `T::const_iterator::value_type` can be converted to `value_type` to avoid nasty surprises. A nice side-effect of this solution is that explicit `typemap`s are not necessary anymore, so they are removed. Additionally, the commit adds a `toString()` method for the Java API of `UnsatCore` and adds examples that show and test the iteration over the unsat core and the statistics. Iterating over `Statistics` now returns instances of `Statistic` instead of `Object[]`, which is a bit cleaner and requires less glue code. --- examples/api/java/CMakeLists.txt | 2 ++ examples/api/java/Statistics.java | 45 +++++++++++++++++++++++ examples/api/java/UnsatCores.java | 54 ++++++++++++++++++++++++++++ src/bindings/java/CMakeLists.txt | 1 + src/bindings/java_iterator_adapter.h | 38 +++++++++++--------- src/expr/datatype.i | 45 +++++++++++------------ src/expr/expr.i | 21 +++++------ src/proof/unsat_core.i | 31 ++++++++-------- src/smt/command.i | 22 +++++------- src/util/statistics.i | 46 +++++++++++------------- 10 files changed, 199 insertions(+), 106 deletions(-) create mode 100644 examples/api/java/Statistics.java create mode 100644 examples/api/java/UnsatCores.java diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 76a55151e..108ab8614 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -12,7 +12,9 @@ set(EXAMPLES_API_JAVA LinearArith ## disabled until bindings for the new API are in place (issue #2284) #PipedInput + Statistics Strings + UnsatCores ) foreach(example ${EXAMPLES_API_JAVA}) diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java new file mode 100644 index 000000000..0dda91aee --- /dev/null +++ b/examples/api/java/Statistics.java @@ -0,0 +1,45 @@ +/********************* */ +/*! \file Statistics.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 An example of accessing CVC4's statistics using the Java API + ** + ** An example of accessing CVC4's statistics using the Java API. + **/ + +import edu.nyu.acsys.CVC4.*; +import java.util.Iterator; + +public class Statistics { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + Type boolType = em.booleanType(); + Expr a = em.mkVar("A", boolType); + Expr b = em.mkVar("B", boolType); + + // A ^ B + smt.assertFormula(em.mkExpr(Kind.AND, a, b)); + + Result res = smt.checkSat(); + + // Get the statistics from the `SmtEngine` and iterate over them. The + // `Statistics` class implements the `Iterable` interface. A + // `Statistic` is a pair that consists of a name and an `SExpr` that stores + // the value of the statistic. + edu.nyu.acsys.CVC4.Statistics stats = smt.getStatistics(); + for (Statistic stat : stats) { + System.out.println(stat.getFirst() + " = " + stat.getSecond()); + } + } +} diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java new file mode 100644 index 000000000..65c01cf5a --- /dev/null +++ b/examples/api/java/UnsatCores.java @@ -0,0 +1,54 @@ +/********************* */ +/*! \file UnsatCore.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 An example of interacting with unsat cores using CVC4's Java API + ** + ** An example of interacting with unsat cores using CVC4's Java API. + **/ + +import edu.nyu.acsys.CVC4.*; +import java.util.Iterator; + +public class UnsatCores { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + // Enable the production of unsat cores + smt.setOption("produce-unsat-cores", new SExpr(true)); + + Type boolType = em.booleanType(); + Expr a = em.mkVar("A", boolType); + Expr b = em.mkVar("B", boolType); + + // A ^ B + smt.assertFormula(em.mkExpr(Kind.AND, a, b)); + // ~(A v B) + smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.OR, a, b))); + + Result res = smt.checkSat(); // result is unsat + + // Retrieve the unsat core + UnsatCore unsatCore = smt.getUnsatCore(); + + // Print the unsat core + System.out.println("Unsat Core: " + unsatCore); + + // Iterate over expressions in the unsat core. The `UnsatCore` class + // implements the `Iterable` interface. + System.out.println("--- Unsat Core ---"); + for (Expr e : unsatCore) { + System.out.println(e); + } + } +} diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 573c2ee91..7b7d93f1d 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -165,6 +165,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java + ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h index bf1b22e1b..270fe7baa 100644 --- a/src/bindings/java_iterator_adapter.h +++ b/src/bindings/java_iterator_adapter.h @@ -30,30 +30,36 @@ #ifndef CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H #define CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H -namespace CVC4 { +#include -template -class JavaIteratorAdapter { - const T& d_t; - typename T::const_iterator d_it; +namespace CVC4 { -public: - JavaIteratorAdapter(const T& t) : - d_t(t), - d_it(d_t.begin()) { +template +class JavaIteratorAdapter +{ + public: + JavaIteratorAdapter(const T& t) : d_t(t), d_it(d_t.begin()) + { + static_assert( + std::is_convertible(), + "value_type must be convertible from T::const_iterator::value_type"); } - bool hasNext() { - return d_it != d_t.end(); - } + bool hasNext() { return d_it != d_t.end(); } - typename T::const_iterator::value_type getNext() { - typename T::const_iterator::value_type ret = *d_it; + value_type getNext() + { + value_type ret = *d_it; ++d_it; return ret; } -};/* class JavaIteratorAdapter */ -}/* CVC4 namespace */ + private: + const T& d_t; + typename T::const_iterator d_it; +}; /* class JavaIteratorAdapter */ + +} // namespace CVC4 #endif /* CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */ diff --git a/src/expr/datatype.i b/src/expr/datatype.i index a903e0241..6bd5eb82c 100644 --- a/src/expr/datatype.i +++ b/src/expr/datatype.i @@ -95,8 +95,11 @@ // iterator() method on the Java side that returns a Java-style // Iterator. %extend CVC4::Datatype { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter + iterator() + { + return CVC4::JavaIteratorAdapter( + *$self); } std::string toString() const { @@ -106,8 +109,12 @@ } } %extend CVC4::DatatypeConstructor { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter + iterator() + { + return CVC4::JavaIteratorAdapter(*$self); } std::string toString() const { @@ -129,12 +136,12 @@ %typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable"; // the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; // add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter " public void remove() { throw new java.lang.UnsupportedOperationException(); } @@ -147,7 +154,7 @@ } } " -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter " public void remove() { throw new java.lang.UnsupportedOperationException(); } @@ -161,18 +168,8 @@ } " // getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately. -%typemap(jni) CVC4::Datatype::iterator::value_type "jobject"; -%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; -%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; -%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; } -%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject"; -%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; -%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; -%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; } +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; #endif /* SWIGJAVA */ @@ -183,7 +180,7 @@ %include "bindings/java_iterator_adapter.h" %include "bindings/java_stream_adapters.h" -%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter; -%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter; +%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter; +%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter; #endif /* SWIGJAVA */ diff --git a/src/expr/expr.i b/src/expr/expr.i index 1d5207c93..b172f60ed 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -92,8 +92,9 @@ namespace CVC4 { %ignore CVC4::Expr::begin() const; %ignore CVC4::Expr::end() const; %extend CVC4::Expr { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter iterator() + { + return CVC4::JavaIteratorAdapter(*$self); } } @@ -101,10 +102,10 @@ namespace CVC4 { %typemap(javainterfaces) CVC4::Expr "java.lang.Iterable"; // the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; // add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter " public void remove() { throw new java.lang.UnsupportedOperationException(); } @@ -118,13 +119,7 @@ namespace CVC4 { } " // getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::Expr::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; -%typemap(jstype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; -%typemap(javaout) CVC4::Expr::const_iterator::value_type { return $jnicall; } +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; #endif /* SWIGJAVA */ @@ -161,7 +156,7 @@ namespace CVC4 { %include "bindings/java_iterator_adapter.h" %include "bindings/java_stream_adapters.h" -%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter; +%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter; #endif /* SWIGJAVA */ diff --git a/src/proof/unsat_core.i b/src/proof/unsat_core.i index cee78da06..d3fd615ce 100644 --- a/src/proof/unsat_core.i +++ b/src/proof/unsat_core.i @@ -21,8 +21,16 @@ %ignore CVC4::UnsatCore::begin() const; %ignore CVC4::UnsatCore::end() const; %extend CVC4::UnsatCore { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter iterator() + { + return CVC4::JavaIteratorAdapter(*$self); + } + + std::string toString() + { + std::stringstream ss; + ss << (*$self); + return ss.str(); } } @@ -30,10 +38,10 @@ %typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable"; // the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; // add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter " public void remove() { throw new java.lang.UnsupportedOperationException(); } @@ -47,13 +55,7 @@ } " // getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::UnsatCore::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::UnsatCore::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; -%typemap(jstype) CVC4::UnsatCore::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; -%typemap(javaout) CVC4::UnsatCore::const_iterator::value_type { return $jnicall; } +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; #endif /* SWIGJAVA */ @@ -61,9 +63,10 @@ #ifdef SWIGJAVA +%include + %include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" -%template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter; +%template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter; #endif /* SWIGJAVA */ diff --git a/src/smt/command.i b/src/smt/command.i index 32bda7bba..ff8094165 100644 --- a/src/smt/command.i +++ b/src/smt/command.i @@ -28,8 +28,10 @@ %ignore CVC4::CommandSequence::begin() const; %ignore CVC4::CommandSequence::end() const; %extend CVC4::CommandSequence { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter iterator() + { + return CVC4::JavaIteratorAdapter( + *$self); } } @@ -37,10 +39,10 @@ %typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable"; // the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; // add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter " public void remove() { throw new java.lang.UnsupportedOperationException(); } @@ -54,13 +56,7 @@ } " // getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; #endif /* SWIGJAVA */ @@ -71,6 +67,6 @@ %include "bindings/java_iterator_adapter.h" %include "bindings/java_stream_adapters.h" -%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter; +%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter; #endif /* SWIGJAVA */ diff --git a/src/util/statistics.i b/src/util/statistics.i index 9ff6757d8..8d1086dcc 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -4,7 +4,6 @@ #ifdef SWIGJAVA #include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" #endif /* SWIGJAVA */ %} @@ -24,24 +23,29 @@ %ignore CVC4::StatisticsBase::begin() const; %ignore CVC4::StatisticsBase::end() const; %extend CVC4::StatisticsBase { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); + CVC4::JavaIteratorAdapter > + iterator() + { + return CVC4::JavaIteratorAdapter >( + *$self); } } // StatisticsBase is "iterable" on the Java side -%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable"; +%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable"; // the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter > "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter > "java.util.Iterator"; // add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " +%typemap(javacode) CVC4::JavaIteratorAdapter > " public void remove() { throw new java.lang.UnsupportedOperationException(); } - public Object[] next() { + public Statistic next() { if(hasNext()) { return getNext(); } else { @@ -50,22 +54,7 @@ } " // getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately. for statistics, the "payload" of the iterator is an Object[]. -// These Object arrays are always of two elements, the first is a String and the second an -// SExpr. (On the C++ side, it is a std::pair.) -%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray"; -%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; -%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; -%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; } -%typemap(out) CVC4::StatisticsBase::const_iterator::value_type { - $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); - jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); - jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"); - jmethodID methodid = jenv->GetMethodID(clazz, "", "(JZ)V"); - jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast(new CVC4::SExpr($1.second)), true)); - }; +%javamethodmodifiers CVC4::JavaIteratorAdapter >::getNext() "private"; #endif /* SWIGJAVA */ @@ -73,9 +62,14 @@ #ifdef SWIGJAVA +%include +%include +%include + %include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" +%include "util/sexpr.h" -%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter; +%template(Statistic) std::pair; +%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter >; #endif /* SWIGJAVA */ -- 2.30.2