diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/api/java/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | examples/api/java/Relations.java | 216 |
2 files changed, 217 insertions, 0 deletions
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 2b364c3d1..108ae3cd3 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -10,6 +10,7 @@ set(EXAMPLES_API_JAVA LinearArith ## disabled until bindings for the new API are in place (issue #2284) #PipedInput + Relations Statistics Strings UnsatCores diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java new file mode 100644 index 000000000..86a394062 --- /dev/null +++ b/examples/api/java/Relations.java @@ -0,0 +1,216 @@ +/********************* */ +/*! \file Relations.java + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mahgoub + ** 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.load("/usr/local/lib/libcvc4jni.so"); + + 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)); + } +} |