From e4a29a6033ecc7ba5ec266f37e8f151f09ead020 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 22 Sep 2020 16:59:41 -0500 Subject: [PATCH] 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/CMakeLists.txt | 16 ++ src/api/cvc4cpp.cpp | 69 ++++- src/api/cvc4cpp.h | 27 ++ src/api/cvc4cppkind.h | 112 ++++++++ src/expr/CMakeLists.txt | 2 + src/expr/emptybag.cpp | 65 +++++ src/expr/emptybag.h | 63 +++++ src/expr/node_manager.cpp | 12 + src/expr/node_manager.h | 9 +- src/expr/type_node.cpp | 11 + src/expr/type_node.h | 10 +- src/parser/parser.cpp | 4 + src/parser/parser.h | 1 + src/parser/smt2/Smt2.g | 10 +- src/parser/smt2/smt2.cpp | 18 +- src/printer/smt2/smt2_printer.cpp | 13 +- src/smt/set_defaults.cpp | 8 +- src/theory/bags/inference_manager.cpp | 35 +++ src/theory/bags/inference_manager.h | 57 ++++ src/theory/bags/kinds | 79 ++++++ src/theory/bags/normal_form.cpp | 27 ++ src/theory/bags/normal_form.h | 44 +++ src/theory/bags/solver_state.cpp | 35 +++ src/theory/bags/solver_state.h | 44 +++ src/theory/bags/term_registry.cpp | 45 ++++ src/theory/bags/term_registry.h | 63 +++++ src/theory/bags/theory_bags.cpp | 139 ++++++++++ src/theory/bags/theory_bags.h | 110 ++++++++ src/theory/bags/theory_bags_rewriter.cpp | 37 +++ src/theory/bags/theory_bags_rewriter.h | 38 +++ .../bags/theory_bags_type_enumerator.cpp | 85 ++++++ src/theory/bags/theory_bags_type_enumerator.h | 91 +++++++ src/theory/bags/theory_bags_type_rules.h | 255 ++++++++++++++++++ src/theory/logic_info.cpp | 5 + src/theory/theory_engine.cpp | 1 + src/theory/theory_id.cpp | 2 + src/theory/theory_id.h | 1 + test/unit/api/solver_black.h | 23 ++ test/unit/api/sort_black.h | 13 + test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/logic_info_white.h | 4 + .../theory/theory_bags_type_rules_black.h | 93 +++++++ 42 files changed, 1765 insertions(+), 12 deletions(-) create mode 100644 src/expr/emptybag.cpp create mode 100644 src/expr/emptybag.h create mode 100644 src/theory/bags/inference_manager.cpp create mode 100644 src/theory/bags/inference_manager.h create mode 100644 src/theory/bags/kinds create mode 100644 src/theory/bags/normal_form.cpp create mode 100644 src/theory/bags/normal_form.h create mode 100644 src/theory/bags/solver_state.cpp create mode 100644 src/theory/bags/solver_state.h create mode 100644 src/theory/bags/term_registry.cpp create mode 100644 src/theory/bags/term_registry.h create mode 100644 src/theory/bags/theory_bags.cpp create mode 100644 src/theory/bags/theory_bags.h create mode 100644 src/theory/bags/theory_bags_rewriter.cpp create mode 100644 src/theory/bags/theory_bags_rewriter.h create mode 100644 src/theory/bags/theory_bags_type_enumerator.cpp create mode 100644 src/theory/bags/theory_bags_type_enumerator.h create mode 100644 src/theory/bags/theory_bags_type_rules.h create mode 100644 test/unit/theory/theory_bags_type_rules_black.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2279c7097..1bc393053 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -402,6 +402,21 @@ libcvc4_add_sources( theory/assertion.h theory/atom_requests.cpp theory/atom_requests.h + theory/bags/inference_manager.cpp + theory/bags/inference_manager.h + theory/bags/normal_form.cpp + theory/bags/normal_form.h + theory/bags/solver_state.cpp + theory/bags/solver_state.h + theory/bags/term_registry.cpp + theory/bags/term_registry.h + theory/bags/theory_bags.cpp + theory/bags/theory_bags.h + theory/bags/theory_bags_rewriter.cpp + theory/bags/theory_bags_rewriter.h + theory/bags/theory_bags_type_enumerator.cpp + theory/bags/theory_bags_type_enumerator.h + theory/bags/theory_bags_type_rules.h theory/booleans/circuit_propagator.cpp theory/booleans/circuit_propagator.h theory/booleans/proof_checker.cpp @@ -908,6 +923,7 @@ set(KINDS_FILES ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds + ${PROJECT_SOURCE_DIR}/src/theory/bags/kinds ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 47cc7234f..401f62cae 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -254,6 +254,19 @@ const static std::unordered_map s_kinds{ {COMPREHENSION, CVC4::Kind::COMPREHENSION}, {CHOOSE, CVC4::Kind::CHOOSE}, {IS_SINGLETON, CVC4::Kind::IS_SINGLETON}, + /* Bags ---------------------------------------------------------------- */ + {UNION_MAX, CVC4::Kind::UNION_MAX}, + {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT}, + {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN}, + {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT}, + {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE}, + {BAG_IS_INCLUDED, CVC4::Kind::BAG_IS_INCLUDED}, + {BAG_COUNT, CVC4::Kind::BAG_COUNT}, + {MK_BAG, CVC4::Kind::MK_BAG}, + {EMPTYBAG, CVC4::Kind::EMPTYBAG}, + {BAG_CARD, CVC4::Kind::BAG_CARD}, + {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE}, + {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -544,6 +557,19 @@ const static std::unordered_map {CVC4::Kind::COMPREHENSION, COMPREHENSION}, {CVC4::Kind::CHOOSE, CHOOSE}, {CVC4::Kind::IS_SINGLETON, IS_SINGLETON}, + /* Bags ------------------------------------------------------------ */ + {CVC4::Kind::UNION_MAX, UNION_MAX}, + {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT}, + {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, + {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, + {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, + {CVC4::Kind::BAG_IS_INCLUDED, BAG_IS_INCLUDED}, + {CVC4::Kind::BAG_COUNT, BAG_COUNT}, + {CVC4::Kind::MK_BAG, MK_BAG}, + {CVC4::Kind::EMPTYBAG, EMPTYBAG}, + {CVC4::Kind::BAG_CARD, BAG_CARD}, + {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE}, + {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, /* Strings --------------------------------------------------------- */ {CVC4::Kind::STRING_CONCAT, STRING_CONCAT}, {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, @@ -951,6 +977,8 @@ bool Sort::isArray() const { return d_type->isArray(); } bool Sort::isSet() const { return d_type->isSet(); } +bool Sort::isBag() const { return TypeNode::fromType(*d_type).isBag(); } + bool Sort::isSequence() const { return d_type->isSequence(); } bool Sort::isUninterpretedSort() const { return d_type->isSort(); } @@ -1069,7 +1097,17 @@ Sort Sort::getSetElementSort() const return Sort(d_solver, SetType(*d_type).getElementType()); } -/* Set sort ------------------------------------------------------------ */ +/* Bag sort ------------------------------------------------------------ */ + +Sort Sort::getBagElementSort() const +{ + CVC4_API_CHECK(isBag()) << "Not a bag sort."; + TypeNode typeNode = TypeNode::fromType(*d_type); + Type type = typeNode.getBagElementType().toType(); + return Sort(d_solver, type); +} + +/* Sequence sort ------------------------------------------------------- */ Sort Sort::getSequenceElementSort() const { @@ -3495,6 +3533,20 @@ Sort Solver::mkSetSort(Sort elemSort) const CVC4_API_SOLVER_TRY_CATCH_END; } +Sort Solver::mkBagSort(Sort elemSort) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) + << "non-null element sort"; + CVC4_API_SOLVER_CHECK_SORT(elemSort); + + TypeNode typeNode = TypeNode::fromType(*elemSort.d_type); + Type type = getNodeManager()->mkBagType(typeNode).toType(); + return Sort(this, type); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Sort Solver::mkSequenceSort(Sort elemSort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3645,6 +3697,21 @@ Term Solver::mkEmptySet(Sort s) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkEmptyBag(Sort s) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s) + << "null sort or bag sort"; + + CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s) + << "bag sort associated to this solver object"; + + return mkValHelper( + CVC4::EmptyBag(TypeNode::fromType(*s.d_type))); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkSepNil(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2cb042540..c66113f31 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -386,6 +386,12 @@ class CVC4_PUBLIC Sort */ bool isSet() const; + /** + * Is this a Bag sort? + * @return true if the sort is a Bag sort + */ + bool isBag() const; + /** * Is this a Sequence sort? * @return true if the sort is a Sequence sort @@ -525,6 +531,13 @@ class CVC4_PUBLIC Sort */ Sort getSetElementSort() const; + /* Bag sort ------------------------------------------------------------ */ + + /** + * @return the element sort of a bag sort + */ + Sort getBagElementSort() const; + /* Sequence sort ------------------------------------------------------- */ /** @@ -2303,6 +2316,13 @@ class CVC4_PUBLIC Solver */ Sort mkSetSort(Sort elemSort) const; + /** + * Create a bag sort. + * @param elemSort the sort of the bag elements + * @return the bag sort + */ + Sort mkBagSort(Sort elemSort) const; + /** * Create a sequence sort. * @param elemSort the sort of the sequence elements @@ -2568,6 +2588,13 @@ class CVC4_PUBLIC Solver */ Term mkEmptySet(Sort s) const; + /** + * Create a constant representing an empty bag of the given sort. + * @param s the sort of the bag elements. + * @return the empty bag constant + */ + Term mkEmptyBag(Sort s) const; + /** * Create a separation logic nil term. * @param sort the sort of the nil term diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 94a212fe5..5910ef1c9 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1964,6 +1964,116 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child) */ IS_SINGLETON, + /* Bags ------------------------------------------------------------------ */ + /** + * Empty bag constant. + * Parameters: 1 + * -[1]: Sort of the bag elements + * Create with: + * mkEmptyBag(Sort sort) + */ + EMPTYBAG, + /** + * Bag max union. + * Parameters: 2 + * -[1]..[2]: Terms of bag sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + UNION_MAX, + /** + * Bag disjoint union (sum). + * Parameters: 2 + * -[1]..[2]: Terms of bag sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + UNION_DISJOINT, + /** + * Bag intersection (min). + * Parameters: 2 + * -[1]..[2]: Terms of bag sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + INTERSECTION_MIN, + /** + * Bag difference subtract (subtracts multiplicities of the second from the + * first). + * Parameters: 2 + * -[1]..[2]: Terms of bag sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + DIFFERENCE_SUBTRACT, + /** + * Bag difference 2 (removes shared elements in the two bags). + * Parameters: 2 + * -[1]..[2]: Terms of bag sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + DIFFERENCE_REMOVE, + /** + * Bag is included (first multiplicities <= second multiplicities). + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + BAG_IS_INCLUDED, + /** + * Element multiplicity in a bag + * Parameters: 2 + * -[1]..[2]: Terms of bag sort (Bag E), [1] an element of sort E + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + BAG_COUNT, + /** + * The bag of the single element given as a parameter. + * Parameters: 1 + * -[1]: Single element + * Create with: + * mkTerm(Kind kind, Term child) + */ + MK_BAG, + /** + * Bag cardinality. + * Parameters: 1 + * -[1]: Bag to determine the cardinality of + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_CARD, + /** + * Returns an element from a given bag. + * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A) + * is equivalent to the term x. + * If the bag is empty, then (choose A) is an arbitrary value. + * If the bag contains distinct elements, then (choose A) will + * deterministically return an element in A. + * Parameters: 1 + * -[1]: Term of bag sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_CHOOSE, + /** + * Bag is_singleton predicate (single element with multiplicity exactly one). + * Parameters: 1 + * -[1]: Term of bag sort, is [1] a singleton bag? + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_IS_SINGLETON, /* Strings --------------------------------------------------------------- */ @@ -2664,6 +2774,8 @@ enum CVC4_PUBLIC Kind : int32_t SELECTOR_TYPE, /* set type, takes as parameter the type of the elements */ SET_TYPE, + /* bag type, takes as parameter the type of the elements */ + BAG_TYPE, /* sort tag */ SORT_TAG, /* specifies types of user-declared 'uninterpreted' sorts */ diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 14d84e320..1cc4e9a33 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -21,6 +21,8 @@ libcvc4_add_sources( buffered_proof_generator.h emptyset.cpp emptyset.h + emptybag.cpp + emptybag.h expr_iomanip.cpp expr_iomanip.h expr_manager_scope.h diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp new file mode 100644 index 000000000..888b3b92a --- /dev/null +++ b/src/expr/emptybag.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file emptybag.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 + **/ + +#include "expr/emptybag.h" + +#include + +#include "expr/type_node.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const EmptyBag& asa) +{ + return out << "emptybag(" << asa.getType() << ')'; +} + +size_t EmptyBagHashFunction::operator()(const EmptyBag& es) const +{ + return TypeNodeHashFunction()(es.getType()); +} + +/** + * Constructs an emptybag of the specified type. Note that the argument + * is the type of the bag itself, NOT the type of the elements. + */ +EmptyBag::EmptyBag(const TypeNode& bagType) : d_type(new TypeNode(bagType)) {} + +EmptyBag::EmptyBag(const EmptyBag& es) : d_type(new TypeNode(es.getType())) {} + +EmptyBag& EmptyBag::operator=(const EmptyBag& es) +{ + (*d_type) = es.getType(); + return *this; +} + +EmptyBag::~EmptyBag() {} +const TypeNode& EmptyBag::getType() const { return *d_type; } +bool EmptyBag::operator==(const EmptyBag& es) const +{ + return getType() == es.getType(); +} + +bool EmptyBag::operator!=(const EmptyBag& es) const { return !(*this == es); } +bool EmptyBag::operator<(const EmptyBag& es) const +{ + return getType() < es.getType(); +} + +bool EmptyBag::operator<=(const EmptyBag& es) const +{ + return getType() <= es.getType(); +} + +bool EmptyBag::operator>(const EmptyBag& es) const { return !(*this <= es); } +bool EmptyBag::operator>=(const EmptyBag& es) const { return !(*this < es); } +} // namespace CVC4 diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h new file mode 100644 index 000000000..a16c12d86 --- /dev/null +++ b/src/expr/emptybag.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file emptybag.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 a class for empty bags + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__EMPTY_BAG_H +#define CVC4__EMPTY_BAG_H + +#include +#include + +namespace CVC4 { + +class TypeNode; + +class CVC4_PUBLIC EmptyBag +{ + public: + /** + * Constructs an emptybag of the specified type. Note that the argument + * is the type of the bag itself, NOT the type of the elements. + */ + EmptyBag(const TypeNode& bagType); + ~EmptyBag(); + EmptyBag(const EmptyBag& other); + EmptyBag& operator=(const EmptyBag& other); + + const TypeNode& getType() const; + bool operator==(const EmptyBag& es) const; + bool operator!=(const EmptyBag& es) const; + bool operator<(const EmptyBag& es) const; + bool operator<=(const EmptyBag& es) const; + bool operator>(const EmptyBag& es) const; + bool operator>=(const EmptyBag& es) const; + + private: + EmptyBag(); + + /** the type of the empty bag itself (not the type of the elements)*/ + std::unique_ptr d_type; +}; /* class EmptyBag */ + +std::ostream& operator<<(std::ostream& out, const EmptyBag& es) CVC4_PUBLIC; + +struct CVC4_PUBLIC EmptyBagHashFunction +{ + size_t operator()(const EmptyBag& es) const; +}; /* struct EmptyBagHashFunction */ + +} // namespace CVC4 + +#endif /* CVC4__EMPTY_BAG_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6ac26fbee..3c3d6df4a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -455,6 +455,18 @@ Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, cons return n; } +TypeNode NodeManager::mkBagType(TypeNode elementType) +{ + CheckArgument( + !elementType.isNull(), elementType, "unexpected NULL element type"); + CheckArgument(elementType.isFirstClass(), + elementType, + "cannot store types that are not first-class in bags. Try " + "option --uf-ho."); + Debug("bags") << "making bags type " << elementType << std::endl; + return mkTypeNode(kind::BAG_TYPE, elementType); +} + TypeNode NodeManager::mkSequenceType(TypeNode elementType) { CheckArgument( diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0d62e686d..ef22101f0 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -565,13 +565,13 @@ class NodeManager { /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - + /** Create a boolean term variable. */ Node mkBooleanTermVariable(); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); - + /** make unique (per Type,Kind) variable. */ Node mkNullaryOperator(const TypeNode& type, Kind k); @@ -876,7 +876,7 @@ class NodeManager { /** Make the type of floating-point with exp bit exponent and sig bit significand */ - inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); inline TypeNode mkFloatingPointType(FloatingPointSize fs); /** Make the type of bitvectors of size size */ @@ -888,6 +888,9 @@ class NodeManager { /** Make the type of set with the given parameterization */ inline TypeNode mkSetType(TypeNode elementType); + /** Make the type of bags with the given parameterization */ + TypeNode mkBagType(TypeNode elementType); + /** Make the type of sequences with the given parameterization */ TypeNode mkSequenceType(TypeNode elementType); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ba3a26058..cbfb57747 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -692,4 +692,15 @@ const DType& TypeNode::getDType() const return (*this)[0].getDType(); } +bool TypeNode::isBag() const +{ + return getKind() == kind::BAG_TYPE; +} + +TypeNode TypeNode::getBagElementType() const +{ + Assert(isBag()); + return (*this)[0]; +} + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0f134353a..9ed952369 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -452,7 +452,7 @@ public: /** * Is this a first-class type? * First-class types are types for which: - * (1) we handle equalities between terms of that type, and + * (1) we handle equalities between terms of that type, and * (2) they are allowed to be parameters of parametric types (e.g. index or element types of arrays). * * Examples of types that are not first-class include constructor types, @@ -518,6 +518,9 @@ public: /** Is this a Set type? */ bool isSet() const; + /** Is this a Bag type? */ + bool isBag() const; + /** Is this a Sequence type? */ bool isSequence() const; @@ -539,6 +542,9 @@ public: /** Get the element type (for set types) */ TypeNode getSetElementType() const; + /** Get the element type (for bag types) */ + TypeNode getBagElementType() const; + /** Get the element type (for sequence types) */ TypeNode getSequenceElementType() const; /** @@ -712,7 +718,7 @@ public: static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); - /** get ensure type condition + /** get ensure type condition * Return value is a condition that implies that n has type tn. */ static Node getEnsureTypeCondition( Node n, TypeNode tn ); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1fdf5dda1..31ab49158 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -561,6 +561,10 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { t = d_solver->mkEmptySet(s); } + else if (k == api::EMPTYBAG) + { + t = d_solver->mkEmptyBag(s); + } else if (k == api::CONST_SEQUENCE) { if (!s.isSequence()) diff --git a/src/parser/parser.h b/src/parser/parser.h index 6f5d7fbe6..d478163b8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -680,6 +680,7 @@ public: * Return term t with a type ascription applied to it. This is used for * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: * - (as emptyset (Set T)) + * - (as emptybag (Bag T)) * - (as univset (Set T)) * - (as sep.nil T) * - (cons T) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 417ef5202..65f72eb28 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2086,7 +2086,15 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Illegal set type."); } t = SOLVER->mkSetSort( args[0] ); - } else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() && + } + else if(name == "Bag" && + PARSER_STATE->isTheoryEnabled(theory::THEORY_BAGS) ) { + if(args.size() != 1) { + PARSER_STATE->parseError("Illegal bag type."); + } + t = SOLVER->mkBagSort( args[0] ); + } + else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() && PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) { if(args.size() != 1) { PARSER_STATE->parseError("Illegal sequence type."); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 73d4c8c52..387117335 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -691,6 +691,21 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::TCLOSURE, "tclosure"); } + if (d_logic.isTheoryEnabled(theory::THEORY_BAGS)) + { + defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort())); + addOperator(api::UNION_MAX, "union_max"); + addOperator(api::UNION_DISJOINT, "union_disjoint"); + addOperator(api::INTERSECTION_MIN, "intersection_min"); + addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract"); + addOperator(api::DIFFERENCE_REMOVE, "difference_remove"); + addOperator(api::BAG_IS_INCLUDED, "bag.is_included"); + addOperator(api::BAG_COUNT, "bag.count"); + addOperator(api::MK_BAG, "mkBag"); + addOperator(api::BAG_CARD, "bag.card"); + addOperator(api::BAG_CHOOSE, "bag.choose"); + addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton"); + } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { defineType("String", d_solver->getStringSort()); defineType("RegLan", d_solver->getRegExpSort()); @@ -821,7 +836,8 @@ void Smt2::checkLogicAllowsFreeSorts() if (!d_logic.isTheoryEnabled(theory::THEORY_UF) && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS) && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES) - && !d_logic.isTheoryEnabled(theory::THEORY_SETS)) + && !d_logic.isTheoryEnabled(theory::THEORY_SETS) + && !d_logic.isTheoryEnabled(theory::THEORY_BAGS)) { parseErrorLogic("Free sort symbols not allowed in "); } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 1ac7cf0c8..9350111c7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -283,6 +283,10 @@ void Smt2Printer::toStream(std::ostream& out, case kind::EMPTYSET: out << "(as emptyset " << n.getConst().getType() << ")"; break; + + case kind::EMPTYBAG: + out << "(as emptybag " << n.getConst().getType() << ")"; + break; case kind::BITVECTOR_EXTRACT_OP: { BitVectorExtract p = n.getConst(); @@ -745,6 +749,9 @@ void Smt2Printer::toStream(std::ostream& out, case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; + // bags + case kind::BAG_TYPE: out << smtKindString(k, d_variant) << " "; break; + // fp theory case kind::FLOATINGPOINT_FP: case kind::FLOATINGPOINT_EQ: @@ -1151,8 +1158,10 @@ static string smtKindString(Kind k, Variant v) case kind::JOIN: return "join"; case kind::PRODUCT: return "product"; case kind::TRANSPOSE: return "transpose"; - case kind::TCLOSURE: - return "tclosure"; + case kind::TCLOSURE: return "tclosure"; + + // bag theory + case kind::BAG_TYPE: return "Bag"; // fp theory case kind::FLOATINGPOINT_FP: return "fp"; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c1e05b10c..2dc0d52ac 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -561,6 +561,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isTheoryEnabled(THEORY_SETS) + || logic.isTheoryEnabled(THEORY_BAGS) // Non-linear arithmetic requires UF to deal with division/mod because // their expansion introduces UFs for the division/mod-by-zero case. // If we are eliminating non-linear arithmetic via solve-int-as-bv, @@ -594,7 +595,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) && !logic.isTheoryEnabled(THEORY_STRINGS) - && !logic.isTheoryEnabled(THEORY_SETS)) + && !logic.isTheoryEnabled(THEORY_SETS) + && !logic.isTheoryEnabled(THEORY_BAGS)) { Trace("smt") << "setting theoryof-mode to term-based" << std::endl; options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); @@ -1274,7 +1276,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // introduces new literals into the search. This includes quantifiers // (quantifier instantiation), and the lemma schemas used in non-linear // and sets. We also can't use it if models are enabled. - if (logic.isTheoryEnabled(THEORY_SETS) || logic.isQuantified() + if (logic.isTheoryEnabled(THEORY_SETS) + || logic.isTheoryEnabled(THEORY_BAGS) + || logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp new file mode 100644 index 000000000..4d18ad926 --- /dev/null +++ b/src/theory/bags/inference_manager.cpp @@ -0,0 +1,35 @@ +/********************* */ +/*! \file inference_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Implementation of the inference manager for the theory of bags + **/ + +#include "theory/bags/inference_manager.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace bags { + +InferenceManager::InferenceManager(Theory& t, + SolverState& s, + ProofNodeManager* pnm) + : InferenceManagerBuffered(t, s, pnm), d_state(s) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h new file mode 100644 index 000000000..4b4edbaef --- /dev/null +++ b/src/theory/bags/inference_manager.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file inference_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 The inference manager for the theory of bags. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H +#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H + +#include "theory/bags/solver_state.h" +#include "theory/inference_manager_buffered.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +/** Inference manager + * + * This class manages inferences produced by the theory of bags. It manages + * whether inferences are processed as external lemmas on the output channel + * of theory of bags or internally as literals asserted to the equality engine + * of theory of bags. The latter literals are referred to as "facts". + */ +class InferenceManager : public InferenceManagerBuffered +{ + typedef context::CDHashSet NodeSet; + + public: + InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); + + private: + /** constants */ + Node d_true; + Node d_false; + /** + * Reference to the state object for the theory of bags. We store the + * (derived) state here, since it has additional methods required in this + * class. + */ + SolverState& d_state; +}; + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */ 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 diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp new file mode 100644 index 000000000..d9248615b --- /dev/null +++ b/src/theory/bags/normal_form.cpp @@ -0,0 +1,27 @@ +/************************* */ +/*! \file normal_form.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 + **/ + +#include "normal_form.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +bool NormalForm::checkNormalConstant(TNode n) +{ + // TODO(projects#223): complete this function + return false; +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 \ No newline at end of file diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h new file mode 100644 index 000000000..73fd8dba8 --- /dev/null +++ b/src/theory/bags/normal_form.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file normal_form.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Normal form for bag constants. + **/ + +#include "cvc4_private.h" +#include + +#ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H +#define CVC4__THEORY__BAGS__NORMAL_FORM_H + +namespace CVC4 { +namespace theory { +namespace bags { + +class NormalForm +{ + public: + /** + * Returns true if n is considered a to be a (canonical) constant bag value. + * A canonical bag value is one whose AST is: + * (disjoint-union (mk-bag e1 n1) ... + * (disjoint-union (mk-bag e_{n-1} n_{n-1}) (mk-bag e_n n_n)))) + * where c1 ... cn are constants and the node identifier of these constants + * are such that: + * c1 > ... > cn. + * Also handles the corner cases of empty bag and singleton bag. + */ + static bool checkNormalConstant(TNode n); +}; +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */ diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp new file mode 100644 index 000000000..77204ae76 --- /dev/null +++ b/src/theory/bags/solver_state.cpp @@ -0,0 +1,35 @@ +/********************* */ +/*! \file solver_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Implementation of bags state object + **/ + +#include "theory/bags/solver_state.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace bags { + +SolverState::SolverState(context::Context* c, + context::UserContext* u, + Valuation val) + : TheoryState(c, u, val) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h new file mode 100644 index 000000000..f5b67cb78 --- /dev/null +++ b/src/theory/bags/solver_state.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file solver_state.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags state object + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H +#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H + +#include +#include + +#include "theory/theory_state.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +class SolverState : public TheoryState +{ + public: + SolverState(context::Context* c, context::UserContext* u, Valuation val); + + private: + /** constants */ + Node d_true; + Node d_false; +}; /* class SolverState */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */ diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp new file mode 100644 index 000000000..60beef29f --- /dev/null +++ b/src/theory/bags/term_registry.cpp @@ -0,0 +1,45 @@ +/********************* */ +/*! \file term_registry.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Implementation of bags term registry object + **/ + +#include "theory/bags/term_registry.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace bags { + +TermRegistry::TermRegistry(SolverState& state, InferenceManager& im) + : d_im(im), + d_proxy(state.getUserContext()), + d_proxy_to_term(state.getUserContext()) +{ +} + +Node TermRegistry::getEmptyBag(TypeNode tn) +{ + std::map::iterator it = d_emptybag.find(tn); + if (it != d_emptybag.end()) + { + return it->second; + } + Node n = NodeManager::currentNM()->mkConst(EmptySet(tn)); + d_emptybag[tn] = n; + return n; +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h new file mode 100644 index 000000000..d284126ee --- /dev/null +++ b/src/theory/bags/term_registry.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file term_registry.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags state object + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H +#define CVC4__THEORY__BAGS__TERM_REGISTRY_H + +#include +#include + +#include "context/cdhashmap.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +/** + * Term registry, the purpose of this class is to maintain a database of + * commonly used terms, and mappings from bags to their "proxy variables". + */ +class TermRegistry +{ + typedef context::CDHashMap NodeMap; + + public: + TermRegistry(SolverState& state, InferenceManager& im); + + /** + * Returns the existing empty bag for type tn + * or creates a new one and returns it. + **/ + Node getEmptyBag(TypeNode tn); + + private: + /** The inference manager */ + InferenceManager& d_im; + /** Map from bag terms to their proxy variables */ + NodeMap d_proxy; + /** Backwards map of above */ + NodeMap d_proxy_to_term; + /** Map from types to empty bag of that type */ + std::map d_emptybag; +}; /* class Term */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */ diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp new file mode 100644 index 000000000..5ddd17302 --- /dev/null +++ b/src/theory/bags/theory_bags.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file theory_bags.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags theory. + **/ + +#include "theory/bags/theory_bags.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace bags { + +TheoryBags::TheoryBags(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm), + d_state(c, u, valuation), + d_im(*this, d_state, pnm), + d_rewriter(), + d_notify(*this, d_im) +{ + // use the official theory state and inference manager objects + d_theoryState = &d_state; + d_inferManager = &d_im; +} + +TheoryBags::~TheoryBags() {} + +TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; } + +bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi) +{ + esi.d_notify = &d_notify; + esi.d_name = "theory::bags::ee"; + return true; +} + +void TheoryBags::finishInit() +{ + Assert(d_equalityEngine != nullptr); + + // choice is used to eliminate witness + d_valuation.setUnevaluatedKind(WITNESS); + + // functions we are doing congruence over + d_equalityEngine->addFunctionKind(UNION_MAX); + d_equalityEngine->addFunctionKind(UNION_DISJOINT); + d_equalityEngine->addFunctionKind(INTERSECTION_MIN); + d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT); + d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE); + d_equalityEngine->addFunctionKind(BAG_COUNT); + d_equalityEngine->addFunctionKind(MK_BAG); + d_equalityEngine->addFunctionKind(BAG_CARD); +} + +void TheoryBags::postCheck(Effort level) {} + +void TheoryBags::notifyFact(TNode atom, + bool polarity, + TNode fact, + bool isInternal) +{ +} + +bool TheoryBags::collectModelValues(TheoryModel* m, + const std::set& termBag) +{ + return true; +} + +TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); } + +Node TheoryBags::getModelValue(TNode node) { return Node::null(); } + +void TheoryBags::preRegisterTerm(TNode node) {} + +TrustNode TheoryBags::expandDefinition(Node n) +{ + // TODO(projects#224): add choose and is_singleton here + return TrustNode::null(); +} + +void TheoryBags::presolve() {} + +/**************************** eq::NotifyClass *****************************/ + +void TheoryBags::eqNotifyNewClass(TNode t) +{ + Assert(false) << "Not implemented yet" << std::endl; +} + +void TheoryBags::eqNotifyMerge(TNode t1, TNode t2) +{ + Assert(false) << "Not implemented yet" << std::endl; +} + +void TheoryBags::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) +{ + Assert(false) << "Not implemented yet" << std::endl; +} + +void TheoryBags::NotifyClass::eqNotifyNewClass(TNode t) +{ + Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:" + << " t = " << t << std::endl; + d_theory.eqNotifyNewClass(t); +} + +void TheoryBags::NotifyClass::eqNotifyMerge(TNode t1, TNode t2) +{ + Debug("bags-eq") << "[bags-eq] eqNotifyMerge:" + << " t1 = " << t1 << " t2 = " << t2 << std::endl; + d_theory.eqNotifyMerge(t1, t2); +} + +void TheoryBags::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) +{ + Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:" + << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason + << std::endl; + d_theory.eqNotifyDisequal(t1, t2, reason); +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h new file mode 100644 index 000000000..44f7ae1b0 --- /dev/null +++ b/src/theory/bags/theory_bags.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file theory_bags.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags theory. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H +#define CVC4__THEORY__BAGS__THEORY_BAGS_H + +#include + +#include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" +#include "theory/bags/theory_bags_rewriter.h" +#include "theory/theory.h" +#include "theory/theory_eq_notify.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +class TheoryBags : public Theory +{ + public: + /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */ + TheoryBags(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm); + ~TheoryBags() override; + + //--------------------------------- initialization + /** get the official theory rewriter of this theory */ + TheoryRewriter* getTheoryRewriter() override; + /** + * Returns true if we need an equality engine. If so, we initialize the + * information regarding how it should be setup. For details, see the + * documentation in Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; + /** finish initialization */ + void finishInit() override; + //--------------------------------- end initialization + + //--------------------------------- standard check + /** Post-check, called after the fact queue of the theory is processed. */ + void postCheck(Effort level) override; + /** Notify fact */ + void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; + //--------------------------------- end standard check + /** Collect model values in m based on the relevant terms given by termSet */ + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; + TrustNode explain(TNode) override; + Node getModelValue(TNode) override; + std::string identify() const override { return "THEORY_BAGS"; } + void preRegisterTerm(TNode node) override; + TrustNode expandDefinition(Node n) override; + void presolve() override; + + private: + /** Functions to handle callbacks from equality engine */ + class NotifyClass : public TheoryEqNotifyClass + { + public: + NotifyClass(TheoryBags& theory, TheoryInferenceManager& inferenceManager) + + : TheoryEqNotifyClass(inferenceManager), d_theory(theory) + { + } + void eqNotifyNewClass(TNode t) override; + void eqNotifyMerge(TNode t1, TNode t2) override; + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; + + private: + TheoryBags& d_theory; + }; + + /** The state of the bags solver at full effort */ + SolverState d_state; + /** The inference manager */ + InferenceManager d_im; + /** Instance of the above class */ + NotifyClass d_notify; + /** The theory rewriter for this theory. */ + TheoryBagsRewriter d_rewriter; + + void eqNotifyNewClass(TNode t); + void eqNotifyMerge(TNode t1, TNode t2); + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); +}; /* class TheoryBags */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */ diff --git a/src/theory/bags/theory_bags_rewriter.cpp b/src/theory/bags/theory_bags_rewriter.cpp new file mode 100644 index 000000000..aaf0ab98c --- /dev/null +++ b/src/theory/bags/theory_bags_rewriter.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file theory_bags_rewriter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags theory rewriter. + **/ + +#include "theory/bags/theory_bags_rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace bags { + +RewriteResponse TheoryBagsRewriter::postRewrite(TNode node) +{ + // TODO(projects#225): complete the code here + return RewriteResponse(REWRITE_DONE, node); +} + +RewriteResponse TheoryBagsRewriter::preRewrite(TNode node) +{ + // TODO(projects#225): complete the code here + return RewriteResponse(REWRITE_DONE, node); +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bags/theory_bags_rewriter.h b/src/theory/bags/theory_bags_rewriter.h new file mode 100644 index 000000000..7be88636a --- /dev/null +++ b/src/theory/bags/theory_bags_rewriter.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file theory_bags_rewriter.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Bags theory rewriter. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H +#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +class TheoryBagsRewriter : public TheoryRewriter +{ + public: + RewriteResponse postRewrite(TNode node) override; + + RewriteResponse preRewrite(TNode node) override; +}; /* class TheoryBagsRewriter */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */ diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp new file mode 100644 index 000000000..7975bb379 --- /dev/null +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file theory_bags_type_enumerator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 bag enumerator implementation + **/ + +#include "theory/bags/theory_bags_type_enumerator.h" + +#include "expr/emptybag.h" +#include "theory/rewriter.h" +#include "theory_bags_type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +BagEnumerator::BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase(type), + d_nodeManager(NodeManager::currentNM()), + d_elementTypeEnumerator(type.getBagElementType(), tep) +{ + d_currentBag = d_nodeManager->mkConst(EmptyBag(type)); + d_element = *d_elementTypeEnumerator; +} + +BagEnumerator::BagEnumerator(const BagEnumerator& enumerator) + : TypeEnumeratorBase(enumerator.getType()), + d_nodeManager(enumerator.d_nodeManager), + d_elementTypeEnumerator(enumerator.d_elementTypeEnumerator), + d_currentBag(enumerator.d_currentBag), + d_element(enumerator.d_element) +{ +} + +BagEnumerator::~BagEnumerator() {} + +Node BagEnumerator::operator*() +{ + Trace("bag-type-enum") << "BagEnumerator::operator* d_currentBag = " + << d_currentBag << std::endl; + + return d_currentBag; +} + +BagEnumerator& BagEnumerator::operator++() +{ + // increase the multiplicity by one + Node one = d_nodeManager->mkConst(Rational(1)); + Node singleton = d_nodeManager->mkNode(kind::MK_BAG, d_element, one); + if (d_currentBag.getKind() == kind::EMPTYBAG) + { + d_currentBag = singleton; + } + else + { + d_currentBag = + d_nodeManager->mkNode(kind::UNION_DISJOINT, singleton, d_currentBag); + } + + d_currentBag = Rewriter::rewrite(d_currentBag); + + Assert(d_currentBag.isConst()); + + Trace("bag-type-enum") << "BagEnumerator::operator++ d_currentBag = " + << d_currentBag << std::endl; + return *this; +} + +bool BagEnumerator::isFinished() +{ + // bags sequence is infinite and it never ends + return false; +} + +} // namespace bags +} // namespace theory +} // namespace CVC4 \ No newline at end of file diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h new file mode 100644 index 000000000..26639afd8 --- /dev/null +++ b/src/theory/bags/theory_bags_type_enumerator.h @@ -0,0 +1,91 @@ +/********************* */ +/*! \file theory_bags_type_enumerator.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 type enumerator for bags + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H +#define CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H + +#include "expr/type_node.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +class BagEnumerator : public TypeEnumeratorBase +{ + public: + BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + BagEnumerator(const BagEnumerator& enumerator); + ~BagEnumerator(); + + Node operator*() override; + + /** + * This operator iterates over the infinite bags constructed from the element + * type . Ideally iterating over bags of {1, 2, 3, ...} will return the + * following infinite sequence of bags, where n in the pair (m, n) means the + * multiplicity of the element m in the bag + * {}, sum = 0, #elements = 0, cardinality = 0 + * + * {(1,1)}, sum = 2, #elements = 1, cardinality = 1 + * + * {(2,1)}, sum = 3, #elements = 2, cardinality = 1 + * {(1,2)}, sum = 3, #elements = 2, cardinality = 2 + * + * {(3, 1)}, sum = 4, #elements = 3, cardinality = 1 + * {(2, 2)}, sum = 4, #elements = 3, cardinality = 2 + * {(1, 3)}, sum = 4, #elements = 3, cardinality = 3 + * + * {(4, 1)}, sum = 5, #elements = 4, cardinality = 1 + * {(3, 2)}, sum = 5, #elements = 4, cardinality = 2 + * {(1, 1),(2, 1)}, sum = 5, #elements = 4, cardinality = 2 + * {(2, 3)}, sum = 5, #elements = 4, cardinality = 3 + * {(1, 4)}, sum = 5, #elements = 4, cardinality = 4 + * + * {(5, 1)}, sum = 6, #elements = 5, cardinality = 1 + * {(4, 2)}, sum = 6, #elements = 5, cardinality = 2 + * {(1, 1), (3,1)}, sum = 6, #elements = 5, cardinality = 2 + * {(3, 3)}, sum = 6, #elements = 5, cardinality = 3 + * {(1, 1), (2,2)}, sum = 6, #elements = 5, cardinality = 3 + * {(1, 2), (2,1)}, sum = 6, #elements = 5, cardinality = 3 + * {(2, 4)}, sum = 6, #elements = 5, cardinality = 4 + * {(1, 5)}, sum = 6, #elements = 5, cardinality = 5 + * + * This seems too expensive to implement. + * For now we are implementing an obvious solution + * {(1,1)}, {(1,2)}, {(1,3)}, ... which works for both fininte and infinite + * types + */ + BagEnumerator& operator++() override; + + bool isFinished() override; + + private: + /** a pointer to the node manager */ + NodeManager* d_nodeManager; + /** an enumerator for the set of pairs of element type x integer type */ + TypeEnumerator d_elementTypeEnumerator; + /** the current set returned by the set enumerator */ + Node d_currentBag; + /** the first value returned by the element type enumerator*/ + Node d_element; +}; /* class BagEnumerator */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */ \ No newline at end of file diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h new file mode 100644 index 000000000..fc5a19348 --- /dev/null +++ b/src/theory/bags/theory_bags_type_rules.h @@ -0,0 +1,255 @@ +/********************* */ +/*! \file theory_bags_type_rules.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Bags theory type rules. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H +#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H + +#include "theory/bags/normal_form.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +struct BinaryOperatorTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT + || n.getKind() == kind::INTERSECTION_MIN + || n.getKind() == kind::DIFFERENCE_SUBTRACT + || n.getKind() == kind::DIFFERENCE_REMOVE); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "operator expects a bag, first argument is not"); + } + TypeNode secondBagType = n[1].getType(check); + if (secondBagType != bagType) + { + if (n.getKind() == kind::INTERSECTION_MIN) + { + bagType = TypeNode::mostCommonTypeNode(secondBagType, bagType); + } + else + { + bagType = TypeNode::leastCommonTypeNode(secondBagType, bagType); + } + if (bagType.isNull()) + { + throw TypeCheckingExceptionPrivate( + n, "operator expects two bags of comparable types"); + } + } + } + return bagType; + } + + static bool computeIsConst(NodeManager* nodeManager, TNode n) + { + // only UNION_DISJOINT has a const rule in kinds. + // Other binary operators do not have const rules in kinds + Assert(n.getKind() == kind::UNION_DISJOINT); + return NormalForm::checkNormalConstant(n); + } +}; /* struct BinaryOperatorTypeRule */ + +struct IsIncludedTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_IS_INCLUDED); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "BAG_IS_INCLUDED operating on non-bag"); + } + TypeNode secondBagType = n[1].getType(check); + if (secondBagType != bagType) + { + if (!bagType.isComparableTo(secondBagType)) + { + throw TypeCheckingExceptionPrivate( + n, "BAG_IS_INCLUDED operating on bags of different types"); + } + } + } + return nodeManager->booleanType(); + } +}; /* struct IsIncludedTypeRule */ + +struct CountTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_COUNT); + TypeNode bagType = n[1].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "checking for membership in a non-bag"); + } + TypeNode elementType = n[0].getType(check); + // TODO(projects#226): comments from sets + // + // T : (Bag Int) + // B : (Bag Real) + // (= (as T (Bag Real)) B) + // (= (bag-count 0.5 B) 1) + // ...where (bag-count 0.5 T) is inferred + + if (!elementType.isComparableTo(bagType.getBagElementType())) + { + std::stringstream ss; + ss << "member operating on bags of different types:\n" + << "child type: " << elementType << "\n" + << "not subtype: " << bagType.getBagElementType() << "\n" + << "in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return nodeManager->integerType(); + } +}; /* struct CountTypeRule */ + +struct MkBagTypeRule +{ + static TypeNode computeType(NodeManager* nm, TNode n, bool check) + { + Assert(n.getKind() == kind::MK_BAG); + if (check) + { + if (n.getNumChildren() != 2) + { + std::stringstream ss; + ss << "operands in term " << n << " are " << n.getNumChildren() + << ", but MK_BAG expects 2 operands."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + TypeNode type1 = n[1].getType(check); + if (!type1.isInteger()) + { + std::stringstream ss; + ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + + return nm->mkBagType(n[0].getType(check)); + } + + static bool computeIsConst(NodeManager* nodeManager, TNode n) + { + Assert(n.getKind() == kind::MK_BAG); + // for a bag to be a constant, both the element and its multiplicity should + // be constants, and the multiplicity should be > 0. + return n[0].isConst() && n[1].isConst() + && n[1].getConst().sgn() == 1; + } +}; /* struct MkBagTypeRule */ + +struct IsSingletonTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_IS_SINGLETON); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found"); + } + } + return nodeManager->booleanType(); + } +}; /* struct IsMkBagTypeRule */ + +struct EmptyBagTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::EMPTYBAG); + EmptyBag emptyBag = n.getConst(); + return emptyBag.getType(); + } +}; /* struct EmptyBagTypeRule */ + +struct CardTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_CARD); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "cardinality operates on a bag, non-bag object found"); + } + } + return nodeManager->integerType(); + } +}; /* struct CardTypeRule */ + +struct ChooseTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_CHOOSE); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "CHOOSE operator expects a bag, a non-bag is found"); + } + } + return bagType.getBagElementType(); + } +}; /* struct ChooseTypeRule */ + +struct BagsProperties +{ + static Cardinality computeCardinality(TypeNode type) + { + return Cardinality::UNKNOWN_CARD; + } + + static bool isWellFounded(TypeNode type) { return type[0].isWellFounded(); } + + static Node mkGroundTerm(TypeNode type) + { + Assert(type.isBag()); + return NodeManager::currentNM()->mkConst(EmptyBag(type)); + } +}; /* struct BagsProperties */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 4bbbdc322..73cd920d2 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -338,6 +338,11 @@ std::string LogicInfo::getLogicString() const { ss << "FS"; ++seen; } + if (d_theories[THEORY_BAGS]) + { + ss << "FB"; + ++seen; + } if(seen != d_sharingTheories) { Unhandled() << "can't extract a logic string from LogicInfo; at least one " diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2d32b34d4..a425441fd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -82,6 +82,7 @@ namespace theory { CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS) diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index 5c11c340a..31b864e7f 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -43,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId) case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break; case THEORY_SEP: out << "THEORY_SEP"; break; case THEORY_SETS: out << "THEORY_SETS"; break; + case THEORY_BAGS: out << "THEORY_BAGS"; break; case THEORY_STRINGS: out << "THEORY_STRINGS"; break; case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break; @@ -65,6 +66,7 @@ std::string getStatsPrefix(TheoryId theoryId) case THEORY_DATATYPES: return "theory::datatypes"; break; case THEORY_SEP: return "theory::sep"; break; case THEORY_SETS: return "theory::sets"; break; + case THEORY_BAGS: return "theory::bags"; break; case THEORY_STRINGS: return "theory::strings"; break; case THEORY_QUANTIFIERS: return "theory::quantifiers"; break; diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index 60e005cf7..e0dfaa507 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -42,6 +42,7 @@ enum TheoryId THEORY_DATATYPES, THEORY_SEP, THEORY_SETS, + THEORY_BAGS, THEORY_STRINGS, THEORY_QUANTIFIERS, diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 7861bf7ae..8a4d878ef 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -48,6 +48,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPredicateSort(); void testMkRecordSort(); void testMkSetSort(); + void testMkBagSort(); void testMkSequenceSort(); void testMkSortConstructorSort(); void testMkTupleSort(); @@ -59,6 +60,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkConst(); void testMkConstArray(); void testMkEmptySet(); + void testMkEmptyBag(); void testMkEmptySequence(); void testMkFalse(); void testMkFloatingPoint(); @@ -425,6 +427,16 @@ void SolverBlack::testMkSetSort() CVC4ApiException&); } +void SolverBlack::testMkBagSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getIntegerSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->mkBitVectorSort(4))); + Solver slv; + TS_ASSERT_THROWS(slv.mkBagSort(d_solver->mkBitVectorSort(4)), + CVC4ApiException&); +} + void SolverBlack::testMkSequenceSort() { TS_ASSERT_THROWS_NOTHING( @@ -596,6 +608,17 @@ void SolverBlack::testMkEmptySet() TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } +void SolverBlack::testMkEmptyBag() +{ + Solver slv; + Sort s = d_solver->mkBagSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(Sort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(s)); + TS_ASSERT_THROWS(d_solver->mkEmptyBag(d_solver->getBooleanSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkEmptyBag(s), CVC4ApiException&); +} + void SolverBlack::testMkEmptySequence() { Solver slv; diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index a12bd969d..32108bf84 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -35,6 +35,7 @@ class SortBlack : public CxxTest::TestSuite void testGetArrayIndexSort(); void testGetArrayElementSort(); void testGetSetElementSort(); + void testGetBagElementSort(); void testGetSequenceElementSort(); void testGetUninterpretedSortName(); void testIsUninterpretedSortParameterized(); @@ -193,10 +194,22 @@ void SortBlack::testGetSetElementSort() { Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); + Sort elementSort = setSort.getSetElementSort(); + TS_ASSERT(elementSort == d_solver.getIntegerSort()); Sort bvSort = d_solver.mkBitVectorSort(32); TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); } +void SortBlack::testGetBagElementSort() +{ + Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(bagSort.getBagElementSort()); + Sort elementSort = bagSort.getBagElementSort(); + TS_ASSERT(elementSort == d_solver.getIntegerSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getBagElementSort(), CVC4ApiException&); +} + void SortBlack::testGetSequenceElementSort() { Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index fed5de90b..f40d9658b 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -14,6 +14,7 @@ cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) +cvc4_add_unit_test_white(theory_bags_type_rules_black theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 341b370c4..7990d9e54 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -538,6 +538,7 @@ public: TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_STRINGS); info.disableTheory(THEORY_SETS); + info.disableTheory(THEORY_BAGS); info.arithOnlyLinear(); info.disableIntegers(); info.lock(); @@ -546,6 +547,7 @@ public: info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); info.disableQuantifiers(); + info.disableTheory(THEORY_BAGS); info.lock(); TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); @@ -553,6 +555,7 @@ public: TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_BV); info.disableTheory(THEORY_DATATYPES); + info.disableTheory(THEORY_BAGS); info.enableIntegers(); info.disableReals(); info.lock(); @@ -564,6 +567,7 @@ public: info.disableTheory(THEORY_UF); info.disableTheory(THEORY_FP); info.disableTheory(THEORY_SEP); + info.disableTheory(THEORY_BAGS); info.lock(); TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" ); TS_ASSERT( info.isPure( THEORY_ARRAYS ) ); diff --git a/test/unit/theory/theory_bags_type_rules_black.h b/test/unit/theory/theory_bags_type_rules_black.h new file mode 100644 index 000000000..e5ec60154 --- /dev/null +++ b/test/unit/theory/theory_bags_type_rules_black.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file theory_bags_type_rules_black.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** 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 Black box testing of bags typing rules + **/ + +#include + +#include "expr/dtype.h" +#include "smt/smt_engine.h" +#include "theory/bags/theory_bags_type_rules.h" +#include "theory/strings/type_enumerator.h" + +using namespace CVC4; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::kind; +using namespace CVC4::theory::bags; +using namespace std; + +typedef expr::Attribute attribute; + +class BagsTypeRuleBlack : public CxxTest::TestSuite +{ + public: + void setUp() override + { + d_em.reset(new ExprManager()); + d_smt.reset(new SmtEngine(d_em.get())); + d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt->finishInit(); + } + + void tearDown() override + { + d_smt.reset(); + d_nm.release(); + d_em.reset(); + } + + std::vector getNStrings(size_t n) + { + std::vector elements(n); + CVC4::theory::strings::StringEnumerator enumerator(d_nm->stringType()); + + for (size_t i = 0; i < n; i++) + { + ++enumerator; + elements[i] = *enumerator; + } + + return elements; + } + + void testCountOperator() + { + vector elements = getNStrings(1); + Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(100))); + + Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag); + Node node = d_nm->mkConst(Rational(10)); + + // node of type Int is not compatible with bag of type (Bag String) + TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag), + TypeCheckingExceptionPrivate&); + } + + void testMkBagOperator() + { + vector elements = getNStrings(1); + Node negative = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1))); + Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0))); + Node positive = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(1))); + + // only positive multiplicity are constants + TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), negative)); + TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), zero)); + TS_ASSERT(MkBagTypeRule::computeIsConst(d_nm.get(), positive)); + } + + private: + std::unique_ptr d_em; + std::unique_ptr d_smt; + std::unique_ptr d_nm; +}; /* class BagsTypeRuleBlack */ -- 2.30.2