tuffy.infer.ds
Class GClause

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

public class GClause
extends java.lang.Object

A ground clause.


Field Summary
 boolean dead
          Whether this clause should be ignored while SampleSAT.
 int[] fcid
          List of original clauses used to generate this grounded clause.
 java.lang.String[] ffcid
          Finer-grained clause origin.
 int id
          ID of this GClause.
 int[] lits
          List of literals in this grounded clause.
static int maxFCID
          The largest fcid seen when parsing the database for all GClause.
 int nsat
          Number of satisfied literals in this GClause.
 double weight
          Weight of this GClause.
 
Constructor Summary
GClause()
           
 
Method Summary
 double cost()
          Return the cost for violating this GClause.
 boolean isHardClause()
          Return whether this clause is a hard clause.
 boolean isPositiveClause()
          Return whether this clause is a positive clause.
 int linkType(int atom)
          Returns +/-1 if this GClause contains this atom; 0 if not.
 void parse(java.sql.ResultSet rs)
          Initialize GClause from results of SQL.
 int replaceAtomID(int oldID, int newID)
          Replaces the ID of a particular atom, assuming that no twins exist.
 boolean selectMCSAT()
          Return true if this clause is not set to ``dead''.
 java.lang.String toLongString(java.util.HashMap<java.lang.Integer,GAtom> atoms)
          Returns string form of this GClause.
 java.lang.String toPGString()
          Returns the string form of this GClause, which is, { , , ..., } | weight where lit_i is the literal ID in lits.
 java.lang.String toString()
          Returns its human-friendly representation.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

id

public int id
ID of this GClause.


weight

public double weight
Weight of this GClause.


lits

public int[] lits
List of literals in this grounded clause. This is from $lits$ attribute in Config#relClauses table.


fcid

public int[] fcid
List of original clauses used to generate this grounded clause. This is from $fcid$ attribute in the clause table when Config.track_clause_provenance set to true.


ffcid

public java.lang.String[] ffcid
Finer-grained clause origin. Similar to fcid, corresponding to attribute $ffcid$ in Config#relClauses table.


nsat

public int nsat
Number of satisfied literals in this GClause. This GClause is true iff. nsat > 0.


dead

public boolean dead
Whether this clause should be ignored while SampleSAT. Used by MC-SAT.


maxFCID

public static int maxFCID
The largest fcid seen when parsing the database for all GClause.

Constructor Detail

GClause

public GClause()
Method Detail

isPositiveClause

public boolean isPositiveClause()
Return whether this clause is a positive clause. Here by positive it means this clause has a positive weight.


isHardClause

public boolean isHardClause()
Return whether this clause is a hard clause. Here by hard it means this clause has a weight larger than Config.hard_weight, which means this clause must be satisfied in reasoning result.


selectMCSAT

public boolean selectMCSAT()
Return true if this clause is not set to ``dead''. This is used in MCSAT.


cost

public double cost()
Return the cost for violating this GClause. For positive clause, if it is violated, cost equals to weight. For negative clause, if it is satisfied, cost equals to -weight. Otherwise, return 0.


linkType

public int linkType(int atom)
Returns +/-1 if this GClause contains this atom; 0 if not. If -1, then the atom in this clause is with negative sense.

Parameters:
atom -

replaceAtomID

public int replaceAtomID(int oldID,
                         int newID)
Replaces the ID of a particular atom, assuming that no twins exist.

Parameters:
oldID -
newID -
Returns:
1 if oldID=>newID, -1 if -oldID=>-newID, 0 if no replacement

parse

public void parse(java.sql.ResultSet rs)
Initialize GClause from results of SQL. This involves set $cid$ to id, $weight$ weight, $lits$ to lits, $fcid$ to fcid.

Parameters:
rs - the ResultSet for SQL. This sql is a sequential scan on table Config#relClauses.

toPGString

public java.lang.String toPGString()
Returns the string form of this GClause, which is, { , , ..., } | weight where lit_i is the literal ID in lits.


toLongString

public java.lang.String toLongString(java.util.HashMap<java.lang.Integer,GAtom> atoms)
Returns string form of this GClause. Compared with toString(), this function also only shows literals violating this clause.

Parameters:
atoms - Map from Literal ID to GAtom object. This is used for obtaining the truth value of GAtom, which is inevitable for determining violation.

toString

public java.lang.String toString()
Returns its human-friendly representation.

Overrides:
toString in class java.lang.Object