#include "maximal.h"

This page has information from files maximal.h and maximal.c.

Contents

Public Routines in File maximal.c

Index

copy_selected_literal_marksmark_maximal_literalsmax_lit_testmaximal_signed_literal
exists_selected_literalmark_selected_literalmax_signed_lit_testnumber_of_maximal_literals
init_maximalmark_selected_literalsmaximal_literalselected_literal

Details

void copy_selected_literal_marks(Literals a, Literals b);

BOOL exists_selected_literal(Literals lits);

void init_maximal(void);

void mark_maximal_literals(Literals lits);

void mark_selected_literal(Literals lit);

void mark_selected_literals(Literals lits, char *selection);

BOOL max_lit_test(Literals lits, Literals lit);
Test if a literal is maximal in a clause (w.r.t. others literals of the either sign). This version does not use a flag. 
BOOL max_signed_lit_test(Literals lits, Literals lit);
Test if a literal is maximal in a clause (w.r.t. others literals of the same sign). This version does not use a flag. 
BOOL maximal_literal(Literals lits, Literals lit, int check);
Check if a literal is maximal in the clause that contains it. The argument "check" should be FLAG_CHECK (check the flag only) or FULL_CHECK (do the full comparicon). 
BOOL maximal_signed_literal(Literals lits, Literals lit, int check);
Check if a literal is maximal in the clause that contains it. This only checks a flag. It does not compute maximality. 
int number_of_maximal_literals(Literals lits, int check);
Return the number of maximal literals. This checks a flag only. 
BOOL selected_literal(Literals lit);

Public Definitions in File maximal.h

enum {  /* how to check for maximal literals */
  FLAG_CHECK,
  FULL_CHECK
};

Introduction