Simulating some notion of linearity

[fuzzypixelz]

I do realize Z3 is designed to work with FOL, but ..

Supoose I'm using a Fixedpoint context, with a set of rules and variables, how difficult would it be fo Z3 to report if a certain relation has been used in a query or not? Or perhaps a report on the proof it came up with, that I can then analyse myself?

I want to do this in order to enforce that a certain relation is used exactly once inside a Fixedpoint. Do you think this is feasible?

[agurfinkel]

Can you clarify what you mean by used. You can examine query to see what relations it depends on. You can build a dependence graph of the rules to to identify that something is used indirectly. In case the system is unsat, you can examine the proof object to see what relations are used, where, and how. You can also add extra logic to your relations to keep track how many times a relation has been used.

[fuzzypixelz]

By used I mean that a certain relation has been consumed in any resolution rule (I mean rules added through Fixedpoint API).
I think the last part of your answer "You can also add extra logic to your relations to keep track how many times a relation has been used." sounds like the way to go.

Could you please highlight the relevant parts of the Z3 API which allow this?

Thank you very much for the quick answer!

[agurfinkel]

This would be in encoding of the problem, rather than something that is specific to Z3 or its API.

You have to setup the rules in such a way that a derivation is only allowed if a rule is applied only once.
If I was modeling a program, I would add a global counter and increment it when a linear step happens, and assume that the counter is at most 1 before any asserts. Then encode this into CHCs.