Difference between revisions of "SMT-LIB Compliance"
From CVC4
| Line 4: | Line 4: | ||
* We do not yet support unsat core extraction (the ''get-unsat-core'' command) | * We do not yet support unsat core extraction (the ''get-unsat-core'' command) | ||
| − | ** this support will be coming Summer/Fall 2013 | + | ** '''Update!''' this support will be coming Summer/Fall 2013 |
* 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) | ||
| − | ** work is ongoing (Summer/Fall 2013) | + | ** '''Update!''' work is ongoing (Summer/Fall 2013) |
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. | ||
Revision as of 08:58, 29 May 2013
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 support unsat core extraction (the get-unsat-core command)
- Update! this support will be coming Summer/Fall 2013
- We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
- Update! work is ongoing (Summer/Fall 2013)
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.
