Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/muz_qe/dl_mk_rule_inliner.cpp

@@ -422,11 +422,8 @@ namespace datalog {
     bool mk_rule_inliner::transform_rule(rule * r0, rule_set& tgt) {
         bool modified = false;
         rule_ref_vector todo(m_rm);
-
         todo.push_back(r0);
 
-
-
         while (!todo.empty()) {
             rule_ref r(todo.back(), m_rm);
             todo.pop_back();
@@ -458,6 +455,10 @@ namespace datalog {
                 }
             }
         }
+        if (modified) {
+            datalog::del_rule(m_mc, *r0);
+        }
+
         return modified;
     }
 
@@ -476,6 +477,14 @@ namespace datalog {
 
             something_done |= !inlining_allowed(pred) && transform_rule(r, tgt);
         }
+
+        if (something_done && m_mc) {
+            for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
+                if (inlining_allowed((*rit)->get_decl())) {
+                    datalog::del_rule(m_mc, **rit);
+                }
+            }
+        }
         
         return something_done;
     }
@@ -847,10 +856,10 @@ namespace datalog {
         m_mc = hsmc.get();
         m_pc = hpc.get();
 
-        plan_inlining(source);
-
         scoped_ptr<rule_set> res = alloc(rule_set, m_context);
 
+        plan_inlining(source);
+
         something_done = transform_rules(source, *res);
 
         VERIFY(res->close()); //this transformation doesn't break the negation stratification
@@ -861,7 +870,7 @@ namespace datalog {
         }
 
         params_ref const& params = m_context.get_params();
-            if (params.get_bool(":inline-linear", true) && inline_linear(res)) {
+        if (params.get_bool(":inline-linear", true) && inline_linear(res)) {
             something_done = true;
         }
 

src/muz_qe/horn_subsume_model_converter.cpp

@@ -174,7 +174,7 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
 
 
 void horn_subsume_model_converter::operator()(model_ref& mr) {
-    TRACE("dl_mc", model_smt2_pp(tout, m, *mr, 0););
+    TRACE("dl_mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
     for (unsigned i = m_funcs.size(); i > 0; ) {
         --i;
         func_decl* h = m_funcs[i].get();

src/muz_qe/pdr_context.cpp

@@ -1844,7 +1844,7 @@ namespace pdr {
             break;
         }
         case l_true: {
-            strm << mk_pp(mk_sat_answer(), m);
+            strm << mk_ismt2_pp(mk_sat_answer(), m);
             break;
         }
         case l_undef: {

src/muz_qe/pdr_context.h

@@ -375,6 +375,8 @@ namespace pdr {
 
         void set_query(func_decl* q) { m_query_pred = q; }
 
+        void set_unsat() { m_last_result = l_false; }
+
         void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
 
         void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }

src/muz_qe/pdr_dl_interface.cpp

@@ -139,9 +139,6 @@ lbool dl_interface::query(expr * query) {
     m_ctx.reopen();
     m_ctx.replace_rules(old_rules);
 
-    if (m_pdr_rules.get_rules().empty()) {
-        return l_false;
-    }
 
     m_context->set_proof_converter(pc);
     m_context->set_model_converter(mc);
@@ -149,6 +146,10 @@ lbool dl_interface::query(expr * query) {
     m_context->set_axioms(bg_assertion);
     m_context->update_rules(m_pdr_rules);
     
+    if (m_pdr_rules.get_rules().empty()) {
+        m_context->set_unsat();
+        return l_false;
+    }
         
     while (true) {
         try {

src/muz_qe/pdr_manager.cpp

@@ -111,6 +111,7 @@ namespace pdr {
                 md->register_decl(pred, fi);
             }
         }
+        TRACE("pdr", model_smt2_pp(tout, m, *md, 0););
         apply(const_cast<model_converter_ref&>(m_mc), md, 0);
     }