From 9abcde9a358f883befbcad910e880263182e5577 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2013 14:42:18 -0700
Subject: [PATCH 1/3] Fix typos
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/smt/asserted_formulas.cpp | 2 +-
src/tactic/bv/max_bv_sharing_tactic.cpp | 2 +-
src/tactic/core/propagate_values_tactic.cpp | 6 +++---
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 3155d9c58..c5d3c08cf 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -653,7 +653,7 @@ void asserted_formulas::propagate_values() {
// will be (silently) eliminated, and models produced by Z3 will not contain them.
flush_cache();
}
- TRACE("propagate_values", tout << "afer:\n"; display(tout););
+ TRACE("propagate_values", tout << "after:\n"; display(tout););
}
void asserted_formulas::propagate_booleans() {
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index 251e2b754..f60487d60 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -269,7 +269,7 @@ class max_bv_sharing_tactic : public tactic {
m_rw.cfg().cleanup();
g->inc_depth();
result.push_back(g.get());
- TRACE("qe", g->display(tout););
+ TRACE("max_bv_sharing", g->display(tout););
SASSERT(g->is_well_sorted());
}
};
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 6d9e6ccbd..1e358177f 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -165,7 +165,7 @@ class propagate_values_tactic : public tactic {
m_occs(*m_goal);
while (true) {
- TRACE("propagate_values", m_goal->display(tout););
+ TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display(tout););
if (forward) {
for (; m_idx < size; m_idx++) {
process_current();
@@ -201,14 +201,14 @@ class propagate_values_tactic : public tactic {
if (round >= m_max_rounds)
break;
IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
- TRACE("propgate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
+ TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
}
end:
m_goal->elim_redundancies();
m_goal->inc_depth();
result.push_back(m_goal);
SASSERT(m_goal->is_well_sorted());
- TRACE("propagate_values", m_goal->display(tout););
+ TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
m_goal = 0;
}
From f32eaee62ef61ae8fb6d09593bb71f551413c10f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2013 15:40:52 -0700
Subject: [PATCH 2/3] 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 <leonardo@microsoft.com>
---
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;
From b417ca657d388a3f635b19f371b5d3975835f412 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2013 16:52:08 -0700
Subject: [PATCH 3/3] Fix set_interruptable usage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/api/api_algebraic.cpp | 4 ++--
src/api/api_ast.cpp | 2 +-
src/api/api_datalog.cpp | 4 ++--
src/api/api_polynomial.cpp | 2 +-
src/api/api_solver.cpp | 2 +-
src/api/api_solver_old.cpp | 4 ++--
src/api/api_tactic.cpp | 2 +-
7 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 7716cbb59..d03a6aff4 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -373,7 +373,7 @@ extern "C" {
scoped_anum_vector roots(_am);
{
cancel_eh<algebraic_numbers::manager> eh(_am);
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as);
_am.isolate_roots(_p, v2a, roots);
@@ -408,7 +408,7 @@ extern "C" {
}
{
cancel_eh<algebraic_numbers::manager> eh(_am);
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as);
int r = _am.eval_sign_at(_p, v2a);
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index e93e1a178..680b59c68 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -681,7 +681,7 @@ extern "C" {
th_rewriter m_rw(m, p);
expr_ref result(m);
cancel_eh<th_rewriter> eh(m_rw);
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 28fe3ed33..0f100e747 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -266,7 +266,7 @@ extern "C" {
lbool r = l_undef;
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);
try {
@@ -291,7 +291,7 @@ extern "C" {
lbool r = l_undef;
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);
try {
diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp
index 3148f972b..25d4ca292 100644
--- a/src/api/api_polynomial.cpp
+++ b/src/api/api_polynomial.cpp
@@ -67,7 +67,7 @@ extern "C" {
expr_ref _r(mk_c(c)->m());
{
cancel_eh<polynomial::manager> eh(pm);
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
pm.psc_chain(_p, _q, v_x, rs);
}
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 9ace149af..ac30a0c21 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -243,7 +243,7 @@ extern "C" {
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*to_solver_ref(s));
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result;
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp
index c89f89873..e0533fbd9 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -73,7 +73,7 @@ extern "C" {
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
flet<bool> _model(mk_c(c)->fparams().m_model, true);
lbool result;
try {
@@ -123,7 +123,7 @@ extern "C" {
expr * const* _assumptions = to_exprs(assumptions);
flet<bool> _model(mk_c(c)->fparams().m_model, true);
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result;
result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
if (result != l_false && m) {
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 5bce218e6..911360047 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -410,7 +410,7 @@ extern "C" {
to_tactic_ref(t)->updt_params(p);
- api::context::set_interruptable(*(mk_c(c)), eh);
+ api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);