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