Lines Matching refs:th_solver

104         th_solver*             m_qsolver = nullptr;
113         scoped_ptr_vector<th_solver>                    m_solvers;
114         ptr_vector<th_solver>                           m_id2solver;
142         th_solver* get_solver(family_id fid, func_decl* f);
143         th_solver* sort2solver(sort* s) { return get_solver(s->get_family_id(), nullptr); }  in sort2solver()
144         th_solver* func_decl2solver(func_decl* f) { return get_solver(f->get_family_id(), f); }  in func_decl2solver()
145         th_solver* quantifier2solver();
146         th_solver* expr2solver(expr* e);
147         th_solver* bool_var2solver(sat::bool_var v);
148         void add_solver(th_solver* th);
258         th_solver* fid2solver(family_id fid) const { return m_id2solver.get(fid, nullptr); }  in fid2solver()
349 …void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()…  in attach_th_var()