Difference between revisions of "SMT-LIB Compliance"
From CVC4
| Line 5: | Line 5: | ||
* We do not yet support the ''to_real'' or ''to_int'' functions, nor the ''is_int'' predicate, from [http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2 the ''Reals_Ints'' theory]. | * We do not yet support the ''to_real'' or ''to_int'' functions, nor the ''is_int'' predicate, from [http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2 the ''Reals_Ints'' theory]. | ||
* 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) | ||
| + | * We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics) | ||
Also: | Also: | ||
Revision as of 12:12, 9 October 2012
Mostly compliant with --lang smt, but you get extra strict/conformance things with the --smtlib command line option.
There are areas where we don't support full functionality, or where we are not compliant:
- We do not yet support the to_real or to_int functions, nor the is_int predicate, from the Reals_Ints theory.
- We do not yet support unsat core extraction (the get-unsat-core command)
- We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
Also:
- We do not yet support Boolean terms, e.g., function symbols that take Boolean arguments or arrays of Boolean. This limitation should be fixed by the 1.0 release.
- We do not yet support abstract values. An array can itself be printed as a term, and even a function can be printed (as a lambda). We plan to support abstract values when running in --smtlib compliance mode, by the 1.0 release.
