Post-Interview Updates
cvc solver
Most common insights/requests:
Communication: Many of you asked for better communication about releases, features, and improvements in order to stay well-informed. To address this issue, we started a blog late last year and began posting to social media (LinkedIn, Twitter/X, and Facebook). Since many of you are not on social media, we are also planning to send occasional emails via our newsletter Google Group (sign up here, note that only cvc5 can post to the group). The newsletter will include highlights about the latest release, pointers to new blog posts, and information about recently-published papers. We also actively respond to questions on the cvc5 GitHub discussions when questions are posted.
Debugging Assistance: The need for descriptive output on timed-out or user-interrupted runs was our most frequently mentioned point, highlighting a critical area for enhancing debugging capabilities. There is already some support for this functionality. Andy Reynolds is going to write a blog post about this feature on our website that will be published by March 15.
Performance Predictability/Stability: Many of you identified performance predictability and instability as a major concern, underscoring the importance of focusing on this area. We have initiated several projects addressing this issue.
Enhanced Documentation: The call for improved documentation was loud and clear, indicating the need to dedicate additional time to this area. The cvc5 user documentation on our website has improved dramatically over the past few years. We encourage you to look at it and provide additional feedback. We also plan to continue improving the documentation and to develop user-focused tutorials.
Encoding Best Practices: Insight into encoding best practices, particularly with quantifiers, was frequently mentioned, pointing to a gap in currently available guidance. We plan to include encoding best practices in an upcoming tutorial paper that will be made available within the next three months.
Model Improvement: The importance of models and their improvement was mentioned by many interviewees. We plan to work with the SMT-LIB Initiative to improve standardization of models and to explore improving the diversity and generality of models.
Proofs: Proof certificates are crucial for many users. The ongoing development of proof capabilities in cvc5 is one of our top priorities.
Guidance on Options: Providing clear guidance on which options to use for different problem types was identified as a key area for improvement. We plan to add additional documentation and tutorials for effectively using cvc5’s options.
Codebase Accessibility: Suggestions to make the codebase less intimidating to new contributors were common, highlighting the need for tutorials and diagrams. We plan to develop more documentation and tutorials for developers in addition to similar efforts for users. We also are engaging in an ongoing effort to refactor the codebase to improve modularity.
Scalability: The scalability of SMT solvers is a perennial problem that was noted as a crucial development area. Improving scalability is an ongoing priority.
Quantifier Pain Points: Despite their importance, quantifiers were mentioned as a major pain point, indicating a need for focused improvement in this area. Improving quantifier performance is also an ongoing priority, and we plan to provide additional encoding best practices for quantifier use.
Many other points were discussed during our interviews. We have cataloged all of this information and plan to carefully go through it to drive future research directions and improvements. We are committed to addressing these areas for improvement and will prioritize our efforts based on both the frequency and the potential impact of the feedback received. Our goal is to create a roadmap that reflects our community's needs and pushes our project to new heights. Updates on all of our work addressing these insights will be posted to our communication channels mentioned above.
We welcome continued discussion on these points and any additional feedback you might have. Your input is crucial as we strive to improve and evolve.
Thank you once again for your valuable contributions and for being an integral part of our journey.
Warm regards,
The cvc5 Team