|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object tuffy.infer.ds.GClause
public class GClause
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, { 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 |
---|
public int id
public double weight
public int[] lits
Config#relClauses
table.
public int[] fcid
Config.track_clause_provenance
set to true.
public java.lang.String[] ffcid
fcid
, corresponding to
attribute $ffcid$ in Config#relClauses
table.
public int nsat
public boolean dead
public static int maxFCID
Constructor Detail |
---|
public GClause()
Method Detail |
---|
public boolean isPositiveClause()
public boolean isHardClause()
Config.hard_weight
,
which means this clause must be satisfied in reasoning result.
public boolean selectMCSAT()
public double cost()
public int linkType(int atom)
atom
- public int replaceAtomID(int oldID, int newID)
oldID
- newID
-
public void parse(java.sql.ResultSet rs)
id
, $weight$ weight
,
$lits$ to lits
, $fcid$ to fcid
.
rs
- the ResultSet for SQL. This sql is a sequential
scan on table Config#relClauses
.public java.lang.String toPGString()
lits
.
public java.lang.String toLongString(java.util.HashMap<java.lang.Integer,GAtom> atoms)
toString()
, this function also only shows
literals violating this clause.
atoms
- Map from Literal ID to GAtom object. This is used
for obtaining the truth value of GAtom, which is inevitable
for determining violation.public java.lang.String toString()
toString
in class java.lang.Object
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |