package smtml

  1. Overview
  2. Docs

Module Smtml.AstSource

SMT-LIB Commands Representation. This module defines types and utilities for representing SMT-LIB commands, which are used to interact with SMT solvers. It includes commands for assertions, declarations, solver control, and metadata management.

Command Types

Sourcetype t =
  1. | Assert of Expr.t
    (*

    Assert expr adds an assertion expr to the current set of constraints.

    *)
  2. | Check_sat of Expr.t list
    (*

    Check_sat assumptions checks the satisfiability of the current set of constraints, optionally using additional assumptions.

    *)
  3. | Declare_const of {
    1. id : Symbol.t;
      (*

      The identifier of the constant.

      *)
    2. sort : Symbol.t;
      (*

      The sort (type) of the declared constant.

      *)
    }
    (*

    Declare_const { id; sort } declares a new constant id of type sort.

    *)
  4. | Declare_fun of {
    1. id : Symbol.t;
      (*

      The identifier of the constant.

      *)
    2. args : Symbol.t list;
      (*

      The sorts (types) of the arguments.

      *)
    3. sort : Symbol.t;
      (*

      The sort (type) of the declared function.

      *)
    }
    (*

    Declare_fun { id; args; sort } declares a new constant id of type args -> sort.

    *)
  5. | Echo of string
    (*

    Echo msg prints the given message msg to the standard output.

    *)
  6. | Exit
    (*

    Exit terminates the SMT solver session.

    *)
  7. | Get_assertions
    (*

    Get_assertions retrieves the current set of asserted formulas.

    *)
  8. | Get_assignment
    (*

    Get_assignment retrieves the current truth assignments for Boolean variables.

    *)
  9. | Get_info of string
    (*

    Get_info key retrieves metadata or configuration information associated with key.

    *)
  10. | Get_option of string
    (*

    Get_option key retrieves the value of the solver option identified by key.

    *)
  11. | Get_model
    (*

    Get_model requests a model for the current set of constraints if the problem is satisfiable.

    *)
  12. | Get_value of Expr.t list
    (*

    Get_value exprs retrieves the values of the given expressions exprs in the current model.

    *)
  13. | Pop of int
    (*

    Pop n removes the top n levels from the assertion stack.

    *)
  14. | Push of int
    (*

    Push n creates n new levels on the assertion stack.

    *)
  15. | Reset
    (*

    Reset clears all assertions and resets the solver state.

    *)
  16. | Reset_assertions
    (*

    Reset_assertions clears all assertions without modifying solver settings.

    *)
  17. | Set_info of Expr.t
    (*

    Set_info expr attaches metadata to the solver using the given expr.

    *)
  18. | Set_logic of Logic.t
    (*

    Set_logic logic specifies the logic to be used by the solver.

    *)
  19. | Set_option of Expr.t
    (*

    Set_option expr sets a solver option with the given expression expr.

    *)

A type representing various SMT-LIB commands.

Script Type

Sourcetype script = t list

A type representing a sequence of SMT-LIB commands.

Pretty Printing

Sourceval pp : t Fmt.t

Pretty-printer for SMT-LIB commands. Formats a command for human-readable output.

Serialization

Sourceval to_string : t -> string

Converts an SMT-LIB command to its string representation.