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 |
