mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
690a392656
This PR enables CI for java tests by adding --java-bindings to ci.yml. It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface. The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
200 lines
7.9 KiB
Java
200 lines
7.9 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 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
|
|
{
|
|
try (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));
|
|
}
|
|
}
|
|
}
|