Searched refs:xk_set (Results 1 – 2 of 2) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1266 interval_set * xk_set = m_infeasible[m_xk]; in updt_infeasible() local
1267 save_set_updt_trail(xk_set); in updt_infeasible()
1269 …TRACE("nlsat_inf_set", tout << "updating infeasible set\n"; m_ism.display(tout, xk_set) << "\n"; m… in updt_infeasible()
1270 new_set = m_ism.mk_union(s, xk_set); in updt_infeasible()
1326 …interval_set * xk_set = m_infeasible[m_xk]; // current set of infeasible interval for current vari… in process_arith_clause() local
1327 SASSERT(!m_ism.is_full(xk_set)); in process_arith_clause()
1358 if (m_ism.subset(curr_set, xk_set)) { in process_arith_clause()
1360 R_propagate(l, xk_set); in process_arith_clause()
1364 tmp = m_ism.mk_union(curr_set, xk_set); in process_arith_clause()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1266 interval_set * xk_set = m_infeasible[m_xk]; in updt_infeasible() local
1267 save_set_updt_trail(xk_set); in updt_infeasible()
1269 …TRACE("nlsat_inf_set", tout << "updating infeasible set\n"; m_ism.display(tout, xk_set) << "\n"; m… in updt_infeasible()
1270 new_set = m_ism.mk_union(s, xk_set); in updt_infeasible()
1326 …interval_set * xk_set = m_infeasible[m_xk]; // current set of infeasible interval for current vari… in process_arith_clause() local
1327 SASSERT(!m_ism.is_full(xk_set)); in process_arith_clause()
1358 if (m_ism.subset(curr_set, xk_set)) { in process_arith_clause()
1360 R_propagate(l, xk_set); in process_arith_clause()
1364 tmp = m_ism.mk_union(curr_set, xk_set); in process_arith_clause()
|