package yices2_bindings

  1. Overview
  2. Docs
val equal_scalar : scalar -> scalar -> Ppx_deriving_runtime.bool
type uninterpreted = Yices2_low.Types.type_t
val equal_uninterpreted : uninterpreted -> uninterpreted -> Ppx_deriving_runtime.bool
type ytype =
  1. | Bool
  2. | Int
  3. | Real
  4. | BV of int
  5. | Scalar of scalar
  6. | Uninterpreted of uninterpreted
  7. | Tuple of Yices2_low.Types.type_t list
  8. | Fun of {
    1. dom : Yices2_low.Types.type_t list;
    2. codom : Yices2_low.Types.type_t;
    }
val equal_ytype : ytype -> ytype -> Ppx_deriving_runtime.bool
type !'a composite = private
  1. | Composite
type rational = Q.t
type !'a termstruct =
  1. | A0 : [ `YICES_ARITH_CONSTANT | `YICES_ARITH_ROOT_ATOM | `YICES_BOOL_CONSTANT | `YICES_BV_CONSTANT | `YICES_SCALAR_CONSTANT | `YICES_UNINTERPRETED_TERM | `YICES_VARIABLE ] * Yices2_low.Types.term_t -> [ `a0 ] termstruct
  2. | A1 : [ `YICES_ABS | `YICES_CEIL | `YICES_FLOOR | `YICES_IS_INT_ATOM | `YICES_NOT_TERM ] * Yices2_low.Types.term_t -> [ `a1 ] composite termstruct
  3. | A2 : [ `YICES_ARITH_GE_ATOM | `YICES_BV_ASHR | `YICES_BV_DIV | `YICES_BV_GE_ATOM | `YICES_BV_LSHR | `YICES_BV_REM | `YICES_BV_SDIV | `YICES_BV_SGE_ATOM | `YICES_BV_SHL | `YICES_BV_SMOD | `YICES_BV_SREM | `YICES_DIVIDES_ATOM | `YICES_EQ_TERM | `YICES_IDIV | `YICES_IMOD | `YICES_RDIV ] * Yices2_low.Types.term_t * Yices2_low.Types.term_t -> [ `a2 ] composite termstruct
  4. | ITE : Yices2_low.Types.term_t * Yices2_low.Types.term_t * Yices2_low.Types.term_t -> [ `a3 ] composite termstruct
  5. | Astar : [ `YICES_BV_ARRAY | `YICES_DISTINCT_TERM | `YICES_OR_TERM | `YICES_TUPLE_TERM | `YICES_XOR_TERM ] * Yices2_low.Types.term_t list -> [ `astar ] composite termstruct
  6. | Bindings : {
    1. c : [ `YICES_FORALL_TERM | `YICES_LAMBDA_TERM ];
    2. vars : Yices2_low.Types.term_t list;
    3. body : Yices2_low.Types.term_t;
    } -> [ `bindings ] composite termstruct
  7. | App : Yices2_low.Types.term_t * Yices2_low.Types.term_t list -> [ `app ] composite termstruct
  8. | Update : {
    1. array : Yices2_low.Types.term_t;
    2. index : Yices2_low.Types.term_t list;
    3. value : Yices2_low.Types.term_t;
    } -> [ `update ] composite termstruct
  9. | Projection : [ `YICES_BIT_TERM | `YICES_SELECT_TERM ] * int * Yices2_low.Types.term_t -> [ `projection ] termstruct
  10. | BV_Sum : (bool list * Yices2_low.Types.term_t option) list -> [ `bvsum ] termstruct
  11. | Sum : (rational * Yices2_low.Types.term_t option) list -> [ `sum ] termstruct
  12. | Product : bool * (Yices2_low.Types.term_t * Unsigned.uint) list -> [ `prod ] termstruct
type yterm =
  1. | Term : 'a termstruct -> yterm
type display = {
  1. width : int;
  2. height : int;
  3. offset : int;
}
type error_report = {
  1. badval : int;
  2. code : Yices2_low.Types.error_code;
  3. column : int;
  4. line : int;
  5. term1 : Yices2_low.Types.term_t;
  6. term2 : Yices2_low.Types.term_t;
  7. type1 : Yices2_low.Types.type_t;
  8. type2 : Yices2_low.Types.type_t;
}