Christian Doczkal (Jul 02 2021 at 10:23): Christian Doczkal (Jul 02 2021 at 10:23):Presentation by @Chantal Keller
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?
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
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:
scope, which produces a lot of first-order statementssmtcoq.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!
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: Sep 15 2024 at 12:01 UTC