blob: 676f4c14b48d194c22bdc27447523c0110098322 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
% Membership is not generation. Open membership constrains; the
% engine residuates, propagates, and enumerates only finite ranges.
% An open constraint comes back as the answer's condition.
Query expression: [Integer value: X]
% A later equality grounds it and the residue discharges.
Query expression: [Natural value: X] :and [Equal left: X right: 5]
% Bounds that pin an integer into a finite range enumerate, the
% same admissible enumeration Between performs explicitly.
Query expression: [Natural value: X] :and [LessThan left: X right: 4]
% Strict rational bounds tighten to integers: 1/2 < X <= 5/2.
Query expression:
[Integer value: X] :and
[GreaterThan left: X right: 1/2] :and
[LessThanEqual left: X right: 5/2]
% An empty interval is no, not a conditioned maybe.
Query expression: [GreaterThan left: X right: 5] :and [LessThan left: X right: 3]
% Explicit bounded generation.
Query expression: [Between value: X lower: 1 upper: 4] :and [GreaterThan left: X right: 2]
% Disjunction branches finitely.
Query expression: [Equal left: X right: 1] :or [Equal left: X right: 2]
|