fix traffic jam

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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
+

src/api/api_datalog.cpp

@@ -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) {
+        for (expr * q : coll.m_queries) {
-            v->m_ast_vector.push_back(coll.m_queries[i].get());
+            v->m_ast_vector.push_back(q);
         }
-        for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
+        for (func_decl * f : coll.m_rels) {
-            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get(), true);
+            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<symbol> names;
         
         to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names);
-        for (unsigned i = 0; i < rules.size(); ++i) {
+        for (expr* r : rules) {
-            v->m_ast_vector.push_back(rules[i].get());
+            v->m_ast_vector.push_back(r);
         }
-        for (unsigned i = 0; i < queries.size(); ++i) {
+        for (expr* q : queries) {
-            v->m_ast_vector.push_back(m.mk_not(queries[i].get()));
+            v->m_ast_vector.push_back(m.mk_not(q));
         }
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(nullptr);

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;

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();
                 

src/muz/rel/dl_instruction.cpp

@@ -44,10 +44,7 @@ namespace datalog {
     }
 
     void execution_context::reset() {
-        reg_vector::iterator it=m_registers.begin();
+        for (relation_base * rel : m_registers) {
-        reg_vector::iterator end=m_registers.end();
-        for(; it != end; ++it) {
-            relation_base * rel = *it;
             if (rel) {
                 rel->deallocate();
             }
@@ -148,10 +145,8 @@ namespace datalog {
     // -----------------------------------
 
     instruction::~instruction() {
-        fn_cache::iterator it = m_fn_cache.begin();
+        for (auto& p : m_fn_cache) {
-        fn_cache::iterator end = m_fn_cache.end();
+            dealloc(p.m_value);
-        for(; it != end; ++it) {
-            dealloc(it->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 {
+        std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            out << "dealloc " << m_reg;
+            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 {
+        std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt;
+            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();
+            for (reg_idx r : m_controls) {
-            idx_vector::const_iterator end=m_controls.end();
-            for(; it != end; ++it) {
-                reg_idx r = *it;
                 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,8 +457,8 @@ 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 {
+        std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            out << "filter_equal " << m_reg << " col: " << m_col << " val: "
+            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,7 +550,8 @@ 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 {
+            return 
                 out << "filter_interpreted " << m_reg << " using "
                     << mk_pp(m_cond, m_cond.get_manager());
         }
@@ -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,8 +921,8 @@ 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 << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col 
+            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 {
@@ -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,8 +1017,8 @@ namespace datalog {
             ctx.set_reg(m_tgt, rel);
             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 << "mk_unary_singleton into " << m_tgt << " sort:" 
+            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]);
         }
@@ -1049,8 +1048,8 @@ 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 {
+        std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            out << "mk_total into " << m_tgt << " sort:" 
+            return out << "mk_total into " << m_tgt << " sort:" 
                        << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig)
                        << " " << m_pred->get_name();
         }
@@ -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 {
+        std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            out << "mark_saturated " << m_pred->get_name().bare_str();
+            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();
+        for (auto* t : m_data) {
-        instr_seq_type::iterator end = m_data.end();
+            dealloc(t);
-        for(; it!=end; ++it) {
-            dealloc(*it);
         }
         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();
+        for (instruction * instr : m_data) {
-        instr_seq_type::const_iterator end = m_data.end();
-        bool success = true;
-        for(; it!=end && success; ++it) {
-
-            instruction * instr=(*it);
             crec.start(instr); //finish is performed by the next start() or by the destructor of crec
 
-            TRACE("dl",      
+            TRACE("dl", instr->display_head_impl(ctx, tout << "% ") << "\n";);
-                tout <<"% ";
+
-                  instr->display_head_impl(ctx, tout);
+            if (ctx.should_terminate() || !instr->perform(ctx)) {
-                tout <<"\n";);
+                return false;
-            success = !ctx.should_terminate() && instr->perform(ctx);
             }
-        return success;
+        }
+        return true;
     }
 
     void instruction_block::process_all_costs() {
-        instr_seq_type::iterator it = m_data.begin();
+        for (auto* t : m_data) {
-        instr_seq_type::iterator end = m_data.end();
+            t->process_all_costs();
-        for(; it!=end; ++it) {
-            (*it)->process_all_costs();
         }
     }
 
 
     void instruction_block::collect_statistics(statistics& st) const {
-        instr_seq_type::const_iterator it = m_data.begin();
+        for (auto* t : m_data) {
-        instr_seq_type::const_iterator end = m_data.end();
+            t->collect_statistics(st);
-        for(; it!=end; ++it) {
-            (*it)->collect_statistics(st);
         }
     }
 
     void instruction_block::make_annotations(execution_context & ctx) {
-        instr_seq_type::iterator it = m_data.begin();
+        for (auto* t : m_data) {
-        instr_seq_type::iterator end = m_data.end();
+            t->make_annotations(ctx);
-        for(; it!=end; ++it) {
-            (*it)->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();
+        for (auto* i : m_data) {
-        instr_seq_type::const_iterator end = m_data.end();
-        for(; it!=end; ++it) {
-            instruction * i = (*it);
             if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) {
                 i->display_indented(_ctx, out, indentation);
             }

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 {
+        virtual std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const {
-            out << "<instruction>";
+            return out << "<instruction>";
         }
         /**
            \brief If relevant, output the body of the current instruction.

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();