Difference between revisions of "SMT-LIB Compliance"
From CVC4
(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…") |
(→SMT-LIBv2 compliance) |
||
Line 1: | Line 1: | ||
− | |||
− | |||
Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2) | Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2) | ||
Revision as of 09:41, 12 July 2012
Mostly compliant with --lang smtlib2 (but we get extra strict/conformance things with --smtlib2)
Commands:
- Bread and butter - supported fully
- ( set-logic ... )
- ( set-info ... )
- ( 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
- ( get-info ... ) - supported, but quotation marks are not compliant
- 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 ...)
- ( set-option ... ) - partial support in options branch
- Models
- ( get-value ... ) - working on it
- ( get-assignment ) - supported fully, assuming get-value is