Module Sidekick_base.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = Types_.statement =
  1. | Stmt_set_logic of string
  2. | Stmt_set_option of string list
  3. | Stmt_set_info of string * string
  4. | Stmt_data of Types_.data list
  5. | Stmt_ty_decl of {
    1. name : ID.t;
    2. arity : int;
    3. ty_const : Types_.ty;
    }
    (*

    new atomic cstor

    *)
  6. | Stmt_decl of {
    1. name : ID.t;
    2. ty_args : Types_.ty list;
    3. ty_ret : Types_.ty;
    4. const : Types_.term;
    }
  7. | Stmt_define of Types_.definition list
  8. | Stmt_assert of Types_.term
  9. | Stmt_assert_clause of Types_.term list
  10. | Stmt_check_sat of (bool * Types_.term) list
  11. | Stmt_get_model
  12. | Stmt_get_value of Types_.term list
  13. | Stmt_exit
include Sidekick_sigs.PRINT with type t := t