*scratch*

QCNFClauseList propagate_literal(const QCNFLiteral& lit, const QCNFClause& c) {
    LOG_PRINT(LOG_DEBUG) << "propagate_literal called with lit=" << lit.first->toString()
			        << " and clause c=" << convertFromQCNFClause(c).toString() << std::endl;
    boost::shared_ptr<Sentence> cnfLit = lit.first;
    // first figure out what kind of literal we have here.
    std::queue<QCNFClause> toProcess;
    QCNFClauseList processed;

    toProcess.push(c);
    while (!toProcess.empty()) {
        QCNFClause qClause = toProcess.front();
        LOG_PRINT(LOG_DEBUG) << "working on " << convertFromQCNFClause(qClause).toString() << std::endl;
        CNFClause cClause = qClause.first;
        toProcess.pop();
        bool addCurrentClause = true;
        if (isSimpleLiteral(cnfLit)) {
            // search for an occurrence of this atom in c
            CNFClause::iterator it = cClause.begin();
            while (it != cClause.end()) {
                boost::shared_ptr<Sentence> currentLit = *it;
                if (isSimpleLiteral(currentLit) && *cnfLit == *currentLit) {	// Propagating P into P
                  popPIntoP(); // could these be methods on the cClause or the literal?
                } else if (isSimpleLiteral(currentLit) && isNegatedLiteral(currentLit, cnfLit)) {
                  propNotPIntoP();// could these be methods on the cClause or the literal?
                } else if (boost::dynamic_pointer_cast<LiquidOp>(currentLit) != 0) {	
                  propPIntoList();// could these be methods on the cClause or the literal?
                } else if (boost::dynamic_pointer_cast<DiamondOp>(currentLit) != 0) {
                  doSomeUndocumentedShit()// could these be methods on the cClause or the literal?
                }
                it++;
            }
        }
        if (addCurrentClause) processed.push_back(qClause);

    }
    LOG_PRINT(LOG_DEBUG) << "returning..." << std::endl;
    return processed;
}