Implement Geoff's idea to have an option stating the users "intent" for invoking Vampire (i.e., proving / disproving)

[quickbeam123]

1) An easy update to use intent for creating the effect of --mode casc_sat (we can now use --intent sat --mode casc instead). 2) Update the samplers and, in particular, merge samplerFOF and samplerFNT (and delete samplerFNT).

[quickbeam123]

In principle it sure does! Except that we are not very good with models for theories at the moment.

[easychair]

I would say that in this case I deeply disagree.

Mode and intent are so much inter-connected that I do not really like the introduction of a new option. It looks unnatural and not nice for running Vampires.

Why is (say) -- mode vampire --intent sat better --mode sat ?

Are there any other intents?

When we are looking for a model, is it still the Vampire mode? If yes, then why?

I propose to revert to previous options.

And yes, adding options and code "just in case they might be helpful in future" is the road to hell. Not only in theorem proving.

Best, Andrei

On Mon, 21 Oct 2024 at 17:46, Martin Suda @.***> wrote:

In principle it sure does! Except that we are not very good with models for theories at the moment.

— Reply to this email directly, view it on GitHub https://github.com/vprover/vampire/pull/616#issuecomment-2427192833, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BP556QXTPQ5XJGJQD3Z4UVU3AVCNFSM6AAAAABQKMLZYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMRXGE4TEOBTGM . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[quickbeam123]

Before we revert, let me just explain:

• as of now, the intent is only used in casc mode, to pick the right schedule. The fact that it could simplify the code (casc_sat was simply a copy-paste of casc with a different schedule choice) points in the direction that intent might be a useful concept (of course, the code could have been written differently, but still)
• in vampire mode (where it currently serves no role), we could make good use of intent to explicitly mark option-value combinations which lead to the loss of completeness: e.g. "You are trying to show SAT by finitely saturating the input, this might not be possible using sa=lrs, consider trying sa=otter instead."

Why is (say) -- mode vampire --intent sat better --mode sat ?

We don't have mode sat at the moment.

When we are looking for a model, is it still the Vampire mode? If yes, then why?

This depends on the definition of Vampire mode. To be honest, I never heard one. For me it's just the default (universal?) mode of operation which does not use strategy schedules.