fix cover retrieval for slicing

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

src/muz_qe/dl_mk_slice.h

@@ -97,10 +97,14 @@ namespace datalog {
            the \c goal must be present in the \c rule_set that is being transformed.
          */
         mk_slice(context & ctx);
+
+        virtual ~mk_slice() { }
         
         rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
 
         func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }
+
+        obj_map<func_decl, func_decl*> const& get_predicates() { return m_predicates; }
     };
 
 };

src/muz_qe/pdr_context.cpp

@@ -20,6 +20,9 @@ Revision History:
 
 Notes:
 
+   TODO:
+   - fix the slicing with covers.
+   - 
    
 --*/
 
@@ -350,7 +353,7 @@ namespace pdr {
         }
     }
 
-    expr_ref pred_transformer::get_cover_delta(int level) {
+    expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) {
         expr_ref result(m.mk_true(), m), v(m), c(m);
         if (level == -1) {
             result = pm.mk_and(m_invariants);                       
@@ -368,6 +371,25 @@ namespace pdr {
         scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
         rep->set_substitution(&sub);
         (*rep)(result);
+
+        // adjust result according to model converter.
+        unsigned arity = m_head->get_arity();
+        model_ref md = alloc(model, m);
+        if (arity == 0) {
+            md->register_decl(m_head, result);
+        }
+        else {
+            func_interp* fi = alloc(func_interp, m, arity);
+            fi->set_else(result);
+            md->register_decl(m_head, fi);
+        }
+        apply(ctx.get_model_converter(), md, 0);
+        if (p_orig->get_arity() == 0) {
+            result = md->get_const_interp(p_orig);
+        }
+        else {
+            result = md->get_func_interp(p_orig)->get_interp();
+        }
         return result;        
     }
 
@@ -1181,10 +1203,10 @@ namespace pdr {
         }
     }
 
-    expr_ref context::get_cover_delta(int level, func_decl* p) {
+    expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p) {
         pred_transformer* pt = 0;
         if (m_rels.find(p, pt)) {
-            return pt->get_cover_delta(level);
+            return pt->get_cover_delta(p_orig, level);
         }
         else {
             IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);

src/muz_qe/pdr_context.h

@@ -126,7 +126,7 @@ namespace pdr {
         qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; }
         expr*  rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }
         unsigned get_num_levels() { return m_levels.size(); }
-        expr_ref get_cover_delta(int level);
+        expr_ref get_cover_delta(func_decl* p_orig, int level);
         void     add_cover(unsigned level, expr* property);
 
         std::ostream& display(std::ostream& strm) const;
@@ -385,6 +385,8 @@ namespace pdr {
 
         void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
 
+        model_converter_ref get_model_converter() { return m_mc; }
+
         void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
 
         void update_rules(datalog::rule_set& rules);
@@ -395,7 +397,7 @@ namespace pdr {
 
         unsigned get_num_levels(func_decl* p);
 
-        expr_ref get_cover_delta(int level, func_decl* p);
+        expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
 
         void add_cover(int level, func_decl* pred, expr* property);
 

src/muz_qe/pdr_dl_interface.cpp

@@ -39,7 +39,8 @@ dl_interface::dl_interface(datalog::context& ctx) :
     m_ctx(ctx), 
     m_pdr_rules(ctx), 
     m_old_rules(ctx),
-    m_context(0) {
+    m_context(0),
+    m_refs(ctx.get_manager()) {
     m_context = alloc(pdr::context, ctx.get_fparams(), ctx.get_params(), ctx.get_manager());
 }
 
@@ -78,6 +79,8 @@ lbool dl_interface::query(expr * query) {
     //we restore the initial state in the datalog context
     m_ctx.ensure_opened();
     m_pdr_rules.reset();
+    m_refs.reset();
+    m_pred2slice.reset();
     m_ctx.get_rmanager().reset_relations();
     ast_manager& m =                      m_ctx.get_manager();
     datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
@@ -116,10 +119,20 @@ lbool dl_interface::query(expr * query) {
         m_ctx.transform_rules(transformer, mc, pc);        
         query_pred = slice->get_predicate(query_pred.get());
         m_ctx.set_output_predicate(query_pred);
+        
+        // track sliced predicates.
+        obj_map<func_decl, func_decl*> const& preds = slice->get_predicates();
+        obj_map<func_decl, func_decl*>::iterator it  = preds.begin();
+        obj_map<func_decl, func_decl*>::iterator end = preds.end();
+        for (; it != end; ++it) {
+            m_pred2slice.insert(it->m_key, it->m_value);
+            m_refs.push_back(it->m_key);
+            m_refs.push_back(it->m_value);
+        }
     }
 
     if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) {
-        unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0);
+        unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules", 0);
         datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
         if (m_ctx.get_params().get_uint(":coalesce-rules", false)) {
             transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
@@ -160,15 +173,23 @@ lbool dl_interface::query(expr * query) {
     }
 }
 
-expr_ref dl_interface::get_cover_delta(int level, func_decl* pred) {
+expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {
-    return m_context->get_cover_delta(level, pred);
+    func_decl* pred = pred_orig;
+    m_pred2slice.find(pred_orig, pred);
+    SASSERT(pred);
+    return m_context->get_cover_delta(level, pred_orig, pred);
 }
 
 void dl_interface::add_cover(int level, func_decl* pred, expr* property) {
+    if (m_ctx.get_params().get_bool(":slice", true)) {
+        throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
+    }
     m_context->add_cover(level, pred, property);
 }
 
 unsigned dl_interface::get_num_levels(func_decl* pred) {
+    m_pred2slice.find(pred, pred);
+    SASSERT(pred);
     return m_context->get_num_levels(pred);
 }
 

src/muz_qe/pdr_dl_interface.h

@@ -37,7 +37,9 @@ namespace pdr {
         datalog::context& m_ctx;
         datalog::rule_set m_pdr_rules;
         datalog::rule_set m_old_rules;
-        context* m_context;
+        context*          m_context;
+        obj_map<func_decl, func_decl*> m_pred2slice;
+        ast_ref_vector    m_refs;
 
         void check_reset();
 

src/muz_qe/pdr_manager.cpp

@@ -58,24 +58,20 @@ namespace pdr {
     expr_ref inductive_property::fixup_clause(expr* fml) const {        
         expr_ref_vector disjs(m);
         datalog::flatten_or(fml, disjs);
-        switch(disjs.size()) {
+        expr_ref result(m);
-        case 0: return expr_ref(m.mk_false(), m);
+        bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
-        case 1: return expr_ref(disjs[0].get(), m);
+        return result;
-        default: return expr_ref(m.mk_or(disjs.size(), disjs.c_ptr()), m);
-        }
     }
 
     expr_ref inductive_property::fixup_clauses(expr* fml) const {
         expr_ref_vector conjs(m);
+        expr_ref result(m);
         datalog::flatten_and(fml, conjs);
         for (unsigned i = 0; i < conjs.size(); ++i) {
             conjs[i] = fixup_clause(conjs[i].get());
         }
-        switch(conjs.size()) {
+        bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
-        case 0: return expr_ref(m.mk_true(), m);
+        return result;
-        case 1: return expr_ref(conjs[0].get(), m);
-        default: return expr_ref(m.mk_and(conjs.size(), conjs.c_ptr()), m);
-        }
     }
 
     std::string inductive_property::to_string() const {