From f32eaee62ef61ae8fb6d09593bb71f551413c10f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Mar 2013 15:40:52 -0700 Subject: [PATCH] Replace std::sort with std::stable_sort when the given relation is just a partial order. This change avoids discrepancies when using different implmentations of std::sort. Signed-off-by: Leonardo de Moura --- src/ast/simplifier/poly_simplifier_plugin.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp index 13e5748dc..402b078a8 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ b/src/ast/simplifier/poly_simplifier_plugin.cpp @@ -18,6 +18,7 @@ Author: #include"ast_pp.h" #include"ast_util.h" #include"ast_smt2_pp.h" +#include"ast_ll_pp.h" poly_simplifier_plugin::poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, decl_kind num): @@ -173,7 +174,7 @@ void poly_simplifier_plugin::mk_monomial(unsigned num_args, expr * * args, expr_ result = args[0]; break; default: - std::sort(args, args + num_args, monomial_element_lt_proc(*this)); + std::stable_sort(args, args + num_args, monomial_element_lt_proc(*this)); result = mk_mul(num_args, args); SASSERT(wf_monomial(result)); break; @@ -465,7 +466,9 @@ void poly_simplifier_plugin::mk_sum_of_monomials(expr_ref_vector & monomials, ex result = monomials.get(0); break; default: { - std::sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this)); + TRACE("mk_sum_sort", tout << "before\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); + std::stable_sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this)); + TRACE("mk_sum_sort", tout << "after\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); if (is_simple_sum_of_monomials(monomials)) { mk_sum_of_monomials_core(monomials.size(), monomials.c_ptr(), result); return;