mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-09 05:13:33 +00:00
Code Activity

remove unused *_signed_project() methods

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-02 18:46:16 -10:00
parent a5488cf6e7
commit 7de648ff81
3 changed files with 0 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_explain.cpp
View file

@ -49,7 +49,6 @@ namespace nlsat {
bool m_factor; bool m_factor;
bool m_add_all_coeffs; bool m_add_all_coeffs;
bool m_add_zero_disc; bool m_add_zero_disc;
bool m_signed_project;
bool m_cell_sample; bool m_cell_sample;
@ -161,7 +160,6 @@ namespace nlsat {
m_minimize_cores = false; m_minimize_cores = false;
m_add_all_coeffs = true; m_add_all_coeffs = true;
m_add_zero_disc = true; m_add_zero_disc = true;
m_signed_project = false;
} }
std::ostream& display(std::ostream & out, polynomial_ref const & p) const { std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
@ -1906,10 +1904,6 @@ namespace nlsat {
m_imp->m_add_zero_disc = f; m_imp->m_add_zero_disc = f;
} }
void explain::set_signed_project(bool f) {
m_imp->m_signed_project = f;
}
void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*m_imp)(n, ls, result); (*m_imp)(n, ls, result);
} }

1
src/nlsat/nlsat_explain.h
View file

@ -46,7 +46,6 @@ namespace nlsat {
void set_factor(bool f); void set_factor(bool f);
void set_add_all_coeffs(bool f); void set_add_all_coeffs(bool f);
void set_add_zero_disc(bool f); void set_add_zero_disc(bool f);
void set_signed_project(bool f);
/** /**
\brief Given a set of literals ls[0], ... ls[n-1] s.t. \brief Given a set of literals ls[0], ... ls[n-1] s.t.

1
src/qe/nlqsat.cpp
View file

@ -833,7 +833,6 @@ namespace qe {
m_answer_simplify(m), m_answer_simplify(m),
m_trail(m), m_trail(m),
m_div_mc(nullptr) { m_div_mc(nullptr) {
s.m_solver.get_explain().set_signed_project(true);
m_nftactic = mk_tseitin_cnf_tactic(m); m_nftactic = mk_tseitin_cnf_tactic(m);
} }