cvc5/examples/api/java/Statistics.java

/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * An example of accessing CVC4's statistics using the Java API.
 */

import edu.stanford.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.stanford.CVC4.Statistics stats = smt.getStatistics();
    for (Statistic stat : stats) {
      System.out.println(stat.getFirst() + " = " + stat.getSecond());
    }
  }
}