tuffy.infer.ds
Class GAtom

java.lang.Object
  extended by tuffy.infer.ds.GAtom

public class GAtom
extends java.lang.Object

A ground atom.


Field Summary
 boolean cut
          Whether this atom is referred to by multiple partitions
 boolean fixed
          Whether the truth value of this GAtom is fixed.
 int id
          ID of this GAtom.
 boolean lowlowTruth
           
 boolean lowTruth
          Recorded truth value for low-cost.
 int pid
          ID of the partition containing this atom
 float prob
           
 java.lang.String rep
          String representation of this GAtom.
 int tallyTrue
          Tallies used in MCSAT.
 boolean truth
          The truth value of this GAtom.
 int wannabe
          The ideal truth value of this GAtom.
 
Constructor Summary
GAtom(int nid)
          Constructor for GAtom.
 
Method Summary
 void assignSatPotential(GClause f)
          Flipping this node will make f unsat->sat.
 void assignUnsatPotential(GClause f)
          Flipping this node will make f sat->unsat.
 boolean critical()
          Whether wannabe == 3.
 boolean criticalForHardClauses()
          Whether changing the truth value of this GAtom will violate several hard clauses.
 double delta()
           
 double delta(KeyBlock keyBlock)
           
 void flip()
          Flip the truth value of this GAtom.
 java.util.ArrayList<GAtom> flip(KeyBlock keyBlock)
           
 void forceFlip()
           
 void invertDelta()
          Exchange the value of rescue and violate.
 void markCritical()
          Set wannabe = 3.
 void markWannaBeFalse()
          Set wannabe = 1.
 void markWannaBeTrue()
          Set wannabe = 2.
 void resetDelta()
          Reset rescue and violate to zero.
 void revokeSatPotential(GClause f)
          Flipping this node no longer makes f unsat->sat.
 void revokeUnsatPotential(GClause f)
          Flipping this node no longer makes f sat->unsat.
 boolean wannaBeFalse()
          Whether wannabe == 1; (false)
 boolean wannaBeTrue()
          Whether wannabe == 2; (true)
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

cut

public boolean cut
Whether this atom is referred to by multiple partitions


fixed

public boolean fixed
Whether the truth value of this GAtom is fixed.


id

public int id
ID of this GAtom.


lowlowTruth

public boolean lowlowTruth

lowTruth

public boolean lowTruth
Recorded truth value for low-cost.


pid

public int pid
ID of the partition containing this atom


prob

public float prob

rep

public java.lang.String rep
String representation of this GAtom.


tallyTrue

public int tallyTrue
Tallies used in MCSAT.


truth

public boolean truth
The truth value of this GAtom.


wannabe

public int wannabe
The ideal truth value of this GAtom. 1 = false; 2 = true; 3 = both.

Constructor Detail

GAtom

public GAtom(int nid)
Constructor for GAtom.

Parameters:
nid - ID of this GAtom.
Method Detail

assignSatPotential

public void assignSatPotential(GClause f)
Flipping this node will make f unsat->sat.

Parameters:
f - GClause that currently not registered.

assignUnsatPotential

public void assignUnsatPotential(GClause f)
Flipping this node will make f sat->unsat.

Parameters:
f - GClause that currently not registered.

critical

public boolean critical()
Whether wannabe == 3. (both)


criticalForHardClauses

public boolean criticalForHardClauses()
Whether changing the truth value of this GAtom will violate several hard clauses.


delta

public double delta()
Returns:
Delta to the total cost if this node is flipped.

delta

public double delta(KeyBlock keyBlock)
Returns:
Delta to the total cost if this node is flipped.

flip

public void flip()
Flip the truth value of this GAtom.


flip

public java.util.ArrayList<GAtom> flip(KeyBlock keyBlock)

forceFlip

public void forceFlip()

invertDelta

public void invertDelta()
Exchange the value of rescue and violate. When the truth value of this GAtom is flipped, this function is called.


markCritical

public void markCritical()
Set wannabe = 3. (both)


markWannaBeFalse

public void markWannaBeFalse()
Set wannabe = 1. (false)


markWannaBeTrue

public void markWannaBeTrue()
Set wannabe = 2. (true)


resetDelta

public void resetDelta()
Reset rescue and violate to zero.


revokeSatPotential

public void revokeSatPotential(GClause f)
Flipping this node no longer makes f unsat->sat.

Parameters:
f - GClause that currently registered as unsat->sat.

revokeUnsatPotential

public void revokeUnsatPotential(GClause f)
Flipping this node no longer makes f sat->unsat.

Parameters:
f - GClause that currently registered as sat->unsat.

wannaBeFalse

public boolean wannaBeFalse()
Whether wannabe == 1; (false)


wannaBeTrue

public boolean wannaBeTrue()
Whether wannabe == 2; (true)