Email Gateway (Aug 23 2022 at 08:12): Email Gateway (Aug 23 2022 at 08:12):From: "John F. Hughes" <jfh@cs.brown.edu>
Trying to do some high-school-algebra-level stuff, I used "try", which
invoked csc4, and eventually the Output panel showed this:
SMT: Invoking SMT solver "cvc4" ...
SMT: Solver:
SMT: Result:
unknown
(error "Cannot get an unsat core unless immediately preceded by
UNSAT/VALID response.")
SMT: Time (ms):
22036
Earlier, I have the following:
sledgehammer_params[minimize=true,preplay_timeout=10,timeout=60,verbose=true,
provers="
vampire cvc4 spass
e z3
"]
declare [[smt_timeout = 120]]
declare [[smt_trace = true]]
======
My question is whether the "unknown" response represents a bug, and if so,
how do I report it?
If not, can someone tell me what it might actually mean ?
--John
Email Gateway (Aug 23 2022 at 08:13):From: Tjark Weber <tjark.weber@it.uu.se>
John,
This is (generally speaking) not a bug. It means that CVC4 was unable
to find either a proof or a counterexample for your particular proof
goal, and gave up.
This can happen for different reasons. It is rarely worthwhile to
investigate further -- in practice it means that CVC4 didn't give a
helpful answer, and you'll have to try something else (e.g., other
solvers, or finding an interactive proof).
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 23 2022 at 08:13):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
Hi John,
No, "unknown" is not a bug. The SMT solver can return one of "sat", "unsat", or "unknown". The "unknown" response means the solver was not able to find a satisfying assignment for the problem it received, nor was it able to prove no such assignment exists. This can happen if some part of the problem was outside its supported feature set or if some resource (runtime, memory, ...) was exhausted.
The follow on error message is directly from CVC4. Without knowledge of the internals of "try", I'm guessing Isabelle constructs an SMT problem that does "(check-sat)" followed by an unconditional "(get-unsat-core)" so it doesn't have to call the solver multiple times or manage an interactive session. In the case of "unknown", there is no unsat core so this command fails. I would say the behavior you're seeing is to be expected.
Thanks,
Matt
Last updated: Nov 21 2024 at 12:39 UTC