00001 package edu.tum.cs.logic;
00002
00003 import java.util.Collection;
00004 import java.util.HashMap;
00005 import java.util.Map;
00006 import java.util.Vector;
00007
00008 import edu.tum.cs.srl.Database;
00009 import edu.tum.cs.util.StringTool;
00010
00011 public class ForAll extends UngroundedFormula {
00012 Formula f;
00013 Collection<String> vars;
00017 Map<String, String> var2domName;
00018
00019 public ForAll(Collection<String> vars, Formula f) {
00020 this.vars = vars;
00021 this.f = f;
00022 this.var2domName = new HashMap<String, String>();
00023 }
00024
00025 public String toString() {
00026 return "FORALL " + StringTool.join(",", vars) + " (" + f.toString() + ")";
00027 }
00028
00029 @Override
00030 public void getVariables(Database db, Map<String, String> ret) throws Exception {
00031 f.getVariables(db, ret);
00032 for(String var : vars) {
00033 var2domName.put(var, ret.remove(var));
00034 }
00035 }
00036
00037 @Override
00038 public Formula ground(Map<String, String> binding, WorldVariables worldVars, Database db) throws Exception {
00039
00040 if(var2domName.size() < vars.size()) {
00041 this.getVariables(db, new HashMap<String, String>());
00042 }
00043
00044 Vector<Formula> parts = new Vector<Formula>();
00045 f.generateGroundings(parts, db, binding, vars.toArray(new String[vars.size()]), 0, var2domName, worldVars, false);
00046 return new Conjunction(parts);
00047 }
00048
00049 @Override
00050 public Formula toCNF() {
00051 throw new RuntimeException("Cannot convert ungrounded formula to CNF.");
00052 }
00053
00054 @Override
00055 public Formula toNNF() {
00056 throw new RuntimeException("Cannot convert ungrounded formula to NNF.");
00057 }
00058 }