open_session () creates a new incremental solver instance.

• returns

  A new stateful solver instance.

put solver entry sends the entry to the solver.

• parameter solver

  The solver instance.

• parameter entry

  The formula entry to send.

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.

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.

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

• parameter solver

  The solver instance.

query_stat () returns the cumulated number of check_sat issued.

• returns

  The total number of satisfiability queries.

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

• returns

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