Lines Matching defs:Solver
263 Z3_solver Solver;
272 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
273 Z3_solver_inc_ref(Context.Context, Solver);
282 if (Solver)
283 Z3_solver_dec_ref(Context.Context, Solver);
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
844 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
872 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
882 void push() override { return Z3_solver_push(Context.Context, Solver); }
885 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
886 return Z3_solver_pop(Context.Context, Solver, NumStates);
892 void reset() override { Z3_solver_reset(Context.Context, Solver); }
895 OS << Z3_solver_to_string(Context.Context, Solver);