Theory of Relations

This simple example demonstrates the combined theory of finite sets and finite relations using a family tree. Relations are defined as sets of tuples with arity \(\geq 1\). The example includes the unary relations \(people, males,\) and \(females\) and the binary relations \(father, mother, parent, ancestor\), and \(descendant\).

We have the following list of constraints:

  • All relations are nonempty.

  • People is the universe set.

  • Males and females are disjoint sets (i.e., \(males \cap females = \phi\)).

  • Fathers are males (i.e., \(father \bowtie people \subseteq males\)) [*].

  • Mothers are females (i.e., \(mother \bowtie people \subseteq females\)).

  • A parent is a father or a mother (i.e., \(parent = father \cup mother\)).

  • Ancestor relation is the transitive closure of parent (i.e., \(ancestor = parent^{+}\)).

  • Descendant relation is the transpose of ancestor (i.e., \(descendant = ancestor^{-1}\)).

  • No self ancestor (i.e., \(\forall x: Person. \langle x, x \rangle \not\in ancestor\)).

examples/api/cpp/relations.cpp

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Mudathir Mohamed, Aina Niemetz, Mathias Preiner
  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 via the C++ API.
 14 */
 15
 16#include <cvc5/cvc5.h>
 17
 18#include <iostream>
 19
 20using namespace cvc5;
 21
 22int main()
 23{
 24  TermManager tm;
 25  Solver 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({personSort});
 43  // (Relation Person)
 44  Sort relationArity1 = tm.mkSetSort(tupleArity1);
 45
 46  // (Tuple Person Person)
 47  Sort tupleArity2 = tm.mkTupleSort({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(Kind::EQUAL, {males, emptySetTerm});
 71  Term isEmpty2 = tm.mkTerm(Kind::EQUAL, {females, emptySetTerm});
 72
 73  // (assert (= people (as set.universe (Relation Person))))
 74  Term peopleAreTheUniverse = tm.mkTerm(Kind::EQUAL, {people, universeSet});
 75  // (assert (not (= males (as set.empty (Relation Person)))))
 76  Term maleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty1});
 77  // (assert (not (= females (as set.empty (Relation Person)))))
 78  Term femaleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty2});
 79
 80  // (assert (= (set.inter males females)
 81  //            (as set.empty (Relation Person))))
 82  Term malesFemalesIntersection = tm.mkTerm(Kind::SET_INTER, {males, females});
 83  Term malesAndFemalesAreDisjoint =
 84      tm.mkTerm(Kind::EQUAL, {malesFemalesIntersection, emptySetTerm});
 85
 86  // (assert (not (= father (as set.empty (Relation Person Person)))))
 87  // (assert (not (= mother (as set.empty (Relation Person Person)))))
 88  Term isEmpty3 = tm.mkTerm(Kind::EQUAL, {father, emptyRelationTerm});
 89  Term isEmpty4 = tm.mkTerm(Kind::EQUAL, {mother, emptyRelationTerm});
 90  Term fatherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty3});
 91  Term motherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty4});
 92
 93  // fathers are males
 94  // (assert (set.subset (rel.join father people) males))
 95  Term fathers = tm.mkTerm(Kind::RELATION_JOIN, {father, people});
 96  Term fathersAreMales = tm.mkTerm(Kind::SET_SUBSET, {fathers, males});
 97
 98  // mothers are females
 99  // (assert (set.subset (rel.join mother people) females))
100  Term mothers = tm.mkTerm(Kind::RELATION_JOIN, {mother, people});
101  Term mothersAreFemales = tm.mkTerm(Kind::SET_SUBSET, {mothers, females});
102
103  // (assert (= parent (set.union father mother)))
104  Term unionFatherMother = tm.mkTerm(Kind::SET_UNION, {father, mother});
105  Term parentIsFatherOrMother =
106      tm.mkTerm(Kind::EQUAL, {parent, unionFatherMother});
107
108  // (assert (= ancestor (rel.tclosure parent)))
109  Term transitiveClosure = tm.mkTerm(Kind::RELATION_TCLOSURE, {parent});
110  Term ancestorFormula = tm.mkTerm(Kind::EQUAL, {ancestor, transitiveClosure});
111
112  // (assert (= descendant (rel.transpose descendant)))
113  Term transpose = tm.mkTerm(Kind::RELATION_TRANSPOSE, {ancestor});
114  Term descendantFormula = tm.mkTerm(Kind::EQUAL, {descendant, transpose});
115
116  // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
117  Term x = tm.mkVar(personSort, "x");
118  Term xxTuple = tm.mkTuple({x, x});
119  Term member = tm.mkTerm(Kind::SET_MEMBER, {xxTuple, ancestor});
120  Term notMember = tm.mkTerm(Kind::NOT, {member});
121
122  Term quantifiedVariables = tm.mkTerm(Kind::VARIABLE_LIST, {x});
123  Term noSelfAncestor =
124      tm.mkTerm(Kind::FORALL, {quantifiedVariables, notMember});
125
126  // formulas
127  solver.assertFormula(peopleAreTheUniverse);
128  solver.assertFormula(maleSetIsNotEmpty);
129  solver.assertFormula(femaleSetIsNotEmpty);
130  solver.assertFormula(malesAndFemalesAreDisjoint);
131  solver.assertFormula(fatherIsNotEmpty);
132  solver.assertFormula(motherIsNotEmpty);
133  solver.assertFormula(fathersAreMales);
134  solver.assertFormula(mothersAreFemales);
135  solver.assertFormula(parentIsFatherOrMother);
136  solver.assertFormula(descendantFormula);
137  solver.assertFormula(ancestorFormula);
138  solver.assertFormula(noSelfAncestor);
139
140  // check sat
141  Result result = solver.checkSat();
142
143  // output
144  std::cout << "Result     = " << result << std::endl;
145  std::cout << "people     = " << solver.getValue(people) << std::endl;
146  std::cout << "males      = " << solver.getValue(males) << std::endl;
147  std::cout << "females    = " << solver.getValue(females) << std::endl;
148  std::cout << "father     = " << solver.getValue(father) << std::endl;
149  std::cout << "mother     = " << solver.getValue(mother) << std::endl;
150  std::cout << "parent     = " << solver.getValue(parent) << std::endl;
151  std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
152  std::cout << "ancestor   = " << solver.getValue(ancestor) << std::endl;
153}