Module Quantifier

module Quantifier: sig .. end

Satisfiability via strategy improvement

val simsat : 'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]

Satisfiability via strategy improvement

val simsat_forward : 'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]

Satisfiability via strategy improvement, forwards version

val maximize : 'a Syntax.context ->
       'a Syntax.formula ->
       'a Syntax.term ->
       [ `Bounded of QQ.t | `Infinity | `MinusInfinity | `Unknown ]

Alternating quantifier optimization

val qe_mbp : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula

Quantifier eliminiation via model-based projection

val easy_sat : 'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]

Alternating quantifier satisfiability

type 'a strategy

type quantifier_prefix = ([ `Exists | `Forall ] * Syntax.symbol) list

val pp_strategy : 'a Syntax.context -> Format.formatter -> 'a strategy -> unit

val show_strategy : 'a Syntax.context -> 'a strategy -> string

val winning_strategy : 'a Syntax.context ->
       quantifier_prefix ->
       'a Syntax.formula ->
       [ `Sat of 'a strategy
       | `Unknown
       | `Unsat of 'a strategy ]

Compute a winning SAT/UNSAT strategy for a formula. The formula is represented in prenex form (quantifier prefix + matrix).

val check_strategy : 'a Syntax.context ->
       quantifier_prefix ->
       'a Syntax.formula -> 'a strategy -> bool

Verify that a SAT strategy is in fact a winning strategy. (To verify an UNSAT strategy, just negate the formula & quantifier prefix)

val normalize : 'a Syntax.context ->
       'a Syntax.formula -> quantifier_prefix * 'a Syntax.formula