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 * This file is part of the cvc5 project.
  3 *
  4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
  5 * in the top-level source directory and their institutional affiliations.
  6 * All rights reserved.  See the file COPYING in the top-level source
  7 * directory for licensing information.
  8 * ****************************************************************************
  9 *
 10 * A simple demonstration of reasoning about relations via the C++ API.
 11 */
 12
 13#include <cvc5/cvc5.h>
 14
 15#include <iostream>
 16
 17using namespace cvc5;
 18
 19int main()
 20{
 21  TermManager tm;
 22  Solver solver(tm);
 23
 24  // Set the logic
 25  solver.setLogic("ALL");
 26
 27  // options
 28  solver.setOption("produce-models", "true");
 29  // we need finite model finding to answer sat problems with universal
 30  // quantified formulas
 31  solver.setOption("finite-model-find", "true");
 32  // we need sets extension to support set.universe operator
 33  solver.setOption("sets-exp", "true");
 34
 35  // (declare-sort Person 0)
 36  Sort personSort = tm.mkUninterpretedSort("Person");
 37
 38  // (Tuple Person)
 39  Sort tupleArity1 = tm.mkTupleSort({personSort});
 40  // (Relation Person)
 41  Sort relationArity1 = tm.mkSetSort(tupleArity1);
 42
 43  // (Tuple Person Person)
 44  Sort tupleArity2 = tm.mkTupleSort({personSort, personSort});
 45  // (Relation Person Person)
 46  Sort relationArity2 = tm.mkSetSort(tupleArity2);
 47
 48  // empty set
 49  Term emptySetTerm = tm.mkEmptySet(relationArity1);
 50
 51  // empty relation
 52  Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
 53
 54  // universe set
 55  Term universeSet = tm.mkUniverseSet(relationArity1);
 56
 57  // variables
 58  Term people = tm.mkConst(relationArity1, "people");
 59  Term males = tm.mkConst(relationArity1, "males");
 60  Term females = tm.mkConst(relationArity1, "females");
 61  Term father = tm.mkConst(relationArity2, "father");
 62  Term mother = tm.mkConst(relationArity2, "mother");
 63  Term parent = tm.mkConst(relationArity2, "parent");
 64  Term ancestor = tm.mkConst(relationArity2, "ancestor");
 65  Term descendant = tm.mkConst(relationArity2, "descendant");
 66
 67  Term isEmpty1 = tm.mkTerm(Kind::EQUAL, {males, emptySetTerm});
 68  Term isEmpty2 = tm.mkTerm(Kind::EQUAL, {females, emptySetTerm});
 69
 70  // (assert (= people (as set.universe (Relation Person))))
 71  Term peopleAreTheUniverse = tm.mkTerm(Kind::EQUAL, {people, universeSet});
 72  // (assert (not (= males (as set.empty (Relation Person)))))
 73  Term maleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty1});
 74  // (assert (not (= females (as set.empty (Relation Person)))))
 75  Term femaleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty2});
 76
 77  // (assert (= (set.inter males females)
 78  //            (as set.empty (Relation Person))))
 79  Term malesFemalesIntersection = tm.mkTerm(Kind::SET_INTER, {males, females});
 80  Term malesAndFemalesAreDisjoint =
 81      tm.mkTerm(Kind::EQUAL, {malesFemalesIntersection, emptySetTerm});
 82
 83  // (assert (not (= father (as set.empty (Relation Person Person)))))
 84  // (assert (not (= mother (as set.empty (Relation Person Person)))))
 85  Term isEmpty3 = tm.mkTerm(Kind::EQUAL, {father, emptyRelationTerm});
 86  Term isEmpty4 = tm.mkTerm(Kind::EQUAL, {mother, emptyRelationTerm});
 87  Term fatherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty3});
 88  Term motherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty4});
 89
 90  // fathers are males
 91  // (assert (set.subset (rel.join father people) males))
 92  Term fathers = tm.mkTerm(Kind::RELATION_JOIN, {father, people});
 93  Term fathersAreMales = tm.mkTerm(Kind::SET_SUBSET, {fathers, males});
 94
 95  // mothers are females
 96  // (assert (set.subset (rel.join mother people) females))
 97  Term mothers = tm.mkTerm(Kind::RELATION_JOIN, {mother, people});
 98  Term mothersAreFemales = tm.mkTerm(Kind::SET_SUBSET, {mothers, females});
 99
100  // (assert (= parent (set.union father mother)))
101  Term unionFatherMother = tm.mkTerm(Kind::SET_UNION, {father, mother});
102  Term parentIsFatherOrMother =
103      tm.mkTerm(Kind::EQUAL, {parent, unionFatherMother});
104
105  // (assert (= ancestor (rel.tclosure parent)))
106  Term transitiveClosure = tm.mkTerm(Kind::RELATION_TCLOSURE, {parent});
107  Term ancestorFormula = tm.mkTerm(Kind::EQUAL, {ancestor, transitiveClosure});
108
109  // (assert (= descendant (rel.transpose descendant)))
110  Term transpose = tm.mkTerm(Kind::RELATION_TRANSPOSE, {ancestor});
111  Term descendantFormula = tm.mkTerm(Kind::EQUAL, {descendant, transpose});
112
113  // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
114  Term x = tm.mkVar(personSort, "x");
115  Term xxTuple = tm.mkTuple({x, x});
116  Term member = tm.mkTerm(Kind::SET_MEMBER, {xxTuple, ancestor});
117  Term notMember = tm.mkTerm(Kind::NOT, {member});
118
119  Term quantifiedVariables = tm.mkTerm(Kind::VARIABLE_LIST, {x});
120  Term noSelfAncestor =
121      tm.mkTerm(Kind::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  std::cout << "Result     = " << result << std::endl;
142  std::cout << "people     = " << solver.getValue(people) << std::endl;
143  std::cout << "males      = " << solver.getValue(males) << std::endl;
144  std::cout << "females    = " << solver.getValue(females) << std::endl;
145  std::cout << "father     = " << solver.getValue(father) << std::endl;
146  std::cout << "mother     = " << solver.getValue(mother) << std::endl;
147  std::cout << "parent     = " << solver.getValue(parent) << std::endl;
148  std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
149  std::cout << "ancestor   = " << solver.getValue(ancestor) << std::endl;
150}