| /dports/math/z3/z3-z3-4.8.13/src/solver/ |
| H A D | check_sat_result.cpp | 21 void check_sat_result::set_reason_unknown(event_handler& eh) { in set_reason_unknown() function in check_sat_result
25 set_reason_unknown("interrupted from keyboard"); in set_reason_unknown()
28 set_reason_unknown("timeout"); in set_reason_unknown()
31 set_reason_unknown("max. resource limit exceeded"); in set_reason_unknown()
34 set_reason_unknown("interrupted"); in set_reason_unknown()
|
| H A D | check_sat_result.h | 64 virtual void set_reason_unknown(char const* msg) = 0;
65 void set_reason_unknown(event_handler& eh);
103 void set_reason_unknown(char const* msg) override { m_unknown = msg; } in set_reason_unknown() function
|
| H A D | combined_solver.cpp | 204 set_reason_unknown(ex.msg()); in get_consequences()
335 void set_reason_unknown(char const* msg) override { in set_reason_unknown() function in combined_solver
336 m_solver1->set_reason_unknown(msg); in set_reason_unknown()
337 m_solver2->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | tactic2solver.cpp | 75 void set_reason_unknown(char const* msg) override;
89 set_reason_unknown("cubing is not supported on tactics"); in cube()
286 void tactic2solver::set_reason_unknown(char const* msg) { in set_reason_unknown() function in __anonbe2803850111::tactic2solver
288 m_result->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | solver.cpp | 94 set_reason_unknown(Z3_CANCELED_MSG); in get_consequences()
98 set_reason_unknown(ex.msg()); in get_consequences()
|
| H A D | solver_pool.cpp | 259 void set_reason_unknown(char const* msg) override { return m_base->set_reason_unknown(msg); } in set_reason_unknown() function in pool_solver
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/solver/ |
| H A D | check_sat_result.cpp | 21 void check_sat_result::set_reason_unknown(event_handler& eh) { in set_reason_unknown() function in check_sat_result
25 set_reason_unknown("interrupted from keyboard"); in set_reason_unknown()
28 set_reason_unknown("timeout"); in set_reason_unknown()
31 set_reason_unknown("max. resource limit exceeded"); in set_reason_unknown()
34 set_reason_unknown("interrupted"); in set_reason_unknown()
|
| H A D | check_sat_result.h | 64 virtual void set_reason_unknown(char const* msg) = 0;
65 void set_reason_unknown(event_handler& eh);
103 void set_reason_unknown(char const* msg) override { m_unknown = msg; } in set_reason_unknown() function
|
| H A D | combined_solver.cpp | 199 set_reason_unknown(ex.msg()); in get_consequences()
330 void set_reason_unknown(char const* msg) override { in set_reason_unknown() function in combined_solver
331 m_solver1->set_reason_unknown(msg); in set_reason_unknown()
332 m_solver2->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | tactic2solver.cpp | 75 void set_reason_unknown(char const* msg) override;
85 set_reason_unknown("cubing is not supported on tactics"); in cube()
282 void tactic2solver::set_reason_unknown(char const* msg) { in set_reason_unknown() function in __anonc3a40cc00111::tactic2solver
284 m_result->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | solver.cpp | 94 set_reason_unknown(Z3_CANCELED_MSG); in get_consequences()
98 set_reason_unknown(ex.msg()); in get_consequences()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_kernel.cpp | 167 void set_reason_unknown(char const* msg) { in set_reason_unknown() function
168 m_kernel.set_reason_unknown(msg); in set_reason_unknown()
375 void kernel::set_reason_unknown(char const* msg) { in set_reason_unknown() function in smt::kernel
376 m_imp->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | smt_kernel.h | 199 void set_reason_unknown(char const* msg);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_kernel.cpp | 167 void set_reason_unknown(char const* msg) { in set_reason_unknown() function
168 m_kernel.set_reason_unknown(msg); in set_reason_unknown()
375 void kernel::set_reason_unknown(char const* msg) { in set_reason_unknown() function in smt::kernel
376 m_imp->set_reason_unknown(msg); in set_reason_unknown()
|
| H A D | smt_kernel.h | 190 void set_reason_unknown(char const* msg);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/fd_solver/ |
| H A D | pb2bv_solver.cpp | 119 void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } in set_reason_unknown() function in pb2bv_solver
|
| H A D | enum2bv_solver.cpp | 123 void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } in set_reason_unknown() function in enum2bv_solver
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/fd_solver/ |
| H A D | pb2bv_solver.cpp | 123 void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } in set_reason_unknown() function in pb2bv_solver
|
| H A D | enum2bv_solver.cpp | 127 void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } in set_reason_unknown() function in enum2bv_solver
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/sat_solver/ |
| H A D | inc_sat_solver.cpp | 222 set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')'); in check_sat_core()
229 set_reason_unknown("(sat.giveup has-uninterpreted)"); in check_sat_core()
244 set_reason_unknown(m_solver.get_reason_unknown()); in check_sat_core()
461 set_reason_unknown(m_solver.get_reason_unknown()); in cube()
542 void set_reason_unknown(char const* msg) override { in set_reason_unknown() function in inc_sat_solver
546 void set_reason_unknown(std::string &&msg) { in set_reason_unknown() function in inc_sat_solver
716 set_reason_unknown(ex.msg()); in internalize_goal()
749 set_reason_unknown(strm.str()); in internalize_goal()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/sat_solver/ |
| H A D | inc_sat_solver.cpp | 220 set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')'); in check_sat_core()
226 set_reason_unknown("(sat.giveup has-uninterpreted)"); in check_sat_core()
241 set_reason_unknown(m_solver.get_reason_unknown()); in check_sat_core()
431 set_reason_unknown(m_solver.get_reason_unknown()); in cube()
512 void set_reason_unknown(char const* msg) override { in set_reason_unknown() function in inc_sat_solver
516 void set_reason_unknown(std::string &&msg) { in set_reason_unknown() function in inc_sat_solver
686 set_reason_unknown(ex.msg()); in internalize_goal()
719 set_reason_unknown(strm.str()); in internalize_goal()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_iuc_solver.h | 153 void set_reason_unknown(char const* msg) override { m_solver.set_reason_unknown(msg); } in set_reason_unknown() function
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_iuc_solver.h | 157 void set_reason_unknown(char const* msg) override { m_solver.set_reason_unknown(msg); } in set_reason_unknown() function
|
| /dports/math/z3/z3-z3-4.8.13/src/api/ |
| H A D | api_solver.cpp | 592 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
600 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
607 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
792 to_solver_ref(s)->set_reason_unknown(eh); in Z3_solver_get_consequences()
802 to_solver_ref(s)->set_reason_unknown(eh); in Z3_solver_get_consequences()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
| H A D | api_solver.cpp | 590 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
598 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
605 to_solver_ref(s)->set_reason_unknown(eh); in _solver_check()
792 to_solver_ref(s)->set_reason_unknown(eh); in Z3_solver_get_consequences()
802 to_solver_ref(s)->set_reason_unknown(eh); in Z3_solver_get_consequences()
|