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
+----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
| | ``(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();`` |
| | | |
| | | |
| | | ``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});`` |
| | | |
helloworld
linear_arith
quickstart
+ relations
sequences
sets
strings
--- /dev/null
+/******************************************************************************
+ * 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;
+}
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
// 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");
// (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);
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");
id
linear_arith
quickstart
+ relations
sequences
sets
strings
--- /dev/null
+#!/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)))
# #############################################################################
#
# 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
(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)
projects / cvc5.git / commitdiff