1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "qe/qe_cmd.h"
8 #include "qe/qe.h"
9 #include "cmd_context/cmd_context.h"
10 #include "cmd_context/parametric_cmd.h"
11
12 class qe_cmd : public parametric_cmd {
13 expr * m_target;
14 public:
qe_cmd(char const * name="elim-quantifiers")15 qe_cmd(char const* name = "elim-quantifiers"):parametric_cmd(name) {}
16
get_usage() const17 char const * get_usage() const override { return "<term> (<keyword> <value>)*"; }
18
get_main_descr() const19 char const * get_main_descr() const override {
20 return "apply quantifier elimination to the supplied expression";
21 }
22
init_pdescrs(cmd_context & ctx,param_descrs & p)23 void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
24 insert_timeout(p);
25 p.insert("print", CPK_BOOL, "(default: true) print the simplified term.");
26 p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
27 }
28
~qe_cmd()29 ~qe_cmd() override {
30 }
31
prepare(cmd_context & ctx)32 void prepare(cmd_context & ctx) override {
33 parametric_cmd::prepare(ctx);
34 m_target = nullptr;
35 }
36
next_arg_kind(cmd_context & ctx) const37 cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
38 if (m_target == nullptr) return CPK_EXPR;
39 return parametric_cmd::next_arg_kind(ctx);
40 }
41
set_next_arg(cmd_context & ctx,expr * arg)42 void set_next_arg(cmd_context & ctx, expr * arg) override {
43 m_target = arg;
44 }
45
execute(cmd_context & ctx)46 void execute(cmd_context & ctx) override {
47 proof_ref pr(ctx.m());
48 qe::simplify_rewriter_star qe(ctx.m());
49 expr_ref result(ctx.m());
50
51 qe(m_target, result, pr);
52
53 if (m_params.get_bool("print", true)) {
54 ctx.display(ctx.regular_stream(), result);
55 ctx.regular_stream() << std::endl;
56 }
57 if (m_params.get_bool("print_statistics", false)) {
58 statistics st;
59 qe.collect_statistics(st);
60 st.display(ctx.regular_stream());
61 }
62 }
63
64 };
65
install_qe_cmd(cmd_context & ctx,char const * cmd_name)66 void install_qe_cmd(cmd_context & ctx, char const * cmd_name) {
67 ctx.insert(alloc(qe_cmd, cmd_name));
68 }
69
70