Implement integer simplification rules #3

New Issue

patrick · 2018-04-13T00:14:00+02:00

patrick commented

2018-04-13 00:14:00 +02:00

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

patrick closed this issue

2018-04-22 13:17:48 +02:00

Sign in to join this conversation.