WeightedClausalKB.java

Go to the documentation of this file.

package edu.tum.cs.logic.sat.weighted;

import java.util.HashMap;
import java.util.Iterator;
import java.util.Set;
import java.util.Vector;
import java.util.Map.Entry;

import edu.tum.cs.logic.Conjunction;
import edu.tum.cs.logic.Formula;
import edu.tum.cs.logic.TrueFalse;
import edu.tum.cs.logic.sat.Clause.TautologyException;

public class WeightedClausalKB implements Iterable<WeightedClause> {

    protected Vector<WeightedClause> clauses;
    protected HashMap<WeightedClause, Formula> cl2Formula;
    protected edu.tum.cs.util.datastruct.Map2List<WeightedFormula, WeightedClause> formula2clauses;

    public WeightedClausalKB(Iterable<WeightedFormula> kb, boolean requirePositiveWeights) throws Exception {
        this();
        for(WeightedFormula wf : kb) {
            addFormula(wf, requirePositiveWeights);
        }
    }
    
    public WeightedClausalKB() {
        clauses = new Vector<WeightedClause>();
        cl2Formula = new HashMap<WeightedClause, Formula>();
        formula2clauses = new edu.tum.cs.util.datastruct.Map2List<WeightedFormula, WeightedClause>();           
    }
   
    public void addFormula(WeightedFormula wf, boolean makeWeightPositive) throws Exception {
        if(makeWeightPositive && wf.weight < 0) {
                wf.weight *= -1;
                wf.formula = new edu.tum.cs.logic.Negation(wf.formula);
        }
        // convert formula to CNF
        Formula cnf = wf.formula.toCNF();
        // add its clauses
        if(cnf instanceof Conjunction) { // conjunction of clauses
            Conjunction c = (Conjunction) cnf;
            int numChildren = c.children.length;
            for(Formula child : c.children) {
                try {
                        addClause(wf, new WeightedClause(child, wf.weight / numChildren, wf.isHard));
                }
                catch(TautologyException e) {}
            }
        } 
        else if(!(cnf instanceof TrueFalse)) { // clause
            try {
                addClause(wf, new WeightedClause(cnf, wf.weight, wf.isHard));
            }
            catch(TautologyException e) {}
        }
    }
    
    public void addClause(WeightedFormula wf, WeightedClause wc) {
        cl2Formula.put(wc, wf.formula);
        clauses.add(wc);
        formula2clauses.add(wf, wc);
    }
    
    public void addClause(WeightedClause wc) {
        addClause(new WeightedFormula(wc, wc.weight, wc.isHard), wc);
    }

    public Iterator<WeightedClause> iterator() {
        return clauses.iterator();
    }

    public int size() {
        return clauses.size();
    }

    public void print() {
        int i = 0;
        for (WeightedClause c : this)
            System.out.printf("%4d  %s\n", ++i, c.toString());
    }

    public HashMap<WeightedClause, Formula> getClause2Formula() {
        return cl2Formula;
    }

    public Set<Entry<WeightedFormula,Vector<WeightedClause>>> getFormulasAndClauses() {
        return formula2clauses.entrySet();
    }
}

---

srldb
Author(s): Dominik Jain, Stefan Waldherr, Moritz Tenorth
autogenerated on Fri Jan 11 09:58:30 2013