aboutsummaryrefslogtreecommitdiffstats
path: root/examples/constraints.sol
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]