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.
bool	is_ground () const
	Is this a ground clause?
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	get_literal (LitNum) const
	Get 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.
Clause	make_copy_with_new_unique_vars (VariableIndex &, TermIndex &) const
	Make a copy of an entire clause, introducing new variables.
void	make_copy_with_new_vars (Literal &, Clause &, VariableIndex &, TermIndex &)
	Make a copy of an entire clause and literal, 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.
void	reverse ()
	Reverse the order of the literals in the clause.
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 &out, const Clause &cl)

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 96 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 236 of file Clause.hpp.

{ return c.begin(); }

cbegin()

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

inline

Definition at line 234 of file Clause.hpp.

{ return c.cbegin(); }

cend()

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

inline

Definition at line 235 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 168 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 237 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 189 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;
}

get_literal()

Literal Clause::get_literal

(

LitNum

l

)

const

Get and return the specified Literal.

Parameters

l	Index of literal to return.

Definition at line 213 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]);
    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_ground()

bool Clause::is_ground

(

)

const

Is this a ground clause?

Do not attempt to follow substitutions.

Definition at line 87 of file Clause.cpp.

                             {
    for (const Literal& l : c) {
        if (!l.is_ground()) {
            return false;
        }
    }
    return true;
}

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_unique_vars()

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

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

Straightforward because the heavy lifting is done elsewhere.

This version uses unique variables, that do not get recycled when backtracking, and are thus suitable for caching copies of clauses.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex

Definition at line 120 of file Clause.cpp.

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

make_copy_with_new_vars() [1/2]

void Clause::make_copy_with_new_vars	(	Literal &	_l,
		Clause &	_c,
		VariableIndex &	vi,
		TermIndex &	ti )

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

Straightforward because the heavy lifting is done elsewhere.

Parameters

_l	New literal.
_c	New clause,
vi	Reference to the VariableIndex
ti	Reference to the TermIndex

Definition at line 133 of file Clause.cpp.

                                                                                              {
    size_t s = c.size();
    unordered_map<Variable*,Term*> new_vars;
    _l.make_copy_with_new_vars_replace_helper(vi, ti, new_vars);
    // NOTE: make sure _c actually has room in it, unless you want 
    // horror!
    for (size_t i = 0; i < s; i++)
        _c.c[i].make_copy_with_new_vars_replace_helper(vi, ti, new_vars);
}

make_copy_with_new_vars() [2/2]

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 107 of file Clause.cpp.

                                                                             {
#ifdef DEBUGMESSAGES
    if (c.size() == 0)
        cerr << "You are making a copy of an empty clause" << endl;
#endif
    size_t s = c.size();
    vector<Literal> new_lits;
    unordered_map<Variable*,Term*> new_vars;
    for (size_t i = 0; i < s; 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 286 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 231 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 239 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;
 }

reverse()

void Clause::reverse

(

)

Reverse the order of the literals in the clause.

Definition at line 253 of file Clause.cpp.

                     {
    std::reverse(c.begin(), c.end());
}

simplify()

SimplificationResult Clause::simplify

(

)

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

Definition at line 143 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 261 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 257 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 272 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 297 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++/source/Clause.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/Clause.cpp