Difference between revisions of "SMT-LIB Compliance"

From CVC4
Jump to: navigation, search
Line 1: Line 1:
−
Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2)
+
Mostly compliant with --lang smt, but you get extra strict/conformance things with the --smtlib command line option.
  
−
Commands:
+
There are areas where we don't support full functionality, or where we are not compliant:
−
* Bread and butter - supported fully
+
 
−
** ( set-logic ... )
+
* 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].
−
** ( set-info ... )
+
* We do not yet support unsat core extraction (the ''get-unsat-core'' command)
−
** ( declare-sort ... )
+
 
−
** ( declare-fun ... )
+
Also:
−
** ( assert ... )
+
 
−
** ( check-sat )
+
* 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.'''
−
** ( exit )
+
* 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.'''
−
* 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
+

Revision as of 12:10, 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)

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=3643"