Difference between revisions of "SMT-LIB Compliance"

From CVC4
Jump to: navigation, search
(Created page with "==SMT-LIBv2 compliance== Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2) Commands: * Bread and butter - supported fully ** ( se…")
 
 
(13 intermediate revisions by the same user not shown)
Line 1: Line 1:
−
==SMT-LIBv2 compliance==
+
CVC4 is mostly SMT-LIB-conforming with ''--lang smt''.  With the ''--smtlib-strict'' command line option, though, you get additional strictness and standards conformance.
  
−
Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2)
+
There are areas where we don't support full functionality, or where we are not compliant:
  
−
Commands:
+
* We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
−
* Bread and butter - supported fully
+
* We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5
−
** ( set-logic ... )
+
 
−
** ( set-info ... )
+
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.
−
** ( declare-sort ... )
+
−
** ( declare-fun ... )
+
−
** ( assert ... )
+
−
** ( check-sat )
+
−
** ( exit )
+
−
* Incrementality - supported fully (with bugs)
+
−
** ( push ... )
+
−
** ( pop ... )
+
−
* Definitions - supported fully
+
−
** ( define-sort ... )
+
−
** ( define-fun ... )
+
−
* Informational output - partial
+
−
** ( get-info ... ) - supported, but quotation marks are not compliant
+
−
*** :error-behavior ("immediate-exit" only)
+
−
*** :name
+
−
*** :authors
+
−
*** :version
+
−
*** :status
+
−
*** :reason-unknown
+
−
*** :all-statistics
+
−
*** ''keyword'' (for solver-specific things, we don't have any yet)
+
−
** ( get-assertions ) - supported
+
−
** ( get-unsat-core ) - nope
+
−
** ( get-proof ) - limited
+
−
* Options
+
−
** ( set-option ... ) - partial support in options branch
+
−
*** :print-success - supported
+
−
*** :expand-definitions - unsupported
+
−
*** :interactive-mode - supported, but doesn't do anything
+
−
*** :produce-proofs - supported
+
−
*** :produce-unsat-cores - unsupported
+
−
*** :produce-models - supported
+
−
*** :produce-assignments - supported
+
−
*** :regular-output-channel - ?
+
−
*** :diagnostic-output-channel - ?
+
−
*** :random-seed - supported
+
−
*** :verbosity - supported, leads to non-conforming output
+
−
*** ''attribute'' (solver-specific, we have several)
+
−
** ( get-option ... )
+
−
*** same support as (set-option ...)
+
−
* Models
+
−
** ( get-value ... ) - working on it
+
−
** ( get-assignment ) - supported fully, assuming get-value is
+

Latest revision as of 10: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"