Clause Class Reference

Representation of clauses. More...

#include <Clause.hpp>

Collaboration diagram for Clause:

Public Member Functions
	Clause (const vector< Literal > &new_lits)
	Construction is just taking a new vector of Literals.
size_t	size () const
	Straightforward get method.
bool	empty () const
	Straightforward get method.
void	clear ()
	Straightforward reset method.
bool	is_positive () const
	A clause is positive if it has no negated literals.
bool	is_negative () const
	A clause is negative if it has only negated literals.
void	remove_duplicates ()
	Get rid of identical literals.
bool	has_complementary_literals () const
	Check whether the clause contains complementary literals.
void	add_lit (const Literal &)
	Add a literal, making sure you don't duplicate.
void	drop_literal (LitNum)
	Get rid of the specified Literal.
Literal	extract_literal (LitNum)
	Get rid of and return the specified Literal.
Literal &	operator[] (size_t)
	Direct read of the specified Literal.
Clause	make_copy_with_new_vars (VariableIndex &, TermIndex &) const
	Make a copy of an entire clause, introducing new variables.
SimplificationResult	simplify ()
	Simplify a clause by dealing with $true, $false, complementary literals, and duplicates.
void	random_reorder ()
	Randomly re-order the literals.
string	to_string (bool=false) const
	Convert to a string.
string	to_prolog_string () const
	Convert to a string that can be read by Prolog.
string	to_tptp_string () const
	Convert to a string that is compatible with the TPTP.
string	make_LaTeX (bool=false) const
	Convert the clause to a LaTeX representation.
vector< Literal >::const_iterator	cbegin () const
vector< Literal >::const_iterator	cend () const
vector< Literal >::iterator	begin ()
vector< Literal >::iterator	end ()

Private Attributes
vector< Literal >	c
	A Clause is just a vector of Literals.

Static Private Attributes
static std::mt19937	d
	Randomness for random reordering.

Friends
ostream &	operator<< (ostream &, const Clause &)

Detailed Description

Representation of clauses.

Essentially straightforward as they are just vectors of Literals. Other classes do all the heavy lifting.

Definition at line 52 of file Clause.hpp.

Constructor & Destructor Documentation

Clause() [1/2]

Clause::Clause ( )

inline

Definition at line 63 of file Clause.hpp.

: c() {}

Clause() [2/2]

Clause::Clause ( const vector< Literal > & new_lits )

inline

Construction is just taking a new vector of Literals.

Parameters

new_lits

Reference to new vector of Literals.

Definition at line 69 of file Clause.hpp.

                                            : c(new_lits) {
    #ifdef DEBUGMESSAGES
        if (new_lits.size() == 0)
            cerr << "Why are you constructing an empty clause?" << endl;
    #endif
    }

Member Function Documentation

add_lit()

void Clause::add_lit

(

const Literal &

l

)

Add a literal, making sure you don't duplicate.

Yes, yes a set<> would be a good idea, but vectors are easy, nicer if you want indexes amd nicer for the cache.

Parameters

l	Reference to Literal to add

Definition at line 87 of file Clause.cpp.

                                     {
    for (size_t i = 0; i < c.size(); i++)
        if (c[i] == l) {
#ifdef DEBUGMESSAGES
            cerr << "Don't duplicate Literals in a clause!" << endl;
#endif
            return;
        }
    c.push_back(l);
}

begin()

vector< Literal >::iterator Clause::begin ( )

inline

Definition at line 192 of file Clause.hpp.

{ return c.begin(); }

cbegin()

vector< Literal >::const_iterator Clause::cbegin ( ) const

inline

Definition at line 190 of file Clause.hpp.

{ return c.cbegin(); }

cend()

vector< Literal >::const_iterator Clause::cend ( ) const

inline

Definition at line 191 of file Clause.hpp.

{ return c.cend(); }

clear()

void Clause::clear ( )

inline

Straightforward reset method.

Definition at line 86 of file Clause.hpp.

{ c.clear(); }

drop_literal()

void Clause::drop_literal

(

LitNum

l

)

Get rid of the specified Literal.

Parameters

l	Index of literal to remove.

