/// \brief Computes the first set for the specified rule (or retrieves the cached version)
item_set grammar::first_for_rule(const rule& rule) const {
    // Return a set containing only the empty item if the rule is 0 items long
    if (rule.items().size() == 0) {
        return *m_EpsilonSet;
    }
    
    // Return the first set of the first item in the rule
    item_set result(this);
    for (size_t itemId = 0; itemId < rule.items().size(); ++itemId) {
        // Remove the epsilon item from the set
        result.erase(an_empty_item_c);

        // Add the items in the first set for this item
        result.merge(first(*rule.items()[itemId]));

        // If the result doesn't contain the empty item, then return it
        if (!result.contains(an_empty_item_c)) {
            return result;
        }
    }

    // The empty item is included
    result.insert(an_empty_item_c);
    return result;
}

  write_broadcast_distribution_table_grammar() : write_broadcast_distribution_table_grammar::base_type(
      write_broadcast_distribution_table_rule) {

    write_broadcast_distribution_table_rule = broadcast_distribution_table_rule << unused_grammar_;
    broadcast_distribution_table_rule = broadcast_distribution_table_grammar_;

    write_broadcast_distribution_table_rule.name("write_broadcast_distribution_table_rule");
    broadcast_distribution_table_rule.name("broadcast_distribution_table_rule");
  }

 unsigned var_counter::get_max_var(const rule & r) {
     m_todo.push_back(r.get_head());
     m_scopes.push_back(0);
     unsigned n = r.get_tail_size();
     bool has_var = false;
     for (unsigned i = 0; i < n; i++) {
         m_todo.push_back(r.get_tail(i));
         m_scopes.push_back(0);
     }
     return get_max_var(has_var);
 }

// decomposes a rule (A -> B C D E ...) into the rules (A -> B#C#D E), (B#C#D -> B#C D), (B#C -> B C), ... respectively.
// might expand 'nonterminals'
// might rewrite 'rule_to_decompose'
void decompose(rule &rule_to_decompose, set<string> &nonterminals, rules &decomposed_rules) {
	string temp;
	if (rule_to_decompose.size() == 2) {
		if (is_in(rule_to_decompose[1], nonterminals)) {
			cerr << " ERROR : irregular occurence of chain rule (i.e. A -> B)! - ignored " << '\n';
			return;
		} else
			decomposed_rules.insert(rule_to_decompose);
	} else {
		for (size_t i = 1; i<rule_to_decompose.size();++i)
			if (!is_in(rule_to_decompose[i], nonterminals)) {
				temp = "#" + rule_to_decompose[i];
				nonterminals.insert(temp);
				decomposed_rules.insert(rule{ temp, rule_to_decompose[i] });
				replace(rule_to_decompose.begin() + i, rule_to_decompose.end(), rule_to_decompose[i], temp);
			}
		while(rule_to_decompose.size() > 3) {
			temp = rule_to_decompose[1] + "#" + rule_to_decompose[2];
			nonterminals.insert(temp);
			decomposed_rules.insert(rule{ temp, rule_to_decompose[1], rule_to_decompose[2] });
			rule_to_decompose[1] = temp;
			rule_to_decompose.erase(rule_to_decompose.begin() + 2);
		}
		decomposed_rules.insert(rule_to_decompose);
	}
}

  void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest)
  {
    //Reset everything
    selects.reset();
    eq_classes.reset();
    cnt = src_manager->get_counter().get_max_rule_var(r)+1;
    done_selects.reset();
    ownership.reset();

    expr_ref_vector phi(m);
    expr_ref_vector preds(m);
    expr_ref new_head = create_head(to_app(r.get_head()));
    unsigned nb_predicates = r.get_uninterpreted_tail_size();
    unsigned tail_size = r.get_tail_size();
    for(unsigned i=0;i<nb_predicates;i++)
    {
      preds.push_back(r.get_tail(i));
    }
    for(unsigned i=nb_predicates;i<tail_size;i++)
    {
      phi.push_back(r.get_tail(i));
    }

    //Retrieve selects
    for(unsigned i=0;i<phi.size();i++)
      retrieve_selects(phi[i].get());

    //Rewrite the predicates
    expr_ref_vector new_tail(m);
    for(unsigned i=0;i<preds.size();i++)
    {
      new_tail.append(instantiate_pred(to_app(preds[i].get())));
    }
    new_tail.append(phi);
    for(obj_map<expr, var*>::iterator it = done_selects.begin(); it!=done_selects.end(); ++it)
    {
      expr_ref tmp(m);
      tmp = &it->get_key();
      new_tail.push_back(m.mk_eq(it->get_value(), tmp));
    }
    proof_ref pr(m);
    src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name());
  }

 void mk_unfold::expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst) {
     SASSERT(tail_idx <= r.get_uninterpreted_tail_size());
     if (tail_idx == r.get_uninterpreted_tail_size()) {
         dst.add_rule(&r);
     }
     else {
         func_decl* p = r.get_decl(tail_idx);
         rule_vector const& p_rules = src.get_predicate_rules(p);
         rule_ref new_rule(rm);
         for (unsigned i = 0; i < p_rules.size(); ++i) {
             rule const& r2 = *p_rules[i];
             if (m_unify.unify_rules(r, tail_idx, r2) &&
                 m_unify.apply(r, tail_idx, r2, new_rule)) {
                 expr_ref_vector s1 = m_unify.get_rule_subst(r, true);
                 expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);                    
                 resolve_rule(rm, r, r2, tail_idx, s1, s2, *new_rule.get());
                 expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst);
             }
         }
     }
 }

    void debug(rule<Iterator, T1, T2, T3, T4>& r, F f)
    {
        typedef rule<Iterator, T1, T2, T3, T4> rule_type;

        typedef
            debug_handler<
                Iterator
              , typename rule_type::context_type
              , typename rule_type::skipper_type
              , F>
        debug_handler;
        r.f = debug_handler(r.f, f, r.name());
    }

