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}