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.
emptyset.h
emptybag.cpp
emptybag.h
+ function_array_const.cpp
+ function_array_const.h
kind_map.h
match_trie.cpp
match_trie.h
--- /dev/null
+/******************************************************************************
+ * 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 <iostream>
+
+#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<TypeNode> 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<TypeNode>()(fc.getType())
+ * std::hash<Node>()(fc.getArrayValue());
+}
+
+} // namespace cvc5::internal
--- /dev/null
+/******************************************************************************
+ * 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 <iosfwd>
+#include <memory>
+
+namespace cvc5::internal {
+
+template <bool ref_count>
+class NodeTemplate;
+typedef NodeTemplate<true> 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<TypeNode> d_type;
+ /** The value, which has type (Array T1 (Array T2 .. (Array Tn T))) */
+ std::unique_ptr<Node> 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 */
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
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
#include <sstream>
#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"
return false;
}
+TypeNode FunctionArrayConstTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::FUNCTION_ARRAY_CONST);
+ const FunctionArrayConst& fc = n.getConst<FunctionArrayConst>();
+ return fc.getType();
+}
+
Cardinality FunctionProperties::computeCardinality(TypeNode type)
{
// Don't assert this; allow other theories to use this cardinality
};
/**
- * 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.
*/
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:
projects / cvc5.git / commitdiff