enable canceling simplex on interrupt, investigating PDR inconsistency

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

src/muz/base/dl_context.cpp

@@ -226,6 +226,7 @@ namespace datalog {
         m_engine(0),
         m_closed(false),
         m_saturation_was_run(false),
+        m_enable_bind_variables(true),
         m_last_status(OK),
         m_last_answer(m),
         m_engine_type(LAST_ENGINE),
@@ -328,8 +329,13 @@ namespace datalog {
     }
 
     expr_ref context::bind_vars(expr* fml, bool is_forall) {
+        if (m_enable_bind_variables) {
             return m_bind_variables(fml, is_forall);
         }
+        else {
+            return expr_ref(fml, m);
+        }
+    }
 
     void context::register_predicate(func_decl * decl, bool named) {
         if (!is_predicate(decl)) {
@@ -680,6 +686,7 @@ namespace datalog {
     }
 
     void context::transform_rules(rule_transformer::plugin* plugin) {
+        flet<bool> _enable_bv(m_enable_bind_variables, false);
         rule_transformer transformer(*this);
         transformer.register_plugin(plugin);
         transform_rules(transformer);
@@ -841,13 +848,6 @@ namespace datalog {
     }
 
     lbool context::query(expr* query) {
-#if 0
-        // TODO: what?
-        if(get_engine() != DUALITY_ENGINE) {
-          new_query();
-          check_rules(m_rule_set);	       
-        }   
-#endif
         m_mc = mk_skip_model_converter();
         m_last_status = OK;
         m_last_answer = 0;
@@ -990,7 +990,6 @@ namespace datalog {
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
 	    expr_ref r = bind_vars(m_rule_fmls[i].get(), true);
 	    rules.push_back(r.get());
-	    //            rules.push_back(m_rule_fmls[i].get());
 	    names.push_back(m_rule_names[i]);
 	    bounds.push_back(m_rule_bounds[i]);
         }

src/muz/base/dl_context.h

@@ -205,6 +205,7 @@ namespace datalog {
 
         bool               m_closed;
         bool               m_saturation_was_run;
+        bool               m_enable_bind_variables;
         execution_result   m_last_status;
         expr_ref           m_last_answer;
         DL_ENGINE          m_engine_type;
@@ -294,6 +295,8 @@ namespace datalog {
          */
         expr_ref bind_vars(expr* fml, bool is_forall);
 
+        bool& bind_vars_enabled() { return m_enable_bind_variables; }
+
         /**
            Register datalog relation.
 

src/muz/pdr/pdr_context.cpp

@@ -729,6 +729,7 @@ namespace pdr {
         obj_map<expr, unsigned>::iterator it  = other.m_prop2level.begin();
         obj_map<expr, unsigned>::iterator end = other.m_prop2level.end();        
         for (; it != end; ++it) {
+            IF_VERBOSE(2, verbose_stream() << "(pdr-inherit: " << mk_pp(it->m_key, m) << ")\n";);
             add_property(it->m_key, it->m_value);
         }
     }

src/muz/transforms/dl_mk_array_blast.cpp

@@ -266,11 +266,13 @@ namespace datalog {
             }
             else {
                 m_rewriter(e, tmp);
-                change = change || (tmp != e);
                 new_conjs.push_back(tmp);
             }
         }
-        
+        if (!inserted) {
+            rules.add_rule(&r);
+            return false;        
+        }
         expr_ref fml1(m), fml2(m), body(m), head(m);
         body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
         head = r.get_head();
@@ -278,8 +280,8 @@ namespace datalog {
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
-        change = ackermanize(r, body, head) || change;
+        change = ackermanize(r, body, head);
-        if (!inserted && !change) {
+        if (!change) {
             rules.add_rule(&r);
             return false;
         }
@@ -287,6 +289,7 @@ namespace datalog {
         fml2 = m.mk_implies(body, head);
         proof_ref p(m);
         rule_set new_rules(m_ctx);
+        TRACE("dl", tout << fml2 << "\n";);
         rm.mk_rule(fml2, p, new_rules, r.name());
         
 

src/muz/transforms/dl_transforms.cpp

@@ -38,6 +38,8 @@ Revision History:
 namespace datalog {
 
     void apply_default_transformation(context& ctx) {
+        flet<bool> _enable_bv(ctx.bind_vars_enabled(), false);
+
         rule_transformer transf(ctx);
         ctx.ensure_closed();
         transf.reset();

src/smt/theory_arith_core.h

@@ -1376,6 +1376,9 @@ namespace smt {
             failed();
             return false;
         }
+        if (get_context().get_cancel_flag()) {
+            return true;
+        }
         CASSERT("arith", satisfy_bounds());
         discard_update_trail();
 
@@ -2145,6 +2148,9 @@ namespace smt {
                 return false;
             }
             TRACE("arith_make_feasible_detail", display(tout););
+            if (get_context().get_cancel_flag()) {
+                return true;
+            }
         }
         TRACE("arith_make_feasible", tout << "make_feasible: sat\n"; display(tout););
         CASSERT("arith", wf_rows());