Module SrkZ3.Solver

module Solver: sig .. end

type 'a t 

val add : 'a t -> 'a Syntax.formula list -> unit

val push : 'a t -> unit

val pop : 'a t -> int -> unit

val reset : 'a t -> unit

val check : 'a t -> 'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]

val to_string : 'a t -> string

val get_model : ?symbols:Syntax.symbol list ->
       'a t ->
       [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]

val get_concrete_model : 'a t ->
       Syntax.symbol list ->
       [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]

val get_unsat_core : 'a t ->
       'a Syntax.formula list ->
       [ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]