From: Andrew Reynolds Date: Tue, 24 May 2022 20:01:19 +0000 (-0500) Subject: Introduce function array constant (#8793) X-Git-Tag: cvc5-1.0.1~99 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43f6eb50ca934b2c0d142fcd4d6b571a8789676f;p=cvc5.git Introduce function array constant (#8793) This introduces the FUNCTION_ARRAY_CONST kind and its payload FunctionArrayConst. This is in preparation for refactoring isConst for functions in higher-order. In particular, the plan is to never consider LAMBDA to denote a value of function sort. Instead, lambdas may be written to function array constants, whose uniqueness is trivial to justify. This refactoring when completed will furthermore eliminate the last remaining static calls to the rewriter, to be done in a followup PR. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index a72a4998a..9462b7cdf 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -35,6 +35,8 @@ libcvc5_add_sources( emptyset.h emptybag.cpp emptybag.h + function_array_const.cpp + function_array_const.h kind_map.h match_trie.cpp match_trie.h diff --git a/src/expr/function_array_const.cpp b/src/expr/function_array_const.cpp new file mode 100644 index 000000000..adefd673a --- /dev/null +++ b/src/expr/function_array_const.cpp @@ -0,0 +1,123 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Function array constant, which is an almost constant function + */ + +#include "expr/function_array_const.h" + +#include + +#include "base/check.h" +#include "expr/node.h" +#include "expr/type_node.h" + +using namespace std; + +namespace cvc5::internal { + +bool isFunctionCompatibleWithArray(const TypeNode& ftype, const TypeNode& atype) +{ + if (!ftype.isFunction()) + { + return false; + } + std::vector argTypes = ftype.getArgTypes(); + TypeNode atc = atype; + for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) + { + if (!atc.isArray() || argTypes[i] != atc.getArrayIndexType()) + { + return false; + } + atc = atc.getArrayConstituentType(); + } + return true; +} + +FunctionArrayConst::FunctionArrayConst(const TypeNode& type, const Node& avalue) + : d_type(), d_avalue() +{ + Assert(avalue.isConst()); + Assert(avalue.getType().isArray()); + Assert(isFunctionCompatibleWithArray(type, avalue.getType())); + + d_type.reset(new TypeNode(type)); + d_avalue.reset(new Node(avalue)); +} + +FunctionArrayConst::FunctionArrayConst(const FunctionArrayConst& other) + : d_type(new TypeNode(other.getType())), + d_avalue(new Node(other.getArrayValue())) +{ +} + +FunctionArrayConst::~FunctionArrayConst() {} +FunctionArrayConst& FunctionArrayConst::operator=( + const FunctionArrayConst& other) +{ + (*d_type) = other.getType(); + (*d_avalue) = other.getArrayValue(); + return *this; +} + +const TypeNode& FunctionArrayConst::getType() const { return *d_type; } + +const Node& FunctionArrayConst::getArrayValue() const { return *d_avalue; } + +bool FunctionArrayConst::operator==(const FunctionArrayConst& fc) const +{ + return getType() == fc.getType() && getArrayValue() == fc.getArrayValue(); +} + +bool FunctionArrayConst::operator!=(const FunctionArrayConst& fc) const +{ + return !(*this == fc); +} + +bool FunctionArrayConst::operator<(const FunctionArrayConst& fc) const +{ + return (getType() < fc.getType()) + || (getType() == fc.getType() && getArrayValue() < fc.getArrayValue()); +} + +bool FunctionArrayConst::operator<=(const FunctionArrayConst& fc) const +{ + return (getType() < fc.getType()) + || (getType() == fc.getType() + && getArrayValue() <= fc.getArrayValue()); +} + +bool FunctionArrayConst::operator>(const FunctionArrayConst& fc) const +{ + return !(*this <= fc); +} + +bool FunctionArrayConst::operator>=(const FunctionArrayConst& fc) const +{ + return !(*this < fc); +} + +std::ostream& operator<<(std::ostream& out, const FunctionArrayConst& fc) +{ + return out << "__function_constant(" << fc.getType() << ", " + << fc.getArrayValue() << ')'; +} + +size_t FunctionArrayConstHashFunction::operator()( + const FunctionArrayConst& fc) const +{ + return std::hash()(fc.getType()) + * std::hash()(fc.getArrayValue()); +} + +} // namespace cvc5::internal diff --git a/src/expr/function_array_const.h b/src/expr/function_array_const.h new file mode 100644 index 000000000..f73345a79 --- /dev/null +++ b/src/expr/function_array_const.h @@ -0,0 +1,85 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Function array constant, which is an almost constant function + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__FUNCTION_ARRAY_CONST_H +#define CVC5__EXPR__FUNCTION_ARRAY_CONST_H + +#include +#include + +namespace cvc5::internal { + +template +class NodeTemplate; +typedef NodeTemplate Node; +class TypeNode; + +/** + * A function array constant is the canonical form of an almost constant + * function. It relies on the fact that array constants have a canonical + * form. + */ +class FunctionArrayConst +{ + public: + /** + * Constructor + * + * @param type The function type of this function array constant + * @param avalue The array value of this function array constant + * + * It should be the case that avalue is a constant array. It further + * more should be the case that if avalue has type + * (Array T1 (Array T2 .. (Array Tn T))) + * then type should be + * (-> T1 T2 ... Tn T) + * Note that T may itself be an array, e.g. for functions returning arrays. + */ + FunctionArrayConst(const TypeNode& type, const Node& avalue); + ~FunctionArrayConst(); + + FunctionArrayConst(const FunctionArrayConst& other); + FunctionArrayConst& operator=(const FunctionArrayConst& other); + + const TypeNode& getType() const; + const Node& getArrayValue() const; + + bool operator==(const FunctionArrayConst& fc) const; + bool operator!=(const FunctionArrayConst& fc) const; + bool operator<(const FunctionArrayConst& fc) const; + bool operator<=(const FunctionArrayConst& fc) const; + bool operator>(const FunctionArrayConst& fc) const; + bool operator>=(const FunctionArrayConst& fc) const; + + private: + /** The (function) type (-> T1 T2 ... Tn T) */ + std::unique_ptr d_type; + /** The value, which has type (Array T1 (Array T2 .. (Array Tn T))) */ + std::unique_ptr d_avalue; +}; + +std::ostream& operator<<(std::ostream& out, const FunctionArrayConst& fc); + +/** Hash function for the FunctionArrayConst constants. */ +struct FunctionArrayConstHashFunction +{ + size_t operator()(const FunctionArrayConst& fc) const; +}; + +} // namespace cvc5::internal + +#endif /* CVC5__EXPR__FUNCTION_ARRAY_CONST_H */ diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 30bccd34c..304679df2 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -44,7 +44,7 @@ constant CARDINALITY_CONSTRAINT_OP \ CardinalityConstraint \ ::cvc5::internal::CardinalityConstraintHashFunction \ "expr/cardinality_constraint.h" \ - "the empty set constant; payload is an instance of the cvc5::internal::CardinalityConstraint class" + "the cardinality constraint operator; payload is an instance of the cvc5::internal::CardinalityConstraint class" parameterized CARDINALITY_CONSTRAINT CARDINALITY_CONSTRAINT_OP 0 "a fixed upper bound on the cardinality of an uninterpreted sort" typerule CARDINALITY_CONSTRAINT_OP ::cvc5::internal::theory::uf::CardinalityConstraintOpTypeRule @@ -55,10 +55,19 @@ constant COMBINED_CARDINALITY_CONSTRAINT_OP \ CombinedCardinalityConstraint \ ::cvc5::internal::CombinedCardinalityConstraintHashFunction \ "expr/cardinality_constraint.h" \ - "the empty set constant; payload is an instance of the cvc5::internal::CombinedCardinalityConstraint class" + "the combined cardinality constraint operator; payload is an instance of the cvc5::internal::CombinedCardinalityConstraint class" parameterized COMBINED_CARDINALITY_CONSTRAINT COMBINED_CARDINALITY_CONSTRAINT_OP 0 "a fixed upper bound on the sum of cardinalities of uninterpreted sorts" typerule COMBINED_CARDINALITY_CONSTRAINT_OP ::cvc5::internal::theory::uf::CombinedCardinalityConstraintOpTypeRule typerule COMBINED_CARDINALITY_CONSTRAINT ::cvc5::internal::theory::uf::CombinedCardinalityConstraintTypeRule + +constant FUNCTION_ARRAY_CONST \ + class \ + FunctionArrayConst \ + ::cvc5::internal::FunctionArrayConstHashFunction \ + "expr/function_array_const.h" \ + "the function constant; payload is an instance of the cvc5::internal::FunctionArrayConst class" +typerule FUNCTION_ARRAY_CONST ::cvc5::internal::theory::uf::FunctionArrayConstTypeRule + endtheory diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index f339a28d5..180504da2 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -19,6 +19,7 @@ #include #include "expr/cardinality_constraint.h" +#include "expr/function_array_const.h" #include "theory/uf/function_const.h" #include "util/cardinality.h" #include "util/rational.h" @@ -222,6 +223,15 @@ bool LambdaTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) return false; } +TypeNode FunctionArrayConstTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::FUNCTION_ARRAY_CONST); + const FunctionArrayConst& fc = n.getConst(); + return fc.getType(); +} + Cardinality FunctionProperties::computeCardinality(TypeNode type) { // Don't assert this; allow other theories to use this cardinality diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index c4a147157..12fc2d679 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -90,7 +90,7 @@ class HoApplyTypeRule }; /** - * Type rule for lambas. Ensures the first argument is a bound varible list + * Type rule for lambdas. Ensures the first argument is a bound varible list * (x1 ... xn). Returns the function type (-> T1 ... Tn T) where T1...Tn are * the types of x1..xn and T is the type of the second argument. */ @@ -103,6 +103,16 @@ class LambdaTypeRule static bool computeIsConst(NodeManager* nodeManager, TNode n); }; /* class LambdaTypeRule */ +/** + * Type rule for function array constants. Returns the function type stored + * in the FUNCTION_ARRAY_CONST payload of the node. + */ +class FunctionArrayConstTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; /* class LambdaTypeRule */ + class FunctionProperties { public: