Commits

Nikolaj Bjorner committed c4cb66b

fix bugs in inliner and usage of unbound variable fix, reported by Arie Gurfinkel

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

Comments (0)

Files changed (16)

src/muz_qe/dl_context.cpp

         
         p.insert(":fix-unbound-vars", CPK_BOOL, "fix unbound variables in tail");
         p.insert(":default-table-checker", CPK_SYMBOL, "see :default-table-checked");
-        p.insert(":inline-linear", CPK_BOOL, "try linear inlining method");
+        p.insert(":inline-linear", CPK_BOOL, "(default true) try linear inlining method");
+        p.insert(":inline-eager", CPK_BOOL, "(default true) try eager inlining of rules");
         PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion"););
 
         pdr::dl_interface::collect_params(p);
         }
     }
     
-#if 0
-    // [Leo] dead code?
-    static func_decl* get_head_relation(ast_manager& m, expr* fml) {
-        while (is_quantifier(fml)) {
-            fml = to_quantifier(fml)->get_expr();            
-        }
-        expr* f1;
-        while (m.is_implies(fml, f1, fml)) {};
-        if (is_app(fml)) {
-            return to_app(fml)->get_decl();
-        }
-        else {
-            return 0;
-        }
-    }
-#endif
-
     void context::display_smt2(
         unsigned num_queries, 
         expr* const* queries, 

src/muz_qe/dl_finite_product_relation.cpp

         }
     };
 
+#if 0
     /**
        Union operation taking advantage of the fact that the inner relation of all the arguments
        is a singleton relation.
 
         // [Leo]: gcc complained about the following class.
         // It does not have a constructor and uses a reference
-#if 0
+
         class inner_relation_copier : public table_row_mutator_fn {
             finite_product_relation & m_tgt;
             const finite_product_relation & m_src;
                 return true;
             }
         };
-#endif
 
         scoped_ptr<table_union_fn> m_t_union_fun;
         offset_row_mapper * m_offset_mapper_obj; //initialized together with m_offset_mapper_fun, and deallocated by it
             NOT_IMPLEMENTED_YET();
         }
     };
+#endif
 
     class finite_product_relation_plugin::converting_union_fn : public relation_union_fn {
         scoped_ptr<relation_union_fn> m_tr_union_fun;

src/muz_qe/dl_mk_coalesce.cpp

         }
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
-        // bool change = false;
         for (; it != end; ++it) {
-            // func_decl* p = it->m_key;
             rule_ref_vector d_rules(rm);
             d_rules.append(it->m_value->size(), it->m_value->c_ptr());
             for (unsigned i = 0; i < d_rules.size(); ++i) {
                         merge_rules(r1, *d_rules[j].get());
                         d_rules[j] = d_rules.back();
                         d_rules.pop_back();
-                        // change = true;
                         --j;
                     }
                 }

src/muz_qe/dl_mk_rule_inliner.cpp

 
     Added linear_inline 2012-9-10 (nbjorner)
 
+    Disable inliner for quantified rules 2012-10-31 (nbjorner)
     
 Notes:
 
         res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
         res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
         res->norm_vars(m_rm);
-        if (m_context.fix_unbound_vars()) {
-            m_rm.fix_unbound_vars(res, true);
-        }
+        m_rm.fix_unbound_vars(res, true);        
         if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
             res = simpl_rule;
             return true;
 
         tgt.norm_vars(m_context.get_rule_manager());
 
-        if (has_quantifier(src)) {
-            return false;
-        }
+        SASSERT(!has_quantifier(src));
 
         if (!m_unifier.unify_rules(tgt, tail_index, src)) {
             return false;
 
             for  (; i < pt_len && !inlining_allowed(r->get_decl(i)); ++i) {};
 
-            if (has_quantifier(*r.get())) {
-                continue;
-            }
+            SASSERT(!has_quantifier(*r.get()));
 
             if (i == pt_len) {
                 //there's nothing we can inline in this rule
         bool something_done = false;
         ref<horn_subsume_model_converter> hsmc;        
         ref<replace_proof_converter> hpc;
+        params_ref const& params = m_context.get_params();
 
         if (source.get_num_rules() == 0) {
             return 0;
         }
 
+        rule_set::iterator end = source.end();
+        for (rule_set::iterator it = source.begin(); it != end; ++ it) {
+            if (has_quantifier(**it)) {
+                return 0;
+            }
+        }
+        
+
         if (mc) {
             hsmc = alloc(horn_subsume_model_converter, m);
         }
 
         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
-
-        // try eager inlining
-        if (do_eager_inlining(res)) {
-            something_done = true;
+        if (params.get_bool(":inline-eager", true)) {
+            TRACE("dl", source.display(tout << "before eager inlining\n"););
+            plan_inlining(source);            
+            something_done = transform_rules(source, *res);            
+            VERIFY(res->close()); //this transformation doesn't break the negation stratification
+            // try eager inlining
+            if (do_eager_inlining(res)) {
+                something_done = true;
+            }
+            TRACE("dl", res->display(tout << "after eager inlining\n"););
         }
 
-        params_ref const& params = m_context.get_params();
         if (params.get_bool(":inline-linear", true) && inline_linear(res)) {
             something_done = true;
         }

src/muz_qe/dl_mk_slice.cpp

             TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";);
             rule* orig0    = m_sliceform2rule.find(fact0);
             /* rule* slice0   = */ m_rule2slice.find(orig0);
-            /* unsigned_vector const& renaming0 = */ m_renaming.find(orig0);
+            /* unsigned_vector const& renaming0 = m_renaming.find(orig0); */
             premises.push_back(p0_new);
             rule_ref r1(rm), r2(rm), r3(rm);
             r1 = orig0;
                 TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";);
                 rule* orig1     = m_sliceform2rule.find(fact1);
                 /* rule* slice1    = */ m_rule2slice.find(orig1);
-                /* unsigned_vector const& renaming1 = */ m_renaming.find(orig1); //TBD
+                /* unsigned_vector const& renaming1 =  m_renaming.find(orig1); TBD */
                 premises.push_back(p1_new);
 
                 // TODO: work with substitutions.

src/muz_qe/dl_mk_subsumption_checker.cpp

         res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
         res->set_accounting_parent_object(m_context, r);
         m_context.get_rule_manager().fix_unbound_vars(res, true);
+        
         return true;
     }
 

src/muz_qe/dl_mk_unbound_compressor.cpp

 
         res = m_context.get_rule_manager().mk( r->get_head(), tails.size(), tails.c_ptr(), tails_negated.c_ptr());
         res->set_accounting_parent_object(m_context, r);
-        m_context.get_rule_manager().fix_unbound_vars(res, true);
+        m_context.get_rule_manager().fix_unbound_vars(res, true);        
     }
 
     void mk_unbound_compressor::add_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index) {

src/muz_qe/dl_rule.cpp

 
 Author:
 
-    Leonardo de Moura (leonardo) 2010-05-17.
+    Krystof Hoder (t-khoder) 2011-10-19.
 
 Revision History:
 
+    Nikolaj Bjorner (nbjorner) 2012-10-31.
+      Check for enabledness of fix_unbound_vars inside call.
+      This function gets called from many rule tansformers.
+
 --*/
 
 #include<algorithm>
 #include"used_symbols.h"
 #include"quant_hoist.h"
 #include"expr_replacer.h"
+#include"bool_rewriter.h"
 
 namespace datalog {
 
         if (r) {
             SASSERT(r->m_ref_cnt>0);
             r->m_ref_cnt--;
-            if(r->m_ref_cnt==0) {
+            if (r->m_ref_cnt==0) {
                 r->deallocate(m);
             }
         }
         
         if (m_ctx.fix_unbound_vars()) {
             unsigned rule_cnt = rules.size();
-            for(unsigned i=0; i<rule_cnt; ++i) {
+            for (unsigned i=0; i<rule_cnt; ++i) {
                 rule_ref r(rules[i].get(), *this);
                 fix_unbound_vars(r, true);
-                if(r.get()!=rules[i].get()) {
+                if (r.get()!=rules[i].get()) {
                     rules[i] = r;
                 }
             }
         body.push_back(to_app(q));
         flatten_body(body);
         func_decl* body_pred = 0;
-        for(unsigned i = 0; i < body.size(); i++) {
+        for (unsigned i = 0; i < body.size(); i++) {
             if (is_uninterp(body[i].get())) {
                 body_pred = body[i]->get_decl();
                 break;
         qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
 
         expr_ref_vector qhead_args(m);
-        for(unsigned i = 0; i < vars.size(); i++) {
+        for (unsigned i = 0; i < vars.size(); i++) {
             qhead_args.push_back(m.mk_var(vars.size()-i-1, vars[i]));
         }
         app_ref qhead(m.mk_app(qpred, qhead_args.c_ptr()), m);
             bool  is_neg = (is_negated != 0 && is_negated[i]); 
             app * curr = tail[i];
 
-            if(is_neg && !is_predicate(curr)) {
+            if (is_neg && !is_predicate(curr)) {
                 curr = m.mk_not(curr);
                 is_neg = false;
             }
-            if(is_neg) {
+            if (is_neg) {
                 has_neg = true;
             }
             app * tail_entry = TAG(app *, curr, is_neg);
-            if(is_predicate(curr)) {
+            if (is_predicate(curr)) {
                 *uninterp_tail=tail_entry;
                 uninterp_tail++;
             }
 
         r->m_uninterp_cnt = static_cast<unsigned>(uninterp_tail - r->m_tail);
 
-        if(has_neg) {
+        if (has_neg) {
             //put negative predicates between positive and interpreted
             app * * it = r->m_tail;
             app * * end = r->m_tail + r->m_uninterp_cnt;
             while(it!=end) {
                 bool  is_neg = GET_TAG(*it)!=0;
-                if(is_neg) {
+                if (is_neg) {
                     --end;
                     std::swap(*it, *end);
                 }
 
     void rule_manager::fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination) {
 
-        if(r->get_uninterpreted_tail_size()==r->get_tail_size()) {
+        if (!m_ctx.fix_unbound_vars()) {
+            return;
+        }
+
+        if (r->get_uninterpreted_tail_size() == r->get_tail_size()) {
             //no interpreted tail to fix
             return;
         }
         unsigned t_len = r->get_tail_size();
         for (unsigned i = ut_len; i < t_len; i++) {
             app * t = r->get_tail(i);
-
             interp_vars.reset();
-
             ::get_free_vars(t, interp_vars);
-            //collect_vars(m, t, interp_vars);
-
             bool has_unbound = false;
             unsigned iv_size = interp_vars.size();
-            for(unsigned i=0; i<iv_size; i++) {
-                if(!interp_vars[i]) { continue; }
-                if(vctr.get(i)==0) {
+            for (unsigned i=0; i<iv_size; i++) {
+                if (!interp_vars[i]) { continue; }
+                if (vctr.get(i)==0) {
                     has_unbound = true;
                     unbound_vars.insert(i);
                 }
             return;
         }
         expr_ref unbound_tail(m);
-        switch(tails_with_unbound.size()) {
-        case 0: unbound_tail = m.mk_true(); break;
-        case 1: unbound_tail = tails_with_unbound[0].get(); break;
-        default: 
-            unbound_tail = m.mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr());
-            break;
-        }
+        bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
 
         unsigned q_var_cnt = unbound_vars.num_elems();
         unsigned max_var = m_var_counter.get_max_var(*r);
         qsorts.resize(q_var_cnt);
 
         unsigned q_idx = 0;
-        for(unsigned v = 0; v <= max_var; ++v) {
+        for (unsigned v = 0; v <= max_var; ++v) {
             sort * v_sort = free_rule_vars[v];
-            if(!v_sort) {
+            if (!v_sort) {
                 //this variable index is not used
                 continue;
             }
 
             unsigned new_idx;
-            if(unbound_vars.contains(v)) {
+            if (unbound_vars.contains(v)) {
                 new_idx = q_idx++;
                 qsorts.push_back(v_sort);
             }
             }
             subst.push_back(m.mk_var(new_idx, v_sort));
         }
-        SASSERT(q_idx==q_var_cnt);
+        SASSERT(q_idx == q_var_cnt);
 
         svector<symbol> qnames;
-        for(unsigned i=0; i<q_var_cnt; i++) {
+        for (unsigned i = 0; i < q_var_cnt; i++) {
             qnames.push_back(symbol(i));
         }
         //quantifiers take this reversed
         qsorts.reverse();
         qnames.reverse();
 
-        expr_ref unbound_tail_pre_quant(m);
+        expr_ref unbound_tail_pre_quant(m), fixed_tail(m), quant_tail(m);
 
         var_subst vs(m, false);
         vs(unbound_tail, subst.size(), subst.c_ptr(), unbound_tail_pre_quant);
 
-        expr_ref quant_tail(m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(),
-            unbound_tail_pre_quant), m);
-
-        expr_ref fixed_tail(m);
+        quant_tail = m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(), unbound_tail_pre_quant);
 
-        if(try_quantifier_elimination) {
+        if (try_quantifier_elimination) {
             TRACE("dl_rule_unbound_fix_pre_qe", 
                 tout<<"rule: ";
                 r->display(m_ctx, tout);
             tout<<"fixed tail: "<<mk_pp(fixed_tail, m)<<"\n";
         );
 
-        if(is_var(fixed_tail) || ::is_quantifier(fixed_tail)) {
+        if (is_var(fixed_tail) || ::is_quantifier(fixed_tail)) {
             fixed_tail = m.mk_eq(fixed_tail, m.mk_true());
         }
         SASSERT(is_app(fixed_tail));
 
-        if(!m.is_true(fixed_tail.get())) {
+        if (!m.is_true(fixed_tail.get())) {
             tail.push_back(to_app(fixed_tail.get()));
             tail_neg.push_back(false);
         }
     bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
         unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size();
         for (unsigned i = 0; i < len; i++) {
-            if(get_tail(i)->get_decl()==p) {
+            if (get_tail(i)->get_decl()==p) {
                 return true;
             }
         }
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
-            if(is_uninterp(n)) {
+            if (is_uninterp(n)) {
                 m_found = true;
                 m_func = n->get_decl();
             }
         unsigned sz = get_tail_size();
         uninterpreted_function_finder_proc proc;
         expr_mark visited;
-        for(unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
+        for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
             for_each_expr(proc, visited, get_tail(i));
         }
         return proc.found(f);
         quantifier_finder_proc() : m_exist(false), m_univ(false) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) {
-            if(n->is_forall()) {
+            if (n->is_forall()) {
                 m_univ = true;
             }
             else {
         unsigned sz = get_tail_size();
         quantifier_finder_proc proc;
         expr_mark visited;
-        for(unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
+        for (unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
             for_each_expr(proc, visited, get_tail(i));
         }
         existential = proc.m_exist;
 
         unsigned next_fresh_var = 0;
         expr_ref_vector subst_vals(m);
-        for(unsigned i=0; i<first_unsused; ++i) {
+        for (unsigned i=0; i<first_unsused; ++i) {
             sort* var_srt = used.contains(i);
-            if(var_srt) {
+            if (var_srt) {
                 subst_vals.push_back(m.mk_var(next_fresh_var++, var_srt));
             }
             else {
             if (is_neg_tail(i))
                 out << "not ";
             app * t = get_tail(i);
-            if(ctx.get_rule_manager().is_predicate(t)) {
+            if (ctx.get_rule_manager().is_predicate(t)) {
                 output_predicate(ctx, t, out);
             }
             else {
             }
         }
         out << '.';
-        if(ctx.output_profile()) {
+        if (ctx.output_profile()) {
             out << " {";
             output_profile(ctx, out);
             out << '}';
     }
 
     bool rule_eq_proc::operator()(const rule * r1, const rule * r2) const {
-        if(r1->get_head()!=r2->get_head()) { return false; }
+        if (r1->get_head()!=r2->get_head()) { return false; }
         unsigned tail_len = r1->get_tail_size();
-        if(r2->get_tail_size()!=tail_len) {
+        if (r2->get_tail_size()!=tail_len) {
             return false;
         }
-        for(unsigned i=0; i<tail_len; ++i) {
-            if(r1->get_tail(i)!=r2->get_tail(i)) {
+        for (unsigned i=0; i<tail_len; ++i) {
+            if (r1->get_tail(i)!=r2->get_tail(i)) {
                 return false;
             }
-            if(r1->is_neg_tail(i)!=r2->is_neg_tail(i)) {
+            if (r1->is_neg_tail(i)!=r2->is_neg_tail(i)) {
                 return false;
             }
         }
     unsigned rule::hash() const {
         unsigned res = get_head()->hash();
         unsigned tail_len = get_tail_size();
-        for(unsigned i=0; i<tail_len; ++i) {
+        for (unsigned i=0; i<tail_len; ++i) {
             res = combine_hash(res, combine_hash(get_tail(i)->hash(), is_neg_tail(i)));
         }
         return res;

src/muz_qe/dl_util.cpp

 
     void del_rule(horn_subsume_model_converter* mc, rule& r) {
         if (mc) {
-            // app* head = r.get_head();
             ast_manager& m = mc->get_manager();
             expr_ref_vector body(m);
             for (unsigned i = 0; i < r.get_tail_size(); ++i) {

src/muz_qe/horn_subsume_model_converter.cpp

         m_rewrite(body_res);
         
     }
-    TRACE("dl",
+    TRACE("mc",
           tout << mk_pp(head, m) << " :- " << mk_pp(body, m) << "\n";
           tout << pred->get_name() << " :- " << mk_pp(body_res.get(), m) << "\n";);
 
     if (m.is_bool(n) && 
         !m_md->has_interpretation(n->get_decl()) &&
         (n->get_family_id() == null_family_id)) {
-        TRACE("dl_mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
+        TRACE("mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
         if (n->get_decl()->get_arity() == 0) {
             m_md->register_decl(n->get_decl(), m.mk_false());
         }
 
 
 void horn_subsume_model_converter::operator()(model_ref& mr) {
-    TRACE("dl_mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
+    TRACE("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();
         add_default_false_interpretation(body, mr);
         SASSERT(m.is_bool(body));
                 
-        TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
+        TRACE("mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
         expr_ref tmp(body);
         mr->eval(tmp, body);
         
-        TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
+        TRACE("mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
                 
         if (arity == 0) {
             expr* e = mr->get_const_interp(h);

src/muz_qe/pdr_context.cpp

 #include "ast_smt2_pp.h"
 #include "qe_lite.h"
 #include "ast_ll_pp.h"
+#include "proof_checker.h"
 
 namespace pdr {
 
             proof_ref pr = get_proof();
             proof_checker checker(m);
             expr_ref_vector side_conditions(m);
-            bool ok = check(pr, side_conditions);
+            bool ok = checker.check(pr, side_conditions);
             if (!ok) {
                 IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
             }

src/muz_qe/pdr_interpolant_provider.cpp

     }
 
     front_end_params dummy_params;
-    cmd_context cctx(dummy_params, false, &m);
+    cmd_context cctx(&dummy_params, false, &m);
     for_each_expr(used_symbol_inserter(cctx), f1);
 
     parse_smt2_commands(cctx, std::istringstream(res_text), false);

src/muz_qe/qe.cpp

 
         void propagate_assignment(model_evaluator& model_eval) {
             if (m_fml) {
-                /* update_status st = */ update_current(model_eval, true);
+                update_current(model_eval, true);
             }
         }
 

src/muz_qe/qe_lite.cpp

     impl(ast_manager& m): m(m), m_der(m) {}
     
     void operator()(app_ref_vector& vars, expr_ref& fml) {
+        if (vars.empty()) {
+            return;
+        }
         expr_ref tmp(fml);
         quantifier_ref q(m);
         proof_ref pr(m);     

src/smt/theory_diff_logic_def.h

     inc_conflicts();
     literal_vector const& lits = m_nc_functor.get_lits();
     context & ctx = get_context();
-    // region& r = ctx.get_region();
     TRACE("arith_conflict", 
           //display(tout);
           tout << "conflict: ";

src/util/diff_logic.h

         for (unsigned i = 0; i < edges.size(); ++i) {
             
             potential0 += m_edges[edges[i]].get_weight();
-            // numeral potential1 = potentials[i];
             if (potential0 != potentials[i] || 
                 nodes[i] != m_edges[edges[i]].get_source()) {
                 TRACE("diff_logic_traverse", tout << "checking index " << i << " ";