Merge branch 'master' into splitEqRew

1 files changed, 45 insertions, 0 deletions

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());
+    }
+  }
+}