-
Here what I was thinking, but I am not clear on the specifics. Is there a method to generate a btor file from pyvsc and pass directly to boolector? Are there better ways to debug constraint runtime performance or address failures? |
Beta Was this translation helpful? Give feedback.
Replies: 2 comments
-
That's an interesting thought. With a .btor or .smt2 file, the user could debug failures by selectively commenting out portions of the file. I'm thinking this would be a fairly advanced usecase, and the average user would need something simpler. Currently, pyvsc makes an attempt to narrow down a solve failure to just the constraint statements that provoke the contradiction. Currently, narrowing is done just by iteratively adding constraints and noting which fail. I could see enhancing this approach -- for example, trying each constraint on its own, pairs of constraints, etc. |
Beta Was this translation helpful? Give feedback.
-
Set This doesn't cover generating .btor .smt2 files, but I don't have an identified use case yet. |
Beta Was this translation helpful? Give feedback.
Set
EN_DEBUG = True
insrc/vsc/model/randomizer.py
in/around line 60.This doesn't cover generating .btor .smt2 files, but I don't have an identified use case yet.