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


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


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.


void 
Clg_Free(
  clause_graph  graph 
)
Free all CLGs


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


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


Last updated on 2012/11/18 14h:16