From 7bfb730fee5e6cf2154768f1d8576cf91b3d49bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Jun 2019 15:28:18 -0700 Subject: [PATCH] fix traffic jam Signed-off-by: Nikolaj Bjorner --- examples/python/trafficjam.py | 128 ++++++++++++++++++ src/api/api_datalog.cpp | 18 +-- src/muz/base/dl_context.cpp | 1 + src/muz/rel/dl_finite_product_relation.cpp | 6 + src/muz/rel/dl_instruction.cpp | 148 +++++++++------------ src/muz/rel/dl_instruction.h | 4 +- src/muz/rel/dl_mk_explanations.cpp | 6 +- 7 files changed, 217 insertions(+), 94 deletions(-) create mode 100644 examples/python/trafficjam.py diff --git a/examples/python/trafficjam.py b/examples/python/trafficjam.py new file mode 100644 index 000000000..38a56048e --- /dev/null +++ b/examples/python/trafficjam.py @@ -0,0 +1,128 @@ +from z3 import * + +class Car(): + def __init__(self, is_vertical, base_pos, length, start, color): + self.is_vertical = is_vertical + self.base = base_pos + self.length = length + self.start = start + self.color = color + + def __eq__(self, other): + return self.color == other.color + + def __ne__(self, other): + return self.color != other.color + +dimension = 6 + +red_car = Car(False, 2, 2, 3, "red") +cars = [ + Car(True, 0, 3, 0, 'yellow'), + Car(False, 3, 3, 0, 'blue'), + Car(False, 5, 2, 0, "brown"), + Car(False, 0, 2, 1, "lgreen"), + Car(True, 1, 2, 1, "light blue"), + Car(True, 2, 2, 1, "pink"), + Car(True, 2, 2, 4, "dark green"), + red_car, + Car(True, 3, 2, 3, "purple"), + Car(False, 5, 2, 3, "light yellow"), + Car(True, 4, 2, 0, "orange"), + Car(False, 4, 2, 4, "black"), + Car(True, 5, 3, 1, "light purple") + ] + +num_cars = len(cars) +B = BoolSort() +bv3 = BitVecSort(3) + + +state = Function('state', [ bv3 for c in cars] + [B]) + +def num(i): + return BitVecVal(i,bv3) + +def bound(i): + return Const(cars[i].color, bv3) + +fp = Fixedpoint() +fp.set("fp.engine","datalog") +fp.set("datalog.generate_explanations",True) +fp.declare_var([bound(i) for i in range(num_cars)]) +fp.register_relation(state) + +def mk_state(car, value): + return state([ (num(value) if (cars[i] == car) else bound(i)) for i in range(num_cars)]) + +def mk_transition(row, col, i0, j, car0): + body = [mk_state(car0, i0)] + for index in range(num_cars): + car = cars[index] + if car0 != car: + if car.is_vertical and car.base == col: + for i in range(dimension): + if i <= row and row < i + car.length and i + car.length <= dimension: + body += [bound(index) != num(i)] + if car.base == row and not car.is_vertical: + for i in range(dimension): + if i <= col and col < i + car.length and i + car.length <= dimension: + body += [bound(index) != num(i)] + + s = "%s %d->%d" % (car0.color, i0, j) + fp.rule(mk_state(car0, j), body, s) + + +def move_down(i, car): + free_row = i + car.length + if free_row < dimension: + mk_transition(free_row, car.base, i, i + 1, car) + + +def move_up(i, car): + free_row = i - 1 + if 0 <= free_row and i + car.length <= dimension: + mk_transition(free_row, car.base, i, i - 1, car) + +def move_left(i, car): + free_col = i - 1; + if 0 <= free_col and i + car.length <= dimension: + mk_transition(car.base, free_col, i, i - 1, car) + + +def move_right(i, car): + free_col = car.length + i + if free_col < dimension: + mk_transition(car.base, free_col, i, i + 1, car) + + +# Initial state: +fp.fact(state([num(cars[i].start) for i in range(num_cars)])) + +# Transitions: +for car in cars: + for i in range(dimension): + if car.is_vertical: + move_down(i, car) + move_up(i, car) + else: + move_left(i, car) + move_right(i, car) + + +def get_instructions(ans): + lastAnd = ans.arg(0).children()[-1] + trace = lastAnd.children()[1] + while trace.num_args() > 0: + print(trace.decl()) + trace = trace.children()[-1] + + +goal = state([ (num(4) if cars[i] == red_car else bound(i)) for i in range(num_cars)]) +fp.query(goal) +get_instructions(fp.get_answer()) + +del goal +del state +del fp + diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index e872bc12d..77c59e2d6 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -280,7 +280,7 @@ extern "C" { RESET_ERROR_CODE(); lbool r = l_undef; unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); - unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_fixedpoint(d)->m_params.get_bool("ctrl_c", true); { scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); @@ -373,11 +373,11 @@ extern "C" { Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); mk_c(c)->save_object(v); - for (unsigned i = 0; i < coll.m_queries.size(); ++i) { - v->m_ast_vector.push_back(coll.m_queries[i].get()); + for (expr * q : coll.m_queries) { + v->m_ast_vector.push_back(q); } - for (unsigned i = 0; i < coll.m_rels.size(); ++i) { - to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get(), true); + for (func_decl * f : coll.m_rels) { + to_fixedpoint_ref(d)->ctx().register_predicate(f, true); } for (unsigned i = 0; i < coll.m_rules.size(); ++i) { to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]); @@ -466,11 +466,11 @@ extern "C" { svector names; to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names); - for (unsigned i = 0; i < rules.size(); ++i) { - v->m_ast_vector.push_back(rules[i].get()); + for (expr* r : rules) { + v->m_ast_vector.push_back(r); } - for (unsigned i = 0; i < queries.size(); ++i) { - v->m_ast_vector.push_back(m.mk_not(queries[i].get())); + for (expr* q : queries) { + v->m_ast_vector.push_back(m.mk_not(q)); } RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(nullptr); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index d4af4693a..9e5e7b23e 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -837,6 +837,7 @@ namespace datalog { } lbool context::query(expr* query) { + expr_ref _query(query, m); m_mc = mk_skip_model_converter(); m_last_status = OK; m_last_answer = nullptr; diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index ccb4584f7..7858ab9a9 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -24,6 +24,7 @@ Revision History: #include "muz/rel/dl_table_relation.h" #include "muz/rel/dl_finite_product_relation.h" #include "ast/rewriter/bool_rewriter.h" +#include "ast/rewriter/th_rewriter.h" namespace datalog { @@ -1409,6 +1410,11 @@ namespace datalog { //create the condition with table values substituted in and relation values properly renamed expr_ref inner_cond(m_manager); inner_cond = m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.c_ptr()); + th_rewriter rw(m_manager); + rw(inner_cond); + if (m_manager.is_false(inner_cond)) { + continue; + } relation_base * new_rel = old_rel.clone(); diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 79508a4f6..98bb2be13 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -44,10 +44,7 @@ namespace datalog { } void execution_context::reset() { - reg_vector::iterator it=m_registers.begin(); - reg_vector::iterator end=m_registers.end(); - for(; it != end; ++it) { - relation_base * rel = *it; + for (relation_base * rel : m_registers) { if (rel) { rel->deallocate(); } @@ -148,10 +145,8 @@ namespace datalog { // ----------------------------------- instruction::~instruction() { - fn_cache::iterator it = m_fn_cache.begin(); - fn_cache::iterator end = m_fn_cache.end(); - for(; it != end; ++it) { - dealloc(it->m_value); + for (auto& p : m_fn_cache) { + dealloc(p.m_value); } } @@ -220,13 +215,13 @@ namespace datalog { void make_annotations(execution_context & ctx) override { ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { const char * rel_name = m_pred->get_name().bare_str(); if (m_store) { - out << "store " << m_reg << " into " << rel_name; + return out << "store " << m_reg << " into " << rel_name; } else { - out << "load " << rel_name << " into " << m_reg; + return out << "load " << rel_name << " into " << m_reg; } } }; @@ -251,8 +246,8 @@ namespace datalog { void make_annotations(execution_context & ctx) override { ctx.set_register_annotation(m_reg, "alloc"); } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "dealloc " << m_reg; + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "dealloc " << m_reg; } }; @@ -286,8 +281,8 @@ namespace datalog { ctx.set_register_annotation(m_src, str); } } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; } }; @@ -305,10 +300,7 @@ namespace datalog { instruction_block * m_body; bool control_is_empty(execution_context & ctx) { - idx_vector::const_iterator it=m_controls.begin(); - idx_vector::const_iterator end=m_controls.end(); - for(; it != end; ++it) { - reg_idx r = *it; + for (reg_idx r : m_controls) { if (ctx.reg(r) && !ctx.reg(r)->fast_empty()) { return false; } @@ -343,9 +335,10 @@ namespace datalog { void make_annotations(execution_context & ctx) override { m_body->make_annotations(ctx); } - void display_head_impl(execution_context const & ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const override { out << "while"; print_container(m_controls, out); + return out; } void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const override { m_body->display_indented(ctx, out, indentation+" "); @@ -413,12 +406,12 @@ namespace datalog { ctx.get_register_annotation(m_rel1, a1); ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); } - void display_head_impl(execution_context const & ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const override { out << "join " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; print_container(m_cols2, out); - out << " into " << m_res; + return out << " into " << m_res; } }; @@ -464,9 +457,9 @@ namespace datalog { a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); ctx.set_register_annotation(m_reg, a.str()); } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "filter_equal " << m_reg << " col: " << m_col << " val: " - << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "filter_equal " << m_reg << " col: " << m_col << " val: " + << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); } }; @@ -508,9 +501,10 @@ namespace datalog { } return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << "filter_identical " << m_reg << " "; print_container(m_cols, out); + return out; } void make_annotations(execution_context & ctx) override { ctx.set_register_annotation(m_reg, "filter_identical"); @@ -556,9 +550,10 @@ namespace datalog { return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "filter_interpreted " << m_reg << " using " - << mk_pp(m_cond, m_cond.get_manager()); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return + out << "filter_interpreted " << m_reg << " using " + << mk_pp(m_cond, m_cond.get_manager()); } void make_annotations(execution_context & ctx) override { std::stringstream a; @@ -609,15 +604,16 @@ namespace datalog { if (ctx.reg(m_res)->fast_empty()) { ctx.make_empty(m_res); } - //TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); + // TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << "filter_interpreted_and_project " << m_src << " into " << m_res; out << " using " << mk_pp(m_cond, m_cond.get_manager()); out << " deleting columns "; print_container(m_cols, out); + return out; } void make_annotations(execution_context & ctx) override { @@ -730,11 +726,12 @@ namespace datalog { } ctx.set_register_annotation(m_delta, str); } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; if (m_delta!=execution_context::void_register) { out << " with delta " << m_delta; } + return out; } }; @@ -786,10 +783,11 @@ namespace datalog { return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; out << (m_projection ? " deleting columns " : " with cycle "); print_container(m_cols, out); + return out; } void make_annotations(execution_context & ctx) override { std::stringstream s; @@ -851,7 +849,7 @@ namespace datalog { } return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { relation_base const* r1 = ctx.reg(m_rel1); relation_base const* r2 = ctx.reg(m_rel2); out << "join_project " << m_rel1; @@ -868,6 +866,7 @@ namespace datalog { print_container(m_cols2, out); out << " into " << m_res << " removing columns "; print_container(m_removed_cols, out); + return out; } void make_annotations(execution_context & ctx) override { std::string s1 = "rel1", s2 = "rel2"; @@ -922,9 +921,9 @@ namespace datalog { } return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col - << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col + << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); } void make_annotations(execution_context & ctx) override { std::stringstream s; @@ -979,12 +978,12 @@ namespace datalog { } return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << "filter_by_negation on " << m_tgt; print_container(m_cols1, out); out << " with " << m_neg_rel; print_container(m_cols2, out); - out << " as the negated table"; + return out << " as the negated table"; } void make_annotations(execution_context & ctx) override { std::string s = "negated relation"; @@ -1018,10 +1017,10 @@ namespace datalog { ctx.set_reg(m_tgt, rel); return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "mk_unary_singleton into " << m_tgt << " sort:" - << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0]) << " val:" - << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0], m_fact[0]); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "mk_unary_singleton into " << m_tgt << " sort:" + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0]) << " val:" + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0], m_fact[0]); } void make_annotations(execution_context & ctx) override { std::string s; @@ -1049,10 +1048,10 @@ namespace datalog { ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "mk_total into " << m_tgt << " sort:" - << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig) - << " " << m_pred->get_name(); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "mk_total into " << m_tgt << " sort:" + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig) + << " " << m_pred->get_name(); } void make_annotations(execution_context & ctx) override { std::string s; @@ -1076,8 +1075,8 @@ namespace datalog { ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { - out << "mark_saturated " << m_pred->get_name().bare_str(); + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { + return out << "mark_saturated " << m_pred->get_name().bare_str(); } void make_annotations(execution_context & ctx) override { } @@ -1100,9 +1099,10 @@ namespace datalog { } return true; } - void display_head_impl(execution_context const& ctx, std::ostream & out) const override { + std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { out << "instr_assert_signature of " << m_tgt << " signature:"; print_container(m_sig, out); + return out; } void make_annotations(execution_context & ctx) override { std::string s; @@ -1128,10 +1128,8 @@ namespace datalog { } void instruction_block::reset() { - instr_seq_type::iterator it = m_data.begin(); - instr_seq_type::iterator end = m_data.end(); - for(; it!=end; ++it) { - dealloc(*it); + for (auto* t : m_data) { + dealloc(t); } m_data.reset(); m_observer = nullptr; @@ -1139,54 +1137,40 @@ namespace datalog { bool instruction_block::perform(execution_context & ctx) const { cost_recorder crec; - instr_seq_type::const_iterator it = m_data.begin(); - instr_seq_type::const_iterator end = m_data.end(); - bool success = true; - for(; it!=end && success; ++it) { - - instruction * instr=(*it); + for (instruction * instr : m_data) { crec.start(instr); //finish is performed by the next start() or by the destructor of crec - TRACE("dl", - tout <<"% "; - instr->display_head_impl(ctx, tout); - tout <<"\n";); - success = !ctx.should_terminate() && instr->perform(ctx); + TRACE("dl", instr->display_head_impl(ctx, tout << "% ") << "\n";); + + if (ctx.should_terminate() || !instr->perform(ctx)) { + return false; + } } - return success; + return true; } void instruction_block::process_all_costs() { - instr_seq_type::iterator it = m_data.begin(); - instr_seq_type::iterator end = m_data.end(); - for(; it!=end; ++it) { - (*it)->process_all_costs(); + for (auto* t : m_data) { + t->process_all_costs(); } } void instruction_block::collect_statistics(statistics& st) const { - instr_seq_type::const_iterator it = m_data.begin(); - instr_seq_type::const_iterator end = m_data.end(); - for(; it!=end; ++it) { - (*it)->collect_statistics(st); + for (auto* t : m_data) { + t->collect_statistics(st); } } void instruction_block::make_annotations(execution_context & ctx) { - instr_seq_type::iterator it = m_data.begin(); - instr_seq_type::iterator end = m_data.end(); - for(; it!=end; ++it) { - (*it)->make_annotations(ctx); + for (auto* t : m_data) { + t->make_annotations(ctx); } } void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, const std::string & indentation) const { rel_context const& ctx = _ctx.get_rel_context(); - instr_seq_type::const_iterator it = m_data.begin(); - instr_seq_type::const_iterator end = m_data.end(); - for(; it!=end; ++it) { - instruction * i = (*it); + for (auto* i : m_data) { if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) { i->display_indented(_ctx, out, indentation); } diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 918763a95..858ac4924 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -225,8 +225,8 @@ namespace datalog { The newline character at the end should not be printed. */ - virtual void display_head_impl(execution_context const & ctx, std::ostream & out) const { - out << ""; + virtual std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const { + return out << ""; } /** \brief If relevant, output the body of the current instruction. diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index f69c1adc1..e1a1d40b9 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -478,11 +478,13 @@ namespace datalog { relation_mutator_fn * explanation_relation_plugin::mk_filter_interpreted_fn(const relation_base & r, app * cond) { - if (&r.get_plugin()!=this) { + if (&r.get_plugin() != this) { + TRACE("dl", tout << "not same plugin\n";); return nullptr; } ast_manager & m = get_ast_manager(); if (!m.is_eq(cond)) { + TRACE("dl", tout << "not equality " << mk_pp(cond, m) << "\n";); return nullptr; } expr * arg1 = cond->get_arg(0); @@ -493,11 +495,13 @@ namespace datalog { } if (!is_var(arg1) || !is_app(arg2)) { + TRACE("dl", tout << "not variable assignemnt\n";); return nullptr; } var * col_var = to_var(arg1); app * new_rule = to_app(arg2); if (!get_context().get_decl_util().is_rule_sort(col_var->get_sort())) { + TRACE("dl", tout << "not rule sort\n";); return nullptr; } unsigned col_idx = col_var->get_idx();