mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-07 15:55:46 +00:00
Code Activity
z3/src/cmd_context/extra_cmds/dbg_cmds.cpp
Arie Gurfinkel 51d3c279d0
QEL: Fast Approximated Quantifier Elimination (#6820) 
* qe_lite: cleanup and comment

no change to code

* mbp_arrays: refactor out partial equality (peq)

Partial array equality, PEQ, is used as an intermediate
expression during MBP for arrays. We need to factor it out
so that it can be shared between MBP-QEL and existing MBP.

Partial array equality (peq) is used in MBP for arrays.
Factoring this out to be used by multiple MBP implementations.

* rewriter: new rewrite rules

These rules are specializes for terms that are created in QEL.
QEL commit is comming later

* datatype_rw: new rewrite rule for ADTs

The rule handles this special case:

    (cons (head x) (tail x)) --> x

* array_rewriter rules for rewriting PEQs

Special rules to simplify PEQs

* th_rewriter: wire PEQ simplifications

* spacer_iuc: avoid terms with default in IUC

Spacer prfers to not have a term representing default value of an array.
This guides IUC from picking such terms in interpolation

* mbp_term_graph: replace root with repr

* mbp_term_graph: formatting

* mbp_term_graph: class_props, getters, setters

Class properties allow to keep information for an equivalence class.

Getters and setters for terms allow accessing information

* mbp_term_graph: auxiliary methods for qel

QEL commit is comming later in the history

* mbp_term_graph: bug fix

* mbp_term_graph: pick, refine repr, compute cgrnd

* mbp_term_graph: internalize deq

* mbp_term_graph: constructor

* mbp_term_graph: optionally internalize equalities

Reperesent equalities explicitly by nodes in the term_graph

* qel

* formatting

* comments on term_lt

* get terms and other api for mbp_qel

* plugins for mbp_qel

* mbp_qel_util: utilities for mbp_qel

* qe_mbp: QEL-based mbp

* qel: expose QEL API

* spacer: replace qe_lite in qe_project_spacer by qel

This changes the default projection engine that spacer uses.

* cmd_context: debug commands for qel and mbp_qel

New commands are

  mbp-qel -- MBP with term graphs
  qel     -- QEL with term graphs
  qe-lite -- older qelite

* qe_mbp: model-based rewriters for arrays

* qe_mbp: QEL-based projection functions

* qsat: wire in QEL-based mbp

* qsat: debug code

* qsat: maybe a bug fix

Changed the code to follow the paper by adding all predicates above a given
level, not just predicates of immediately preceding level.

* chore: use new api to create solver in qsat

* mbp_term_graph use all_of idiom

* feat: solver for integer multiplication

* array_peq: formatting, no change to code

* mbp_qel_util: block comment + format

* mbt_term_graph: clang-format

* bug fix. Move dt rewrite to qe_mbp

* array_peq: add header

* run clang format on mbp plugins

* clang format on mul solver

* format do-while

* format

* format do-while

* update release notes

---------

Co-authored-by: hgvk94 <hgvk94@gmail.com>
Co-authored-by: Isabel Garcia <igarciac@uwaterloo.ca>
2023-08-02 09:34:06 -07:00

794 lines
28 KiB
C++
Raw Blame History

/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
dbg_cmds.cpp
Abstract:
SMT2 front-end commands for debugging purposes.
Author:
Leonardo (leonardo) 2011-04-01
Notes:
--*/
#include<iomanip>
#include "ast/ast.h"
#include "cmd_context/cmd_context.h"
#include "cmd_context/cmd_util.h"
#include "ast/rewriter/rewriter.h"
#include "ast/shared_occs.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/ast_lt.h"
#include "cmd_context/simplify_cmd.h"
#include "ast/ast_smt2_pp.h"
#include "ast/simplifiers/bound_manager.h"
#include "ast/used_vars.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_util.h"
#include "util/gparams.h"
#include "qe/qe_mbp.h"
#include "qe/qe_mbi.h"
#include "qe/mbp/mbp_term_graph.h"
#include "qe/mbp/mbp_qel.h"
#include "qe/lite/qe_lite_tactic.h"
#include "qe/lite/qel.h"
BINARY_SYM_CMD(get_quantifier_body_cmd,
"dbg-get-qbody",
"<symbol> <quantifier>",
"store the body of the quantifier in the global variable <symbol>",
CPK_EXPR,
expr *, {
if (!is_quantifier(arg))
throw cmd_exception("invalid command, term must be a quantifier");
store_expr_ref(ctx, m_sym, to_quantifier(arg)->get_expr());
});
BINARY_SYM_CMD(set_cmd,
"dbg-set",
"<symbol> <term>",
"store <term> in the global variable <symbol>",
CPK_EXPR,
expr *, {
store_expr_ref(ctx, m_sym, arg);
});
UNARY_CMD(pp_var_cmd, "dbg-pp-var", "<symbol>", "pretty print a global variable that references an AST", CPK_SYMBOL, symbol const &, {
expr * t = get_expr_ref(ctx, arg);
SASSERT(t != 0);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
BINARY_SYM_CMD(shift_vars_cmd,
"dbg-shift-vars",
"<symbol> <uint>",
"shift the free variables by <uint> in the term referenced by the global variable <symbol>, the result is stored in <symbol>",
CPK_UINT,
unsigned, {
expr * t = get_expr_ref(ctx, m_sym);
expr_ref r(ctx.m());
var_shifter s(ctx.m());
s(t, arg, r);
store_expr_ref(ctx, m_sym, r.get());
});
UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "assert negation", CPK_EXPR, expr *, {
expr_ref ne(ctx.m().mk_not(arg), ctx.m());
ctx.assert_expr(ne);
});
UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
ctx.regular_stream() << get_num_exprs(arg) << std::endl;
});
class subst_cmd : public cmd {
unsigned m_idx;
expr * m_source;
symbol m_target;
ptr_vector<expr> m_subst;
public:
subst_cmd():cmd("dbg-subst") {}
char const * get_usage() const override { return "<symbol> (<symbol>*) <symbol>"; }
char const * get_descr(cmd_context & ctx) const override { return "substitute the free variables in the AST referenced by <symbol> using the ASTs referenced by <symbol>*"; }
unsigned get_arity() const override { return 3; }
void prepare(cmd_context & ctx) override { m_idx = 0; m_source = nullptr; }
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
if (m_idx == 1) return CPK_SYMBOL_LIST;
return CPK_SYMBOL;
}
void set_next_arg(cmd_context & ctx, symbol const & s) override {
if (m_idx == 0) {
m_source = get_expr_ref(ctx, s);
}
else {
m_target = s;
}
m_idx++;
}
void set_next_arg(cmd_context & ctx, unsigned num, symbol const * s) override {
m_subst.reset();
unsigned i = num;
while (i > 0) {
--i;
m_subst.push_back(get_expr_ref(ctx, s[i]));
}
m_idx++;
}
void execute(cmd_context & ctx) override {
beta_reducer p(ctx.m());
expr_ref r = p(m_source, m_subst.size(), m_subst.data());
store_expr_ref(ctx, m_target, r.get());
}
};
UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "<term>", "apply the Boolean rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
params_ref p;
p.set_bool("flat", false);
SASSERT(p.get_bool("flat", true) == false);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "<term>", "apply the Boolean (flattening) rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool("flat", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
UNARY_CMD(elim_and_cmd, "dbg-elim-and", "<term>", "apply the Boolean rewriter (eliminating AND operator and flattening) to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool("flat", true);
p.set_bool("elim_and", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
class lt_cmd : public cmd {
expr * m_t1;
expr * m_t2;
public:
lt_cmd():cmd("dbg-lt") {}
char const * get_usage() const override { return "<term> <term>"; }
char const * get_descr(cmd_context & ctx) const override { return "return true if the first term is smaller than the second one in the internal Z3 total order on terms."; }
unsigned get_arity() const override { return 2; }
void prepare(cmd_context & ctx) override { m_t1 = nullptr; }
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_t1 == nullptr)
m_t1 = arg;
else
m_t2 = arg;
}
void execute(cmd_context & ctx) override {
bool r = lt(m_t1, m_t2);
ctx.regular_stream() << (r ? "true" : "false") << std::endl;
}
};
UNARY_CMD(some_value_cmd, "dbg-some-value", "<sort>", "retrieve some value of the given sort", CPK_SORT, sort *, {
ast_manager & m = ctx.m();
expr_ref val(m);
val = m.get_some_value(arg);
ctx.display(ctx.regular_stream(), val);
ctx.regular_stream() << std::endl;
});
void tst_params(cmd_context & ctx) {
params_ref p1;
params_ref p2;
p1.set_uint("val", 100);
p2.append(p1);
SASSERT(p2.get_uint("val", 0) == 100);
p2.set_uint("val", 200);
SASSERT(p2.get_uint("val", 0) == 200);
SASSERT(p1.get_uint("val", 0) == 100);
p2.append(p1);
SASSERT(p2.get_uint("val", 0) == 100);
SASSERT(p1.get_uint("val", 0) == 100);
ctx.regular_stream() << "worked" << std::endl;
}
ATOMIC_CMD(params_cmd, "dbg-params", "test parameters", tst_params(ctx););
UNARY_CMD(translator_cmd, "dbg-translator", "<term>", "test AST translator", CPK_EXPR, expr *, {
ast_manager & m = ctx.m();
scoped_ptr<ast_manager> m2 = alloc(ast_manager, m.proof_mode());
ast_translation proc(m, *m2);
expr_ref s(m);
expr_ref t(*m2);
s = arg;
t = proc(s.get());
ctx.regular_stream() << mk_ismt2_pp(s, m) << "\n--->\n" << mk_ismt2_pp(t, *m2) << std::endl;
});
UNARY_CMD(sexpr_cmd, "dbg-sexpr", "<sexpr>", "display an s-expr", CPK_SEXPR, sexpr *, {
arg->display(ctx.regular_stream());
ctx.regular_stream() << std::endl;
});
#define GUARDED_CODE(CODE) try { CODE } catch (z3_error & ex) { throw ex; } catch (z3_exception & ex) { ctx.regular_stream() << "(error \"" << escaped(ex.msg()) << "\")" << std::endl; }
UNARY_CMD(set_next_id, "dbg-set-next-id", "<unsigned>", "set the next expression id to be at least the given value", CPK_UINT, unsigned, {
ctx.m().set_next_expr_id(arg);
});
UNARY_CMD(used_vars_cmd, "dbg-used-vars", "<expr>", "test used_vars functor", CPK_EXPR, expr *, {
used_vars proc;
if (is_quantifier(arg))
arg = to_quantifier(arg)->get_expr();
proc(arg);
ctx.regular_stream() << "(vars";
for (unsigned i = 0; i < proc.get_max_found_var_idx_plus_1(); i++) {
sort * s = proc.get(i);
ctx.regular_stream() << "\n (" << std::left << std::setw(6) << i << " ";
if (s != 0)
ctx.display(ctx.regular_stream(), s, 10);
else
ctx.regular_stream() << "<not-used>";
ctx.regular_stream() << ")";
}
ctx.regular_stream() << ")" << std::endl;
});
UNARY_CMD(elim_unused_vars_cmd, "dbg-elim-unused-vars", "<expr>", "eliminate unused vars from a quantifier", CPK_EXPR, expr *, {
if (!is_quantifier(arg)) {
ctx.display(ctx.regular_stream(), arg);
return;
}
expr_ref r = elim_unused_vars(ctx.m(), to_quantifier(arg), gparams::get_ref());
SASSERT(!is_quantifier(r) || !to_quantifier(r)->may_have_unused_vars());
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
});
class instantiate_cmd_core : public cmd {
protected:
quantifier * m_q;
ptr_vector<expr> m_args;
public:
instantiate_cmd_core(char const * name):cmd(name) {}
char const * get_usage() const override { return "<quantifier> (<symbol>*)"; }
char const * get_descr(cmd_context & ctx) const override { return "instantiate the quantifier using the given expressions."; }
unsigned get_arity() const override { return 2; }
void prepare(cmd_context & ctx) override { m_q = nullptr; m_args.reset(); }
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
if (m_q == nullptr) return CPK_EXPR;
else return CPK_EXPR_LIST;
}
void set_next_arg(cmd_context & ctx, expr * s) override {
if (!is_quantifier(s))
throw cmd_exception("invalid command, quantifier expected.");
m_q = to_quantifier(s);
}
void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) override {
if (num != m_q->get_num_decls())
throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments.");
unsigned i = num;
while (i-- > 0) {
sort * s = ts[i]->get_sort();
if (s != m_q->get_decl_sort(i)) {
std::ostringstream buffer;
buffer << "invalid command, sort mismatch at position " << i;
throw cmd_exception(buffer.str());
}
}
m_args.append(num, ts);
}
void execute(cmd_context & ctx) override {
expr_ref r = instantiate(ctx.m(), m_q, m_args.data());
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
}
};
class instantiate_cmd : public instantiate_cmd_core {
public:
instantiate_cmd():instantiate_cmd_core("dbg-instantiate") {}
};
class instantiate_nested_cmd : public instantiate_cmd_core {
public:
instantiate_nested_cmd():instantiate_cmd_core("dbg-instantiate-nested") {}
char const * get_descr(cmd_context & ctx) const override { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; }
void set_next_arg(cmd_context & ctx, expr * s) override {
instantiate_cmd_core::set_next_arg(ctx, s);
if (!is_quantifier(m_q->get_expr()))
throw cmd_exception("invalid command, nested quantifier expected");
m_q = to_quantifier(m_q->get_expr());
}
};
class print_dimacs_cmd : public cmd {
public:
print_dimacs_cmd():cmd("display-dimacs") {}
char const * get_usage() const override { return ""; }
char const * get_descr(cmd_context & ctx) const override { return "print benchmark in DIMACS format"; }
unsigned get_arity() const override { return 0; }
void prepare(cmd_context & ctx) override {}
void execute(cmd_context & ctx) override { ctx.display_dimacs(); }
};
class mbp_cmd : public cmd {
expr* m_fml;
ptr_vector<expr> m_vars;
public:
mbp_cmd():cmd("mbp") {}
char const * get_usage() const override { return "<expr> (<vars>)"; }
char const * get_descr(cmd_context & ctx) const override { return "perform model based projection"; }
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
if (m_fml == nullptr) return CPK_EXPR;
return CPK_EXPR_LIST;
}
void set_next_arg(cmd_context& ctx, expr * arg) override { m_fml = arg; }
void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context & ctx) override { m_fml = nullptr; m_vars.reset(); }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
app_ref_vector vars(m);
model_ref mdl;
if (!ctx.is_model_available(mdl) || !ctx.get_check_sat_result()) {
throw cmd_exception("model is not available");
}
for (expr* v : m_vars) {
if (!is_uninterp_const(v)) {
throw cmd_exception("invalid variable argument. Uninterpreted variable expected");
}
vars.push_back(to_app(v));
}
qe::mbproj mbp(m, gparams::get_module("smt"));
expr_ref fml(m_fml, m);
mbp.spacer(vars, *mdl.get(), fml);
ctx.regular_stream() << fml << "\n";
}
};
class get_interpolant_cmd : public cmd {
scoped_ptr<expr_ref> m_a;
scoped_ptr<expr_ref> 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 {
ast_manager& m = ctx.m();
if (!m.is_bool(arg))
throw default_exception("argument to interpolation is not Boolean");
if (!m_a)
m_a = alloc(expr_ref, arg, m);
else
m_b = alloc(expr_ref, arg, m);
}
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);
if (!m_a || !m_b)
throw default_exception("interpolation requires two arguments");
if (!m.is_bool(*m_a) || !m.is_bool(*m_b))
throw default_exception("interpolation requires two Boolean arguments");
expr_ref itp(m);
lbool r = mbi.pogo(ctx.get_solver_factory(), *m_a, *m_b, itp);
switch (r) {
case l_true:
ctx.regular_stream() << "sat\n";
break;
case l_undef:
ctx.regular_stream() << "unknown\n";
break;
case l_false:
ctx.regular_stream() << itp << "\n";
break;
}
}
};
class mbi_cmd : public cmd {
expr* m_a;
expr* m_b;
ptr_vector<func_decl> m_vars;
public:
mbi_cmd():cmd("mbi") {}
char const * get_usage() const override { return "<expr> <expr> (vars)"; }
char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
unsigned get_arity() const override { return 3; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
if (m_a == nullptr) return CPK_EXPR;
if (m_b == nullptr) return CPK_EXPR;
return CPK_FUNC_DECL_LIST;
}
void set_next_arg(cmd_context& ctx, expr * arg) override {
if (m_a == nullptr)
m_a = arg;
else
m_b = arg;
}
void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr; m_vars.reset(); }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
func_decl_ref_vector vars(m);
for (func_decl* v : m_vars) {
vars.push_back(v);
}
qe::interpolator mbi(m);
expr_ref a(m_a, m);
expr_ref b(m_b, m);
expr_ref itp(m);
solver_factory& sf = ctx.get_solver_factory();
params_ref p;
solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
sA->assert_expr(a);
sB->assert_expr(b);
qe::prop_mbi_plugin pA(sA.get());
qe::prop_mbi_plugin pB(sB.get());
pA.set_shared(vars);
pB.set_shared(vars);
lbool res = mbi.pingpong(pA, pB, itp);
ctx.regular_stream() << res << " " << itp << "\n";
}
};
class eufi_cmd : public cmd {
expr* m_a;
expr* m_b;
ptr_vector<func_decl> m_vars;
public:
eufi_cmd():cmd("eufi") {}
char const * get_usage() const override { return "<expr> <expr> (vars)"; }
char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
unsigned get_arity() const override { return 3; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
if (m_a == nullptr) return CPK_EXPR;
if (m_b == nullptr) return CPK_EXPR;
return CPK_FUNC_DECL_LIST;
}
void set_next_arg(cmd_context& ctx, expr * arg) override {
if (m_a == nullptr)
m_a = arg;
else
m_b = arg;
}
void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr; m_vars.reset(); }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
func_decl_ref_vector vars(m);
for (func_decl* v : m_vars) {
vars.push_back(v);
}
qe::interpolator mbi(m);
expr_ref a(m_a, m);
expr_ref b(m_b, m);
expr_ref itp(m);
solver_factory& sf = ctx.get_solver_factory();
params_ref p;
solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sNotB = sf(m, p, false /* no proofs */, true, true, symbol::null);
sA->assert_expr(a);
sB->assert_expr(b);
qe::uflia_mbi pA(sA.get(), sNotA.get());
qe::prop_mbi_plugin pB(sB.get());
pA.set_shared(vars);
pB.set_shared(vars);
lbool res = mbi.pogo(pA, pB, itp);
ctx.regular_stream() << res << " " << itp << "\n";
}
};
class euf_project_cmd : public cmd {
unsigned m_arg_index;
ptr_vector<expr> m_lits;
ptr_vector<func_decl> m_vars;
public:
euf_project_cmd():cmd("euf-project") {}
char const * get_usage() const override { return "(exprs) (vars)"; }
char const * get_descr(cmd_context & ctx) const override { return "perform congruence projection"; }
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
if (m_arg_index == 0) return CPK_EXPR_LIST;
return CPK_FUNC_DECL_LIST;
}
void set_next_arg(cmd_context& ctx, unsigned num, expr * const* args) override {
m_lits.append(num, args);
m_arg_index = 1;
}
void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context & ctx) override { m_arg_index = 0; m_lits.reset(); m_vars.reset(); }
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
func_decl_ref_vector vars(m);
expr_ref_vector lits(m);
for (func_decl* v : m_vars) vars.push_back(v);
for (expr* e : m_lits) lits.push_back(e);
flatten_and(lits);
solver_factory& sf = ctx.get_solver_factory();
params_ref pa;
solver_ref s = sf(m, pa, false, true, true, symbol::null);
solver_ref se = sf(m, pa, false, true, true, symbol::null);
s->assert_expr(lits);
lbool r = s->check_sat();
if (r != l_true) {
ctx.regular_stream() << "sat check " << r << "\n";
return;
}
model_ref mdl;
s->get_model(mdl);
qe::uflia_mbi plugin(s.get(), se.get());
plugin.set_shared(vars);
plugin.project(mdl, lits);
ctx.regular_stream() << lits << "\n";
}
};
class mbp_qel_cmd : public cmd {
unsigned m_arg_index;
ptr_vector<expr> m_lits;
ptr_vector<expr> m_vars;
public:
mbp_qel_cmd() : cmd("mbp-qel"){};
char const *get_usage() const override { return "(exprs) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "Model based projection using e-graphs";
}
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
return CPK_EXPR_LIST;
}
void set_next_arg(cmd_context &ctx, unsigned num,
expr *const *args) override {
if (m_arg_index == 0) {
m_lits.append(num, args);
m_arg_index = 1;
}
else { m_vars.append(num, args); }
}
void prepare(cmd_context &ctx) override {
m_arg_index = 0;
m_lits.reset();
m_vars.reset();
}
void execute(cmd_context &ctx) override {
ast_manager &m = ctx.m();
app_ref_vector vars(m);
expr_ref fml(m);
expr_ref_vector lits(m);
for (expr *v : m_vars) vars.push_back(to_app(v));
for (expr *e : m_lits) lits.push_back(e);
fml = mk_and(lits);
solver_factory &sf = ctx.get_solver_factory();
params_ref pa;
solver_ref s = sf(m, pa, false, true, true, symbol::null);
s->assert_expr(fml);
lbool r = s->check_sat();
if (r != l_true) return;
model_ref mdl;
s->get_model(mdl);
mbp::mbp_qel mbptg(m, pa);
mbptg(vars, fml, *mdl.get());
ctx.regular_stream() << "------------------------------ " << std::endl;
ctx.regular_stream() << "Orig tg: " << mk_and(lits) << std::endl;
ctx.regular_stream() << "To elim: ";
for (expr *v : m_vars) {
ctx.regular_stream() << to_app(v)->get_decl()->get_name() << " ";
}
ctx.regular_stream() << std::endl;
ctx.regular_stream() << "output " << fml << std::endl;
}
};
class qel_cmd : public cmd {
unsigned m_arg_index;
ptr_vector<expr> m_lits;
ptr_vector<func_decl> m_vars;
public:
qel_cmd() : cmd("qel"){};
char const *get_usage() const override { return "(lits) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "QE lite over e-graphs";
}
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
if (m_arg_index == 0) return CPK_EXPR_LIST;
return CPK_FUNC_DECL_LIST;
}
void set_next_arg(cmd_context &ctx, unsigned num,
expr *const *args) override {
m_lits.append(num, args);
m_arg_index = 1;
}
void set_next_arg(cmd_context &ctx, unsigned num,
func_decl *const *ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context &ctx) override {
m_arg_index = 0;
m_lits.reset();
m_vars.reset();
}
void execute(cmd_context &ctx) override {
ast_manager &m = ctx.m();
func_decl_ref_vector vars(m);
app_ref_vector vars_apps(m);
expr_ref_vector lits(m);
ctx.regular_stream() << "------------------------------ " << std::endl;
for (func_decl *v : m_vars) {
vars.push_back(v);
vars_apps.push_back(m.mk_const(v));
}
for (expr *e : m_lits) lits.push_back(e);
expr_ref fml(m.mk_and(lits), m);
ctx.regular_stream() << "[tg] Before: " << fml << std::endl
<< "[tg] Vars: ";
for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " ";
ctx.regular_stream() << std::endl;
params_ref pa;
// the following is the same code as in qe_mbp in spacer
qel qe(m, pa);
qe(vars_apps, fml);
ctx.regular_stream() << "[tg] After: " << fml << std::endl
<< "[tg] Vars: ";
for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " ";
ctx.regular_stream() << std::endl;
}
};
class qe_lite_cmd : public cmd {
unsigned m_arg_index;
ptr_vector<expr> m_lits;
ptr_vector<func_decl> m_vars;
public:
qe_lite_cmd() : cmd("qe-lite"){};
char const *get_usage() const override { return "(lits) (vars)"; }
char const *get_descr(cmd_context &ctx) const override {
return "QE lite over e-graphs";
}
unsigned get_arity() const override { return 2; }
cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
if (m_arg_index == 0) return CPK_EXPR_LIST;
return CPK_FUNC_DECL_LIST;
}
void set_next_arg(cmd_context &ctx, unsigned num,
expr *const *args) override {
m_lits.append(num, args);
m_arg_index = 1;
}
void set_next_arg(cmd_context &ctx, unsigned num,
func_decl *const *ts) override {
m_vars.append(num, ts);
}
void prepare(cmd_context &ctx) override {
m_arg_index = 0;
m_lits.reset();
m_vars.reset();
}
void execute(cmd_context &ctx) override {
ast_manager &m = ctx.m();
func_decl_ref_vector vars(m);
app_ref_vector vars_apps(m);
expr_ref_vector lits(m);
ctx.regular_stream() << "------------------------------ " << std::endl;
for (func_decl *v : m_vars) {
vars.push_back(v);
vars_apps.push_back(m.mk_const(v));
}
for (expr *e : m_lits) lits.push_back(e);
expr_ref fml(m.mk_and(lits), m);
ctx.regular_stream() << "[der] Before: " << fml << std::endl
<< "[der] Vars: ";
for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " ";
ctx.regular_stream() << std::endl;
params_ref pa;
// the following is the same code as in qe_mbp in spacer
qe_lite qe(m, pa, false);
qe(vars_apps, fml);
ctx.regular_stream() << "[der] After: " << fml << std::endl
<< "[der] Vars: ";
for (app *a : vars_apps) ctx.regular_stream() << app_ref(a, m) << " ";
ctx.regular_stream() << std::endl;
}
};
void install_dbg_cmds(cmd_context &ctx) {
ctx.insert(alloc(print_dimacs_cmd));
ctx.insert(alloc(get_quantifier_body_cmd));
ctx.insert(alloc(set_cmd));
ctx.insert(alloc(pp_var_cmd));
ctx.insert(alloc(shift_vars_cmd));
ctx.insert(alloc(assert_not_cmd));
ctx.insert(alloc(size_cmd));
ctx.insert(alloc(subst_cmd));
ctx.insert(alloc(bool_rewriter_cmd));
ctx.insert(alloc(bool_frewriter_cmd));
ctx.insert(alloc(elim_and_cmd));
install_simplify_cmd(ctx, "dbg-th-rewriter");
ctx.insert(alloc(lt_cmd));
ctx.insert(alloc(some_value_cmd));
ctx.insert(alloc(params_cmd));
ctx.insert(alloc(translator_cmd));
ctx.insert(alloc(sexpr_cmd));
ctx.insert(alloc(used_vars_cmd));
ctx.insert(alloc(elim_unused_vars_cmd));
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(mbp_qel_cmd));
ctx.insert(alloc(mbi_cmd));
ctx.insert(alloc(euf_project_cmd));
ctx.insert(alloc(eufi_cmd));
ctx.insert(alloc(qel_cmd));
ctx.insert(alloc(qe_lite_cmd));
}
View git blame Copy permalink