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\) ).

*

\(\bowtie\) denotes the relational join operator as defined in [ MRTB17 ] .

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 
 20 using namespace cvc5;
 21 
 22 int 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   // (Set (Tuple Person))
 43   Sort relationArity1 = solver.mkSetSort(tupleArity1);
 44 
 45   // (Tuple Person Person)
 46   Sort tupleArity2 = solver.mkTupleSort({personSort, personSort});
 47   // (Set (Tuple 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 (Set (Tuple Person)))))
 73   Term peopleAreTheUniverse = solver.mkTerm(EQUAL, {people, universeSet});
 74   // (assert (not (= males (as set.empty (Set (Tuple Person))))))
 75   Term maleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty1});
 76   // (assert (not (= females (as set.empty (Set (Tuple Person))))))
 77   Term femaleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty2});
 78 
 79   // (assert (= (set.inter males females)
 80   //            (as set.empty (Set (Tuple 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 (Set (Tuple Person Person))))))
 86   // (assert (not (= mother (as set.empty (Set (Tuple 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({personSort, personSort}, {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 }