diff options
Diffstat (limited to 'examples/api/java/Statistics.java')
-rw-r--r-- | examples/api/java/Statistics.java | 45 |
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()); + } + } +} |