From 437c346559d920edcd19c28777747093ceba4e20 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 17 Dec 2021 13:23:16 -0600 Subject: [PATCH] Add relations.cpp, relations.py examples (#7801) --- docs/examples/relations.rst | 22 ++++ docs/theories/sets-and-relations.rst | 14 +-- examples/api/cpp/CMakeLists.txt | 1 + examples/api/cpp/relations.cpp | 150 ++++++++++++++++++++++++++ examples/api/java/Relations.java | 61 ++--------- examples/api/python/CMakeLists.txt | 1 + examples/api/python/relations.py | 152 +++++++++++++++++++++++++++ examples/api/python/sets.py | 2 +- examples/api/smtlib/relations.smt2 | 75 ++++++------- 9 files changed, 380 insertions(+), 98 deletions(-) create mode 100644 examples/api/cpp/relations.cpp create mode 100644 examples/api/python/relations.py 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:: + /api/cpp/relations.cpp /api/java/Relations.java + /api/python/relations.py /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 , ..., )`` | ``Sort s = solver.mkTypleSort(sorts);`` | -| | | | -| | | ``Datatype dt = s.getDatatype();`` | -| | | | -| | | ``Term c = dt[0].getConstructor();`` | -| | | | -| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +| Tuple Constructor | ``(tuple , ..., )`` | ``Term t = solver.mkTuple({, ..., }, {Term_1>, ..., });`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| 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 s = solver.mkSetSort(cvc5::api::Sort tupleSort);`` | +| Relation Sort | ``(Set (Tuple , ..., ))`` | ``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 + +#include + +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) -- 2.30.2