mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

revert changes to tactic.cpp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-01 12:56:00 -07:00
parent cce287eed1
commit 0914748184
2 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -335,9 +335,6 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
SASSERT(num == 2);
if (butil().is_bv(args[0])) {
reduce_eq(args[0], args[1], result);
std::cout << "reduce eq: " << mk_pp(args[0], m()) << "\n" << mk_pp(args[1], m()) << "\n";
std::cout << mk_pp(result, m()) << "\n";
return BR_DONE;
}
return BR_FAILED;

6
src/tactic/tactic.cpp
View file

@ -41,13 +41,11 @@ struct tactic_report::imp {
goal const & m_goal;
stopwatch m_watch;
double m_start_memory;
unsigned m_start_exprs;
imp(char const * id, goal const & g):
m_id(id),
m_goal(g),
m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)),
m_start_exprs(g.num_exprs()){
m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
m_watch.start();
}
@ -55,7 +53,7 @@ struct tactic_report::imp {
m_watch.stop();
double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
verbose_stream() << "(" << m_id
<< " :num-exprs " << m_start_exprs << " -> " << m_goal.num_exprs()
<< " :num-exprs " << m_goal.num_exprs()
<< " :num-asts " << m_goal.m().get_num_asts()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory