Variable

A variable has an unsigned integer as its value. A variable can also be treated as an unsigned integer.

• Constructors

We can construct a variable via a default constructor, a copy constructor, or a constructor that takes in an unsigned integer.

• Static member variables

const static Variable start is the minimum variable. const static Variable under is the only undefined variable with the value unsigned(-1) and each valid variable should has a less value.

Literal

A literal has an unsigned integer as its value and it can also be treated as an unsigned integer. For example, if x₁ has value 1, the literal x₁ has value 3 and not x₁ has value 2.

• Constructors

We can construct a variable via a default constructor, a copy constructor, a constructor that takes in an unsigned integer, or a constructor that takes in a variable and a sign.

• Variable Var()

This function returns the variable of the literal.

• bool Sign()

This function returns the sign of the literal, where true means positive and false means negative.

• bool NSign()

This function returns the negation of the sign of the literal.

• const Literal operator ~()

This function returns the negated literal

Clause

We remark that the member Literal * _lits must be managed outside.

• Clause(Literal lit)

Create a unit clause.

• Clause(Literal lit0, Literal lit1)

Create a binary clause.

• Clause(const Literal * lits, unsigned size)

Create a clause with a given size.

• Clause(const vector & lits)

Create a clause with literals in the given vector.

• Copy constructor

The output clause shares the address of _lits with the input clause.

• Destructor

The destruction does not free the memory for _lits. Call Free() if you want to free it.

• Clause Copy()

Returns a copied clause with reallocated memory for _lits

• void Free()

Free the memory for _lits.

• unsigned Size()

Returns the number of literals.

• void Shrink(unsigned size)

Reduce the number of literals given by size.

• Literal & operator [] ( unsigned i )

Returns the i-th literal.

• Literal & Last_Lit()

Returns the last literal.

• void Erase_Lit(unsigned i)

Erase the i-th literal and move the last to the position i.

• void Swap_Lits(unsigned i, unsigned j)

Swap two literals at positions i and j.

• void Swap(Clause & clause)

Swap the literals of two clauses.

• void Sort(QSorter & sorter)

Sort the literals wrt the unsigned values of the variables.

• void Sort(const unsigned * var_rank)

Sort the literals wrt the variable rank as var_rank

• void Display(ostream & out)

Display the clause.

CNF formula

• CNF_Formula(Variable max_var)

Create an empty CNF formula with a stated maximum variable.

• CNF_Formula(istream & fin)

Create a CNF formula from a file in DIMACS format.

• void Add_Unary_Clause( Literal lit )

Add an unary clause with the literal given by lit.

• void Add_Binary_Clause( Literal lit0, Literal lit1 )

Add a binary clause with the literals given by lit0 and lit1.

• void Add_Ternary_Clause( Literal lit0, Literal lit1, Literal lit2 )

Add a ternary clause with the literals given by lit0, lit1 and lit2.

• void Add_Clause( Clause & cl )

Add a clause, where the memory for storing literals will be reallocate.

• void Input_Clause( Clause & cl )

Input a clause, where the memory of _lits will be used by the CNF formula.

• Variable Max_Var() const

Return the admitted maximum variable.

• unsigned Num_Clauses() const

Return the number of clauses.

• Clause & operator [] ( unsigned i )

Returns the i-th clause.

EPCCL theories

Weighted CNF formula

Format