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.
type t = | Assert of Expr.tAssert expr adds an assertion expr to the current set of constraints.
| Check_sat of Expr.t listCheck_sat assumptions checks the satisfiability of the current set of constraints, optionally using additional assumptions.
| Declare_const of {id : Symbol.t;The identifier of the constant.
*)sort : Symbol.t;The sort (type) of the declared constant.
*)}Declare_const { id; sort } declares a new constant id of type sort.
| Echo of stringEcho msg prints the given message msg to the standard output.
| ExitExit terminates the SMT solver session.
| Get_assertionsGet_assertions retrieves the current set of asserted formulas.
| Get_assignmentGet_assignment retrieves the current truth assignments for Boolean variables.
| Get_info of stringGet_info key retrieves metadata or configuration information associated with key.
| Get_option of stringGet_option key retrieves the value of the solver option identified by key.
| Get_modelGet_model requests a model for the current set of constraints if the problem is satisfiable.
| Get_value of Expr.t listGet_value exprs retrieves the values of the given expressions exprs in the current model.
| Pop of intPop n removes the top n levels from the assertion stack.
| Push of intPush n creates n new levels on the assertion stack.
| ResetReset clears all assertions and resets the solver state.
| Reset_assertionsReset_assertions clears all assertions without modifying solver settings.
| Set_info of Expr.tSet_info expr attaches metadata to the solver using the given expr.
| Set_logic of Logic.tSet_logic logic specifies the logic to be used by the solver.
| Set_option of Expr.tSet_option expr sets a solver option with the given expression expr.
A type representing various SMT-LIB commands.
type script = t listA type representing a sequence of SMT-LIB commands.
val to_string : t -> stringConverts an SMT-LIB command to its string representation.