search

Barnard-PL-Labs / tsltools

Library and tools for the TSL specification format
Other
7 stars 4 forks source link

ModuloTheories not generating enough assumptions about equality #68

Open leoqiao18 opened 11 months ago

leoqiao18 commented 11 months ago

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 commented 11 months ago

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 commented 10 months ago

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

We need

https://github.com/Barnard-PL-Labs/tsltools/blob/4cb59f988c32a63f71424f1411c5092b6d9ab23d/test/regression/ModuloTheories/lia_next.tslmt#L6

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)

https://github.com/Barnard-PL-Labs/tsltools/blob/4cb59f988c32a63f71424f1411c5092b6d9ab23d/src/TSL/ModuloTheories/Sygus/Assumption.hs#L64

santolucito commented 10 months ago

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