Add relations.cpp, relations.py examples (#7801)

9 files changed, 380 insertions, 98 deletions

diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst
index a1a0541f7..85d3977fa 100644
--- a/docs/examples/relations.rst
+++ b/docs/examples/relations.rst
@@ -1,8 +1,30 @@
 Theory of Relations
 ===================
 
+This simple example demonstrates the combined
+`theory of finite sets and finite relations <../theories/sets-and-relations.html>`_ using a family tree.
+Relations are defined as sets of tuples with arity :math:`\geq 1`.
+The example includes the unary relations :math:`people, males,` and  :math:`females`
+and the binary relations :math:`father, mother, parent, ancestor`, and :math:`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., :math:`males \cap females = \phi`).
+- Fathers are males (i.e., :math:`father \bowtie people \subseteq males`) [*]_.
+- Mothers are females (i.e., :math:`mother \bowtie people \subseteq females`).
+- A parent is a father or a mother (i.e., :math:`parent = father \cup mother`).
+- Ancestor relation is the transitive closure of parent (i.e., :math:`ancestor = parent^{+}`).
+- Descendant relation is the transpose of ancestor (i.e., :math:`descendant = ancestor^{-1}`).
+- No self ancestor (i.e., :math:`\forall x: Person. \langle x, x \rangle \not\in ancestor`).
+
+.. [*] :math:`\bowtie` denotes the relational join operator as defined in :cite:`MengRTB17`.
 
 .. api-examples::
+    <examples>/api/cpp/relations.cpp
     <examples>/api/java/Relations.java
+    <examples>/api/python/relations.py
     <examples>/api/smtlib/relations.smt2
 
diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 33c0d4cd0..8dd76dbfb 100644
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -167,19 +167,13 @@ More details can be found in :cite:`MengRTB17`.
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 |                      | ``(declare-const t (Tuple Int Int))``        | ``Sort s_int = solver.getIntegerSort();``                                          |
 |                      |                                              |                                                                                    |
-|                      |                                              | ``Sort s = solver.mkTypleSort({s_int, s_int});``                                   |
+|                      |                                              | ``Sort s = solver.mkTupleSort({s_int, s_int});``                                   |
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Term t = solver.mkConst(s, "t");``                                               |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Tuple Constructor    | ``(mkTuple <Term_1>, ..., <Term_n>)``        | ``Sort s = solver.mkTypleSort(sorts);``                                            |
-|                      |                                              |                                                                                    |
-|                      |                                              | ``Datatype dt = s.getDatatype();``                                                 |
-|                      |                                              |                                                                                    |
-|                      |                                              | ``Term c = dt[0].getConstructor();``                                               |
-|                      |                                              |                                                                                    |
-|                      |                                              | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
+| Tuple Constructor    | ``(tuple <Term_1>, ..., <Term_n>)``          | ``Term t = solver.mkTuple({<Sort_1>, ..., <Sort_n>}, {Term_1>, ..., <Term_n>});``  |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Tuple Selector       | ``((_ tupSel i) t)``                         | ``Sort s = solver.mkTypleSort(sorts);``                                            |
+| Tuple Selector       | ``((_ tuple_select i) t)``                         | ``Sort s = solver.mkTupleSort(sorts);``                                            |
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Datatype dt = s.getDatatype();``                                                 |
 |                      |                                              |                                                                                    |
@@ -187,7 +181,7 @@ More details can be found in :cite:`MengRTB17`.
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});``                          |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Reation Sort         | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    | ``Sort s = solver.mkSetSort(cvc5::api::Sort tupleSort);``                          |
+| Relation Sort        | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    | ``Sort s = solver.mkSetSort(cvc5::api::Sort tupleSort);``                          |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Constants            | ``(declare-const X (Set (Tuple Int Int)``    | ``Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});``                  |
 |                      |                                              |                                                                                    |
diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
index 5f3298d19..defb716c3 100644
--- a/examples/api/cpp/CMakeLists.txt
+++ b/examples/api/cpp/CMakeLists.txt
@@ -23,6 +23,7 @@ set(CVC5_EXAMPLES_API
   helloworld
   linear_arith
   quickstart
+  relations
   sequences
   sets
   strings
diff --git a/examples/api/cpp/relations.cpp b/examples/api/cpp/relations.cpp
new file mode 100644
index 000000000..cf462bd4a
--- /dev/null
+++ b/examples/api/cpp/relations.cpp
@@ -0,0 +1,150 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A simple demonstration of reasoning about relations with cvc5 via C++ API.
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+using namespace cvc5::api;
+
+int main()
+{
+  Solver solver;
+
+  // Set the logic
+  solver.setLogic("ALL");
+
+  // options
+  solver.setOption("produce-models", "true");
+  // we need finite model finding to answer sat problems with universal
+  // quantified formulas
+  solver.setOption("finite-model-find", "true");
+  // we need sets extension to support set.universe operator
+  solver.setOption("sets-ext", "true");
+
+  // (declare-sort Person 0)
+  Sort personSort = solver.mkUninterpretedSort("Person");
+
+  // (Tuple Person)
+  Sort tupleArity1 = solver.mkTupleSort({personSort});
+  // (Set (Tuple Person))
+  Sort relationArity1 = solver.mkSetSort(tupleArity1);
+
+  // (Tuple Person Person)
+  Sort tupleArity2 = solver.mkTupleSort({personSort, personSort});
+  // (Set (Tuple Person Person))
+  Sort relationArity2 = solver.mkSetSort(tupleArity2);
+
+  // empty set
+  Term emptySetTerm = solver.mkEmptySet(relationArity1);
+
+  // empty relation
+  Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
+
+  // universe set
+  Term universeSet = solver.mkUniverseSet(relationArity1);
+
+  // variables
+  Term people = solver.mkConst(relationArity1, "people");
+  Term males = solver.mkConst(relationArity1, "males");
+  Term females = solver.mkConst(relationArity1, "females");
+  Term father = solver.mkConst(relationArity2, "father");
+  Term mother = solver.mkConst(relationArity2, "mother");
+  Term parent = solver.mkConst(relationArity2, "parent");
+  Term ancestor = solver.mkConst(relationArity2, "ancestor");
+  Term descendant = solver.mkConst(relationArity2, "descendant");
+
+  Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
+  Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
+
+  // (assert (= people (as set.universe (Set (Tuple Person)))))
+  Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
+  // (assert (not (= males (as set.empty (Set (Tuple Person))))))
+  Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
+  // (assert (not (= females (as set.empty (Set (Tuple Person))))))
+  Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
+
+  // (assert (= (set.inter males females)
+  //            (as set.empty (Set (Tuple Person)))))
+  Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
+  Term malesAndFemalesAreDisjoint =
+      solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
+
+  // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+  // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+  Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
+  Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
+  Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
+  Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
+
+  // fathers are males
+  // (assert (set.subset (rel.join father people) males))
+  Term fathers = solver.mkTerm(RELATION_JOIN, father, people);
+  Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males);
+
+  // mothers are females
+  // (assert (set.subset (rel.join mother people) females))
+  Term mothers = solver.mkTerm(RELATION_JOIN, mother, people);
+  Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females);
+
+  // (assert (= parent (set.union father mother)))
+  Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
+  Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
+
+  // (assert (= ancestor (rel.tclosure parent)))
+  Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
+  Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transitiveClosure);
+
+  // (assert (= descendant (rel.transpose descendant)))
+  Term transpose = solver.mkTerm(RELATION_TRANSPOSE, ancestor);
+  Term descendantFormula = solver.mkTerm(EQUAL, descendant, transpose);
+
+  // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
+  Term x = solver.mkVar(personSort, "x");
+  Term xxTuple = solver.mkTuple({personSort, personSort}, {x, x});
+  Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
+  Term notMember = solver.mkTerm(NOT, member);
+
+  Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x);
+  Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
+
+  // formulas
+  solver.assertFormula(peopleAreTheUniverse);
+  solver.assertFormula(maleSetIsNotEmpty);
+  solver.assertFormula(femaleSetIsNotEmpty);
+  solver.assertFormula(malesAndFemalesAreDisjoint);
+  solver.assertFormula(fatherIsNotEmpty);
+  solver.assertFormula(motherIsNotEmpty);
+  solver.assertFormula(fathersAreMales);
+  solver.assertFormula(mothersAreFemales);
+  solver.assertFormula(parentIsFatherOrMother);
+  solver.assertFormula(descendantFormula);
+  solver.assertFormula(ancestorFormula);
+  solver.assertFormula(noSelfAncestor);
+
+  // check sat
+  Result result = solver.checkSat();
+
+  // output
+  std::cout << "Result     = " << result << std::endl;
+  std::cout << "people     = " << solver.getValue(people) << std::endl;
+  std::cout << "males      = " << solver.getValue(males) << std::endl;
+  std::cout << "females    = " << solver.getValue(females) << std::endl;
+  std::cout << "father     = " << solver.getValue(father) << std::endl;
+  std::cout << "mother     = " << solver.getValue(mother) << std::endl;
+  std::cout << "parent     = " << solver.getValue(parent) << std::endl;
+  std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
+  std::cout << "ancestor   = " << solver.getValue(ancestor) << std::endl;
+}
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index 95aede591..8f0c48090 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -17,49 +17,6 @@ import static io.github.cvc5.api.Kind.*;
 
 import io.github.cvc5.api.*;
 
-/*
-This file uses the API to make a sat call equivalent to the following benchmark:
-(set-logic ALL)
-
-(set-option :finite-model-find true)
-(set-option :produce-models true)
-(set-option :sets-ext true)
-
-(declare-sort Person 0)
-
-(declare-fun people () (Set (Tuple Person)))
-(declare-fun males () (Set (Tuple Person)))
-(declare-fun females () (Set (Tuple Person)))
-(declare-fun father () (Set (Tuple Person Person)))
-(declare-fun mother () (Set (Tuple Person Person)))
-(declare-fun parent () (Set (Tuple Person Person)))
-(declare-fun ancestor () (Set (Tuple Person Person)))
-(declare-fun descendant () (Set (Tuple Person Person)))
-
-(assert (= people (as set.universe (Set (Tuple Person)))))
-(assert (not (= males (as set.empty (Set (Tuple Person))))))
-(assert (not (= females (as set.empty (Set (Tuple Person))))))
-(assert (= (set.inter males females) (as set.empty (Set (Tuple Person)))))
-; father relation is not empty
-(assert (not (= father (as set.empty (Set (Tuple Person Person))))))
-; mother relation is not empty
-(assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
-; fathers are males
-(assert (set.subset (rel.join father people) males))
-; mothers are females
-(assert (set.subset (rel.join mother people) females))
-; parent
-(assert (= parent (set.union father mother)))
-; no self ancestor
-(assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
-; descendant
-(assert (= descendant (rel.tclosure parent)))
-; ancestor
-(assert (= ancestor (rel.transpose descendant)))
-(check-sat)
-(get-model)
- */
-
 public class Relations
 {
   public static void main(String[] args) throws CVC5ApiException
@@ -71,9 +28,11 @@ public class Relations
 
       // options
       solver.setOption("produce-models", "true");
+      // we need finite model finding to answer sat problems with universal
+      // quantified formulas
       solver.setOption("finite-model-find", "true");
+      // we need sets extension to support set.universe operator
       solver.setOption("sets-ext", "true");
-      solver.setOption("output-language", "smt2");
 
       // (declare-sort Person 0)
       Sort personSort = solver.mkUninterpretedSort("Person");
@@ -117,8 +76,8 @@ public class Relations
       // (assert (not (= females (as set.empty (Set (Tuple Person))))))
       Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 
-      // (assert (= (set.inter males females) (as set.empty (Set (Tuple
-      // Person)))))
+      // (assert (= (set.inter males females)
+      //            (as set.empty (Set (Tuple Person)))))
       Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
       Term malesAndFemalesAreDisjoint =
           solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
@@ -144,13 +103,13 @@ public class Relations
       Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
       Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
 
-      // (assert (= descendant (rel.tclosure parent)))
+      // (assert (= ancestor (rel.tclosure parent)))
       Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
-      Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
+      Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transitiveClosure);
 
-      // (assert (= ancestor (rel.transpose descendant)))
-      Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant);
-      Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
+      // (assert (= descendant (rel.transpose ancestor)))
+      Term transpose = solver.mkTerm(RELATION_TRANSPOSE, ancestor);
+      Term descendantFormula = solver.mkTerm(EQUAL, descendant, transpose);
 
       // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
       Term x = solver.mkVar(personSort, "x");
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index 0051859b1..d6233f0c5 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -25,6 +25,7 @@ set(EXAMPLES_API_PYTHON
   id
   linear_arith
   quickstart
+  relations
   sequences
   sets
   strings
diff --git a/examples/api/python/relations.py b/examples/api/python/relations.py
new file mode 100644
index 000000000..5c3e35808
--- /dev/null
+++ b/examples/api/python/relations.py
@@ -0,0 +1,152 @@
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+#   Mudathir Mohamed, Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple demonstration of the solving capabilities of the cvc5 relations solver
+# through the Python API. This is a direct translation of relations.cpp.
+##
+
+import pycvc5
+from pycvc5 import Kind
+
+if __name__ == "__main__":
+    solver = pycvc5.Solver()
+
+    # Set the logic
+    solver.setLogic("ALL")
+
+    # options
+    solver.setOption("produce-models", "true")
+    # we need finite model finding to answer sat problems with universal
+    # quantified formulas
+    solver.setOption("finite-model-find", "true")
+    # we need sets extension to support set.universe operator
+    solver.setOption("sets-ext", "true")
+
+    integer = solver.getIntegerSort()
+    set_ = solver.mkSetSort(integer)
+
+    # Verify union distributions over intersection
+    # (A union B) intersection C = (A intersection C) union (B intersection C)
+
+    # (declare-sort Person 0)
+    personSort = solver.mkUninterpretedSort("Person")
+
+    # (Tuple Person)
+    tupleArity1 = solver.mkTupleSort([personSort])
+    # (Set (Tuple Person))
+    relationArity1 = solver.mkSetSort(tupleArity1)
+
+    # (Tuple Person Person)
+    tupleArity2 = solver.mkTupleSort([personSort, personSort])
+    # (Set (Tuple Person Person))
+    relationArity2 = solver.mkSetSort(tupleArity2)
+
+    # empty set
+    emptySetTerm = solver.mkEmptySet(relationArity1)
+
+    # empty relation
+    emptyRelationTerm = solver.mkEmptySet(relationArity2)
+
+    # universe set
+    universeSet = solver.mkUniverseSet(relationArity1)
+
+    # variables
+    people = solver.mkConst(relationArity1, "people")
+    males = solver.mkConst(relationArity1, "males")
+    females = solver.mkConst(relationArity1, "females")
+    father = solver.mkConst(relationArity2, "father")
+    mother = solver.mkConst(relationArity2, "mother")
+    parent = solver.mkConst(relationArity2, "parent")
+    ancestor = solver.mkConst(relationArity2, "ancestor")
+    descendant = solver.mkConst(relationArity2, "descendant")
+
+    isEmpty1 = solver.mkTerm(Kind.Equal, males, emptySetTerm)
+    isEmpty2 = solver.mkTerm(Kind.Equal, females, emptySetTerm)
+
+    # (assert (= people (as set.universe (Set (Tuple Person)))))
+    peopleAreTheUniverse = solver.mkTerm(Kind.Equal, people, universeSet)
+    # (assert (not (= males (as set.empty (Set (Tuple Person))))))
+    maleSetIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty1)
+    # (assert (not (= females (as set.empty (Set (Tuple Person))))))
+    femaleSetIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty2)
+
+    # (assert (= (set.inter males females)
+    #            (as set.empty (Set (Tuple Person)))))
+    malesFemalesIntersection = solver.mkTerm(Kind.SetInter, males, females)
+    malesAndFemalesAreDisjoint = solver.mkTerm(Kind.Equal, malesFemalesIntersection, emptySetTerm)
+
+    # (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+    # (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+    isEmpty3 = solver.mkTerm(Kind.Equal, father, emptyRelationTerm)
+    isEmpty4 = solver.mkTerm(Kind.Equal, mother, emptyRelationTerm)
+    fatherIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty3)
+    motherIsNotEmpty = solver.mkTerm(Kind.Not, isEmpty4)
+
+    # fathers are males
+    # (assert (set.subset (rel.join father people) males))
+    fathers = solver.mkTerm(Kind.RelationJoin, father, people)
+    fathersAreMales = solver.mkTerm(Kind.SetSubset, fathers, males)
+
+    # mothers are females
+    # (assert (set.subset (rel.join mother people) females))
+    mothers = solver.mkTerm(Kind.RelationJoin, mother, people)
+    mothersAreFemales = solver.mkTerm(Kind.SetSubset, mothers, females)
+
+    # (assert (= parent (set.union father mother)))
+    unionFatherMother = solver.mkTerm(Kind.SetUnion, father, mother)
+    parentIsFatherOrMother = solver.mkTerm(Kind.Equal, parent, unionFatherMother)
+
+    # (assert (= ancestor (rel.tclosure parent)))
+    transitiveClosure = solver.mkTerm(Kind.RelationTclosure, parent)
+    ancestorFormula = solver.mkTerm(Kind.Equal, ancestor, transitiveClosure)
+
+    # (assert (= descendant (rel.transpose ancestor)))
+    transpose = solver.mkTerm(Kind.RelationTranspose, ancestor)
+    descendantFormula = solver.mkTerm(Kind.Equal, descendant, transpose)
+
+    # (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
+    x = solver.mkVar(personSort, "x")
+    xxTuple = solver.mkTuple([personSort, personSort], [x, x])
+    member = solver.mkTerm(Kind.SetMember, xxTuple, ancestor)
+    notMember = solver.mkTerm(Kind.Not, member)
+
+    quantifiedVariables = solver.mkTerm(Kind.VariableList, x)
+    noSelfAncestor = solver.mkTerm(Kind.Forall, quantifiedVariables, notMember)
+
+    # formulas
+    solver.assertFormula(peopleAreTheUniverse)
+    solver.assertFormula(maleSetIsNotEmpty)
+    solver.assertFormula(femaleSetIsNotEmpty)
+    solver.assertFormula(malesAndFemalesAreDisjoint)
+    solver.assertFormula(fatherIsNotEmpty)
+    solver.assertFormula(motherIsNotEmpty)
+    solver.assertFormula(fathersAreMales)
+    solver.assertFormula(mothersAreFemales)
+    solver.assertFormula(parentIsFatherOrMother)
+    solver.assertFormula(descendantFormula)
+    solver.assertFormula(ancestorFormula)
+    solver.assertFormula(noSelfAncestor)
+
+    # check sat
+    result = solver.checkSat()
+
+    # output
+    print("Result     = {}".format(result))
+    print("people     = {}".format(solver.getValue(people)))
+    print("males      = {}".format(solver.getValue(males)))
+    print("females    = {}".format(solver.getValue(females)))
+    print("father     = {}".format(solver.getValue(father)))
+    print("mother     = {}".format(solver.getValue(mother)))
+    print("parent     = {}".format(solver.getValue(parent)))
+    print("descendant = {}".format(solver.getValue(descendant)))
+    print("ancestor   = {}".format(solver.getValue(ancestor)))
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 4bd6c4029..76ab4e527 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -12,7 +12,7 @@
 # #############################################################################
 #
 # A simple demonstration of the solving capabilities of the cvc5 sets solver
-# through the Python API. This is a direct translation of sets-new.cpp.
+# through the Python API. This is a direct translation of sets.cpp.
 ##
 
 import pycvc5
diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2
index c8ece3aa7..971f1d832 100644
--- a/examples/api/smtlib/relations.smt2
+++ b/examples/api/smtlib/relations.smt2
@@ -1,41 +1,44 @@
 (set-logic ALL)
-(set-info :status sat)
 
-(declare-fun r1 () (Set (Tuple String Int)))
-(declare-fun r2 () (Set (Tuple Int String)))
-(declare-fun r () (Set (Tuple String String)))
-(declare-fun s () (Set (Tuple String String)))
-(declare-fun t () (Set (Tuple String Int Int String)))
-(declare-fun lt1 () (Set (Tuple Int Int)))
-(declare-fun lt2 () (Set (Tuple Int Int)))
-(declare-fun i () Int)
+(set-option :produce-models true)
+; we need finite model finding to answer sat problems with universal
+; quantified formulas
+(set-option :finite-model-find true)
+; we need sets extension to support set.universe operator
+(set-option :sets-ext true)
 
-(assert
-  (= r1
-    (set.insert
-      (tuple "a" 1)
-      (tuple "b" 2)
-      (tuple "c" 3)
-      (set.singleton (tuple "d" 4)))))
-(assert
-  (= r2
-    (set.insert
-      (tuple 1 "1")
-      (tuple 2 "2")
-      (tuple 3 "3")
-      (set.singleton (tuple 17 "17")))))
-(assert (= r (rel.join r1 r2)))
-(assert (= s (rel.transpose r)))
-(assert (= t (rel.product r1 r2)))
-(assert
-  (=
-    lt1
-     (set.insert
-       (tuple 1 2)
-       (tuple 2 3)
-       (tuple 3 4)
-       (set.singleton (tuple 4 5)))))
-(assert (= lt2 (rel.tclosure lt1)))
-(assert (= i (set.card t)))
+(declare-sort Person 0)
+
+(declare-fun people () (Set (Tuple Person)))
+(declare-fun males () (Set (Tuple Person)))
+(declare-fun females () (Set (Tuple Person)))
+(declare-fun father () (Set (Tuple Person Person)))
+(declare-fun mother () (Set (Tuple Person Person)))
+(declare-fun parent () (Set (Tuple Person Person)))
+(declare-fun ancestor () (Set (Tuple Person Person)))
+(declare-fun descendant () (Set (Tuple Person Person)))
+
+(assert (= people (as set.universe (Set (Tuple Person)))))
+(assert (not (= males (as set.empty (Set (Tuple Person))))))
+(assert (not (= females (as set.empty (Set (Tuple Person))))))
+(assert (= (set.inter males females) (as set.empty (Set (Tuple Person)))))
+
+; father relation is not empty
+(assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+; mother relation is not empty
+(assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+; fathers are males
+(assert (set.subset (rel.join father people) males))
+; mothers are females
+(assert (set.subset (rel.join mother people) females))
+; parent
+(assert (= parent (set.union father mother)))
+; no self ancestor
+(assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
+; ancestor
+(assert (= ancestor (rel.tclosure parent)))
+; ancestor
+(assert (= descendant (rel.transpose ancestor)))
 
 (check-sat)
+(get-model)