mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
98e884a740
This PRs updates java examples using the new Java API, by converting C++ examples to Java. Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API. All examples are not included in the build which would be added in a future PR.
198 lines
7.6 KiB
Java
198 lines
7.6 KiB
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 cvc5.Kind.*;
|
|
|
|
import cvc5.*;
|
|
|
|
/*
|
|
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));
|
|
}
|
|
}
|