Logo Search packages:      
Sourcecode: undertaker version File versions  Download package

std::list< SatChecker::AssignmentMap > CodeSatStream::blockCoverage ( ConfigurationModel model,
MissingSet &  missingSet 
)

Check for configuration coverage.

This method tries finds a set of configurations so that each and every block (excluding dead blocks) is selected at least once.

Parameters:
modelIf not NULL, take the constraints of the goven model into account

Definition at line 256 of file CodeSatStream.cpp.

References ModelContainer::getMainModel().

                                                                                                               {
    std::set<std::string>::iterator i;
    std::set<std::string> blocks_set;
    std::list<SatChecker::AssignmentMap> ret;
    std::set<SatChecker::AssignmentMap> found_solutions;

    StringList empty;
    StringList &sl = empty;

    if (model) {
        const std::string magic("ALWAYS_ON");
        RsfMap::const_iterator j = model->find(magic);
        if (j != model->end()) {
            sl = (*j).second;
            std::cout << "I: " << sl.size() << " Items have been forcefully set" << std::endl;
        }

    }

    try {
      for(i = _blocks.begin(); i != _blocks.end(); ++i) {
            StringJoiner formula;
            SatChecker::AssignmentMap current_solution;

            formula.push_back((*i));
            formula.push_back(getCodeConstraints());
            if (model)
                formula.push_back(getKconfigConstraints(model, missingSet));

            for (MissingSet::iterator it = missingSet.begin(); it != missingSet.end(); it++)
                formula.push_back("!" + (*it));

            std::string main_arch(ModelContainer::getMainModel());
            if (main_arch.size() > 0) {
                // stolen from http://www.codepedia.com/1/CppToUpperCase
                // explicit cast needed to resolve ambiguity
                std::transform(main_arch.begin(), main_arch.end(), main_arch.begin(),
                               (int(*)(int))std::toupper);
                formula.push_back("CONFIG_" + main_arch);
            }

            for (StringList::const_iterator sli=sl.begin(); sli != sl.end(); ++sli) {
                formula.push_back(*sli);
            }

          if (blocks_set.find(*i) == blocks_set.end()) {
                /* does the new contributes to the set of configurations? */
                bool new_solution = false;
                SatChecker sc(formula.join("\n&&\n"));

                // unsolvable, i.e. we have found some defect!
                if (!sc())
                    continue;

                const SatChecker::AssignmentMap &assignments = sc.getAssignment();
                SatChecker::AssignmentMap::const_iterator it;
                for (it = assignments.begin(); it != assignments.end(); it++) {
                    static const boost::regex item_regexp("^CONFIG_(.*)$", boost::regex::perl);
                    static const boost::regex block_regexp("^B\\d+$", boost::regex::perl);

                    if (boost::regex_match((*it).first, item_regexp)) {
                        current_solution.insert(std::make_pair<std::string,bool>((*it).first, (*it).second));
                        continue;
                    }

                    if ((*it).second && boost::regex_match((*it).first, block_regexp)) {
                        blocks_set.insert((*it).first);
                        new_solution = true;
                    }
                }

                if (found_solutions.find(current_solution) == found_solutions.end()) {
                    found_solutions.insert(current_solution);

                    if (new_solution)
                        ret.push_back(assignments);
                }
            }
        }
    } catch (SatCheckerError &e) {
        std::cerr << "Couldn't process " << _filename << ": "
                  << e.what() << std::endl;
    }
    return ret;
}

Here is the call graph for this function:


Generated by  Doxygen 1.6.0   Back to index