diff options
Diffstat (limited to 'examples/api/java/Sets.java')
| -rw-r--r-- | examples/api/java/Sets.java | 101 |
1 files changed, 51 insertions, 50 deletions
diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index 602014c96..3edc49ae6 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -21,72 +21,73 @@ public class Sets { public static void main(String args[]) throws CVC5ApiException { - Solver slv = new Solver(); - - // Optionally, set the logic. We need at least UF for equality predicate, - // integers (LIA) and sets (FS). - slv.setLogic("QF_UFLIAFS"); + try (Solver slv = new Solver()) + { + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS"); - // Produce models - slv.setOption("produce-models", "true"); - slv.setOption("output-language", "smt2"); + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); - Sort integer = slv.getIntegerSort(); - Sort set = slv.mkSetSort(integer); + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); - // Verify union distributions over intersection - // (A union B) intersection C = (A intersection C) union (B intersection C) - { - Term A = slv.mkConst(set, "A"); - Term B = slv.mkConst(set, "B"); - Term C = slv.mkConst(set, "C"); + // Verify union distributions over intersection + // (A union B) intersection C = (A intersection C) union (B intersection C) + { + Term A = slv.mkConst(set, "A"); + Term B = slv.mkConst(set, "B"); + Term C = slv.mkConst(set, "C"); - Term unionAB = slv.mkTerm(UNION, A, B); - Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); - Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); - Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); - Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); - Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); - } + System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + } - // Verify emptset is a subset of any set - { - Term A = slv.mkConst(set, "A"); - Term emptyset = slv.mkEmptySet(set); + // Verify emptset is a subset of any set + { + Term A = slv.mkConst(set, "A"); + Term emptyset = slv.mkEmptySet(set); - Term theorem = slv.mkTerm(SUBSET, emptyset, A); + Term theorem = slv.mkTerm(SUBSET, emptyset, A); - System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); - } + System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); + } - // Find me an element in {1, 2} intersection {2, 3}, if there is one. - { - Term one = slv.mkInteger(1); - Term two = slv.mkInteger(2); - Term three = slv.mkInteger(3); + // Find me an element in {1, 2} intersection {2, 3}, if there is one. + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); - Term singleton_one = slv.mkTerm(SINGLETON, one); - Term singleton_two = slv.mkTerm(SINGLETON, two); - Term singleton_three = slv.mkTerm(SINGLETON, three); - Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); - Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); - Term x = slv.mkConst(integer, "x"); + Term x = slv.mkConst(integer, "x"); - Term e = slv.mkTerm(MEMBER, x, intersection); + Term e = slv.mkTerm(MEMBER, x, intersection); - Result result = slv.checkSatAssuming(e); - System.out.println("cvc5 reports: " + e + " is " + result + "."); + Result result = slv.checkSatAssuming(e); + System.out.println("cvc5 reports: " + e + " is " + result + "."); - if (result.isSat()) - { - System.out.println("For instance, " + slv.getValue(x) + " is a member."); + if (result.isSat()) + { + System.out.println("For instance, " + slv.getValue(x) + " is a member."); + } } } } -}
\ No newline at end of file +} |