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…")
 
(SMT-LIBv2 compliance)
Line 1: Line 1:
==SMT-LIBv2 compliance==
 
 
 
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
  • 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