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