From 5177cc4a9a58df192c6a844ca13abf7e7cd3be15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jun 2019 09:08:20 +0200 Subject: [PATCH] change lt Signed-off-by: Nikolaj Bjorner --- src/ast/ast_lt.h | 4 ++++ src/ast/rewriter/bool_rewriter.cpp | 6 ++++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_lt.h b/src/ast/ast_lt.h index a5899ba9a..bea512ed4 100644 --- a/src/ast/ast_lt.h +++ b/src/ast/ast_lt.h @@ -28,6 +28,10 @@ struct ast_to_lt { bool operator()(ast * n1, ast * n2) const { return lt(n1, n2); } }; +struct ast_lt { + bool operator()(ast * n1, ast * n2) const { return n1->get_id() < n2->get_id(); } +}; + bool lex_lt(unsigned num, ast * const * n1, ast * const * n2); inline bool lex_lt(unsigned num, expr * const * n1, expr * const * n2) { return lex_lt(num, reinterpret_cast(n1), reinterpret_cast(n2)); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index a51e00886..a9861093a 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -234,7 +234,8 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args return BR_DONE; } if (s) { - std::sort(buffer.begin(), buffer.end(), ast_to_lt()); + ast_lt lt; + std::sort(buffer.begin(), buffer.end(), lt); result = m().mk_or(sz, buffer.c_ptr()); return BR_DONE; } @@ -272,7 +273,8 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args, } if (mk_nflat_or_core(flat_args.size(), flat_args.c_ptr(), result) == BR_FAILED) { if (!ordered) { - std::sort(flat_args.begin(), flat_args.end(), ast_to_lt()); + ast_lt lt; + std::sort(flat_args.begin(), flat_args.end(), lt); } result = m().mk_or(flat_args.size(), flat_args.c_ptr()); }