Difference between revisions of "SMT-LIB Compliance"

From CVC4
Jump to: navigation, search
 
(6 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 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 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:
+
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.
−
 
+
−
* We do not yet support Boolean terms, e.g., function symbols that take Boolean arguments or arrays of Boolean.
+
−
<br/>'''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'').
+
−
<br/>'''We plan to support abstract values when running in --smtlib compliance mode, by the 1.0 release.'''
+

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.

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=SMT-LIB_Compliance&oldid=5300"