mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

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.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-25 15:40:52 -07:00
parent 9abcde9a35
commit f32eaee62e
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/simplifier/poly_simplifier_plugin.cpp
View file

@ -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;