陈 一 镭 Yilei Chen
  • Main
  • Next
  • Outputs
  • Inputs
  • Life
  • Misc
    • Cryptographers seldom sleep well
    • My Favorite Open Problem
    • Random tapes
    • Superluminal fiction
    • Top 10 fake college ranking
    • Why study Chinese
  • Courses
    • Cryptography S2023
    • Lattices F2022
    • Cryptography S2022
    • Cryptography S2021

Comparison between CVC4 and Alt-Ergo

Input language

CVC4 and Alt-Ergo have their native input language: .cvc and .mlw respectively. They both support smt-lib, where CVC4 claims a partial compliance, and Alt-Ergo support even a more limited usage.

Compatibility of SMT-LIB through theories

Most of the basic theories are supported by both Alt-Ergo and CVC4, including Boolean Operations, Arithmetic over Integers, Rationals and Reals, Quantifiers, Arrays, and User-defined Types. However, in order to carry out a "fair" comparison, we have to looking at their common language, which is SMT2. 
Here is the summary of their compatibility of .smt2 language:
Theory CVC4 Alt-Ergo
Boolean Logics SMT-LIB convertible SMT-LIB convertible
Linear Arith SMT-LIB convertible Support, but error exists in real-int unification
Non-linear Arith Partially support Support, but error exists in real-int unification
Array SMT-LIB convertible SMT-LIB convertible
Bit-vector SMT-LIB convertible Not specially defined
User-defined Types Partially compatible Partially compatible


Comparison of performance through Logics

Here's the last step before integration - we want to evaluate whether CVC4 or Alt-Ergo works on a particular logic given the input in SMT2 format. In the table below, what we mean "Works" implies their parser successfully handle the input. Some conditions after "Works" implies a partial compatibility. In the last column, we describe the conclusion and the choice of our integrator.
Logics CVC4 Alt-Ergo Comparison (Choice)
AUFLIA  Works Works Close performance, CVC4 advance
AUFLIRA Works Works Close performance, CVC4 advance
AUFNIRA Works Works Close performance, CVC4 advance
LRA Unknown Unknown Unknown
QF_ABV Works BV not compatible CVC4
QF_AUFBV Works BV not compatible CVC4
QF_AUFLIA Works Works CVC4 outperforms
QF_AX Works Works Both work, CVC4 faster
QF_BV Works BV not compatible CVC4
QF_IDL Works Works CVC4 outperforms
QF_LIA Works Works CVC4 outperforms
QF_LRA Works Works, besides Real-Int unification CVC4 outperforms
QF_NIA Limit support on Non-linear Arith Works, besides Real-Int unification Alt-Ergo
QF_NRA Limit support on Non-linear Arith Works, besides Real-Int unification Alt-Ergo
QF_RDL Works Works, besides Real-Int unification CVC4
QF_UF Works Works CVC4 outperforms
QF_UFBV Works BV not compatible CVC4
QF_UFIDL Works Works, besides Real-Int unification CVC4
QF_UFLIA Works Works CVC4 outperforms
QF_UFLRA Works Works, besides Real-Int unification CVC4
QF_UFNRA Limit support on Non-linear Arith Works, besides Real-Int unification Alt-Ergo
UFLRA Memory crash Memory crash Abort
UFNIA Memory crash Memory crash Abort

<<< Back to project page