Definition at line 135 of file Clause.cpp.

                                  {
    if (c.size() == 0) {
#ifdef DEBUGMESSAGES
        cerr << "Can't drop_literal from empty clause" << endl;
#endif
        return;
    }
    if (l > c.size() - 1) {
#ifdef DEBUGMESSAGES
        cerr << "drop_literal argument is out of range" << endl;
#endif
        return;
    }
    if (c.size() == 1) {
        c.pop_back();
        return;
    }
    c[l] = c.back();
    c.pop_back();
}

empty()

bool Clause::empty ( ) const

inline

Straightforward get method.

Definition at line 82 of file Clause.hpp.

{ return c.empty(); }

end()

vector< Literal >::iterator Clause::end ( )

inline

Definition at line 193 of file Clause.hpp.

{ return c.end(); }

extract_literal()

Literal Clause::extract_literal

(

LitNum

l

)

Get rid of and return the specified Literal.

Parameters

l	Index of literal to remove.

Definition at line 156 of file Clause.cpp.

                                        {
     Literal error_lit;
     if (c.size() == 0) {
#ifdef DEBUGMESSAGES
        cerr << "Can't extract_literal from empty clause" << endl;
#endif
        return error_lit;
    }
    if (l > c.size() - 1) {
#ifdef DEBUGMESSAGES
        cerr << "extract_literal argument is out of range" << endl;
#endif
        return error_lit;
    }
    Literal lit(c[l]);
    if (c.size() == 1) {
        c.pop_back();
        return lit;
    }
    c[l] = c.back();
    c.pop_back();
    return lit;
}

has_complementary_literals()

bool Clause::has_complementary_literals

(

)

const

Check whether the clause contains complementary literals.

This does not take account of substitutions as it is mainly used for simplification before any substitutions happen.

Definition at line 74 of file Clause.cpp.

                                              {
    size_t s = c.size();
    if (s < 2) 
        return false;
    for (size_t i = 0; i < s - 1; i++) {
        for (size_t j = i+1; j < s; j++) {
            if (c[i].is_complement_of(c[j])) 
                return true;
        }
    }
    return false;
}

is_negative()

bool Clause::is_negative

(

)

const

A clause is negative if it has only negated literals.

Definition at line 42 of file Clause.cpp.

                               {
#ifdef DEBUGMESSAGES
    if (c.size() == 0)
        cerr << "Don't check an empty clause for negativity" << endl;
#endif
  for (size_t i = 0; i < c.size(); i++) {
    if (c[i].is_positive())
      return false;
  }
  return true;
}

is_positive()

bool Clause::is_positive

(

)

const

A clause is positive if it has no negated literals.

Definition at line 30 of file Clause.cpp.

                               {
#ifdef DEBUGMESSAGES
    if (c.size() == 0)
        cerr << "Don't check an empty clause for positivity" << endl;
#endif
  for (size_t i = 0; i < c.size(); i++) {
    if (c[i].is_negative())
      return false;
  }
  return true;
}

make_copy_with_new_vars()

Clause Clause::make_copy_with_new_vars	(	VariableIndex &	vi,
		TermIndex &	ti ) const

Make a copy of an entire clause, introducing new variables.

Straightforward because the heavy lifting is done elsewhere.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex

Definition at line 98 of file Clause.cpp.

                                                                             {
#ifdef DEBUGMESSAGES
    if (c.size() == 0)
        cerr << "You are making a copy of an empty clause" << endl;
#endif
    vector<Literal> new_lits;
    unordered_map<Variable*,Term*> new_vars;
    for (size_t i = 0; i < c.size(); i++)
        new_lits.push_back(c[i].make_copy_with_new_vars_helper(vi, ti, new_vars));
    return Clause(new_lits);
}

make_LaTeX()

string Clause::make_LaTeX

(

bool

subbed = false

)

const

Convert the clause to a LaTeX representation.

Assumes you are in Math Mode.

Parameters

subbed

implement substitution if true.

Definition at line 231 of file Clause.cpp.

                                           {
  commas::comma com(c.size());
  string s ("\\textcolor{blue}{\\{} ");
  for (const Literal& l : c) {
      s += l.make_LaTeX(subbed);
      s += com();
  }
  s += "\\textcolor{blue}{\\}}";
  return s;
}

operator[]()

Literal & Clause::operator[]

(

size_t

i

)

Direct read of the specified Literal.

There is no check on whether you've given a sensible index, so behave yourself!

Parameters

i	Index of required Literal

