diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-16 00:18:48 +0000 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-15 17:18:48 -0700 |
commit | 62d361071ea54c9b7cba882313ab4dedef6f1286 (patch) | |
tree | 2e721a2fb77769a2824955a2b47fdf8b86203da3 /examples | |
parent | fc8907afc08d7b418471a537f9c23e9964df82df (diff) |
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<Expr>::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.
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/java/CMakeLists.txt | 2 | ||||
-rw-r--r-- | examples/api/java/Statistics.java | 45 | ||||
-rw-r--r-- | examples/api/java/UnsatCores.java | 54 |
3 files changed, 101 insertions, 0 deletions
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<Statistic>` 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<Expr>` interface. + System.out.println("--- Unsat Core ---"); + for (Expr e : unsatCore) { + System.out.println(e); + } + } +} |