Difference between revisions of "SMT-LIB Compliance"
From CVC4
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | CVC4 is mostly SMT-LIB-conforming with ''--lang smt''. With the ''--smtlib'' command line option, though, you get additional strictness and standards conformance. | + | CVC4 is mostly SMT-LIB-conforming with ''--lang smt''. With the ''--smtlib-strict'' command line option, though, you get additional strictness and standards conformance. |
There are areas where we don't support full functionality, or where we are not compliant: | There are areas where we don't support full functionality, or where we are not compliant: | ||
| − | |||
| − | |||
* We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics) | * We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics) | ||
| + | * We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5 | ||
Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input. | Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input. | ||
Latest revision as of 09:47, 27 September 2014
CVC4 is mostly SMT-LIB-conforming with --lang smt. With the --smtlib-strict command line option, though, you get additional strictness and standards conformance.
There are areas where we don't support full functionality, or where we are not compliant:
- We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
- We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5
Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input.
