diff options
Diffstat (limited to 'examples/api/java/Statistics.java')
| -rw-r--r-- | examples/api/java/Statistics.java | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 7db7cc4f3..635be65f6 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * An example of accessing CVC4's statistics using the Java API. + * An example of accessing cvc5's statistics using the Java API. */ import static io.github.cvc5.api.Kind.*; @@ -158,52 +158,52 @@ public class Statistics Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm); Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm); - // (assert (= people (as univset (Set (Tuple Person))))) + // (assert (= people (as set.universe (Set (Tuple Person))))) Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); - // (assert (not (= males (as emptyset (Set (Tuple Person)))))) + // (assert (not (= males (as set.empty (Set (Tuple Person)))))) Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); - // (assert (not (= females (as emptyset (Set (Tuple Person)))))) + // (assert (not (= females (as set.empty (Set (Tuple Person)))))) Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); - // (assert (= (intersection males females) (as emptyset (Set (Tuple + // (assert (= (set.inter males females) (as set.empty (Set (Tuple // Person))))) - Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females); + Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females); Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); - // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) - // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) + // (assert (not (= father (as set.empty (Set (Tuple Person Person)))))) + // (assert (not (= mother (as set.empty (Set (Tuple Person Person)))))) Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm); Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm); Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3); Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4); // fathers are males - // (assert (subset (join father people) males)) - Term fathers = solver.mkTerm(JOIN, father, people); - Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males); + // (assert (set.subset (rel.join father people) males)) + Term fathers = solver.mkTerm(RELATION_JOIN, father, people); + Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males); // mothers are females - // (assert (subset (join mother people) females)) - Term mothers = solver.mkTerm(JOIN, mother, people); - Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females); + // (assert (set.subset (rel.join mother people) females)) + Term mothers = solver.mkTerm(RELATION_JOIN, mother, people); + Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females); - // (assert (= parent (union father mother))) - Term unionFatherMother = solver.mkTerm(UNION, father, mother); + // (assert (= parent (set.union father mother))) + Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother); Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); - // (assert (= parent (union father mother))) - Term transitiveClosure = solver.mkTerm(TCLOSURE, parent); + // (assert (= descendant (rel.tclosure parent))) + Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent); Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure); - // (assert (= parent (union father mother))) - Term transpose = solver.mkTerm(TRANSPOSE, descendant); + // (assert (= ancestor (rel.transpose descendant))) + Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant); Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); - // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) + // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor)))) Term var = solver.mkVar(personSort, "x"); DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var); - Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); + Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var); |