Stream: Coq Workshop 2021

Topic: [S2T3] General automation in Coq ...


view this post on Zulip Christian Doczkal (Jul 02 2021 at 10:23):

Presentation by @Chantal Keller

view this post on Zulip Vadim Zaliva (Aug 30 2021 at 17:50):

I am little late watching the presentation, but I have a question. How essential is SMT solver to the Sniper? Could it reduce the goal and produce enough first-order facts to be solved some other builtin tactics, like firstorder?

view this post on Zulip Jean-Marie Madiot (Nov 19 2021 at 15:20):

Vadim Zaliva said:

I am little late watching the presentation, but I have a question. How essential is SMT solver to the Sniper? Could it reduce the goal and produce enough first-order facts to be solved some other builtin tactics, like firstorder?

pinging @Valentin Blot @LouiseDDP @Chantal Keller @Pierre Vial in case one of them can reply

view this post on Zulip Pierre Vial (Nov 19 2021 at 15:41):

Jean-Marie Madiot said:

Vadim Zaliva said:

I am little late watching the presentation, but I have a question. How essential is SMT solver to the Sniper? Could it reduce the goal and produce enough first-order facts to be solved some other builtin tactics, like firstorder?

pinging Valentin Blot LouiseDDP Chantal Keller Pierre Vial in case one of them can reply

Yes, I think so. The tactic snipe is split in two:

If you want, you may just use scope and use another tactic or external solver. If ever you try, we would certainly be interested to know about what it gave you!

view this post on Zulip Pierre Vial (Nov 19 2021 at 15:43):

@Vadim Zaliva You may find a slightly different presentation of Sniper here, which may help answer your question:
https://www.irif.fr/_media/gt-scalp/pierre-vial.pdf


Last updated: Aug 11 2022 at 01:03 UTC