mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
adding a new toy for Clemens
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6963451704
commit
9c8800bdde
|
@ -1729,10 +1729,10 @@ namespace smt {
|
|||
return m_user_propagator->add_expr(e);
|
||||
}
|
||||
|
||||
void user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
|
||||
if (!m_user_propagator)
|
||||
throw default_exception("user propagator must be initialized");
|
||||
m_user_propagator->register_declared(r);
|
||||
m_user_propagator->register_created(r);
|
||||
}
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
|
||||
|
|
|
@ -249,8 +249,8 @@ namespace smt {
|
|||
return m_kernel.user_propagate_register(e);
|
||||
}
|
||||
|
||||
void user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
|
||||
m_kernel.user_propagate_register_declared(r);
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& r) {
|
||||
m_kernel.user_propagate_register_created(r);
|
||||
}
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
|
||||
|
@ -305,7 +305,6 @@ namespace smt {
|
|||
return m_imp->get_formula(i);
|
||||
}
|
||||
|
||||
|
||||
void kernel::push() {
|
||||
m_imp->push();
|
||||
}
|
||||
|
@ -485,8 +484,8 @@ namespace smt {
|
|||
return m_imp->user_propagate_register(e);
|
||||
}
|
||||
|
||||
void kernel::user_propagate_register_declared(user_propagator::register_created_eh_t& r) {
|
||||
m_imp->user_propagate_register_declared(r);
|
||||
void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) {
|
||||
m_imp->user_propagate_register_created(r);
|
||||
}
|
||||
|
||||
func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
|
||||
|
|
|
@ -303,7 +303,7 @@ namespace smt {
|
|||
|
||||
unsigned user_propagate_register(expr* e);
|
||||
|
||||
void user_propagate_register_declared(user_propagator::register_created_eh_t& r);
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& r);
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
|
||||
|
||||
|
|
|
@ -241,6 +241,14 @@ namespace {
|
|||
return m_context.user_propagate_register(e);
|
||||
}
|
||||
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& c) override {
|
||||
m_context.user_propagate_register_created(c);
|
||||
}
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
|
||||
return m_context.user_propagate_declare(name, n, domain, range);
|
||||
}
|
||||
|
||||
struct scoped_minimize_core {
|
||||
smt_solver& s;
|
||||
expr_ref_vector m_assumptions;
|
||||
|
|
|
@ -319,15 +319,21 @@ public:
|
|||
user_propagator::final_eh_t m_final_eh;
|
||||
user_propagator::eq_eh_t m_eq_eh;
|
||||
user_propagator::eq_eh_t m_diseq_eh;
|
||||
user_propagator::register_created_eh_t m_created_eh;
|
||||
|
||||
expr_ref_vector m_vars;
|
||||
unsigned_vector m_var2internal;
|
||||
unsigned_vector m_internal2var;
|
||||
unsigned_vector m_limit;
|
||||
|
||||
|
||||
user_propagator::push_eh_t i_push_eh;
|
||||
user_propagator::pop_eh_t i_pop_eh;
|
||||
user_propagator::fixed_eh_t i_fixed_eh;
|
||||
user_propagator::final_eh_t i_final_eh;
|
||||
user_propagator::eq_eh_t i_eq_eh;
|
||||
user_propagator::eq_eh_t i_diseq_eh;
|
||||
|
||||
user_propagator::register_created_eh_t i_created_eh;
|
||||
|
||||
|
||||
struct callback : public user_propagator::callback {
|
||||
|
@ -403,15 +409,43 @@ public:
|
|||
m_ctx->user_propagate_register_diseq(i_diseq_eh);
|
||||
}
|
||||
|
||||
void init_i_created_eh() {
|
||||
if (!m_created_eh)
|
||||
return;
|
||||
i_created_eh = [this](void* ctx, user_propagator::callback* cb, expr* e, unsigned i) {
|
||||
unsigned j = m_vars.size();
|
||||
m_vars.push_back(e);
|
||||
m_internal2var.setx(i, j, 0);
|
||||
m_var2internal.setx(j, i, 0);
|
||||
};
|
||||
m_ctx->user_propagate_register_created(i_created_eh);
|
||||
}
|
||||
|
||||
void init_i_push_pop() {
|
||||
i_push_eh = [this](void* ctx) {
|
||||
m_limit.push_back(m_vars.size());
|
||||
m_push_eh(ctx);
|
||||
};
|
||||
i_pop_eh = [this](void* ctx, unsigned n) {
|
||||
unsigned old_sz = m_limit.size() - n;
|
||||
unsigned num_vars = m_limit[old_sz];
|
||||
m_vars.shrink(num_vars);
|
||||
m_limit.shrink(old_sz);
|
||||
m_pop_eh(ctx, n);
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
void user_propagate_delay_init() {
|
||||
if (!m_user_ctx)
|
||||
return;
|
||||
m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
|
||||
init_i_push_pop();
|
||||
m_ctx->user_propagate_init(m_user_ctx, i_push_eh, i_pop_eh, m_fresh_eh);
|
||||
init_i_fixed_eh();
|
||||
init_i_final_eh();
|
||||
init_i_eq_eh();
|
||||
init_i_diseq_eh();
|
||||
init_i_created_eh();
|
||||
|
||||
unsigned i = 0;
|
||||
for (expr* v : m_vars) {
|
||||
|
@ -463,6 +497,14 @@ public:
|
|||
m_vars.push_back(e);
|
||||
return m_vars.size() - 1;
|
||||
}
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
|
||||
return m_ctx->user_propagate_declare(name, n, domain, range);
|
||||
}
|
||||
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
|
||||
m_ctx->user_propagate_register_created(created_eh);
|
||||
}
|
||||
};
|
||||
|
||||
static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {
|
||||
|
|
|
@ -189,8 +189,12 @@ bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) {
|
|||
}
|
||||
|
||||
bool theory_user_propagator::internalize_term(app* term) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
for (auto arg : *term)
|
||||
ensure_enode(arg);
|
||||
unsigned v = add_expr(term);
|
||||
if (m_created_eh)
|
||||
m_created_eh(m_user_context, this, term, v);
|
||||
return true;
|
||||
}
|
||||
|
||||
void theory_user_propagator::collect_statistics(::statistics & st) const {
|
||||
|
|
|
@ -96,7 +96,7 @@ namespace smt {
|
|||
void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
|
||||
void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
|
||||
void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
|
||||
void register_declared(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; }
|
||||
void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; }
|
||||
func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
|
||||
|
||||
bool has_fixed() const { return (bool)m_fixed_eh; }
|
||||
|
|
|
@ -200,6 +200,14 @@ public:
|
|||
m_t2->user_propagate_clear();
|
||||
}
|
||||
|
||||
void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override {
|
||||
m_t2->user_propagate_register_created(created_eh);
|
||||
}
|
||||
|
||||
func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override {
|
||||
return m_t2->user_propagate_declare(name, n, domain, range);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
tactic * and_then(tactic * t1, tactic * t2) {
|
||||
|
|
Loading…
Reference in a new issue