mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

isolate constraints in a constraint_set

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-07 09:16:14 -08:00
parent a59745c2f2
commit 024ca86386
2 changed files with 1 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/lar_solver.cpp
View file

@ -530,7 +530,7 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term,
impq &term_max) { impq &term_max) {
settings().backup_costs = false; settings().backup_costs = false;
bool ret = false; bool ret = false;
TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n"; print_constraints(tout); tout << ", strategy = " << (int)settings().simplex_strategy() << "\n";); TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n" << constraints() << ", strategy = " << (int)settings().simplex_strategy() << "\n";);
switch (settings().simplex_strategy()) { switch (settings().simplex_strategy()) {
case simplex_strategy_enum::tableau_rows: case simplex_strategy_enum::tableau_rows:
@ -1286,21 +1286,6 @@ std::string lar_solver::get_variable_name(var_index j) const {
} }
// ********** print region start // ********** print region start
std::ostream& lar_solver::print_constraint(constraint_index ci, std::ostream & out) const {
return m_constraints.display(out, ci);
}
std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std::ostream & out) const {
return m_constraints.display_indices_only(out, ci);
}
std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const {
return m_constraints.display(out, var_str, ci);
}
std::ostream& lar_solver::print_constraints(std::ostream& out) const {
return out << m_constraints;
}
std::ostream& lar_solver::print_terms(std::ostream& out) const { std::ostream& lar_solver::print_terms(std::ostream& out) const {
for (auto it : m_terms) { for (auto it : m_terms) {

11
src/math/lp/lar_solver.h
View file

@ -489,17 +489,6 @@ public:
void set_variable_name(var_index vi, std::string); void set_variable_name(var_index vi, std::string);
// ********** print region start // ********** print region start
private:
std::ostream& print_constraint(constraint_index ci, std::ostream & out) const;
std::ostream& print_constraints(std::ostream& out) const ;
std::ostream& print_constraint_indices_only(constraint_index ci, std::ostream & out) const;
std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
public:
std::ostream& print_terms(std::ostream& out) const; std::ostream& print_terms(std::ostream& out) const;