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:
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 |