import edu.neu.ccs.demeterf.IDb;

/**
 * This class implements the Shannon Decomposition for a given formula.
 * It will reduce the
 * formula based on a literal.
 */
class CNFReducer extends IDb{
    // I (BC) Don't like these side-effects, but it's ok
    //  since the type/method matching is shallow, there's
    //  not really an easier way to do it
    int sat = 0, 
        unsat = 0;


    // These can all go away if we make these 'BuilIn's
    Weight combine(Weight w){ return w; }
    Variable combine(Variable v){ return v; }
    LiteralList combine(LiteralEmpty emp){ return emp; }
    ClauseEmpty combine(ClauseEmpty cls){ return cls; }


    // Reduce a Single Literal to:
    //   True, False, or the original Literal
    Literal combine(Literal l, Object o, Literal arg) {
        if (l.sameVarAs(arg)){
            if (l.sameSignAs(arg))
                return new TrueLit();
            return new FalseLit();
        }
        return l;
    }
    

    // Cover the cases of a single Literal Reduction
    Literals combine (LiteralCons lst, TrueLit res, LiteralList rest){
        return new SatLiteral();
    }
    Literals combine (LiteralCons lst, FalseLit res, LiteralList rest){
        return rest;
    }
    Literals combine (LiteralCons lst, Literal res, LiteralList rest){
        return new LiteralCons(res, rest);
    }

    // This LiteralList is already Satisfied
    Literals combine (LiteralCons lst, Literal res, SatLiteral sat){
        return sat;
    }


    // Cover the cases of a 'Literals' reduction
    Clause combine(Clause cls, Weight w, SatLiteral l){
        sat += w.get_v();
        return new SatClause();
    }
    Clause combine(Clause cls, Weight w, LiteralEmpty l){
        unsat += w.get_v();
        return new UnsatClause();
    }
    Clause combine(Clause cls, Weight w, LiteralCons l){
        return new ConcreteClause(w,l);
    }
    

    // Ignore Clauses that are not Concrete (Sat or Unsat)
    ClauseList combine(ClauseCons cons, Object cl, ClauseList rest){
        return rest;
    }
    ClauseList combine(ClauseCons cons, ConcreteClause cl, ClauseList rest){
        return new ClauseCons(cl,rest);
    }


    // Track Sat and Unsat counts
    Integer combine(SatAbsent sa){ return sat; }
    Integer combine(UnsatAbsent ua){ return unsat; }
    Integer combine(SatCount sa, Integer cnt){ return cnt+sat; }
    Integer combine(UnsatCount ua, Integer cnt){ return cnt+unsat; }

    // Re-package the Clauses and Counts into a Formula
    Formula combine(Formula form, ClauseList cl, Integer osat, Integer ounsat){
        return new Formula(cl, new SatCount(osat), new UnsatCount(ounsat));
    }
}