Module CLogic.CLCmd

type t =
  1. | If of CExpr.t * t list * t list
    (*

    Conditional execution of logic command

    *)
  2. | Unfold of {
    1. pred : string;
    2. params : CExpr.t list;
    3. bindings : (string * string) list option;
    4. recursive : bool;
    }
    (*

    Unfolding of a specific predicate

    *)
  3. | Unfold_all of string
    (*

    Recursively unfold all predicates with the given name (with a fuel).

    *)
  4. | Fold of string * CExpr.t list
    (*

    Fold a predicate

    *)
  5. | Apply of string * CExpr.t list
    (*

    Apply a lemma

    *)
  6. | Assert of CAssert.t * string list
    (*

    Assert for verification, takes an assertion and binders

    *)
  7. | Branch of CFormula.t
    (*

    The symbolic engine should branch on the given formula

    *)
  8. | Invariant of {
    1. assertion : CAssert.t;
    2. bindings : string list;
    }
    (*

    Loop invariant

    *)
  9. | SymbExec
    (*

    Ignore the next function specification and symbolically execute instead

    *)
val pp : t Fmt.t