static int 
AddToClause(
  int  pos_lit, 
  int  neg_lit, 
  int  size 
)
Insert pos_lit, where neg_lit is the corresponding literal of opposite polarity. If neg_lit is already in the clause then the clause is cancelled; if pos_lit is already in the clause then it is not reinserted.

Defined in clgClg.c

clause_graph 
Clg_Conj(
  clause_graph  left, 
  clause_graph  right 
)
Create a CLG representing a conjunction of two CLGs

Defined in clgClg.c

clause_graph 
Clg_Disj(
  clause_graph  left, 
  clause_graph  right 
)
Create a CLG representing a disjunction of two CLGs

Defined in clgClg.c

void 
Clg_Extract(
  clause_graph  head, 
  int  type, 
  Clg_Commit  commit, 
  void * data 
)
Calls commit with each extracted clause as an argument. type indicates the style of clause (eg, ZChaff all-positive integer format); *data is passed to commit as an extra argument. Clauses have duplicated literals suppressed and clauses with both positive and negative occurrences of the same literal are skipped.

Defined in clgClg.c

void 
Clg_Free(
  clause_graph  graph 
)
Free all CLGs

Defined in clgClg.c

clause_graph 
Clg_Lit(
  int  literal 
)
Create a CLG representing a single literal

Defined in clgClg.c

int 
Clg_Size(
  clause_graph  graph 
)
Return the number of clauses stored in the CLG

Defined in clgClg.c

static void 
Extract(
  clause_graph  head, 
  node_ptr  follow, 
  int  clause_size, 
  int  type, 
  Clg_Commit  commit, 
  void * data 
)
Walk the data structure from the head, creating clauses each time one is seen complete. See Footnote 936 for details of algorithm

Defined in clgClg.c

static clause_graph 
new_clg(
    
)
Allocate a new CLG node.

Defined in clgClg.c

Last updated on 2011/06/16 12h:15