mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
219 lines
8.3 KiB
Java
219 lines
8.3 KiB
Java
/********************* */
|
|
/*! \file Relations.java
|
|
** \verbatim
|
|
** Top contributors (to current version):
|
|
** Mudathir Mohamed, Andres Noetzli
|
|
** This file is part of the CVC4 project.
|
|
** Copyright (c) 2009-2020 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.\endverbatim
|
|
**
|
|
** \brief Reasoning about relations with CVC4 via Java API.
|
|
**
|
|
** A simple demonstration of reasoning about strings with CVC4 via Jave API.
|
|
**/
|
|
|
|
import edu.stanford.CVC4.*;
|
|
|
|
/*
|
|
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) {
|
|
System.loadLibrary("cvc4jni");
|
|
|
|
ExprManager manager = new ExprManager();
|
|
SmtEngine smtEngine = new SmtEngine(manager);
|
|
|
|
// Set the logic
|
|
smtEngine.setLogic("ALL");
|
|
|
|
// options
|
|
smtEngine.setOption("produce-models", new SExpr(true));
|
|
smtEngine.setOption("finite-model-find", new SExpr(true));
|
|
smtEngine.setOption("sets-ext", new SExpr(true));
|
|
smtEngine.setOption("output-language", new SExpr("smt2"));
|
|
|
|
// (declare-sort Person 0)
|
|
Type personType = manager.mkSort("Person", 0);
|
|
vectorType vector1 = new vectorType();
|
|
vector1.add(personType);
|
|
|
|
// (Tuple Person)
|
|
Type tupleArity1 = manager.mkTupleType(vector1);
|
|
// (Set (Tuple Person))
|
|
SetType relationArity1 = manager.mkSetType(tupleArity1);
|
|
|
|
vectorType vector2 = new vectorType();
|
|
vector2.add(personType);
|
|
vector2.add(personType);
|
|
// (Tuple Person Person)
|
|
DatatypeType tupleArity2 = manager.mkTupleType(vector2);
|
|
// (Set (Tuple Person Person))
|
|
SetType relationArity2 = manager.mkSetType(tupleArity2);
|
|
|
|
// empty set
|
|
EmptySet emptySet = new EmptySet(relationArity1);
|
|
Expr emptySetExpr = manager.mkConst(emptySet);
|
|
|
|
// empty relation
|
|
EmptySet emptyRelation = new EmptySet(relationArity2);
|
|
Expr emptyRelationExpr = manager.mkConst(emptyRelation);
|
|
|
|
// universe set
|
|
Expr universeSet =
|
|
manager.mkNullaryOperator(relationArity1, Kind.UNIVERSE_SET);
|
|
|
|
// variables
|
|
Expr people = manager.mkVar("people", relationArity1);
|
|
Expr males = manager.mkVar("males", relationArity1);
|
|
Expr females = manager.mkVar("females", relationArity1);
|
|
Expr father = manager.mkVar("father", relationArity2);
|
|
Expr mother = manager.mkVar("mother", relationArity2);
|
|
Expr parent = manager.mkVar("parent", relationArity2);
|
|
Expr ancestor = manager.mkVar("ancestor", relationArity2);
|
|
Expr descendant = manager.mkVar("descendant", relationArity2);
|
|
|
|
Expr isEmpty1 = manager.mkExpr(Kind.EQUAL, males, emptySetExpr);
|
|
Expr isEmpty2 = manager.mkExpr(Kind.EQUAL, females, emptySetExpr);
|
|
|
|
// (assert (= people (as univset (Set (Tuple Person)))))
|
|
Expr peopleAreTheUniverse = manager.mkExpr(Kind.EQUAL, people, universeSet);
|
|
// (assert (not (= males (as emptyset (Set (Tuple Person))))))
|
|
Expr maleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty1);
|
|
// (assert (not (= females (as emptyset (Set (Tuple Person))))))
|
|
Expr femaleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty2);
|
|
|
|
// (assert (= (intersection males females) (as emptyset (Set (Tuple
|
|
// Person)))))
|
|
Expr malesFemalesIntersection =
|
|
manager.mkExpr(Kind.INTERSECTION, males, females);
|
|
Expr malesAndFemalesAreDisjoint =
|
|
manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr);
|
|
|
|
// (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
|
|
// (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
|
|
Expr isEmpty3 = manager.mkExpr(Kind.EQUAL, father, emptyRelationExpr);
|
|
Expr isEmpty4 = manager.mkExpr(Kind.EQUAL, mother, emptyRelationExpr);
|
|
Expr fatherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty3);
|
|
Expr motherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty4);
|
|
|
|
// fathers are males
|
|
// (assert (subset (join father people) males))
|
|
Expr fathers = manager.mkExpr(Kind.JOIN, father, people);
|
|
Expr fathersAreMales = manager.mkExpr(Kind.SUBSET, fathers, males);
|
|
|
|
// mothers are females
|
|
// (assert (subset (join mother people) females))
|
|
Expr mothers = manager.mkExpr(Kind.JOIN, mother, people);
|
|
Expr mothersAreFemales = manager.mkExpr(Kind.SUBSET, mothers, females);
|
|
|
|
// (assert (= parent (union father mother)))
|
|
Expr unionFatherMother = manager.mkExpr(Kind.UNION, father, mother);
|
|
Expr parentIsFatherOrMother =
|
|
manager.mkExpr(Kind.EQUAL, parent, unionFatherMother);
|
|
|
|
// (assert (= parent (union father mother)))
|
|
Expr transitiveClosure = manager.mkExpr(Kind.TCLOSURE, parent);
|
|
Expr descendantFormula =
|
|
manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure);
|
|
|
|
// (assert (= parent (union father mother)))
|
|
Expr transpose = manager.mkExpr(Kind.TRANSPOSE, descendant);
|
|
Expr ancestorFormula = manager.mkExpr(Kind.EQUAL, ancestor, transpose);
|
|
|
|
// (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
|
|
Expr x = manager.mkBoundVar("x", personType);
|
|
Expr constructor = tupleArity2.getDatatype().get(0).getConstructor();
|
|
Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x);
|
|
Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor);
|
|
Expr notMember = manager.mkExpr(Kind.NOT, member);
|
|
vectorExpr vectorExpr = new vectorExpr();
|
|
vectorExpr.add(x);
|
|
Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x);
|
|
Expr noSelfAncestor =
|
|
manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember);
|
|
|
|
// formulas
|
|
Expr formula1 = manager.mkExpr(Kind.AND,
|
|
peopleAreTheUniverse,
|
|
maleSetIsNotEmpty,
|
|
femaleSetIsNotEmpty,
|
|
malesAndFemalesAreDisjoint);
|
|
|
|
Expr formula2 = manager.mkExpr(Kind.AND,
|
|
formula1,
|
|
fatherIsNotEmpty,
|
|
motherIsNotEmpty,
|
|
fathersAreMales,
|
|
mothersAreFemales);
|
|
|
|
Expr formula3 = manager.mkExpr(Kind.AND,
|
|
formula2,
|
|
parentIsFatherOrMother,
|
|
descendantFormula,
|
|
ancestorFormula,
|
|
noSelfAncestor);
|
|
|
|
// check sat
|
|
Result result = smtEngine.checkSat(formula3);
|
|
|
|
// output
|
|
System.out.println("CVC4 reports: " + formula3 + " is " + result + ".");
|
|
System.out.println("people = " + smtEngine.getValue(people));
|
|
System.out.println("males = " + smtEngine.getValue(males));
|
|
System.out.println("females = " + smtEngine.getValue(females));
|
|
System.out.println("father = " + smtEngine.getValue(father));
|
|
System.out.println("mother = " + smtEngine.getValue(mother));
|
|
System.out.println("parent = " + smtEngine.getValue(parent));
|
|
System.out.println("descendant = " + smtEngine.getValue(descendant));
|
|
System.out.println("ancestor = " + smtEngine.getValue(ancestor));
|
|
}
|
|
}
|