| 1 | package tuffy.infer.ds; |
| 2 | |
| 3 | import java.util.ArrayList; |
| 4 | |
| 5 | import tuffy.util.Config; |
| 6 | |
| 7 | /** |
| 8 | * A ground atom. |
| 9 | */ |
| 10 | public class GAtom { |
| 11 | |
| 12 | /** |
| 13 | * ID of this GAtom. |
| 14 | */ |
| 15 | public int id = 0; |
| 16 | |
| 17 | /** |
| 18 | * ID of the partition containing this atom |
| 19 | */ |
| 20 | public int pid = 0; |
| 21 | |
| 22 | /** |
| 23 | * Whether this atom is referred to by multiple partitions |
| 24 | */ |
| 25 | public boolean cut = false; |
| 26 | |
| 27 | /** |
| 28 | * The truth value of this GAtom. |
| 29 | */ |
| 30 | public boolean truth = false; |
| 31 | |
| 32 | /** |
| 33 | * The ideal truth value of this GAtom. |
| 34 | * 1 = false; 2 = true; 3 = both. |
| 35 | */ |
| 36 | public int wannabe = 0; |
| 37 | |
| 38 | /** |
| 39 | * Whether wannabe == 3. (both) |
| 40 | * |
| 41 | */ |
| 42 | public boolean critical(){ |
| 43 | return wannabe == 3; |
| 44 | } |
| 45 | |
| 46 | /** |
| 47 | * Whether wannabe == 1; (false) |
| 48 | * |
| 49 | */ |
| 50 | public boolean wannaBeFalse(){ |
| 51 | return (wannabe & 1) > 0; |
| 52 | } |
| 53 | |
| 54 | /** |
| 55 | * Whether wannabe == 2; (true) |
| 56 | * |
| 57 | */ |
| 58 | public boolean wannaBeTrue(){ |
| 59 | return (wannabe & 2) > 0; |
| 60 | } |
| 61 | |
| 62 | /** |
| 63 | * Set wannabe = 3. (both) |
| 64 | */ |
| 65 | public void markCritical(){ |
| 66 | wannabe = 3; |
| 67 | } |
| 68 | |
| 69 | /** |
| 70 | * Set wannabe = 1. (false) |
| 71 | */ |
| 72 | public void markWannaBeFalse(){ |
| 73 | wannabe |= 1; |
| 74 | } |
| 75 | |
| 76 | /** |
| 77 | * Set wannabe = 2. (true) |
| 78 | */ |
| 79 | public void markWannaBeTrue(){ |
| 80 | wannabe |= 2; |
| 81 | } |
| 82 | |
| 83 | /** |
| 84 | * Recorded truth value for low-cost. |
| 85 | */ |
| 86 | public boolean lowTruth = false; |
| 87 | |
| 88 | /** |
| 89 | * |
| 90 | */ |
| 91 | public boolean lowlowTruth = false; |
| 92 | |
| 93 | /** |
| 94 | * Whether the truth value of this GAtom is |
| 95 | * fixed. |
| 96 | */ |
| 97 | public boolean fixed = false; |
| 98 | |
| 99 | public int nSamples = 0; |
| 100 | |
| 101 | /** |
| 102 | * Tallies used in MCSAT. |
| 103 | */ |
| 104 | public int tallyTrue = 0; |
| 105 | public float prob = 0; |
| 106 | |
| 107 | /** |
| 108 | * Two cost of changing the truth value of this GAtom. Violate |
| 109 | * is the cost that will increases after flipping. Rescue is the |
| 110 | * cost that will decreases after flipping. |
| 111 | */ |
| 112 | private double violate = 0, rescue = 0; |
| 113 | |
| 114 | /** |
| 115 | * String representation of this GAtom. |
| 116 | */ |
| 117 | public String rep = null; |
| 118 | |
| 119 | |
| 120 | /** |
| 121 | * Flip the truth value of this GAtom. |
| 122 | */ |
| 123 | public void flip(){ |
| 124 | if(!fixed) |
| 125 | truth = !truth; |
| 126 | } |
| 127 | |
| 128 | |
| 129 | public void forceFlip(){ |
| 130 | truth = !truth; |
| 131 | } |
| 132 | |
| 133 | public ArrayList<GAtom> flip(KeyBlock keyBlock){ |
| 134 | |
| 135 | if(!keyBlock.hasKey(this)){ |
| 136 | ArrayList<GAtom> influenced = new ArrayList<GAtom>(); |
| 137 | influenced.add(this); |
| 138 | this.forceFlip(); |
| 139 | return influenced; |
| 140 | } |
| 141 | |
| 142 | // flip from TRUE to FALSE will not influence others |
| 143 | if(this.truth == true){ |
| 144 | |
| 145 | ArrayList<GAtom> influenced = new ArrayList<GAtom>(); |
| 146 | influenced.add(this); |
| 147 | this.forceFlip(); |
| 148 | return influenced; |
| 149 | } |
| 150 | |
| 151 | ArrayList<GAtom> blockMates = keyBlock.getBlockMates(this); |
| 152 | ArrayList<GAtom> influenced = new ArrayList<GAtom>(); |
| 153 | |
| 154 | for(GAtom gatom : blockMates){ |
| 155 | |
| 156 | if(gatom == this || gatom.truth == true){ |
| 157 | influenced.add(gatom); |
| 158 | gatom.forceFlip(); |
| 159 | } |
| 160 | } |
| 161 | |
| 162 | return influenced; |
| 163 | |
| 164 | } |
| 165 | |
| 166 | /** |
| 167 | * Reset {@link GAtom#rescue} and {@link GAtom#violate} to zero. |
| 168 | */ |
| 169 | public void resetDelta(){ |
| 170 | violate = rescue = 0; |
| 171 | } |
| 172 | |
| 173 | /** |
| 174 | * Exchange the value of {@link GAtom#rescue} and |
| 175 | * {@link GAtom#violate}. When the truth value of this |
| 176 | * GAtom is flipped, this function is called. |
| 177 | */ |
| 178 | public void invertDelta(){ |
| 179 | double tv = violate; |
| 180 | violate = rescue; |
| 181 | rescue = tv; |
| 182 | } |
| 183 | |
| 184 | /** |
| 185 | * |
| 186 | * Whether changing the truth value of this GAtom will |
| 187 | * violate several hard clauses. |
| 188 | */ |
| 189 | public boolean criticalForHardClauses(){ |
| 190 | return violate > Config.hard_threshold; |
| 191 | } |
| 192 | |
| 193 | /** |
| 194 | * @return Delta to the total cost if this node is flipped. |
| 195 | */ |
| 196 | public double delta(){ |
| 197 | return violate - rescue; |
| 198 | } |
| 199 | |
| 200 | /** |
| 201 | * @return Delta to the total cost if this node is flipped. |
| 202 | */ |
| 203 | public double delta(KeyBlock keyBlock){ |
| 204 | |
| 205 | if(!keyBlock.hasKey(this)){ |
| 206 | return violate - rescue; |
| 207 | } |
| 208 | |
| 209 | double sum = 0; |
| 210 | |
| 211 | // flip from TRUE to FALSE will not influence others |
| 212 | if(this.truth == true){ |
| 213 | return violate - rescue; |
| 214 | } |
| 215 | |
| 216 | ArrayList<GAtom> blockMates = keyBlock.getBlockMates(this); |
| 217 | |
| 218 | for(GAtom gatom : blockMates){ |
| 219 | |
| 220 | if(gatom == this || gatom.truth == true){ |
| 221 | sum += gatom.delta(); |
| 222 | } |
| 223 | } |
| 224 | |
| 225 | return sum; |
| 226 | } |
| 227 | |
| 228 | /** |
| 229 | * Flipping this node will make f unsat->sat. |
| 230 | * @param f GClause that currently not registered. |
| 231 | */ |
| 232 | public void assignSatPotential(GClause f){ |
| 233 | if(f.weight > 0){ |
| 234 | rescue += f.weight; |
| 235 | }else{ |
| 236 | violate -= f.weight; |
| 237 | } |
| 238 | } |
| 239 | |
| 240 | /** |
| 241 | * Flipping this node will make f sat->unsat. |
| 242 | * @param f GClause that currently not registered. |
| 243 | */ |
| 244 | public void assignUnsatPotential(GClause f){ |
| 245 | if(f.weight > 0){ |
| 246 | violate += f.weight; |
| 247 | }else{ |
| 248 | rescue -= f.weight; |
| 249 | } |
| 250 | } |
| 251 | |
| 252 | /** |
| 253 | * Flipping this node no longer makes f unsat->sat. |
| 254 | * @param f GClause that currently registered as unsat->sat. |
| 255 | */ |
| 256 | public void revokeSatPotential(GClause f){ |
| 257 | if(f.weight > 0){ |
| 258 | rescue -= f.weight; |
| 259 | }else{ |
| 260 | violate += f.weight; |
| 261 | } |
| 262 | } |
| 263 | |
| 264 | /** |
| 265 | * Flipping this node no longer makes f sat->unsat. |
| 266 | * @param f GClause that currently registered as sat->unsat. |
| 267 | */ |
| 268 | public void revokeUnsatPotential(GClause f){ |
| 269 | if(f.weight > 0){ |
| 270 | violate -= f.weight; |
| 271 | }else{ |
| 272 | rescue += f.weight; |
| 273 | } |
| 274 | } |
| 275 | |
| 276 | /** |
| 277 | * Constructor for GAtom. |
| 278 | * @param nid ID of this GAtom. |
| 279 | */ |
| 280 | public GAtom(int nid) { |
| 281 | id = nid; |
| 282 | } |
| 283 | } |