/// \brief Updates the follow set cache using the content of a particular rule
void grammar::fill_follow(const rule& rule, item_map<item_set>::type& dependencies) const {
    // Empty rules don't change the follow set for anything
    if (rule.items().size() == 0) return;
    
    // Iterate through the items in this rule
    for (size_t pos=0; pos<rule.items().size(); ++pos) {
        // Get the current item
        const item_container& thisItem = rule.items()[pos];
        
        // Terminal items aren't processed by this call (we don't bother to generate follow sets for them)
        if (thisItem->type() == item::terminal) continue;
        
        // Retrieve the follow set for this item
        item_set_map::iterator followSet = m_CachedFollowSets.find(thisItem);
        if (followSet == m_CachedFollowSets.end()) {
            followSet = m_CachedFollowSets.insert(item_set_map::value_type(thisItem, item_set(this))).first;
        }
        
        // The follow set of this item is the combination of the first sets for all of the following items
        // If it's at the end, it also includes the follow set for the nonterminal for this rule
        size_t nextPos = pos+1;
        for (;nextPos < rule.items().size(); ++nextPos) {
            // Get this following item
            const item_container& followingItem = rule.items()[nextPos];
            
            // Get the set FIRST(followingItem)
            const item_set& firstSet = first(followingItem);
            
            // Add to the follow set
            followSet->second.merge(firstSet);
            
            // Finished if the first set doesn't include the empty set
            if (!firstSet.contains(an_empty_item_c)) break;
        }
        
        // If we reach the end, then we need to include FOLLOW(rule.nonterminal) in the set for FOLLOW(thisItem)
        if (nextPos >= rule.items().size()) {
            item_set_map::iterator depend = dependencies.find(thisItem);
            if (depend == dependencies.end()) {
                depend = dependencies.insert(item_map<item_set>::type::value_type(thisItem, item_set(this))).first;
            }
            
            depend->second.insert(rule.nonterminal());
        }
        
        // If this item is an EBNF rule, then we need to process each of its children
        const ebnf* ebnfItem = thisItem->cast_ebnf();
        if (ebnfItem) {
            for (ebnf::rule_iterator subRule = ebnfItem->first_rule(); subRule != ebnfItem->last_rule(); ++subRule) {
                fill_follow(**subRule, dependencies);
            }
        }
    }
}

    void debug(rule<Iterator, T0, T1, T2>& r)
    {
        typedef rule<Iterator, T0, T1, T2> rule_type;

        typedef
            debug_handler<
                Iterator
              , typename rule_type::context_type
              , typename rule_type::skipper_type
              , simple_trace>
        debug_handler;
        r.f = debug_handler(r.f, simple_trace(), r.name());
    }

    void debug(rule<OutputIterator, T1, T2, T3, T4>& r, F f)
    {
        typedef rule<OutputIterator, T1, T2, T3, T4> rule_type;

        typedef
            debug_handler<
                OutputIterator
              , typename rule_type::context_type
              , typename rule_type::delimiter_type
              , typename rule_type::properties
              , F>
        debug_handler;
        r.f = debug_handler(r.f, f, r.name());
    }

 bool mk_coalesce::same_body(rule const& r1, rule const& r2) const {
     SASSERT(r1.get_decl() == r2.get_decl());
     unsigned sz = r1.get_uninterpreted_tail_size();
     if (sz != r2.get_uninterpreted_tail_size()) {
         return false;
     }
     for (unsigned i = 0; i < sz; ++i) {
         if (r1.get_decl(i) != r2.get_decl(i)) {
             return false;
         }
         if (r1.is_neg_tail(i) != r2.is_neg_tail(i)) {
             return false;
         }
     }
     return true;
 }    

    void resolve_rule(replace_proof_converter* pc, rule& r1, rule& r2, unsigned idx, 
                      expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
        if (!pc) return;
        ast_manager& m = s1.get_manager();
        dl_decl_util util(m);
        expr_ref fml1(m), fml2(m), fml3(m);
        r1.to_formula(fml1);
        r2.to_formula(fml2);
        res.to_formula(fml3);
        vector<expr_ref_vector> substs;
        svector<std::pair<unsigned, unsigned> > positions;
        substs.push_back(s1);
        substs.push_back(s2);

        scoped_coarse_proof _sc(m);
        proof_ref pr(m);
        proof_ref_vector premises(m);
        premises.push_back(m.mk_asserted(fml1));
        premises.push_back(m.mk_asserted(fml2));
        positions.push_back(std::make_pair(idx+1, 0));

        TRACE("dl", 
              tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
              tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";); 

 void mk_coalesce::extract_conjs(expr_ref_vector const& sub, rule const& rl, expr_ref& result) {
     obj_map<expr, unsigned> indices;
     bool_rewriter bwr(m);
     rule_ref r(const_cast<rule*>(&rl), rm);
     ptr_vector<sort> sorts;
     expr_ref_vector revsub(m), conjs(m);
     rl.get_vars(sorts);
     revsub.resize(sorts.size());  
     svector<bool> valid(sorts.size(), true);
     for (unsigned i = 0; i < sub.size(); ++i) {
         expr* e = sub[i];
         sort* s = m.get_sort(e);
         expr_ref w(m.mk_var(i, s), m);
         if (is_var(e)) {
             unsigned v = to_var(e)->get_idx();
             SASSERT(v < valid.size());
             if (sorts[v]) {
                 SASSERT(s == sorts[v]);
                 if (valid[v]) {
                     revsub[v] = w;
                     valid[v] = false;
                 }
                 else {
                     SASSERT(revsub[v].get());
                     SASSERT(m.get_sort(revsub[v].get()) == s);
                     conjs.push_back(m.mk_eq(revsub[v].get(), w));    
                 }
             }
         }
         else {
             SASSERT(m.is_value(e));
             SASSERT(m.get_sort(e) == m.get_sort(w));
             conjs.push_back(m.mk_eq(e, w));
         }
     }
     for (unsigned i = 0; i < sorts.size(); ++i) {
         if (valid[i] && sorts[i] && !revsub[i].get()) {
             revsub[i] = m.mk_var(m_idx++, sorts[i]);
         }
     }
     var_subst vs(m, false);
     for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) {
         vs(r->get_tail(i), revsub.size(), revsub.c_ptr(), result);
         conjs.push_back(result);
     }
     bwr.mk_and(conjs.size(), conjs.c_ptr(), result);
 }

    void mk_coalesce::merge_rules(rule_ref& tgt, rule const& src) {
        SASSERT(same_body(*tgt.get(), src));
        m_sub1.reset();
        m_sub2.reset();
        m_idx = 0;
        app_ref pred(m), head(m);
        expr_ref fml1(m), fml2(m), fml(m);
        app_ref_vector tail(m);
        ptr_vector<sort> sorts1, sorts2;
        expr_ref_vector conjs1(m), conjs(m);
        rule_ref res(rm);
        bool_rewriter bwr(m);
        svector<bool> is_neg;
        tgt->get_vars(sorts1);
        src.get_vars(sorts2);

        mk_pred(head, src.get_head(), tgt->get_head()); 
        for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {
            mk_pred(pred, src.get_tail(i), tgt->get_tail(i));
            tail.push_back(pred);
            is_neg.push_back(src.is_neg_tail(i));
        }           
        extract_conjs(m_sub1, src, fml1);
        extract_conjs(m_sub2, *tgt.get(),  fml2);
        bwr.mk_or(fml1, fml2, fml);
        SASSERT(is_app(fml));
        tail.push_back(to_app(fml));
        is_neg.push_back(false);
        res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
        if (m_ctx.generate_proof_trace()) {
            src.to_formula(fml1);
            tgt->to_formula(fml2);
            res->to_formula(fml);
#if 0
            sort* ps = m.mk_proof_sort();
            sort* domain[3] = { ps, ps, m.mk_bool_sort() };
            func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps);  // TBD: ad-hoc proof rule
            expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml };
            // ...m_pc->insert(m.mk_app(merge, 3, args));
#else
            svector<std::pair<unsigned, unsigned> > pos;
            vector<expr_ref_vector> substs;
            proof* p = src.get_proof();
            p = m.mk_hyper_resolve(1, &p, fml, pos, substs);
            res->set_proof(m, p);
#endif
        }
        tgt = res;
    }

  frame_grammar() : frame_grammar::base_type(possible_frame_rule){

    possible_frame_rule  = confirmed_request_grammar_
                         | unconfirmed_request_grammar_
                         | simple_ack_grammar_
                         | complex_ack_grammar_
                         | segment_ack_grammar_
                         | error_grammar_
                         | reject_grammar_
                         | abort_grammar_
                         | eps;

    possible_frame_rule.name("possible_frame_rule");

    /*
       debug(possible_frame_rule);
     */
  }

 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) {
             if (r.is_neg_tail(i)) {
                 body.push_back(m.mk_not(r.get_tail(i)));
             }
             else {
                 body.push_back(r.get_tail(i));
             }
         }
         mc->insert(r.get_head(), body.size(), body.c_ptr());
     }
 }

bool context::check_subsumes(rule const& stronger_rule, rule const& weaker_rule) {
    if (stronger_rule.get_head() != weaker_rule.get_head()) {
        return false;
    }
    for (unsigned i = 0; i < stronger_rule.get_tail_size(); ++i) {
        app* t = stronger_rule.get_tail(i);
        bool found = false;
        for (unsigned j = 0; j < weaker_rule.get_tail_size(); ++j) {
            app* s = weaker_rule.get_tail(j);
            if (s == t) {
                found = true;
                break;
            }
        }
        if (!found) {
            return false;
        }
    }
    return true;
}