sig
  val simsat :
    'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
  val simsat_forward :
    'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
  val maximize :
    'a Syntax.context ->
    'a Syntax.formula ->
    'a Syntax.term ->
    [ `Bounded of QQ.t | `Infinity | `MinusInfinity | `Unknown ]
  val qe_mbp : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val easy_sat :
    'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
  type 'a strategy
  type quantifier_prefix = ([ `Exists | `Forall ] * Syntax.symbol) list
  val pp_strategy :
    'a Syntax.context -> Format.formatter -> 'a Quantifier.strategy -> unit
  val show_strategy : 'a Syntax.context -> 'a Quantifier.strategy -> string
  val winning_strategy :
    'a Syntax.context ->
    Quantifier.quantifier_prefix ->
    'a Syntax.formula ->
    [ `Sat of 'a Quantifier.strategy
    | `Unknown
    | `Unsat of 'a Quantifier.strategy ]
  val check_strategy :
    'a Syntax.context ->
    Quantifier.quantifier_prefix ->
    'a Syntax.formula -> 'a Quantifier.strategy -> bool
  val normalize :
    'a Syntax.context ->
    'a Syntax.formula -> Quantifier.quantifier_prefix * 'a Syntax.formula
end