Theory Reference: Sets and Relations

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Mudathir Mohamed, Andres Noetzli, Andrew Reynolds
  4 *
  5 * This file is part of the cvc5 project.
  6 *
  7 * Copyright (c) 2009-2024 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 * A simple demonstration of reasoning about relations with cvc5 via Java API.
 14 */
 15
 16import static io.github.cvc5.Kind.*;
 17
 18import io.github.cvc5.*;
 19
 20public class Relations
 21{
 22  public static void main(String[] args) throws CVC5ApiException
 23  {
 24    TermManager tm = new TermManager();
 25    Solver solver = new Solver(tm);
 26    {
 27      // Set the logic
 28      solver.setLogic("ALL");
 29
 30      // options
 31      solver.setOption("produce-models", "true");
 32      // we need finite model finding to answer sat problems with universal
 33      // quantified formulas
 34      solver.setOption("finite-model-find", "true");
 35      // we need sets extension to support set.universe operator
 36      solver.setOption("sets-exp", "true");
 37
 38      // (declare-sort Person 0)
 39      Sort personSort = tm.mkUninterpretedSort("Person");
 40
 41      // (Tuple Person)
 42      Sort tupleArity1 = tm.mkTupleSort(new Sort[] {personSort});
 43      // (Relation Person)
 44      Sort relationArity1 = tm.mkSetSort(tupleArity1);
 45
 46      // (Tuple Person Person)
 47      Sort tupleArity2 = tm.mkTupleSort(new Sort[] {personSort, personSort});
 48      // (Relation Person Person)
 49      Sort relationArity2 = tm.mkSetSort(tupleArity2);
 50
 51      // empty set
 52      Term emptySetTerm = tm.mkEmptySet(relationArity1);
 53
 54      // empty relation
 55      Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
 56
 57      // universe set
 58      Term universeSet = tm.mkUniverseSet(relationArity1);
 59
 60      // variables
 61      Term people = tm.mkConst(relationArity1, "people");
 62      Term males = tm.mkConst(relationArity1, "males");
 63      Term females = tm.mkConst(relationArity1, "females");
 64      Term father = tm.mkConst(relationArity2, "father");
 65      Term mother = tm.mkConst(relationArity2, "mother");
 66      Term parent = tm.mkConst(relationArity2, "parent");
 67      Term ancestor = tm.mkConst(relationArity2, "ancestor");
 68      Term descendant = tm.mkConst(relationArity2, "descendant");
 69
 70      Term isEmpty1 = tm.mkTerm(EQUAL, males, emptySetTerm);
 71      Term isEmpty2 = tm.mkTerm(EQUAL, females, emptySetTerm);
 72
 73      // (assert (= people (as set.universe (Relation Person))))
 74      Term peopleAreTheUniverse = tm.mkTerm(EQUAL, people, universeSet);
 75      // (assert (not (= males (as set.empty (Relation Person)))))
 76      Term maleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty1);
 77      // (assert (not (= females (as set.empty (Relation Person)))))
 78      Term femaleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty2);
 79
 80      // (assert (= (set.inter males females)
 81      //            (as set.empty (Relation Person))))
 82      Term malesFemalesIntersection = tm.mkTerm(SET_INTER, males, females);
 83      Term malesAndFemalesAreDisjoint = tm.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 84
 85      // (assert (not (= father (as set.empty (Relation Person Person)))))
 86      // (assert (not (= mother (as set.empty (Relation Person Person)))))
 87      Term isEmpty3 = tm.mkTerm(EQUAL, father, emptyRelationTerm);
 88      Term isEmpty4 = tm.mkTerm(EQUAL, mother, emptyRelationTerm);
 89      Term fatherIsNotEmpty = tm.mkTerm(NOT, isEmpty3);
 90      Term motherIsNotEmpty = tm.mkTerm(NOT, isEmpty4);
 91
 92      // fathers are males
 93      // (assert (set.subset (rel.join father people) males))
 94      Term fathers = tm.mkTerm(RELATION_JOIN, father, people);
 95      Term fathersAreMales = tm.mkTerm(SET_SUBSET, fathers, males);
 96
 97      // mothers are females
 98      // (assert (set.subset (rel.join mother people) females))
 99      Term mothers = tm.mkTerm(RELATION_JOIN, mother, people);
100      Term mothersAreFemales = tm.mkTerm(SET_SUBSET, mothers, females);
101
102      // (assert (= parent (set.union father mother)))
103      Term unionFatherMother = tm.mkTerm(SET_UNION, father, mother);
104      Term parentIsFatherOrMother = tm.mkTerm(EQUAL, parent, unionFatherMother);
105
106      // (assert (= ancestor (rel.tclosure parent)))
107      Term transitiveClosure = tm.mkTerm(RELATION_TCLOSURE, parent);
108      Term ancestorFormula = tm.mkTerm(EQUAL, ancestor, transitiveClosure);
109
110      // (assert (= descendant (rel.transpose ancestor)))
111      Term transpose = tm.mkTerm(RELATION_TRANSPOSE, ancestor);
112      Term descendantFormula = tm.mkTerm(EQUAL, descendant, transpose);
113
114      // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
115      Term x = tm.mkVar(personSort, "x");
116      Term xxTuple = tm.mkTuple(new Term[] {x, x});
117      Term member = tm.mkTerm(SET_MEMBER, xxTuple, ancestor);
118      Term notMember = tm.mkTerm(NOT, member);
119
120      Term quantifiedVariables = tm.mkTerm(VARIABLE_LIST, x);
121      Term noSelfAncestor = tm.mkTerm(FORALL, quantifiedVariables, notMember);
122
123      // formulas
124      solver.assertFormula(peopleAreTheUniverse);
125      solver.assertFormula(maleSetIsNotEmpty);
126      solver.assertFormula(femaleSetIsNotEmpty);
127      solver.assertFormula(malesAndFemalesAreDisjoint);
128      solver.assertFormula(fatherIsNotEmpty);
129      solver.assertFormula(motherIsNotEmpty);
130      solver.assertFormula(fathersAreMales);
131      solver.assertFormula(mothersAreFemales);
132      solver.assertFormula(parentIsFatherOrMother);
133      solver.assertFormula(descendantFormula);
134      solver.assertFormula(ancestorFormula);
135      solver.assertFormula(noSelfAncestor);
136
137      // check sat
138      Result result = solver.checkSat();
139
140      // output
141      System.out.println("Result     = " + result);
142      System.out.println("people     = " + solver.getValue(people));
143      System.out.println("males      = " + solver.getValue(males));
144      System.out.println("females    = " + solver.getValue(females));
145      System.out.println("father     = " + solver.getValue(father));
146      System.out.println("mother     = " + solver.getValue(mother));
147      System.out.println("parent     = " + solver.getValue(parent));
148      System.out.println("descendant = " + solver.getValue(descendant));
149      System.out.println("ancestor   = " + solver.getValue(ancestor));
150    }
151    Context.deletePointers();
152  }
153}