Definition at line 180 of file Clause.cpp.

                                    {
#ifdef DEBUGMESSAGES
    if (i > c.size() - 1)
        cerr << "You're out of range accessing a clause" << endl;
#endif
    return c[i];
}

random_reorder()

void Clause::random_reorder

(

)

Randomly re-order the literals.

Definition at line 188 of file Clause.cpp.

                            {
  // Make a permutation.
  vector<size_t> new_order;
  size_t s = c.size();
  for (size_t i = 0; i < s; i++)
    new_order.push_back(i);
  std::shuffle(new_order.begin(), new_order.end(), d);
  // Re-order.
  vector<Literal> new_c = c; 
  for (size_t i = 0; i < s; i++) {
    c[i] = new_c[new_order[i]];
  }
}

remove_duplicates()

void Clause::remove_duplicates

(

)

Get rid of identical literals.

This does not take account of substitutions as it is mainly used for simplification before any substitutions happen.

Definition at line 54 of file Clause.cpp.

                                {
    size_t s = c.size();
    if (s < 2)
        return;
    vector<Literal> new_c;
    for (size_t i = 0; i < s - 1; i++) {
        bool found = false;
        for (size_t j = i+1; j < s; j++ ) {
            if (c[i] == c[j]) {
                found = true;
                break;
            }
        }
        if (!found) 
            new_c.push_back(c[i]);
    }
    new_c.push_back(c[s - 1]);
    c = new_c;
 }

simplify()

SimplificationResult Clause::simplify

(

)

Simplify a clause by dealing with $true, $false, complementary literals, and duplicates.

Definition at line 110 of file Clause.cpp.

                                       {
    // Do this first in case someone has made a clause with 
    // both $true and $false in it.
    vector<Literal> new_clause;
    bool clause_is_true = false;
    for (Literal& lit : c)  {
        if (lit.is_false()) 
            continue;
        if (lit.is_true()) {
            clause_is_true = true;
            continue;
        }
        new_clause.push_back(lit);
    }
    c = new_clause;
    if (clause_is_true)
        return SimplificationResult::Tautology;
    remove_duplicates();
    if (c.size() == 0)
        return SimplificationResult::Contradiction;
    if (has_complementary_literals())
        return SimplificationResult::Tautology;
    return SimplificationResult::OK;
}

size()

size_t Clause::size ( ) const

inline

Straightforward get method.

Definition at line 78 of file Clause.hpp.

{ return c.size(); }

to_prolog_string()

string Clause::to_prolog_string

(

)

const

Convert to a string that can be read by Prolog.

Does not apply substitutions.

Definition at line 206 of file Clause.cpp.

                                      {
  commas::comma com(c.size());
  string result("[ ");
  for (const Literal& l : c) {
      result += l.to_prolog_string();
      result += com();
  }
  result += " ]";
  return result;
}

to_string()

string Clause::to_string

(

bool

subbed = false

)

const

Convert to a string.

Parameters

subbed

Implement substitutions if true.

Definition at line 202 of file Clause.cpp.

                                          {
    return vector_to_string(c, subbed, "{ ", " }", ", ");
}

to_tptp_string()

string Clause::to_tptp_string

(

)

const

Convert to a string that is compatible with the TPTP.

Does not apply substitutions.

Definition at line 217 of file Clause.cpp.

                                    {
  commas::comma com(c.size());
  string result("( ");
  for (const Literal& l : c) {
      result += l.to_tptp_string();
      string s = com();
      if (s == string(", "))
        s = string(" | "); 
      result += s;
  }
  result += " )";
  return result;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Clause & cl )

friend

Definition at line 242 of file Clause.cpp.

                                                    {
  out << "{ ";
  size_t s = cl.c.size();
  size_t i = 1;
  for (const Literal& l : cl.c) {
      out << l.to_string();
      if (i < s)
          out << " " << unicode_symbols::LogSym::or_sym << " ";
      i++;
  }
  out << " }";
  return out;
}

Member Data Documentation

c

vector<Literal> Clause::c

private

A Clause is just a vector of Literals.

Definition at line 57 of file Clause.hpp.

d

std::mt19937 Clause::d

staticprivate

Randomness for random reordering.

Definition at line 61 of file Clause.hpp.

---

The documentation for this class was generated from the following files:

• /Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/Clause.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/Clause.cpp