Updates are posted every other month, sometimes more frequently.
by Yoni Zohar, 15 Feb 2024
Introduction The theory of sequences in cvc5 is relatively new. In essence, it is meant to model data structures such as List in Java, or std::vector in c++. Unlike the theory of arrays (which is actually a theory of maps), the theory of sequences is very rich, and allows, in addition to array-like read and write operations, to also use operators such as concatenation, sub-list, length, and more. Read More
by Alex Ozdemir, 26 Jan 2024
cvc5 is an SMT solver with support for many theories: integers, reals, bit-vectors, algebraic datatypes, separation logic, sets, bags, and more. This means that is can find satisfying solutions for formulas involving these kinds of objects. In this post, I explain the process of adding a new theory to cvc5: the theory of prime-order finite fields. Read More
by Amalee Wilson, 15 Dec 2023
Partitioning is a divide-and-conquer approach where a difficult problem is split into hopefully easier subproblems that can be solved in parallel. This strategy is notoriously difficult to get right with SMT problems. We found that while it’s no panacea, partitioning can be used to diversify solving and reliably improve performance in a portfolio. Read More