ModuloTheories not generating enough assumptions about equality

[leoqiao18]

An issue in a spec that came from @w14 :

#LIA
always guarantee {
    y = 0 -> X y = 0;
    true -> [y <- 0];
}

This should be realizable by always assigning 0 to y. But tsl synthesize fails at the ltlsynt step.

The problem comes from a lack of assumptions generated by the ModuloTheories step. Running tsl theorize gives the following theorized spec:

always assume {
G !((eq y int0()) && ((eq y int0()) && (!(eq y int0()) && !(eq y int0()))));
G !((eq y int0()) && ((eq y int0()) && !(eq y int0())));
G !((eq y int0()) && ((eq y int0()) && !(eq y int0())));
G !((eq y int0()) && (!(eq y int0()) && !(eq y int0())));
G !((eq y int0()) && !(eq y int0()));
G !((eq y int0()) && !(eq y int0()));
G !((eq y int0()) && (!(eq y int0()) && !(eq y int0())));
G !((eq y int0()) && !(eq y int0()));
G !((eq y int0()) && !(eq y int0()));
}
always guarantee {
((eq y int0()) -> (X (eq y int0())));
((true) -> [y <- int0()]);
}

Notice that the ModuloTheories step only adds a bunch of repeated points about how y cannot be equal to 0 and not be equal to 0 at the same time. It did not add anything about how assigning 0 to y causes y to be equal to 0 in the next time step.

This might be related to the issue that @santolucito talked about in #64

[santolucito]

Ya I think we'll need to look at the sygus logs to figure out what queries are being made, and why we aren't getting the right assumptions added

[santolucito]

Looks like we need to try to schedule a call with @wonhyukchoi to fix this issue

We need

tsltools/test/regression/ModuloTheories/lia_next.tslmt

Line 6 in 4cb59f9

/* G (((eq y int0()) && [y <- int0()]) -> X (eq y int0())); */

and it seems we don't have support for this in the new implementation of TSL-MT (I am pretty sure it was there in the old implementation that @wonhyukchoi made for the PLDI paper though)

tsltools/src/TSL/ModuloTheories/Sygus/Assumption.hs

Line 64 in 4cb59f9

"((p x) & [x <- x]) -> X (p x) type assumptions not yet supported."

[santolucito]

Also, I'm actually thinking, at least as a hack for now, just brute force generating all the assumptions of this particular form. Would be fairly easy and this is the most common equality+temporal form we need