cvc5/examples/api/java/Relations.java

/******************************************************************************
 * 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 CVC4 via Java API.
 */

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)
(set-option :output-language "smt2")
(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 univset (Set (Tuple Person)))))
(assert (not (= males (as emptyset (Set (Tuple Person))))))
(assert (not (= females (as emptyset (Set (Tuple Person))))))
(assert (= (intersection males females) (as emptyset (Set (Tuple Person)))))

; father relation is not empty
(assert (not (= father (as emptyset (Set (Tuple Person Person))))))
; mother relation is not empty
(assert (not (= mother (as emptyset (Set (Tuple Person Person))))))

; fathers are males
(assert (subset (join father people) males))
; mothers are females
(assert (subset (join mother people) females))

; parent
(assert (= parent (union father mother)))

; no self ancestor
(assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))

; descendant
(assert (= descendant (tclosure parent)))

; ancestor
(assert (= ancestor (transpose descendant)))

(check-sat)
(get-model)
 */

public class Relations
{
  public static void main(String[] args) throws CVC5ApiException
  {
    Solver solver = new Solver();

    // Set the logic
    solver.setLogic("ALL");

    // options
    solver.setOption("produce-models", "true");
    solver.setOption("finite-model-find", "true");
    solver.setOption("sets-ext", "true");
    solver.setOption("output-language", "smt2");

    // (declare-sort Person 0)
    Sort personSort = solver.mkUninterpretedSort("Person");

    // (Tuple Person)
    Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
    // (Set (Tuple Person))
    Sort relationArity1 = solver.mkSetSort(tupleArity1);

    // (Tuple Person Person)
    Sort tupleArity2 = solver.mkTupleSort(new Sort[] {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 univset (Set (Tuple Person)))))
    Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
    // (assert (not (= males (as emptyset (Set (Tuple Person))))))
    Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
    // (assert (not (= females (as emptyset (Set (Tuple Person))))))
    Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);

    // (assert (= (intersection males females) (as emptyset (Set (Tuple
    // Person)))))
    Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females);
    Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);

    // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
    // (assert (not (= mother (as emptyset (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 (subset (join father people) males))
    Term fathers = solver.mkTerm(JOIN, father, people);
    Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males);

    // mothers are females
    // (assert (subset (join mother people) females))
    Term mothers = solver.mkTerm(JOIN, mother, people);
    Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females);

    // (assert (= parent (union father mother)))
    Term unionFatherMother = solver.mkTerm(UNION, father, mother);
    Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);

    // (assert (= parent (union father mother)))
    Term transitiveClosure = solver.mkTerm(TCLOSURE, parent);
    Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);

    // (assert (= parent (union father mother)))
    Term transpose = solver.mkTerm(TRANSPOSE, descendant);
    Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);

    // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
    Term x = solver.mkVar(personSort, "x");
    DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
    Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x);
    Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
    Term notMember = solver.mkTerm(NOT, member);

    Term quantifiedVariables = solver.mkTerm(BOUND_VAR_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
    System.out.println("Result     = " + result);
    System.out.println("people     = " + solver.getValue(people));
    System.out.println("males      = " + solver.getValue(males));
    System.out.println("females    = " + solver.getValue(females));
    System.out.println("father     = " + solver.getValue(father));
    System.out.println("mother     = " + solver.getValue(mother));
    System.out.println("parent     = " + solver.getValue(parent));
    System.out.println("descendant = " + solver.getValue(descendant));
    System.out.println("ancestor   = " + solver.getValue(ancestor));
  }
}