Commits

Nikolaj Bjorner committed 7553c3c

fix bugs in model generation reported by Ken

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

Comments (0)

Files changed (6)

src/muz_qe/dl_mk_rule_inliner.cpp

     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();
                 }
             }
         }
+        if (modified) {
+            datalog::del_rule(m_mc, *r0);
+        }
+
         return modified;
     }
 
 
             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;
     }
         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
         }
 
         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

 
 
 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

             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

 
         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

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

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