Implement integer simplification rules #3

Closed
opened 2018-04-13 00:14:00 +02:00 by patrick · 0 comments
Owner

After detecting integer variables in #2, advanced rules specific to integers can be implemented.

These include the following rewrite rules:

  • (X in I) === (X = I)

Example 1

forall V1, V2 (p(V1, V2) <-> (V2 in (V1 * V1) and V1 in 1..n))

should become

int(p/2)
forall N1, N2 (p(N1, N2) <-> (N2 = (N1 * N1) and N1 in 1..n))

Example 2

forall V1 (prime(V1) <-> (V1 in 2..n and not exists U1, U2 (V1 in (U1 * U2) and U1 in 2..n and U2 in 2..n)))

should become

int(prime/1)
forall N (prime(N) <-> (I in 2..n and not exists J1, J2 (N = J1 * J2 and J1 in 2..n and J2 in 2..n)))
After detecting integer variables in #2, advanced rules specific to integers can be implemented. These include the following rewrite rules: - `(X in I) === (X = I)` #### Example 1 forall V1, V2 (p(V1, V2) <-> (V2 in (V1 * V1) and V1 in 1..n)) should become int(p/2) forall N1, N2 (p(N1, N2) <-> (N2 = (N1 * N1) and N1 in 1..n)) #### Example 2 forall V1 (prime(V1) <-> (V1 in 2..n and not exists U1, U2 (V1 in (U1 * U2) and U1 in 2..n and U2 in 2..n))) should become int(prime/1) forall N (prime(N) <-> (I in 2..n and not exists J1, J2 (N = J1 * J2 and J1 in 2..n and J2 in 2..n)))
patrick added this to the anthem 0.1.9 milestone 2018-04-13 00:14:00 +02:00
patrick added the
enhancement
label 2018-04-13 00:14:00 +02:00
patrick self-assigned this 2018-04-13 00:47:10 +02:00
Sign in to join this conversation.
No Milestone
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: patrick/anthem#3
No description provided.