From 6c421a82211f8e9c1e8d4d0725bedce567fe5aa6 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 31 Mar 2022 10:17:22 -0500 Subject: [PATCH] Add examples/bags.cpp (#8463) --- docs/examples/bags.rst | 9 +++ docs/examples/examples.rst | 1 + docs/theories/bags.rst | 3 + examples/api/cpp/CMakeLists.txt | 1 + examples/api/cpp/bags.cpp | 105 +++++++++++++++++++++++++++ examples/api/java/Bags.java | 112 +++++++++++++++++++++++++++++ examples/api/java/BitVectors.java | 6 +- examples/api/java/CMakeLists.txt | 1 + examples/api/java/Combination.java | 3 +- examples/api/java/HelloWorld.java | 3 +- examples/api/java/LinearArith.java | 4 +- examples/api/java/Relations.java | 2 +- examples/api/java/Sets.java | 8 +-- examples/api/java/Utils.java | 14 ++-- examples/api/python/CMakeLists.txt | 1 + examples/api/python/bags.py | 86 ++++++++++++++++++++++ 16 files changed, 335 insertions(+), 24 deletions(-) create mode 100644 docs/examples/bags.rst create mode 100644 examples/api/cpp/bags.cpp create mode 100644 examples/api/java/Bags.java create mode 100644 examples/api/python/bags.py diff --git a/docs/examples/bags.rst b/docs/examples/bags.rst new file mode 100644 index 000000000..ae3b267e2 --- /dev/null +++ b/docs/examples/bags.rst @@ -0,0 +1,9 @@ +Theory of Bags +================= + + +.. api-examples:: + /api/cpp/bags.cpp + /api/java/Bags.java + /api/python/bags.py + /api/smtlib/bags.smt2 diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index b9303f1d9..9812027ed 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -11,6 +11,7 @@ input mechanisms. helloworld exceptions + bags bitvectors bitvectors_and_arrays extract diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst index d3e32fb28..d29d3905e 100644 --- a/docs/theories/bags.rst +++ b/docs/theories/bags.rst @@ -82,5 +82,8 @@ The semantics of supported bag operators is given in the table below. Below is a more extensive example on how to use finite bags: .. api-examples:: + /api/cpp/bags.cpp + /api/cpp/Bags.java + /api/cpp/bags.py /api/smtlib/bags.smt2 diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index 6d462da5d..02496fe8f 100644 --- a/examples/api/cpp/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt @@ -14,6 +14,7 @@ ## set(CVC5_EXAMPLES_API + bags bitvectors bitvectors_and_arrays combination diff --git a/examples/api/cpp/bags.cpp b/examples/api/cpp/bags.cpp new file mode 100644 index 000000000..6df2bc46e --- /dev/null +++ b/examples/api/cpp/bags.cpp @@ -0,0 +1,105 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * Copyright (c) 2009-2022 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 bags. + */ + +#include + +#include + +using namespace std; +using namespace cvc5; + +int main() +{ + Solver slv; + slv.setLogic("ALL"); + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("incremental", "true"); + + Sort bag = slv.mkBagSort(slv.getStringSort()); + Term A = slv.mkConst(bag, "A"); + Term B = slv.mkConst(bag, "B"); + Term C = slv.mkConst(bag, "C"); + Term x = slv.mkConst(slv.getStringSort(), "x"); + + Term intersectionAC = slv.mkTerm(BAG_INTER_MIN, {A, C}); + Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, {B, C}); + + // union disjoint does not distribute over intersection + { + Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, {A, B}); + Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionDisjointAB, C}); + Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, {intersectionAC, intersectionBC}); + Term guess = slv.mkTerm(EQUAL, {lhs, rhs}); + cout << "cvc5 reports: " << guess.notTerm() << " is " + << slv.checkSatAssuming(guess.notTerm()) << "." << endl; + + cout << A << ": " << slv.getValue(A) << endl; + cout << B << ": " << slv.getValue(B) << endl; + cout << C << ": " << slv.getValue(C) << endl; + cout << lhs << ": " << slv.getValue(lhs) << endl; + cout << rhs << ": " << slv.getValue(rhs) << endl; + } + + // union max distributes over intersection + { + Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, {A, B}); + Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionMaxAB, C}); + Term rhs = slv.mkTerm(BAG_UNION_MAX, {intersectionAC, intersectionBC}); + Term theorem = slv.mkTerm(EQUAL, {lhs, rhs}); + cout << "cvc5 reports: " << theorem.notTerm() << " is " + << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; + } + + // Verify emptbag is a subbag of any bag + { + Term emptybag = slv.mkEmptyBag(bag); + Term theorem = slv.mkTerm(BAG_SUBBAG, {emptybag, A}); + + cout << "cvc5 reports: " << theorem.notTerm() << " is " + << slv.checkSatAssuming(theorem.notTerm()) << "." << endl; + } + + // find an element with multiplicity 4 in the disjoint union of + // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|} + + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + Term four = slv.mkInteger(4); + Term a = slv.mkString("a"); + Term b = slv.mkString("b"); + Term c = slv.mkString("c"); + + Term bag_a_2 = slv.mkTerm(BAG_MAKE, {a, two}); + Term bag_b_3 = slv.mkTerm(BAG_MAKE, {b, three}); + Term bag_b_1 = slv.mkTerm(BAG_MAKE, {b, one}); + Term bag_c_2 = slv.mkTerm(BAG_MAKE, {c, two}); + Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2, bag_b_3}); + Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_b_1, bag_c_2}); + Term union_disjoint = + slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2}); + + Term count_x = slv.mkTerm(BAG_COUNT, {x, union_disjoint}); + Term e = slv.mkTerm(EQUAL, {four, count_x}); + Result result = slv.checkSatAssuming(e); + + cout << "cvc5 reports: " << e << " is " << result << "." << endl; + if (result.isSat()) + { + cout << x << ": " << slv.getValue(x) << endl; + } + } +} diff --git a/examples/api/java/Bags.java b/examples/api/java/Bags.java new file mode 100644 index 000000000..f1c74ca97 --- /dev/null +++ b/examples/api/java/Bags.java @@ -0,0 +1,112 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 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 bags with cvc5. + */ + +import static io.github.cvc5.Kind.*; + +import io.github.cvc5.*; + +public class Bags +{ + public static void main(String args[]) throws CVC5ApiException + + { + try (Solver slv = new Solver()) + { + slv.setLogic("ALL"); + + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("incremental", "true"); + + Sort bag = slv.mkBagSort(slv.getStringSort()); + Term A = slv.mkConst(bag, "A"); + Term B = slv.mkConst(bag, "B"); + Term C = slv.mkConst(bag, "C"); + Term x = slv.mkConst(slv.getStringSort(), "x"); + + Term intersectionAC = slv.mkTerm(BAG_INTER_MIN, new Term[] {A, C}); + Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, new Term[] {B, C}); + + // union disjoint does not distribute over intersection + { + Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {A, B}); + Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionDisjointAB, C}); + Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {intersectionAC, intersectionBC}); + Term guess = slv.mkTerm(EQUAL, new Term[] {lhs, rhs}); + + System.out.println("cvc5 reports: " + guess.notTerm() + " is " + + slv.checkSatAssuming(guess.notTerm()) + "."); + + System.out.println(A + ": " + slv.getValue(A)); + System.out.println(B + ": " + slv.getValue(B)); + System.out.println(C + ": " + slv.getValue(C)); + System.out.println(lhs + ": " + slv.getValue(lhs)); + System.out.println(rhs + ": " + slv.getValue(rhs)); + } + + // union max distributes over intersection + { + Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, new Term[] {A, B}); + Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionMaxAB, C}); + Term rhs = slv.mkTerm(BAG_UNION_MAX, new Term[] {intersectionAC, intersectionBC}); + Term theorem = slv.mkTerm(EQUAL, new Term[] {lhs, rhs}); + System.out.println("cvc5 reports: " + theorem.notTerm() + " is " + + slv.checkSatAssuming(theorem.notTerm()) + "."); + } + + // Verify emptbag is a subbag of any bag + { + Term emptybag = slv.mkEmptyBag(bag); + Term theorem = slv.mkTerm(BAG_SUBBAG, new Term[] {emptybag, A}); + + System.out.println("cvc5 reports: " + theorem.notTerm() + " is " + + slv.checkSatAssuming(theorem.notTerm()) + "."); + } + + // find an element with multiplicity 4 in the disjoint union of + // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|} + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + Term four = slv.mkInteger(4); + Term a = slv.mkString("a"); + Term b = slv.mkString("b"); + Term c = slv.mkString("c"); + + Term bag_a_2 = slv.mkTerm(BAG_MAKE, new Term[] {a, two}); + Term bag_b_3 = slv.mkTerm(BAG_MAKE, new Term[] {b, three}); + Term bag_b_1 = slv.mkTerm(BAG_MAKE, new Term[] {b, one}); + Term bag_c_2 = slv.mkTerm(BAG_MAKE, new Term[] {c, two}); + + Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2, bag_b_3}); + + Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_b_1, bag_c_2}); + + Term union_disjoint = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2_b_3, bag_b_1_c_2}); + + Term count_x = slv.mkTerm(BAG_COUNT, new Term[] {x, union_disjoint}); + Term e = slv.mkTerm(EQUAL, new Term[] {four, count_x}); + Result result = slv.checkSatAssuming(e); + + System.out.println("cvc5 reports: " + e + " is " + result + "."); + if (result.isSat()) + { + System.out.println(x + ": " + slv.getValue(x)); + } + } + } + } +} \ No newline at end of file diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 2abbc35fe..72aaadc4b 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -88,8 +88,7 @@ public class BitVectors System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm()); System.out.println(" Expect UNSAT. "); - System.out.println( - " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); + System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); System.out.println(" Popping context. "); slv.pop(); @@ -105,8 +104,7 @@ public class BitVectors System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm()); System.out.println(" Expect UNSAT. "); - System.out.println( - " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); + System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm())); Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm(); Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x}; diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index bd4eb179a..159d0e928 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -14,6 +14,7 @@ ## set(EXAMPLES_API_JAVA + Bags BitVectors BitVectorsAndArrays Combination diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 60a9e803b..0754fd707 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -86,8 +86,7 @@ public class Combination System.out.println("Given the following assertions:\n" + assertions + "\n"); System.out.println("Prove x /= y is entailed. \n" - + "cvc5: " + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)) - + ".\n"); + + "cvc5: " + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)) + ".\n"); System.out.println("Call checkSat to show that the assertions are satisfiable. \n" + "cvc5: " + slv.checkSat() + ".\n"); diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 7cef12966..1b4499950 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -23,8 +23,7 @@ public class HelloWorld { Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!"); - System.out.println( - helloworld + " is " + slv.checkSatAssuming(helloworld)); + System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld)); } } } diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 7ba565ff3..fe9d6b4b7 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -57,8 +57,8 @@ public class LinearArith Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds); System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5."); System.out.println("cvc5 should report UNSAT."); - System.out.println("Result from cvc5 is: " - + slv.checkSatAssuming(diff_leq_two_thirds.notTerm())); + System.out.println( + "Result from cvc5 is: " + slv.checkSatAssuming(diff_leq_two_thirds.notTerm())); slv.pop(); System.out.println(); diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index a4b568ccd..f7fbf4bf3 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -113,7 +113,7 @@ public class Relations // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor)))) Term x = solver.mkVar(personSort, "x"); - Term xxTuple = solver.mkTuple(new Sort[]{personSort, personSort}, new Term[] {x, x}); + Term xxTuple = solver.mkTuple(new Sort[] {personSort, personSort}, new Term[] {x, x}); Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index 6002c0e69..1a2cff031 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -50,8 +50,8 @@ public class Sets Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - System.out.println("cvc5 reports: " + theorem + " is " - + slv.checkSatAssuming(theorem.notTerm()) + "."); + System.out.println( + "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + "."); } // Verify set.empty is a subset of any set @@ -61,8 +61,8 @@ public class Sets Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A); - System.out.println("cvc5 reports: " + theorem + " is " - + slv.checkSatAssuming(theorem.notTerm()) + "."); + System.out.println( + "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + "."); } // Find me an element in {1, 2} intersection {2, 3}, if there is one. diff --git a/examples/api/java/Utils.java b/examples/api/java/Utils.java index 9a2054d86..3ea56c55f 100644 --- a/examples/api/java/Utils.java +++ b/examples/api/java/Utils.java @@ -13,13 +13,12 @@ * Utility methods. */ -import java.util.ArrayList; -import java.util.List; - import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import java.util.ArrayList; +import java.util.List; public class Utils { @@ -46,8 +45,7 @@ public class Utils { ss.append(' '); } - ss.append('(').append(params[i]).append(' ').append(params[i].getSort()) - .append(')'); + ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')'); } ss.append(") ").append(sort).append(' ').append(body).append(')'); return ss.toString(); @@ -59,8 +57,7 @@ public class Utils * @param terms the terms for which the synthesis solutions were retrieved * @param sols the synthesis solutions of the given terms */ - public static void printSynthSolutions(Term[] terms, Term[] sols) - throws CVC5ApiException + public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException { System.out.println('('); for (int i = 0; i < terms.length; ++i) @@ -75,8 +72,7 @@ public class Utils } body = sols[i].getChild(1); } - System.out.println(" " - + defineFunToString(terms[i], params.toArray(new Term[0]), body)); + System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body)); } System.out.println(')'); } diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index d6233f0c5..f03db7c54 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -14,6 +14,7 @@ ## set(EXAMPLES_API_PYTHON + bags bitvectors_and_arrays bitvectors combination diff --git a/examples/api/python/bags.py b/examples/api/python/bags.py new file mode 100644 index 000000000..9172a97f5 --- /dev/null +++ b/examples/api/python/bags.py @@ -0,0 +1,86 @@ +#!/usr/bin/env python +############################################################################### +# Top contributors (to current version): +# Mudathir Mohamed +# +# 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 bags. +## + +import cvc5 +from cvc5 import Kind + +if __name__ == "__main__": + slv = cvc5.Solver() + slv.setLogic("ALL") + + # Produce models + slv.setOption("produce-models", "true") + slv.setOption("incremental", "true") + + bag = slv.mkBagSort(slv.getStringSort()) + A = slv.mkConst(bag, "A") + B = slv.mkConst(bag, "B") + C = slv.mkConst(bag, "C") + x = slv.mkConst(slv.getStringSort(), "x") + + intersectionAC = slv.mkTerm(Kind.BagInterMin, A, C) + intersectionBC = slv.mkTerm(Kind.BagInterMin, B, C) + + # union disjoint does not distribute over intersection + unionDisjointAB = slv.mkTerm(Kind.BagUnionDisjoint, A, B) + lhs = slv.mkTerm(Kind.BagInterMin, unionDisjointAB, C) + rhs = slv.mkTerm(Kind.BagUnionDisjoint, intersectionAC, intersectionBC) + guess = slv.mkTerm(Kind.Equal, lhs, rhs) + print("cvc5 reports: {} is {}".format(guess.notTerm(), slv.checkSatAssuming(guess.notTerm()))) + + print("{}: {}".format(A, slv.getValue(A))) + print("{}: {}".format(B, slv.getValue(B))) + print("{}: {}".format(C, slv.getValue(C))) + print("{}: {}".format(lhs, slv.getValue(lhs))) + print("{}: {}".format(rhs, slv.getValue(rhs))) + + # union max distributes over intersection + unionMaxAB = slv.mkTerm(Kind.BagUnionMax, A, B) + lhs = slv.mkTerm(Kind.BagInterMin, unionMaxAB, C) + rhs = slv.mkTerm(Kind.BagUnionMax, intersectionAC, intersectionBC) + theorem = slv.mkTerm(Kind.Equal, lhs, rhs) + print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) + + # Verify emptbag is a subbag of any bag + emptybag = slv.mkEmptyBag(bag) + theorem = slv.mkTerm(Kind.BagSubbag, emptybag, A) + print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm()))) + + # find an element with multiplicity 4 in the disjoint union of + # {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|} + one = slv.mkInteger(1) + two = slv.mkInteger(2) + three = slv.mkInteger(3) + four = slv.mkInteger(4) + a = slv.mkString("a") + b = slv.mkString("b") + c = slv.mkString("c") + + bag_a_2 = slv.mkTerm(Kind.BagMake, a, two) + bag_b_3 = slv.mkTerm(Kind.BagMake, b, three) + bag_b_1 = slv.mkTerm(Kind.BagMake, b, one) + bag_c_2 = slv.mkTerm(Kind.BagMake, c, two) + bag_a_2_b_3 = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2, bag_b_3) + bag_b_1_c_2 = slv.mkTerm(Kind.BagUnionDisjoint, bag_b_1, bag_c_2) + UnionDisjoint = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2_b_3, bag_b_1_c_2) + + count_x = slv.mkTerm(Kind.BagCount, x, UnionDisjoint) + e = slv.mkTerm(Kind.Equal, four, count_x) + result = slv.checkSatAssuming(e) + + print("cvc5 reports: {} is {}.".format(e, result)) + if result.isSat(): + print("{}: {} ".format(x, slv.getValue(x))) -- 2.30.2