mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-21 10:40:35 +02:00
parent b1dbea328a
commit 89e8a1392c
2 changed files with 21 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/muz/base/dl_context.cpp
View file

@ -773,19 +773,19 @@ namespace datalog {
DL_ENGINE get_engine() const { return m_engine_type; }
void operator()(expr* e) {
if (a.is_int_real(e)) {
m_engine_type = SPACER_ENGINE;
}
else if (is_var(e) && m.is_bool(e)) {
m_engine_type = SPACER_ENGINE;
}
else if (dt.is_datatype(m.get_sort(e))) {
m_engine_type = SPACER_ENGINE;
if (a.is_int_real(e)) {
m_engine_type = SPACER_ENGINE;
}
else if (is_var(e) && m.is_bool(e)) {
m_engine_type = SPACER_ENGINE;
}
else if (dt.is_datatype(m.get_sort(e))) {
m_engine_type = SPACER_ENGINE;
}
}
};
void context::configure_engine() {
void context::configure_engine(expr* q) {
if (m_engine_type != LAST_ENGINE) {
return;
}
@ -817,6 +817,10 @@ namespace datalog {
expr_fast_mark1 mark;
engine_type_proc proc(m);
m_engine_type = DATALOG_ENGINE;
std::cout << "configure engine " << m_rule_set.get_num_rules() << " " << m_rule_fmls.size() << " " << q << "\n";
if (q) {
quick_for_each_expr(proc, mark, q);
}
for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
rule * r = m_rule_set.get_rule(i);
quick_for_each_expr(proc, mark, r->get_head());
@ -837,12 +841,13 @@ namespace datalog {
}
lbool context::query(expr* query) {
std::cout << "query: " << mk_pp(query, m) << "\n";
expr_ref _query(query, m);
m_mc = mk_skip_model_converter();
m_last_status = OK;
m_last_answer = nullptr;
m_last_ground_answer = nullptr;
switch (get_engine()) {
switch (get_engine(query)) {
case DATALOG_ENGINE:
case SPACER_ENGINE:
case BMC_ENGINE:
@ -855,7 +860,7 @@ namespace datalog {
default:
UNREACHABLE();
}
ensure_engine();
ensure_engine(query);
lbool r = m_engine->query(query);
if (r != l_undef && get_params().print_certificate()) {
display_certificate(std::cout) << "\n";
@ -893,9 +898,9 @@ namespace datalog {
return m_engine->get_proof();
}
void context::ensure_engine() {
void context::ensure_engine(expr* e) {
if (!m_engine.get()) {
m_engine = m_register_engine.mk_engine(get_engine());
m_engine = m_register_engine.mk_engine(get_engine(e));
m_engine->updt_params();
// break abstraction.

6
src/muz/base/dl_context.h
View file

@ -227,13 +227,13 @@ namespace datalog {
bool saturation_was_run() const { return m_saturation_was_run; }
void notify_saturation_was_run() { m_saturation_was_run = true; }
void configure_engine();
void configure_engine(expr* e);
ast_manager & get_manager() const { return m; }
rule_manager & get_rule_manager() { return m_rule_manager; }
smt_params & get_fparams() const { return m_fparams; }
fp_params const& get_params() const { return *m_params; }
DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
DL_ENGINE get_engine(expr* e = nullptr) { configure_engine(e); return m_engine_type; }
register_engine_base& get_register_engine() { return m_register_engine; }
th_rewriter& get_rewriter() { return m_rewriter; }
var_subst & get_var_subst() { return m_var_subst; }
@ -609,7 +609,7 @@ namespace datalog {
void flush_add_rules();
void ensure_engine();
void ensure_engine(expr* e = nullptr);
// auxiliary functions for SMT2 pretty-printer.
void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);