examples/api/java/Statistics.java

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * An example of accessing cvc5's statistics using the Java API.
  14  */
  15
  16 import static io.github.cvc5.Kind.*;
  17
  18 import io.github.cvc5.*;
  19 import java.util.List;
  20 import java.util.Map;
  21
  22 public class Statistics
  23 {
  24   public static void main(String[] args)
  25   {
  26     try (Solver solver = new Solver())
  27     {
  28       // Get the statistics from the `Solver` and iterate over them. The
  29       // `Statistics` class implements the `Iterable<Pair<String, Stat>>` interface.
  30       io.github.cvc5.Statistics stats = solver.getStatistics();
  31       // short version
  32       System.out.println("Short version:");
  33       System.out.println(stats);
  34
  35       System.out.println("-------------------------------------------------------");
  36
  37       System.out.println("Long version:");
  38
  39       // long version
  40       for (Map.Entry<String, Stat> pair : stats)
  41       {
  42         Stat stat = pair.getValue();
  43         if (stat.isInt())
  44         {
  45           System.out.println(pair.getKey() + " = " + stat.getInt());
  46         }
  47         else if (stat.isDouble())
  48         {
  49           System.out.println(pair.getKey() + " = " + stat.getDouble());
  50         }
  51         else if (stat.isString())
  52         {
  53           System.out.println(pair.getKey() + " = " + stat.getString());
  54         }
  55         else if (stat.isHistogram())
  56         {
  57           System.out.println("-------------------------------------------------------");
  58           System.out.println(pair.getKey() + " : Map");
  59           for (Map.Entry<String, Long> entry : stat.getHistogram().entrySet())
  60           {
  61             System.out.println(entry.getKey() + " = " + entry.getValue());
  62           }
  63           System.out.println("-------------------------------------------------------");
  64         }
  65       }
  66     }
  67   }
  68
  69   private static Solver getSolver()
  70   {
  71     Solver solver = new Solver();
  72
  73     // String type
  74     Sort string = solver.getStringSort();
  75
  76     // std::string
  77     String str_ab = "ab";
  78     // String constants
  79     Term ab = solver.mkString(str_ab);
  80     Term abc = solver.mkString("abc");
  81     // String variables
  82     Term x = solver.mkConst(string, "x");
  83     Term y = solver.mkConst(string, "y");
  84     Term z = solver.mkConst(string, "z");
  85
  86     // String concatenation: x.ab.y
  87     Term lhs = solver.mkTerm(STRING_CONCAT, x, ab, y);
  88     // String concatenation: abc.z
  89     Term rhs = solver.mkTerm(STRING_CONCAT, abc, z);
  90     // x.ab.y = abc.z
  91     Term formula1 = solver.mkTerm(EQUAL, lhs, rhs);
  92
  93     // Length of y: |y|
  94     Term leny = solver.mkTerm(STRING_LENGTH, y);
  95     // |y| >= 0
  96     Term formula2 = solver.mkTerm(GEQ, leny, solver.mkInteger(0));
  97
  98     // Regular expression: (ab[c-e]*f)|g|h
  99     Term r = solver.mkTerm(REGEXP_UNION,
 100         solver.mkTerm(REGEXP_CONCAT,
 101             solver.mkTerm(STRING_TO_REGEXP, solver.mkString("ab")),
 102             solver.mkTerm(REGEXP_STAR,
 103                 solver.mkTerm(REGEXP_RANGE, solver.mkString("c"), solver.mkString("e"))),
 104             solver.mkTerm(STRING_TO_REGEXP, solver.mkString("f"))),
 105         solver.mkTerm(STRING_TO_REGEXP, solver.mkString("g")),
 106         solver.mkTerm(STRING_TO_REGEXP, solver.mkString("h")));
 107
 108     // String variables
 109     Term s1 = solver.mkConst(string, "s1");
 110     Term s2 = solver.mkConst(string, "s2");
 111     // String concatenation: s1.s2
 112     Term s = solver.mkTerm(STRING_CONCAT, s1, s2);
 113
 114     // s1.s2 in (ab[c-e]*f)|g|h
 115     Term formula3 = solver.mkTerm(STRING_IN_REGEXP, s, r);
 116
 117     // Make a query
 118     Term q = solver.mkTerm(AND, formula1, formula2, formula3);
 119
 120     // options
 121     solver.setOption("produce-models", "true");
 122     solver.setOption("finite-model-find", "true");
 123     solver.setOption("sets-ext", "true");
 124     solver.setOption("output-language", "smt2");
 125
 126     // (declare-sort Person 0)
 127     Sort personSort = solver.mkUninterpretedSort("Person");
 128
 129     // (Tuple Person)
 130     Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
 131     // (Set (Tuple Person))
 132     Sort relationArity1 = solver.mkSetSort(tupleArity1);
 133
 134     // (Tuple Person Person)
 135     Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
 136     // (Set (Tuple Person Person))
 137     Sort relationArity2 = solver.mkSetSort(tupleArity2);
 138
 139     // empty set
 140     Term emptySetTerm = solver.mkEmptySet(relationArity1);
 141
 142     // empty relation
 143     Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
 144
 145     // universe set
 146     Term universeSet = solver.mkUniverseSet(relationArity1);
 147
 148     // variables
 149     Term people = solver.mkConst(relationArity1, "people");
 150     Term males = solver.mkConst(relationArity1, "males");
 151     Term females = solver.mkConst(relationArity1, "females");
 152     Term father = solver.mkConst(relationArity2, "father");
 153     Term mother = solver.mkConst(relationArity2, "mother");
 154     Term parent = solver.mkConst(relationArity2, "parent");
 155     Term ancestor = solver.mkConst(relationArity2, "ancestor");
 156     Term descendant = solver.mkConst(relationArity2, "descendant");
 157
 158     Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
 159     Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
 160
 161     // (assert (= people (as set.universe (Set (Tuple Person)))))
 162     Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
 163     // (assert (not (= males (as set.empty (Set (Tuple Person))))))
 164     Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
 165     // (assert (not (= females (as set.empty (Set (Tuple Person))))))
 166     Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 167
 168     // (assert (= (set.inter males females) (as set.empty (Set (Tuple
 169     // Person)))))
 170     Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
 171     Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 172
 173     // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
 174     // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
 175     Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
 176     Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
 177     Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
 178     Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
 179
 180     // fathers are males
 181     // (assert (set.subset (rel.join father people) males))
 182     Term fathers = solver.mkTerm(RELATION_JOIN, father, people);
 183     Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males);
 184
 185     // mothers are females
 186     // (assert (set.subset (rel.join mother people) females))
 187     Term mothers = solver.mkTerm(RELATION_JOIN, mother, people);
 188     Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females);
 189
 190     // (assert (= parent (set.union father mother)))
 191     Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
 192     Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
 193
 194     // (assert (= descendant (rel.tclosure parent)))
 195     Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
 196     Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
 197
 198     // (assert (= ancestor (rel.transpose descendant)))
 199     Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant);
 200     Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
 201
 202     // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor))))
 203     Term var = solver.mkVar(personSort, "x");
 204     DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
 205     Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getTerm(), var, var);
 206     Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
 207     Term notMember = solver.mkTerm(NOT, member);
 208
 209     Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var);
 210     Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
 211
 212     // formulas
 213     solver.assertFormula(peopleAreTheUniverse);
 214     solver.assertFormula(maleSetIsNotEmpty);
 215     solver.assertFormula(femaleSetIsNotEmpty);
 216     solver.assertFormula(malesAndFemalesAreDisjoint);
 217     solver.assertFormula(fatherIsNotEmpty);
 218     solver.assertFormula(motherIsNotEmpty);
 219     solver.assertFormula(fathersAreMales);
 220     solver.assertFormula(mothersAreFemales);
 221     solver.assertFormula(parentIsFatherOrMother);
 222     solver.assertFormula(descendantFormula);
 223     solver.assertFormula(ancestorFormula);
 224     solver.assertFormula(noSelfAncestor);
 225
 226     // check sat
 227     solver.checkSatAssuming(q);
 228
 229     return solver;
 230   }
 231 }