Difference between revisions of "SMT-LIB Compliance"

From CVC4
Jump to: navigation, search
Line 1: Line 1:
−
Mostly compliant with --lang smt, but you get extra strict/conformance things with the --smtlib command line option.
+
CVC4 is mostly SMT-LIB-conforming with ''--lang smt''.  With the ''--smtlib'' 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:

Revision as of 13:14, 9 October 2012

CVC4 is mostly SMT-LIB-conforming with --lang smt. With the --smtlib 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 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.
Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=SMT-LIB_Compliance&oldid=3648"