--- /dev/null
+Theory of Bags
+=================
+
+
+.. api-examples::
+ <examples>/api/cpp/bags.cpp
+ <examples>/api/java/Bags.java
+ <examples>/api/python/bags.py
+ <examples>/api/smtlib/bags.smt2
helloworld
exceptions
+ bags
bitvectors
bitvectors_and_arrays
extract
Below is a more extensive example on how to use finite bags:
.. api-examples::
+ <examples>/api/cpp/bags.cpp
+ <examples>/api/cpp/Bags.java
+ <examples>/api/cpp/bags.py
<examples>/api/smtlib/bags.smt2
##
set(CVC5_EXAMPLES_API
+ bags
bitvectors
bitvectors_and_arrays
combination
--- /dev/null
+/******************************************************************************
+ * 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 <cvc5/cvc5.h>
+
+#include <iostream>
+
+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;
+ }
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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
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();
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};
##
set(EXAMPLES_API_JAVA
+ Bags
BitVectors
BitVectorsAndArrays
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");
{
Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
- System.out.println(
- helloworld + " is " + slv.checkSatAssuming(helloworld));
+ System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld));
}
}
}
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();
// (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);
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
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.
* 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
{
{
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();
* @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)
}
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(')');
}
##
set(EXAMPLES_API_PYTHON
+ bags
bitvectors_and_arrays
bitvectors
combination
--- /dev/null
+#!/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)))
projects / cvc5.git / commitdiff