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.
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
${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)
{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},
{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},
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(); }
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
{
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;
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>(
+ 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;
*/
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
*/
Sort getSetElementSort() const;
+ /* Bag sort ------------------------------------------------------------ */
+
+ /**
+ * @return the element sort of a bag sort
+ */
+ Sort getBagElementSort() const;
+
/* Sequence sort ------------------------------------------------------- */
/**
*/
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
*/
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
* 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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 --------------------------------------------------------------- */
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 */
buffered_proof_generator.h
emptyset.cpp
emptyset.h
+ emptybag.cpp
+ emptybag.h
expr_iomanip.cpp
expr_iomanip.h
expr_manager_scope.h
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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
--- /dev/null
+/********************* */
+/*! \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 <iosfwd>
+#include <memory>
+
+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<TypeNode> 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 */
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(
/** 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);
/** Make the type of floating-point with <code>exp</code> bit exponent and
<code>sig</code> 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 <code>size</code> */
/** 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);
return (*this)[0].getDType();
}
+bool TypeNode::isBag() const
+{
+ return getKind() == kind::BAG_TYPE;
+}
+
+TypeNode TypeNode::getBagElementType() const
+{
+ Assert(isBag());
+ return (*this)[0];
+}
+
}/* CVC4 namespace */
/**
* 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,
/** Is this a Set type? */
bool isSet() const;
+ /** Is this a Bag type? */
+ bool isBag() const;
+
/** Is this a Sequence type? */
bool isSequence() const;
/** 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;
/**
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 );
{
t = d_solver->mkEmptySet(s);
}
+ else if (k == api::EMPTYBAG)
+ {
+ t = d_solver->mkEmptyBag(s);
+ }
else if (k == api::CONST_SEQUENCE)
{
if (!s.isSequence())
* 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)
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.");
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());
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 ");
}
case kind::EMPTYSET:
out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
break;
+
+ case kind::EMPTYBAG:
+ out << "(as emptybag " << n.getConst<EmptyBag>().getType() << ")";
+ break;
case kind::BITVECTOR_EXTRACT_OP:
{
BitVectorExtract p = n.getConst<BitVectorExtract>();
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:
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";
|| 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,
{
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);
// 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()))
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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<Node, NodeHashFunction> 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 */
--- /dev/null
+# 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
--- /dev/null
+/************************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <expr/node.h>
+
+#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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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 */
--- /dev/null
+/********************* */
+/*! \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<TypeNode, Node>::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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<Node, Node, NodeHashFunction> 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<TypeNode, Node> d_emptybag;
+}; /* class Term */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
--- /dev/null
+/********************* */
+/*! \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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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 <memory>
+
+#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<Node>& 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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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<BagEnumerator>(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<BagEnumerator>(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
--- /dev/null
+/********************* */
+/*! \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<BagEnumerator>
+{
+ 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
--- /dev/null
+/********************* */
+/*! \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<Rational>().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<EmptyBag>();
+ 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 */
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 "
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)
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;
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;
THEORY_DATATYPES,
THEORY_SEP,
THEORY_SETS,
+ THEORY_BAGS,
THEORY_STRINGS,
THEORY_QUANTIFIERS,
void testMkPredicateSort();
void testMkRecordSort();
void testMkSetSort();
+ void testMkBagSort();
void testMkSequenceSort();
void testMkSortConstructorSort();
void testMkTupleSort();
void testMkConst();
void testMkConstArray();
void testMkEmptySet();
+ void testMkEmptyBag();
void testMkEmptySequence();
void testMkFalse();
void testMkFloatingPoint();
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(
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;
void testGetArrayIndexSort();
void testGetArrayElementSort();
void testGetSetElementSort();
+ void testGetBagElementSort();
void testGetSequenceElementSort();
void testGetUninterpretedSortName();
void testIsUninterpretedSortParameterized();
{
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());
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)
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_STRINGS);
info.disableTheory(THEORY_SETS);
+ info.disableTheory(THEORY_BAGS);
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableQuantifiers();
+ info.disableTheory(THEORY_BAGS);
info.lock();
TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_BV);
info.disableTheory(THEORY_DATATYPES);
+ info.disableTheory(THEORY_BAGS);
info.enableIntegers();
info.disableReals();
info.lock();
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 ) );
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#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<Node, Node> 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<Node> getNStrings(size_t n)
+ {
+ std::vector<Node> 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<Node> 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<Node> 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<ExprManager> d_em;
+ std::unique_ptr<SmtEngine> d_smt;
+ std::unique_ptr<NodeManager> d_nm;
+}; /* class BagsTypeRuleBlack */
projects / cvc5.git / commitdiff