Module Smt_internal.MakeSource

Parameters

module F : Libsolver.F

Signature

Sourcetype t
Sourceval open_session : unit -> t

open_session () creates a new incremental solver instance.

  • returns

    A new stateful solver instance.

Sourceval put : t -> Binsec.Formula.entry -> unit

put solver entry sends the entry to the solver.

  • parameter solver

    The solver instance.

  • parameter entry

    The formula entry to send.

Sourceval check_sat : t -> Binsec.Formula.status

check_sat solver checks if the current formula is satisfiable.

  • parameter solver

    The solver instance.

  • returns

    SAT, UNSAT or UNKNOWN.

get_bv_value solver expr returns the assignment of the expression expr if check_sat returned SAT. Invalid uses may fail in an unpredictable fashion.

  • parameter solver

    The solver instance that returned SAT.

  • parameter expr

    The expression to get the assignment.

  • returns

    The bitvector assignment of expr.

get_ax_values solver expr returns the assignment of the array expr if check_sat returned SAT. Invalid uses may fail in an unpredictable fashion.

  • parameter solver

    The solver instance that returned SAT.

  • parameter expr

    The expression to get the assignment.

  • returns

    The pair address/value assignments of expr.

Sourceval close_session : t -> unit

close_session solver will destroy the solver instance and release its ressources. Calling any function on this instance afterward is invalid and may fail in an unpredictable fashion.

  • parameter solver

    The solver instance to destroy.

Sourceval check_sat_and_close : t -> Binsec.Formula.status

check_sat_and_close solver is the same as caching the result of check_sat before calling close_session.

  • parameter solver

    The solver instance.

Sourceval query_stat : unit -> int

query_stat () returns the cumulated number of check_sat issued.

  • returns

    The total number of satisfiability queries.

Sourceval time_stat : unit -> float

time_stat () return the cumulated elapsed time with an open solver session.

  • returns

    The total number of second passed with an open solver session.