| 1 | package tuffy.infer.ds; |
| 2 | |
| 3 | import java.sql.Array; |
| 4 | import java.sql.ResultSet; |
| 5 | import java.util.ArrayList; |
| 6 | import java.util.HashMap; |
| 7 | |
| 8 | import tuffy.util.Config; |
| 9 | import tuffy.util.ExceptionMan; |
| 10 | import tuffy.util.ProbMan; |
| 11 | /** |
| 12 | * A ground clause. |
| 13 | * |
| 14 | */ |
| 15 | public class GClause { |
| 16 | |
| 17 | /** |
| 18 | * ID of this GClause. |
| 19 | */ |
| 20 | public int id; |
| 21 | |
| 22 | /** |
| 23 | * Weight of this GClause. |
| 24 | */ |
| 25 | public double weight = 0; |
| 26 | |
| 27 | /** |
| 28 | * List of literals in this grounded clause. This |
| 29 | * is from $lits$ attribute in {@link Config#relClauses} |
| 30 | * table. |
| 31 | */ |
| 32 | public int[] lits = null; |
| 33 | |
| 34 | /** |
| 35 | * List of original clauses used to generate this |
| 36 | * grounded clause. This is from $fcid$ attribute |
| 37 | * in the clause table when |
| 38 | * {@link Config#track_clause_provenance} set to true. |
| 39 | */ |
| 40 | public int[] fcid = null; // list of id to fo clauses collectivley generating this gclause |
| 41 | |
| 42 | /** |
| 43 | * Finer-grained clause origin. |
| 44 | * Similar to {@link GClause#fcid}, corresponding to |
| 45 | * attribute $ffcid$ in {@link Config#relClauses} table. |
| 46 | */ |
| 47 | public String[] ffcid = null; |
| 48 | |
| 49 | /** |
| 50 | * Number of satisfied literals in this GClause. This |
| 51 | * GClause is true iff. nsat > 0. |
| 52 | */ |
| 53 | public int nsat = 0; |
| 54 | |
| 55 | /** |
| 56 | * Whether this clause should be ignored while SampleSAT. |
| 57 | * Used by MC-SAT. |
| 58 | */ |
| 59 | public boolean dead = false; |
| 60 | |
| 61 | |
| 62 | /** |
| 63 | * The largest fcid seen when parsing the database for all GClause. |
| 64 | */ |
| 65 | public static int maxFCID = -1; |
| 66 | |
| 67 | /** |
| 68 | * Return whether this clause is a positive clause. Here by |
| 69 | * positive it means this clause has a positive weight. |
| 70 | */ |
| 71 | public boolean isPositiveClause(){ |
| 72 | return weight >= 0; |
| 73 | } |
| 74 | |
| 75 | /** |
| 76 | * Return whether this clause is a hard clause. Here by hard |
| 77 | * it means this clause has a weight larger than {@link Config#hard_weight}, |
| 78 | * which means this clause must be satisfied in reasoning result. |
| 79 | */ |
| 80 | public boolean isHardClause(){ |
| 81 | return Math.abs(weight) >= Config.hard_weight; |
| 82 | } |
| 83 | |
| 84 | /** |
| 85 | * |
| 86 | * Return true if this clause is not set to ``dead''. This is used |
| 87 | * in MCSAT. |
| 88 | */ |
| 89 | public boolean selectMCSAT(){ |
| 90 | if(cost() > 0) return false; |
| 91 | double r = ProbMan.nextDouble(); |
| 92 | return r < (1 - Math.exp(-Math.abs((weight)) * Config.mcsat_sample_para)); |
| 93 | } |
| 94 | |
| 95 | /** |
| 96 | * Return the cost for violating this GClause. For positive |
| 97 | * clause, if it is violated, cost equals to weight. |
| 98 | * For negative clause, if it is satisfied, cost equals to |
| 99 | * -weight. Otherwise, return 0. |
| 100 | */ |
| 101 | public double cost(){ |
| 102 | if(weight > 0 && nsat == 0){ |
| 103 | return weight; |
| 104 | } |
| 105 | if(weight < 0 && nsat > 0){ |
| 106 | return -weight; |
| 107 | } |
| 108 | return 0; |
| 109 | } |
| 110 | |
| 111 | /** |
| 112 | * Returns +/-1 if this GClause contains this atom; 0 if not. |
| 113 | * If -1, then the atom in this clause is with negative sense. |
| 114 | * @param atom |
| 115 | */ |
| 116 | public int linkType(int atom){ |
| 117 | for(int l : lits){ |
| 118 | if(l==atom) return 1; |
| 119 | if(l==-atom) return -1; |
| 120 | } |
| 121 | return 0; |
| 122 | } |
| 123 | |
| 124 | /** |
| 125 | * Replaces the ID of a particular atom, assuming that |
| 126 | * no twins exist. |
| 127 | * @param oldID |
| 128 | * @param newID |
| 129 | * @return 1 if oldID=>newID, -1 if -oldID=>-newID, 0 if no replacement |
| 130 | */ |
| 131 | public int replaceAtomID(int oldID, int newID){ |
| 132 | for(int k=0; k<lits.length; k++){ |
| 133 | if(lits[k] == oldID){ |
| 134 | lits[k] = newID; |
| 135 | return 1; |
| 136 | }else if(lits[k] == -oldID){ |
| 137 | lits[k] = -newID; |
| 138 | return -1; |
| 139 | } |
| 140 | } |
| 141 | return 0; |
| 142 | } |
| 143 | |
| 144 | /** |
| 145 | * Initialize GClause from results of SQL. This involves set |
| 146 | * $cid$ to {@link GClause#id}, $weight$ {@link GClause#weight}, |
| 147 | * $lits$ to {@link GClause#lits}, $fcid$ to {@link GClause#fcid}. |
| 148 | * @param rs the ResultSet for SQL. This sql is a sequential |
| 149 | * scan on table {@link Config#relClauses}. |
| 150 | * |
| 151 | */ |
| 152 | public void parse(ResultSet rs){ |
| 153 | try { |
| 154 | id = rs.getInt("cid"); |
| 155 | weight = rs.getDouble("weight"); |
| 156 | |
| 157 | Array a = rs.getArray("lits"); |
| 158 | Integer[] ilits = (Integer[]) a.getArray(); |
| 159 | lits = new int[ilits.length]; |
| 160 | for(int i=0; i<lits.length; i++){ |
| 161 | lits[i] = ilits[i]; |
| 162 | } |
| 163 | if(Config.track_clause_provenance){ |
| 164 | Array fc = rs.getArray("fcid"); |
| 165 | Integer[] ifc = (Integer[]) fc.getArray(); |
| 166 | ArrayList<Integer> lfcid = new ArrayList<Integer>(); |
| 167 | for(int i=0; i< ifc.length; i++){ |
| 168 | // ignoring soft evidence unit clauses |
| 169 | if(ifc[i] != null && ifc[i] != 0){ |
| 170 | lfcid.add(ifc[i]); |
| 171 | // ADDED BY CE ON NOV. 29 |
| 172 | if(Math.abs(ifc[i]) > GClause.maxFCID){ |
| 173 | GClause.maxFCID = Math.abs(ifc[i]); |
| 174 | } |
| 175 | } |
| 176 | } |
| 177 | fcid = new int[lfcid.size()]; |
| 178 | for(int i=0; i<fcid.length; i++){ |
| 179 | fcid[i] = lfcid.get(i); |
| 180 | } |
| 181 | |
| 182 | fc = rs.getArray("ffcid"); |
| 183 | String[] sfc = (String[]) fc.getArray(); |
| 184 | ArrayList<String> lsfc = new ArrayList<String>(); |
| 185 | for(int i=0; i< sfc.length; i++){ |
| 186 | // ignoring soft evidence unit clauses |
| 187 | if(sfc[i] != null && sfc[i] != "0"){ |
| 188 | lsfc.add(sfc[i]); |
| 189 | } |
| 190 | } |
| 191 | ffcid = new String[lsfc.size()]; |
| 192 | for(int i=0; i<ffcid.length; i++){ |
| 193 | ffcid[i] = lsfc.get(i); |
| 194 | } |
| 195 | } |
| 196 | } catch (Exception e) { |
| 197 | ExceptionMan.handle(e); |
| 198 | } |
| 199 | } |
| 200 | |
| 201 | /** |
| 202 | * Returns the string form of this GClause, which is, |
| 203 | * |
| 204 | * { <lit_1>, <lit_2>, ..., <lit_n> } | weight |
| 205 | * |
| 206 | * where lit_i is the literal ID in {@link GClause#lits}. |
| 207 | */ |
| 208 | public String toPGString(){ |
| 209 | StringBuilder sb = new StringBuilder(); |
| 210 | sb.append("{"); |
| 211 | for(int i=0; i<lits.length; i++){ |
| 212 | sb.append(lits[i]); |
| 213 | if(i < lits.length-1) sb.append(","); |
| 214 | } |
| 215 | sb.append("} | " + weight); |
| 216 | return sb.toString(); |
| 217 | } |
| 218 | |
| 219 | /** |
| 220 | * Returns string form of this GClause. Compared |
| 221 | * with {@link GClause#toString()}, this function also only shows |
| 222 | * literals violating this clause. |
| 223 | * |
| 224 | * @param atoms Map from Literal ID to GAtom object. This is used |
| 225 | * for obtaining the truth value of GAtom, which is inevitable |
| 226 | * for determining violation. |
| 227 | */ |
| 228 | public String toLongString(HashMap<Integer, GAtom> atoms){ |
| 229 | StringBuilder sb = new StringBuilder(); |
| 230 | sb.append("ViolatedGroundClause" + id + " [weight=" + weight + |
| 231 | ", satisfied=" + (nsat > 0) + "]\n"); |
| 232 | for(int l : lits){ |
| 233 | GAtom a = atoms.get(Math.abs(l)); |
| 234 | boolean vio = false; |
| 235 | if((weight<0) == ((l > 0) == (a.truth))){ |
| 236 | vio = true; |
| 237 | } |
| 238 | if(vio){ |
| 239 | sb.append("\t"); |
| 240 | sb.append(a.truth ? " " : "!"); |
| 241 | sb.append(a.rep + "\n"); |
| 242 | } |
| 243 | } |
| 244 | return sb.toString(); |
| 245 | } |
| 246 | |
| 247 | /** |
| 248 | * Returns its human-friendly representation. |
| 249 | */ |
| 250 | public String toString(){ |
| 251 | StringBuilder sb = new StringBuilder(); |
| 252 | sb.append(weight + ": ["); |
| 253 | for(int l : lits){ |
| 254 | sb.append(l + ","); |
| 255 | } |
| 256 | sb.append("]"); |
| 257 | return sb.toString(); |
| 258 | } |
| 259 | |
| 260 | } |