Home

cvc5

cvc5 is an automatic theorem prover for Satisifiability Modulo Theories (SMT) (for a more formal introduction to SMT see the following book chapter Satisfiability Modulo Theories). Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories. It can be used to prove the validity (or, dually, the satisfiability) of a formula with respect to several built-in logical theories and their combination.

Web site

For more information and the latest news about cvc5, visit the cvc5 web site.

Architecture

See the cvc5 system description at TACAS 2022.

• Arithmetic
  • cvc5 solves linear real arithmetic using an implementation of Simplex for DPLL(T). For a more complete introduction see the tech report.
  • The linear arithmetic module includes heuristics from Section 2.5 of Alberto Griggio's thesis and a few currently unpublished ones.
  • Integers are currently handled by first solving the real relaxation of the constraints, and then using a combination of Cuts from Proofs and branching to ensure integer solutions. This approach and the equational solver used are described in A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic.
  • A technical report is planned to explain a number of small details and extensions including analysis to improve simplex's conflicts, handling disequalities, supporting model generation in cvc5's combination framework, heuristically propagating equalities over sharing terms, tableau row based propagation, and terminating simplex with unknown.
  • Non-linear arithmetic is solved by incremental linearization or cylindrical algebraic coverings. Additional subsolvers for transcendental functions and other extended operators (IAND and pow2) are integrated as well.
• Arrays
  • Arrays are implemented in a manner inspired by the Generalized, efficient array decision procedures paper with a few major modifications.
• Bitvectors
  • Bitvectors is implemented primarily via a lazy schema for bitblasting. See Anders Franzen's thesis chapter 3.
• Combination
  • Theory combination is based on the care graph framework described in both Being careful about theory combination and Sharing is Caring: Combination of Theories.
• Datatypes
  • cvc5 implements An Abstract Decision Procedure for a Theory of Inductive Data Types.
  • This procedure has been extended to incorporate coinductive datatypes.
  • The datatypes decision procedure is optimized via the use of shared selectors.
• Quantifiers
  • E-matching and conflict-based quantifier instantiation [http://homepage.cs.uiowa.edu/~ajreynol/fmcad14.pdf].
  • Finite model finding [http://homepage.cs.uiowa.edu/~ajreynol/thesis.pdf].
  • Techniques for finding counterexamples for conjectures in the presence of recursive functions [http://homepage.cs.uiowa.edu/~ajreynol/ijcar16a.pdf].
  • Automated induction for datatypes [http://homepage.cs.uiowa.edu/~ajreynol/vmcai15.pdf].
  • A decision procedure for quantified linear arithmetic with one alternation [http://homepage.cs.uiowa.edu/~ajreynol/report-inst-la15.pdf].
  • Support for syntax-guided synthesis, as described in [http://homepage.cs.uiowa.edu/~ajreynol/cav15a.pdf].
• SAT Solver
  • The main sat solver is based on minisat v2.2.0.
  • Additionally, we (optionally, and enabled by default for certain theories) use non-clausal analysis to cut down search space of minisat. For more details see the article A branching heuristic in CVC4.
• Separation Logic
  • A decision procedure for a fragment quantifier-free separation logic containing negation, separation star and magic wand is implemented and can be composed with other decision procedures supported by cvc5. For details see A Decision Procedure for Separation Logic in SMT.
• Sets
  • Adaptation of tableau-based decision procedure described here.
• Strings
  • Original approach described in our CAV 2014 paper: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.
  • Decision procedure for regular memberships with length [http://homepage.cs.uiowa.edu/~ajreynol/frocos15.pdf].
• Uninterpreted functions
  • UF (without cardinality) is handled in a manner inspired by Simplify's tech report.
  • UF + cardinality is described this presentation and is used for finite model finding.