How can I avoid long solver times? #4267
-
I'd like to use dafny to write programs that generate circuits and be able to prove properties about the circuits that are generated. At the moment I'm just starting out and am learning my way around dafny. I worked through the "Program Proofs" book, which I really enjoyed, and have received helpful feedback on stack exchange for specific questions. I'm having the problem though, that as soon as I move from simple examples to a real problem that I'd like to solve, that I'm constantly hitting prohibitively long solver times. Presumably either:
Below I'm attaching a link to a github commit where I'm creating a structure to represent a circuit, and then adding a function that will combine two of the circuits into a single circuit. As soon as I try to write a lemma to prove properties about this function, I quickly hit long solve times. The lemma is at the bottom of the file, and the final expression in a 'calc' statement is just the unrolling of a function, yet this unrolling causes the solver to timeout. What am I missing? benreynwar/dafny_experiments@2ab30fd Also, any additional suggestions on how whether this problem is appropriate for dafny or whether I'm going about it in the wrong manner would be very much appreciated! My normal languages are python and verilog, so this is quite a different approach from what I'm used to. |
Beta Was this translation helpful? Give feedback.
Replies: 3 comments 2 replies
-
I did manage to get the property I was stuck on solved in the end (benreynwar/dafny_experiments@73d66c4). |
Beta Was this translation helpful? Give feedback.
-
There are a few things I could suggest here. First (and perhaps this is what you're saying has already helped) it might be helpful to add the Doing this is probably especially important for predicates that use Once you've made more functions and predicates opaque, writing some additional lemmas about them that use opaque predicates in their Besides that, there are some changes upcoming in Dafny that I think may make this program verify at least a little more quickly. Stay tuned! |
Beta Was this translation helpful? Give feedback.
-
One other suggestion if you haven't already looked at it is that we have a guide on optimizing proofs that goes into a little more detail on some of the things I mentioned above: https://dafny.org/latest/VerificationOptimization/VerificationOptimization |
Beta Was this translation helpful? Give feedback.
One other suggestion if you haven't already looked at it is that we have a guide on optimizing proofs that goes into a little more detail on some of the things I mentioned above: https://dafny.org/latest/VerificationOptimization/VerificationOptimization