1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     simplify_cmd.cpp
7 
8 Abstract:
9     SMT2 front-end 'simplify' command.
10 
11 Author:
12 
13     Leonardo (leonardo) 2011-04-20
14 
15 Notes:
16 
17 --*/
18 #include "cmd_context/cmd_context.h"
19 #include "ast/rewriter/th_rewriter.h"
20 #include "ast/shared_occs.h"
21 #include "ast/ast_smt_pp.h"
22 #include "ast/for_each_expr.h"
23 #include "cmd_context/parametric_cmd.h"
24 #include "util/scoped_timer.h"
25 #include "util/scoped_ctrl_c.h"
26 #include "util/cancel_eh.h"
27 #include<iomanip>
28 
29 class simplify_cmd : public parametric_cmd {
30 
31 
32     expr *                   m_target;
33 public:
simplify_cmd(char const * name="simplify")34     simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {}
35 
get_usage() const36     char const * get_usage() const override { return "<term> (<keyword> <value>)*"; }
37 
get_main_descr() const38     char const * get_main_descr() const override {
39         return "simplify the given term using builtin theory simplification rules.";
40     }
41 
init_pdescrs(cmd_context & ctx,param_descrs & p)42     void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
43         th_rewriter::get_param_descrs(p);
44         insert_timeout(p);
45         p.insert("print", CPK_BOOL, "(default: true)  print the simplified term.");
46         p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
47         p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
48     }
49 
~simplify_cmd()50     ~simplify_cmd() override {
51     }
52 
prepare(cmd_context & ctx)53     void prepare(cmd_context & ctx) override {
54         parametric_cmd::prepare(ctx);
55         m_target   = nullptr;
56     }
57 
next_arg_kind(cmd_context & ctx) const58     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
59         if (m_target == nullptr) return CPK_EXPR;
60         return parametric_cmd::next_arg_kind(ctx);
61     }
62 
set_next_arg(cmd_context & ctx,expr * arg)63     void set_next_arg(cmd_context & ctx, expr * arg) override {
64         m_target = arg;
65     }
66 
execute(cmd_context & ctx)67     void execute(cmd_context & ctx) override {
68         if (m_target == nullptr)
69             throw cmd_exception("invalid simplify command, argument expected");
70         expr_ref r(ctx.m());
71         proof_ref pr(ctx.m());
72         if (m_params.get_bool("som", false))
73             m_params.set_bool("flat", true);
74         th_rewriter s(ctx.m(), m_params);
75         th_solver solver(ctx);
76         s.set_solver(alloc(th_solver, ctx));
77         unsigned cache_sz;
78         unsigned num_steps = 0;
79         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);
80         unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);
81         bool failed = false;
82         cancel_eh<reslimit> eh(ctx.m().limit());
83         {
84             scoped_rlimit _rlimit(ctx.m().limit(), rlimit);
85             scoped_ctrl_c ctrlc(eh);
86             scoped_timer timer(timeout, &eh);
87             cmd_context::scoped_watch sw(ctx);
88             try {
89                 s(m_target, r, pr);
90             }
91             catch (z3_error & ex) {
92                 throw ex;
93             }
94             catch (z3_exception & ex) {
95                 ctx.regular_stream() << "(error \"simplifier failed: " << ex.msg() << "\")" << std::endl;
96                 failed = true;
97                 r = m_target;
98             }
99             cache_sz  = s.get_cache_size();
100             num_steps = s.get_num_steps();
101             s.cleanup();
102         }
103         if (m_params.get_bool("print", true)) {
104             ctx.display(ctx.regular_stream(), r);
105             ctx.regular_stream() << std::endl;
106         }
107         if (!failed && m_params.get_bool("print_proofs", false) && pr.get()) {
108             ast_smt_pp pp(ctx.m());
109             pp.set_logic(ctx.get_logic());
110             pp.display_expr_smt2(ctx.regular_stream(), pr.get());
111             ctx.regular_stream() << std::endl;
112         }
113         if (m_params.get_bool("print_statistics", false)) {
114             shared_occs s1(ctx.m());
115             if (!failed)
116                 s1(r);
117             unsigned long long max_mem = memory::get_max_used_memory();
118             unsigned long long mem = memory::get_allocation_size();
119             ctx.regular_stream() << "(:time " << std::fixed << std::setprecision(2) << ctx.get_seconds() << " :num-steps " << num_steps
120                                  << " :memory " << std::fixed << std::setprecision(2) << static_cast<double>(mem)/static_cast<double>(1024*1024)
121                                  << " :max-memory " << std::fixed << std::setprecision(2) << static_cast<double>(max_mem)/static_cast<double>(1024*1024)
122                                  << " :cache-size: " << cache_sz
123                                  << " :num-nodes-before " << get_num_exprs(m_target);
124             if (!failed)
125                 ctx.regular_stream() << " :num-shared " << s1.num_shared() << " :num-nodes " << get_num_exprs(r);
126             ctx.regular_stream() << ")" << std::endl;
127         }
128     }
129 };
130 
131 
install_simplify_cmd(cmd_context & ctx,char const * cmd_name)132 void install_simplify_cmd(cmd_context & ctx, char const * cmd_name) {
133     ctx.insert(alloc(simplify_cmd, cmd_name));
134 }
135