SMT-LIB Compliance

SMT-LIBv2 compliance

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