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-ext", "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}