Ppx_sat_runtime (gillian.Ppx_sat

val if_then_else : 
  Gillian.Gil_syntax.Formula.t ->
  then_branch:(unit -> 'a Gillian.Monadic.Delayed.t) ->
  else_branch:(unit -> 'a Gillian.Monadic.Delayed.t) ->
  'a Gillian.Monadic.Delayed.t

val if_sure_then_else : 
  Gillian.Gil_syntax.Formula.t ->
  then_branch:(unit -> 'a Gillian.Monadic.Delayed.t) ->
  else_branch:(unit -> 'a Gillian.Monadic.Delayed.t) ->
  'a Gillian.Monadic.Delayed.t

val branch_entailment : 
  (Gillian.Gil_syntax.Formula.t * (unit -> 'a Gillian.Monadic.Delayed.t)) list ->
  'a Gillian.Monadic.Delayed.t

val true_formula : Gillian.Gil_syntax.Formula.t