Lines Matching defs:Solver

270   Z3_solver Solver = [this] {
297     Z3_solver_dec_ref(Context.Context, Solver);
301     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
858     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
872     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
886     Z3_solver_set_params(Context.Context, Solver, Params);
887     Z3_lbool res = Z3_solver_check(Context.Context, Solver);
897   void push() override { return Z3_solver_push(Context.Context, Solver); }
900     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
901     return Z3_solver_pop(Context.Context, Solver, NumStates);
907   void reset() override { Z3_solver_reset(Context.Context, Solver); }
910     OS << Z3_solver_to_string(Context.Context, Solver);
957   Z3_stats S = Z3_solver_get_statistics(C, Solver);