diff options
Diffstat (limited to 'examples/constraints.sol')
| -rw-r--r-- | examples/constraints.sol | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/examples/constraints.sol b/examples/constraints.sol new file mode 100644 index 0000000..676f4c1 --- /dev/null +++ b/examples/constraints.sol @@ -0,0 +1,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] |