Home
last modified time | relevance | path

Searched refs:use_drat (Results 1 – 8 of 8) sorted by relevance

/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Deuf_proof.cpp72 if (!use_drat()) in drat_bool_def()
103 if (!use_drat()) in log_antecedents()
H A Deuf_solver.cpp128 if (use_drat()) in add_solver()
217 if (!probing && use_drat()) in get_antecedents()
H A Deuf_solver.h310 bool use_drat() { return s().get_config().m_drat && (init_drat(), true); } in use_drat() function
H A Dbv_solver.cpp337 if (!probing && ctx.use_drat()) in get_antecedents()
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Deuf_proof.cpp90 if (!use_drat()) in drat_bool_def()
121 if (!use_drat()) in log_antecedents()
H A Deuf_solver.cpp138 if (use_drat()) in add_solver()
228 if (!probing && use_drat()) in get_antecedents()
H A Deuf_solver.h334 bool use_drat() { return s().get_config().m_drat && (init_drat(), true); } in use_drat() function
H A Dbv_solver.cpp344 if (!probing && ctx.use_drat()) in get_antecedents()