否定和德摩根定律不属于约束C++20偏序



按约束进行偏序的规则指的是AND和OR,但不指not:

13.5.4 Partial ordering by constraints [temp.constr.order]
(1.2) ...
- The constraint A ∧ B subsumes A, but A does not subsume A ∧ B.
- The constraint A subsumes A ∨ B, but A ∨ B does not subsume A.

这些规则基于原子约束和约束规范化的定义:

13.5.3 Constraint normalization [temp.constr.normal]
1 The normal form of an expression E is a constraint that is defined
as follows:
(1.1) The normal form of an expression ( E ) is the normal form of E.
(1.2) The normal form of an expression E1 || E2 is the disjunction
of the normal forms of E1 and E2.
(1.3) The normal form of an expression E1 && E2 is the conjunction
of the normal forms of E1 and E2.

否定(即!E1(是专门不处理的。

因此,以下代码正确使用部分排序:

void foo(auto i) requires std::integral<decltype(i)> {
std::cout << "integral 1" << std::endl;
}
void foo(auto i) requires std::integral<decltype(i)> && true {
std::cout << "integral 2" << std::endl;
}
int main() {
foo(0); // integral 2
}

而这个代码由于模糊性而失败:

template<typename T>
concept not_integral = !std::integral<T>;
template<typename T>
concept not_not_integral = !not_integral<T>;
void foo(auto i) requires not_not_integral<decltype(i)> {
std::cout << "integral 1" << std::endl;
}
void foo(auto i) requires std::integral<decltype(i)> && true {
std::cout << "integral 2" << std::endl;
}
int main() {
foo(0);
}

代码:https://godbolt.org/z/RYjqr2


以上导致德摩根定律不适用于概念:

template<class P>
concept has_field_moo_but_not_foo
= has_field_moo<P> && !has_field_foo<P>;

不等同于:

template<class P>
concept has_field_moo_but_not_foo
= !(has_field_foo<P> || !has_field_moo<P>);

前者将参与部分排序,而后者则不参与。

代码:https://godbolt.org/z/aRhmyy


是否决定不将否定作为约束规范化的一部分来处理,以简化编译器供应商的实现?或者试图支持它是否存在逻辑缺陷?

是否决定不将否定作为约束规范化的一部分来处理,以简化编译器供应商的实现?

是。这概括为需要在编译器中使用SAT求解器。

在[temp.contr.op]/5中添加了一个例子来证明这一点,尽管它没有提供决策的基本原理:

template <class T> concept sad = false;
template <class T> int f1(T) requires (!sad<T>);
template <class T> int f1(T) requires (!sad<T>) && true;
int i1 = f1(42);        // ambiguous, !sad<T> atomic constraint expressions ([temp.constr.atomic])
// are not formed from the same expression
template <class T> concept not_sad = !sad<T>;
template <class T> int f2(T) requires not_sad<T>;
template <class T> int f2(T) requires not_sad<T> && true;
int i2 = f2(42);        // OK, !sad<T> atomic constraint expressions both come from not_­sad
template <class T> int f3(T) requires (!sad<typename T::type>);
int i3 = f3(42);        // error: associated constraints not satisfied due to substitution failure
template <class T> concept sad_nested_type = sad<typename T::type>;
template <class T> int f4(T) requires (!sad_nested_type<T>);
int i4 = f4(42);        // OK, substitution failure contained within sad_­nested_­type

特别注意f3f4之间的差异。requires !sad<typename T::type>是否意味着没有sad嵌套类型,或者存在不是sad的嵌套类型?它实际上意味着后者,而对f4的约束意味着前者。

最新更新