From 65885f7ebad4c4e8227c248f8073e20c5262c174 Mon Sep 17 00:00:00 2001 From: Matteo Date: Tue, 17 Oct 2017 16:55:52 +0200 Subject: [PATCH] add_constraint API --- src/api/api_datalog.cpp | 4 +++ src/api/z3_fixedpoint.h | 4 ++- src/muz/base/dl_context.h | 5 ++++ src/muz/base/dl_engine_base.h | 3 +++ src/muz/spacer/spacer_callback.h | 6 ++--- src/muz/spacer/spacer_context.cpp | 37 +++++++++++--------------- src/muz/spacer/spacer_context.h | 2 +- src/muz/spacer/spacer_dl_interface.cpp | 4 +++ src/muz/spacer/spacer_dl_interface.h | 2 ++ 9 files changed, 40 insertions(+), 27 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 7d2e38269..fd31a65f8 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -619,6 +619,10 @@ extern "C" { Z3_CATCH; } + void Z3_API Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl){ + to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); + } + #include "api_datalog_spacer.inc" }; diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index 6836c4766..b4c3eee49 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -367,7 +367,7 @@ extern "C" { void Z3_API Z3_fixedpoint_set_reduce_app_callback( Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb); - typedef void (*Z3_fixedpoint_new_lemma_eh)(void *state, Z3_ast *lemma, unsigned level); + typedef void (*Z3_fixedpoint_new_lemma_eh)(void *state, Z3_ast lemma, unsigned level); typedef void (*Z3_fixedpoint_predecessor_eh)(void *state); typedef void (*Z3_fixedpoint_unfold_eh)(void *state); @@ -377,6 +377,8 @@ extern "C" { Z3_fixedpoint_predecessor_eh predecessor_eh, Z3_fixedpoint_unfold_eh unfold_eh); + void Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl); + /*@}*/ /*@}*/ diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index a8567637c..b49c7e665 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -596,6 +596,11 @@ namespace datalog { m_engine->add_callback(state, new_lemma_eh, predecessor_eh, unfold_eh); } + void add_constraint (expr *c, unsigned lvl){ + ensure_engine(); + m_engine->add_constraint(c, lvl); + } + private: /** diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index 910dd2695..9fc90ab1d 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -112,6 +112,9 @@ namespace datalog { const t_unfold_eh unfold_eh) { throw default_exception(std::string("add_lemma_exchange_callbacks is not supported for ") + m_name); } + virtual void add_constraint (expr *c, unsigned lvl){ + throw default_exception(std::string("add_constraint is not supported for ") + m_name); + } virtual void updt_params() {} virtual void cancel() {} virtual void cleanup() {} diff --git a/src/muz/spacer/spacer_callback.h b/src/muz/spacer/spacer_callback.h index d5b47b90e..35805c7bc 100644 --- a/src/muz/spacer/spacer_callback.h +++ b/src/muz/spacer/spacer_callback.h @@ -45,15 +45,15 @@ namespace spacer { m_predecessor_eh(predecessor_eh), m_unfold_eh(unfold_eh) {} - inline bool new_lemma() override { return true; } + inline bool new_lemma() override { return m_new_lemma_eh != nullptr; } void new_lemma_eh(expr *lemma, unsigned level) override; - inline bool predecessor() override { return true; } + inline bool predecessor() override { return m_predecessor_eh != nullptr; } void predecessor_eh() override; - inline bool unfold() override { return true; } + inline bool unfold() override { return m_unfold_eh != nullptr; } void unfold_eh() override; diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 726edadc1..a4faf88cf 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1229,21 +1229,21 @@ void lemma::mk_expr_core() { normalize(m_body, m_body); if (!m_zks.empty() && has_zk_const(m_body)) { - app_ref_vector zks(m); + app_ref_vector zks(m); zks.append(m_zks); - zks.reverse(); - expr_abstract(m, 0, - zks.size(), (expr* const*)zks.c_ptr(), m_body, - m_body); - ptr_buffer sorts; - svector names; - for (unsigned i=0, sz=zks.size(); i < sz; ++i) { - sorts.push_back(get_sort(zks.get(i))); - names.push_back(zks.get(i)->get_decl()->get_name()); - } - m_body = m.mk_quantifier(true, zks.size(), - sorts.c_ptr(), - names.c_ptr(), + zks.reverse(); + expr_abstract(m, 0, + zks.size(), (expr* const*)zks.c_ptr(), m_body, + m_body); + ptr_buffer sorts; + svector names; + for (unsigned i=0, sz=zks.size(); i < sz; ++i) { + sorts.push_back(get_sort(zks.get(i))); + names.push_back(zks.get(i)->get_decl()->get_name()); + } + m_body = m.mk_quantifier(true, zks.size(), + sorts.c_ptr(), + names.c_ptr(), m_body, 15, symbol(m_body->get_id())); } SASSERT(m_body); @@ -3590,17 +3590,11 @@ expr_ref context::get_constraints (unsigned level) return m_pm.mk_and (constraints); } -void context::add_constraints (unsigned level, const expr_ref& c) +void context::add_constraint (unsigned level, const expr_ref& c) { if (!c.get()) { return; } if (m.is_true(c)) { return; } - expr_ref_vector constraints (m); - constraints.push_back (c); - flatten_and (constraints); - - for (unsigned i = 0, sz = constraints.size(); i < sz; ++i) { - expr *c = constraints.get (i); expr *e1, *e2; if (m.is_implies(c, e1, e2)) { SASSERT (is_app (e1)); @@ -3613,7 +3607,6 @@ void context::add_constraints (unsigned level, const expr_ref& c) } else{ this->m_stats.m_num_lemmas_discarded++; - } } } } diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 8b8055ad5..9d6d8d0a5 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -882,7 +882,7 @@ public: pob& get_root() const { return m_pob_queue.get_root(); } expr_ref get_constraints (unsigned lvl); - void add_constraints (unsigned lvl, const expr_ref& c); + void add_constraint (unsigned lvl, const expr_ref& c); void new_lemma_eh(pred_transformer &pt, lemma *lem); diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index 571687e16..57c225b38 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -360,3 +360,7 @@ void dl_interface::add_callback(void *state, const datalog::t_unfold_eh unfold_eh){ m_context->callbacks().push_back(alloc(user_callback, *m_context, state, new_lemma_eh, predecessor_eh, unfold_eh)); } + +void dl_interface::add_constraint (expr *c, unsigned lvl){ + m_context->add_constraint(c,lvl); +} diff --git a/src/muz/spacer/spacer_dl_interface.h b/src/muz/spacer/spacer_dl_interface.h index fb5ac3803..2980e2a0f 100644 --- a/src/muz/spacer/spacer_dl_interface.h +++ b/src/muz/spacer/spacer_dl_interface.h @@ -84,6 +84,8 @@ public: const datalog::t_predecessor_eh predecessor_eh, const datalog::t_unfold_eh unfold_eh); + void add_constraint (expr *c, unsigned lvl); + }; }