From e4a29a6033ecc7ba5ec266f37e8f151f09ead020 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 22 Sep 2020 16:59:41 -0500 Subject: Add skeleton for theory of bags (multisets) (#5100) This PR adds initial headers and mostly empty source files for the theory of bags (multisets). It acts as a basis for future commits. It includes straightforward implementation for typing rules an enumerator for bags. --- src/theory/bags/kinds | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 src/theory/bags/kinds (limited to 'src/theory/bags/kinds') diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds new file mode 100644 index 000000000..8093448a0 --- /dev/null +++ b/src/theory/bags/kinds @@ -0,0 +1,79 @@ +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. +# + +theory THEORY_BAGS \ + ::CVC4::theory::bags::TheoryBags \ + "theory/bags/theory_bags.h" +typechecker "theory/bags/theory_bags_type_rules.h" +rewriter ::CVC4::theory::bags::TheoryBagsRewriter \ + "theory/bags/theory_bags_rewriter.h" + +properties parametric +properties check propagate presolve + +# constants +constant EMPTYBAG \ + ::CVC4::EmptyBag \ + ::CVC4::EmptyBagHashFunction \ + "expr/emptybag.h" \ + "the empty bag constant; payload is an instance of the CVC4::EmptyBag class" + +# the type +operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements" +cardinality BAG_TYPE \ + "::CVC4::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \ + "theory/bags/theory_bags_type_rules.h" +well-founded BAG_TYPE \ + "::CVC4::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \ + "theory/bags/theory_bags_type_rules.h" +enumerator BAG_TYPE \ + "::CVC4::theory::bags::BagEnumerator" \ + "theory/bags/theory_bags_type_enumerator.h" + +# operators +operator UNION_MAX 2 "union for bags (max)" +operator UNION_DISJOINT 2 "disjoint union for bags (sum)" +operator INTERSECTION_MIN 2 "bag intersection (min)" + +# {("a", 2), ("b", 3)} \ {("a", 1)} = {("a", 1), ("b", 3)} +operator DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicities)" + +# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)} +operator DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)" + +operator BAG_IS_INCLUDED 2 "inclusion predicate for bags (less than or equal multiplicities)" +operator BAG_COUNT 2 "multiplicity of an element in a bag" +operator MK_BAG 2 "constructs a bag from one element along with its multiplicity" + +# The operator bag-is-singleton returns whether the given bag is a singleton +operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton" + +operator BAG_CARD 1 "bag cardinality operator" + +# The operator choose returns an element from a given bag. +# If bag A = {("a", 1)}, then the term (choose A) is equivalent to the term a. +# If the bag is empty, then (choose A) is an arbitrary value. +# If the bag has cardinality > 1, then (choose A) will deterministically return an element in A. +operator BAG_CHOOSE 1 "return an element in the bag given as a parameter" + +typerule UNION_MAX ::CVC4::theory::bags::BinaryOperatorTypeRule +typerule UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule +typerule INTERSECTION_MIN ::CVC4::theory::bags::BinaryOperatorTypeRule +typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule +typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule +typerule BAG_IS_INCLUDED ::CVC4::theory::bags::IsIncludedTypeRule +typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule +typerule MK_BAG ::CVC4::theory::bags::MkBagTypeRule +typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule +typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule +typerule BAG_CHOOSE ::CVC4::theory::bags::ChooseTypeRule +typerule BAG_IS_SINGLETON ::CVC4::theory::bags::IsSingletonTypeRule + +construle UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule +construle MK_BAG ::CVC4::theory::bags::MkBagTypeRule + +endtheory \ No newline at end of file -- cgit v1.2.3