About order of arguments in Spacer query

[panda2134]

I found that when I use (query Relation) in CHC files, Spacer generates a new relation called query!0 in the proof certificates. What's the relation between query!0 and the relation I queried for? It seems like the order of arguments can differ, therefore it's hard to extract the real arguments applied to the relation I gave to Z3.

[panda2134]

An example: https://gist.github.com/panda2134/3f5a2f822bd81f4407407005d672ef5b

The query!0 generated on my machine seems to have a reversed order of arguments when compared with the original queried relation.

[agurfinkel]

query command expects a single nullary relation as an argument. Say the query is (query Foo), then it is preprocessed by adding an extra rule (rule (=> Foo query!0)). The new predicate query!0 is used to mark that specific query command. It should have no arguments and should never be examined by the user.

[panda2134]

Got this! But let's say I'd like to retrieve the variables used in the counterexample from the proof given by spacer, since I've encoded them as arguments of Counterex. However, there's no instance of Counterex in the proof tree at all, and some values are indeed applied to several query!0 instances there. Why does this happen?

[agurfinkel]

Usually this means that the model/proof is not properly reconstructed because of pre-processing steps. The most common is inlining.
If you disable all inlining (look for fp.xform.**inline** options) you should get proofs/cexs without missing predicates.

[panda2134]

Thanks!