mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix ubuntu's build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-14 18:26:49 -10:00
parent b46c67ce14
commit f17c3c3b12
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/nla_grobner.cpp
View file

@ -280,14 +280,12 @@ void grobner_core::del_equation(equation * eq) {
} }
void grobner_core::simplify_using_to_superpose(equation& eq) { void grobner_core::simplify_using_to_superpose(equation& eq) {
bool result = false;
bool simplified; bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
do { do {
simplified = false; simplified = false;
for (equation* p : m_to_superpose) { for (equation* p : m_to_superpose) {
if (simplify_source_target(p, &eq)) { if (simplify_source_target(p, &eq)) {
result = true;
simplified = true; simplified = true;
} }
if (canceled() || eq.expr()->is_scalar()) { if (canceled() || eq.expr()->is_scalar()) {
@ -297,8 +295,11 @@ void grobner_core::simplify_using_to_superpose(equation& eq) {
} }
while (simplified && !eq.expr()->is_scalar()); while (simplified && !eq.expr()->is_scalar());
TRACE("grobner", tout << "simplification result: "; display_equation(tout, eq);); TRACE("grobner",
if (simplified) { tout << "simplification result: "; display_equation(tout, eq);}
else {tout << "no simplification\n";});
} }
const nex* grobner_core::get_highest_monomial(const nex* e) const { const nex* grobner_core::get_highest_monomial(const nex* e) const {
switch (e->type()) { switch (e->type()) {

2
src/math/lp/nla_grobner.h
View file

@ -179,7 +179,7 @@ private:
void init(); void init();
void compute_basis(); void compute_basis();
void compute_basis_init(); void compute_basis_init();
std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex* e); std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix(std::ostream & out) const; void display_matrix(std::ostream & out) const;
std::ostream& display(std::ostream& out) const { return m_gc.display(out); } std::ostream& display(std::ostream& out) const { return m_gc.display(out); }
void add_row(unsigned); void add_row(unsigned);