From b509f2700e31b4189ac76e4d0eabdde050535c0a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Oct 2021 03:20:19 -0500 Subject: [PATCH] Add cardinality constraint utilities (#7286) This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF. This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms. --- src/expr/CMakeLists.txt | 2 + src/expr/cardinality_constraint.cpp | 101 ++++++++++++++++++++++++++ src/expr/cardinality_constraint.h | 105 ++++++++++++++++++++++++++++ 3 files changed, 208 insertions(+) create mode 100644 src/expr/cardinality_constraint.cpp create mode 100644 src/expr/cardinality_constraint.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 437f0b54f..e73960676 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -24,6 +24,8 @@ libcvc5_add_sources( attribute_unique_id.h bound_var_manager.cpp bound_var_manager.h + cardinality_constraint.cpp + cardinality_constraint.h emptyset.cpp emptyset.h emptybag.cpp diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp new file mode 100644 index 000000000..3841228fb --- /dev/null +++ b/src/expr/cardinality_constraint.cpp @@ -0,0 +1,101 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cardinality constraint operator + */ + +#include "expr/cardinality_constraint.h" + +#include + +#include "expr/type_node.h" + +namespace cvc5 { + +CardinalityConstraint::CardinalityConstraint(const TypeNode& type, + const Integer& ub) + : d_type(new TypeNode(type)), d_ubound(ub) +{ + AlwaysAssert(type.isSort()) + << "Unexpected cardinality constraints for " << type; +} + +CardinalityConstraint::CardinalityConstraint(const CardinalityConstraint& other) + : d_type(new TypeNode(other.getType())), d_ubound(other.getUpperBound()) +{ +} + +CardinalityConstraint::~CardinalityConstraint() {} + +const TypeNode& CardinalityConstraint::getType() const { return *d_type; } + +const Integer& CardinalityConstraint::getUpperBound() const { return d_ubound; } + +bool CardinalityConstraint::operator==(const CardinalityConstraint& cc) const +{ + return getType() == cc.getType() && getUpperBound() == cc.getUpperBound(); +} + +bool CardinalityConstraint::operator!=(const CardinalityConstraint& cc) const +{ + return !(*this == cc); +} + +std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc) +{ + return out << "fmf.card(" << cc.getType() << ", " << cc.getUpperBound() + << ')'; +} + +CombinedCardinalityConstraint::CombinedCardinalityConstraint(const Integer& ub) + : d_ubound(ub) +{ +} + +CombinedCardinalityConstraint::CombinedCardinalityConstraint( + const CombinedCardinalityConstraint& other) + : d_ubound(other.getUpperBound()) +{ +} + +CombinedCardinalityConstraint::~CombinedCardinalityConstraint() {} + +const Integer& CombinedCardinalityConstraint::getUpperBound() const +{ + return d_ubound; +} + +bool CombinedCardinalityConstraint::operator==( + const CombinedCardinalityConstraint& cc) const +{ + return getUpperBound() == cc.getUpperBound(); +} + +bool CombinedCardinalityConstraint::operator!=( + const CombinedCardinalityConstraint& cc) const +{ + return !(*this == cc); +} + +std::ostream& operator<<(std::ostream& out, + const CombinedCardinalityConstraint& cc) +{ + return out << "fmf.card(" << cc.getUpperBound() << ')'; +} + +size_t CombinedCardinalityConstraintHashFunction::operator()( + const CombinedCardinalityConstraint& cc) const +{ + return cc.getUpperBound().hash(); +} + +} // namespace cvc5 diff --git a/src/expr/cardinality_constraint.h b/src/expr/cardinality_constraint.h new file mode 100644 index 000000000..a51ba545c --- /dev/null +++ b/src/expr/cardinality_constraint.h @@ -0,0 +1,105 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cardinality constraint operator + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__CARDINALITY_CONSTRAINT_H +#define CVC5__EXPR__CARDINALITY_CONSTRAINT_H + +#include +#include + +#include "util/integer.h" +#include "util/hash.h" + +namespace cvc5 { + +class TypeNode; + +/** + * A cardinality constraint, handled in the cardinality extension of the UF + * solver, used for finite model finding. + */ +class CardinalityConstraint +{ + public: + /** + * Constructs a cardinality constraint of the specified type, which should + * be an uninterpreted sort. + */ + CardinalityConstraint(const TypeNode& ufType, const Integer& ub); + ~CardinalityConstraint(); + CardinalityConstraint(const CardinalityConstraint& other); + + /** Get the type of the cardinality constraint */ + const TypeNode& getType() const; + /** Get the upper bound value of the cardinality constraint */ + const Integer& getUpperBound() const; + + bool operator==(const CardinalityConstraint& cc) const; + bool operator!=(const CardinalityConstraint& cc) const; + + private: + /** The type that the cardinality constraint is for */ + std::unique_ptr d_type; + /** The upper bound on the cardinality of the above type */ + const Integer d_ubound; +}; + +std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc); + +using CardinalityConstraintHashFunction = PairHashFunction, + IntegerHashFunction>; + +/** + * A combined cardinality constraint, handled in the cardinality extension of + * the UF solver, used for finite model finding for bounding the sum of + * cardinalities of all uninterpreted sorts. + */ +class CombinedCardinalityConstraint +{ + public: + /** + * Constructs a cardinality constraint of the specified type, which should + * be an uninterpreted sort. + */ + CombinedCardinalityConstraint(const Integer& ub); + ~CombinedCardinalityConstraint(); + CombinedCardinalityConstraint(const CombinedCardinalityConstraint& other); + + /** Get the upper bound value of the cardinality constraint */ + const Integer& getUpperBound() const; + + bool operator==(const CombinedCardinalityConstraint& cc) const; + bool operator!=(const CombinedCardinalityConstraint& cc) const; + + private: + /** The upper bound on the cardinality of the above type */ + const Integer d_ubound; +}; + +std::ostream& operator<<(std::ostream& out, + const CombinedCardinalityConstraint& cc); + +struct CombinedCardinalityConstraintHashFunction +{ + size_t operator()(const CombinedCardinalityConstraint& cc) const; +}; + +} // namespace cvc5 + +#endif -- 2.30.2