Module Smt2_solver.SolverSource

Parameters

Signature

Sourceval visit_formula : Sexpr.Expr.t list -> unit
Sourceval iter_free_variables : (string -> Sexpr.Expr.t -> unit) -> unit
Sourceval iter_free_arrays : (string -> Sexpr.Memory.t -> unit) -> unit
Sourceval assert_formula : Sexpr.Expr.t -> unit
Sourceval assert_distinct : Sexpr.Expr.t -> Sexpr.Expr.t -> unit
Sourceval check_sat : ?timeout:float -> unit -> Libsolver.status
Sourceval check_sat_assuming : ?timeout:float -> Sexpr.Expr.t -> Libsolver.status
Sourceval get_value : Sexpr.Expr.t -> Z.t
Sourceval fold_array_values : (Z.t -> Z.t -> 'a -> 'a) -> Sexpr.Memory.t -> 'a -> 'a
Sourceval push : unit -> unit
Sourceval pop : unit -> unit
Sourceval close : unit -> unit