mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-21 10:29:42 -06:00
parent c816d45a7d
commit 4e81085292
2 changed files with 30 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/cmd_context/basic_cmds.cpp
View file

@ -31,8 +31,6 @@ Notes:
#include "cmd_context/cmd_util.h"
#include "cmd_context/simplify_cmd.h"
#include "cmd_context/eval_cmd.h"
#include "qe/qe_mbp.h"
#include "qe/qe_mbi.h"
class help_cmd : public cmd {
svector<symbol> m_cmds;
@ -851,33 +849,6 @@ public:
void finalize(cmd_context & ctx) override {}
};
class get_interpolant_cmd : public cmd {
expr* m_a;
expr* m_b;
public:
get_interpolant_cmd():cmd("get-interpolant") {}
char const * get_usage() const override { return "<expr> <expr>"; }
char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
return CPK_EXPR;
}
void set_next_arg(cmd_context& ctx, expr * arg) override {
if (m_a == nullptr)
m_a = arg;
else
m_b = arg;
}
void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr; }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
qe::interpolator mbi(m);
expr_ref itp(m);
lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
ctx.regular_stream() << itp << "\n";
}
};
// provides "help" for builtin cmds
class builtin_cmd : public cmd {
@ -928,7 +899,6 @@ void install_ext_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(echo_cmd));
ctx.insert(alloc(labels_cmd));
ctx.insert(alloc(declare_map_cmd));
ctx.insert(alloc(get_interpolant_cmd));
ctx.insert(alloc(builtin_cmd, "reset", nullptr, "reset the shell (all declarations and assertions will be erased)"));
install_simplify_cmd(ctx);
install_eval_cmd(ctx);

30
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -376,6 +376,35 @@ public:
}
};
class get_interpolant_cmd : public cmd {
expr* m_a;
expr* m_b;
public:
get_interpolant_cmd():cmd("get-interpolant") {}
char const * get_usage() const override { return "<expr> <expr>"; }
char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
return CPK_EXPR;
}
void set_next_arg(cmd_context& ctx, expr * arg) override {
if (m_a == nullptr)
m_a = arg;
else
m_b = arg;
}
void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr; }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
qe::interpolator mbi(m);
expr_ref itp(m);
lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
ctx.regular_stream() << itp << "\n";
}
};
class mbi_cmd : public cmd {
expr* m_a;
expr* m_b;
@ -550,6 +579,7 @@ void install_dbg_cmds(cmd_context & ctx) {
ctx.insert(alloc(instantiate_cmd));
ctx.insert(alloc(instantiate_nested_cmd));
ctx.insert(alloc(set_next_id));
ctx.insert(alloc(get_interpolant_cmd));
ctx.insert(alloc(mbp_cmd));
ctx.insert(alloc(mbi_cmd));
ctx.insert(alloc(euf_project_cmd));