Literal Class Reference

Basic representation of literals, bundling together (pointers to) a Predicate, a collection of arguments each a (pointer to a) Term, an arity and a polarity. More...

#include <Literal.hpp>

Collaboration diagram for Literal:

Public Member Functions
	Literal (Predicate *, const vector< Term * > &, Arity, bool)
	Construct a Literal from existing material.
Predicate *	get_pred () const
	Basic get method.
Arity	get_arity () const
	Basic get method.
bool	get_polarity () const
	Basic get method.
const vector< Term * > &	get_args () const
	Basic get method.
Term *	operator[] (size_t i) const
	Basic get method.
bool	is_positive () const
	Basic manipulation - entirely self-explanatory.
bool	is_negative () const
	Basic manipulation - entirely self-explanatory.
void	make_positive ()
	Basic manipulation - entirely self-explanatory.
void	make_negative ()
	Basic manipulation - entirely self-explanatory.
void	invert ()
	Basic manipulation - entirely self-explanatory.
void	make_empty ()
	Basic manipulation - entirely self-explanatory.
bool	is_empty () const
	Basic manipulation - entirely self-explanatory.
void	clear ()
	Basic manipulation - entirely self-explanatory.
size_t	get_pred_as_index () const
	Turn a Literal into an array index.
bool	is_ground () const
	Is the literal ground?
bool	is_true () const
	Is this equivalent to $true?
bool	is_false () const
	Is this equivalent to $false?
bool	contains_variable (Variable *) const
	Does this Literal contain the specified variable?
void	get_variables (set< Term * > &) const
	Get the variables in this literal without taking account of substitutions.
bool	is_compatible_with (const Literal *) const
	Literals can only be unified if the polarity and actual predicate are the same.
bool	is_complement_of (const Literal &) const
	Test whether one literal is exactly the same as another, with the exception of the polarity.
string	get_small_lit () const
	Get the predicate and polarity as a string.
string	to_string (bool=false) const
	Full conversion of Literal to string.
string	to_prolog_string () const
	Convert to a string in a format readable by Prolog.
string	to_tptp_string (bool=false) const
	Convert to a string in a format compatible with the TPTP.
string	make_LaTeX (bool=false) const
	Make a useable LaTeX version.
string	make_Graphviz (bool=false) const
	Make a useable Graphviz version.
bool	operator== (const Literal &) const
	Equality without taking account of substutions.
bool	subbed_equal (Literal *) const
	Equality, taking account of substitutions.
Literal	make_copy_with_new_vars (VariableIndex &, TermIndex &) const
	Make a copy of the Literal but with a new set of variables.
Literal	make_copy_with_new_vars_helper (VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &) const
	Helper function for make_copy_with_new_vars.
Literal	make_copy_with_new_unique_vars_helper (VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &) const
	Helper function for make_copy_with_unique_new_vars.
void	make_copy_with_new_vars_replace_helper (VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &)
	Helper function for making copies with new variables.
void	replace_variable (Variable *, Variable *, TermIndex *)
	Replace one variable with another throughout.
void	replace_variable_with_term (Term *, Variable *, TermIndex *)
	Replace one variable with a term throughout.

Private Attributes
Predicate *	pred
vector< Term * >	args
Arity	arity
bool	polarity

Friends
ostream &	operator<< (ostream &out, const Literal &l)

Detailed Description

Basic representation of literals, bundling together (pointers to) a Predicate, a collection of arguments each a (pointer to a) Term, an arity and a polarity.

Definition at line 50 of file Literal.hpp.

Constructor & Destructor Documentation

Literal() [1/2]

Literal::Literal ( )

inline

Definition at line 57 of file Literal.hpp.

: pred(nullptr), args(), arity(0), polarity(true) {}

Literal() [2/2]

Literal::Literal	(	Predicate *	new_p,
		const vector< Term * > &	new_args,
		Arity	new_ar,
		bool	new_pol )

Construct a Literal from existing material.

Parameters

new_p	Pointer to a Predicate
new_args	Reference to a vector of pointers to Terms
new_ar	New value for arity
new_pol	Set true for positive literal, false for negative (negated).

Definition at line 28 of file Literal.cpp.

: pred(new_p)
, args(new_args)
, arity(new_ar)
, polarity(new_pol)
{
  #ifdef DEBUGMESSAGES
    if (new_p == nullptr) {
      cerr << "Why would you construct an empty predicate?" << endl;
    }
  #endif
    if (new_p->get_arity() != new_args.size()) {
        cerr << "Number of arguments doesn't match predicate arity" << endl;
        cerr << "Are you mixing up your predicate names?" << endl;
    }
}

Member Function Documentation

clear()

void Literal::clear ( )

inline

Basic manipulation - entirely self-explanatory.

Definition at line 119 of file Literal.hpp.

{ pred = nullptr; args.clear(), arity = 0; polarity = true; } 

contains_variable()

bool Literal::contains_variable

(

Variable *

v

)

const

Does this Literal contain the specified variable?

Parameters

v	Pointer to Variable to search for.

Definition at line 131 of file Literal.cpp.

                                                 {
  for (size_t i = 0; i < args.size(); i++) {
    // Note that this takes account of substitutions.
    if (args[i]->contains_variable(v))
      return true;
  }
  return false;
}

get_args()

const vector< Term * > & Literal::get_args ( ) const

inline

Basic get method.

Definition at line 83 of file Literal.hpp.

{ return args; }

get_arity()

Arity Literal::get_arity ( ) const

inline

Basic get method.

Definition at line 75 of file Literal.hpp.

{ return arity; }

get_polarity()

bool Literal::get_polarity ( ) const

inline

Basic get method.

Definition at line 79 of file Literal.hpp.

{ return polarity; }

get_pred()

Predicate * Literal::get_pred ( ) const

inline

Basic get method.

Definition at line 71 of file Literal.hpp.

{ return pred; }

get_pred_as_index()

size_t Literal::get_pred_as_index ( ) const

inline

Turn a Literal into an array index.

This is straightforward: positive literals have even indices and negative literals odd.

Definition at line 126 of file Literal.hpp.

                                            {
        size_t index = pred->get_ID() << 1;
        if (!polarity)
            index |= 0x00000001;
        return index;
    };

get_small_lit()

string Literal::get_small_lit

(

)

const

Get the predicate and polarity as a string.

Definition at line 177 of file Literal.cpp.

                                    {
  string result;
  if (!polarity)
      result += unicode_symbols::LogSym::neg;
  result += pred->to_string();
  return result;
}

get_variables()

void Literal::get_variables

(

set< Term * > &

_vs

)

const

Get the variables in this literal without taking account of substitutions.

Parameters

_vs	Set of Term* representing variables.

Definition at line 140 of file Literal.cpp.

                                                  {
  for (const Term* arg : args) {
    set<Term*> vs = arg->all_variables();
    for (Term* v : vs) {
      _vs.insert(v);
    }
  }
 }

invert()

void Literal::invert ( )

inline

Basic manipulation - entirely self-explanatory.

Definition at line 107 of file Literal.hpp.

{ polarity = !polarity; }

is_compatible_with()

bool Literal::is_compatible_with

(

const Literal *

l

)

const

Literals can only be unified if the polarity and actual predicate are the same.

One does not generally expect literals to be differentiated by arity, but it's possible so we check that too.

Parameters

l	Pointer to Literal to compare with.

Definition at line 84 of file Literal.cpp.

                                                       {
  #ifdef DEBUGMESSAGES
    if (pred == nullptr || l->pred == nullptr) {
      cerr << "You shouldn't be checking compatibility of empty Literals" << endl;
    }
  #endif
    return (pred == l->pred &&
      polarity == l->polarity &&
      arity == l->arity);
}

is_complement_of()

bool Literal::is_complement_of

(

const Literal &

l

)

const

Test whether one literal is exactly the same as another, with the exception of the polarity.

This also requires that the argument lists are the same.

Parameters

l	Literal to compare with.

Definition at line 95 of file Literal.cpp.

                                                     {
  return (pred == l.pred &&
          args == l.args &&
          arity == l.arity &&
          !polarity == l.polarity);
}

is_empty()

bool Literal::is_empty ( ) const

inline

Basic manipulation - entirely self-explanatory.

Definition at line 115 of file Literal.hpp.

{ return (pred == nullptr); }

is_false()

bool Literal::is_false

(

)

const

Is this equivalent to $false?

Definition at line 121 of file Literal.cpp.

                             {
  return ((polarity && 
          (pred->get_name() == string("$false")) && 
          (pred->get_arity() == 0)) 
          ||
          (!polarity && 
          (pred->get_name() == string("$true")) && 
          (pred->get_arity() == 0)));
}

is_ground()

bool Literal::is_ground

(

)

const

Is the literal ground?

Do not attempt to follow substitutions.

Definition at line 102 of file Literal.cpp.

                              {
  for (Term* t : args) {
    if (!t->is_ground()) {
      return false;
    }
  }
  return true;
}

is_negative()

bool Literal::is_negative ( ) const

inline

Basic manipulation - entirely self-explanatory.

Definition at line 95 of file Literal.hpp.

{ return !polarity; }

is_positive()

bool Literal::is_positive ( ) const

inline

Basic manipulation - entirely self-explanatory.

Definition at line 91 of file Literal.hpp.

{ return polarity; }

is_true()

bool Literal::is_true

(

)

const

Is this equivalent to $true?

Definition at line 111 of file Literal.cpp.

                            {
  return ((polarity && 
          (pred->get_name() == string("$true")) && 
          (pred->get_arity() == 0)) 
          ||
          (!polarity && 
          (pred->get_name() == string("$false")) && 
          (pred->get_arity() == 0)));
}

make_copy_with_new_unique_vars_helper()

Literal Literal::make_copy_with_new_unique_vars_helper	(	VariableIndex &	vi,
		TermIndex &	ti,
		unordered_map< Variable *, Term * > &	new_vars ) const

Helper function for make_copy_with_unique_new_vars.

Iterates over the args using the corresponding method in the Term class to do the real work.

This version uses unique variables, not recycled when backtracking, and thus suitable for caching clauses.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex
new_vars	Reference to an unordered_map from pointers to Variables, to pointers to Terms. Initially empty. On completion contains a map from variables, to the terms corresponding to the new variables made to replace them.

Definition at line 58 of file Literal.cpp.

                                                                                                {
    vector<Term*> new_args;
    for (size_t i = 0; i < arity; i++)
        new_args.push_back(args[i]->make_copy_with_new_unique_vars_helper(vi, ti, new_vars));
    Literal result(pred, new_args, arity, polarity);
    return result;
}

make_copy_with_new_vars()

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

Make a copy of the Literal but with a new set of variables.

All the heavy lifting is done by the Term class. Essentially just initializes an unordered_map and calls the corresponging helper.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex

Definition at line 75 of file Literal.cpp.

                                                                               {
  #ifdef DEBUGMESSAGES
    if (pred == nullptr)
      cerr << "You shouldn't be making copies of empty Literals" << endl;
  #endif
    unordered_map<Variable*,Term*> new_vars;
    return make_copy_with_new_vars_helper(vi, ti, new_vars);
}

make_copy_with_new_vars_helper()

Literal Literal::make_copy_with_new_vars_helper	(	VariableIndex &	vi,
		TermIndex &	ti,
		unordered_map< Variable *, Term * > &	new_vars ) const

Helper function for make_copy_with_new_vars.

Iterates over the args using the corresponding method in the Term class to do the real work.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex
new_vars	Reference to an unordered_map from pointers to Variables, to pointers to Terms. Initially empty. On completion contains a map from variables, to the terms corresponding to the new variables made to replace them.

Definition at line 48 of file Literal.cpp.

                                                                                                {
    vector<Term*> new_args;
    for (size_t i = 0; i < arity; i++)
        new_args.push_back(args[i]->make_copy_with_new_vars_helper(vi, ti, new_vars));
    Literal result(pred, new_args, arity, polarity);
    return result;
}

make_copy_with_new_vars_replace_helper()

void Literal::make_copy_with_new_vars_replace_helper	(	VariableIndex &	vi,
		TermIndex &	ti,
		unordered_map< Variable *, Term * > &	new_vars )

Helper function for making copies with new variables.

Iterates over the args using the corresponding method in the Term class to do the real work.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex
new_vars	Reference to an unordered_map from pointers to Variables, to pointers to Terms. Initially empty. On completion contains a map from variables, to the terms corresponding to the new variables made to replace them.

Definition at line 68 of file Literal.cpp.

                                                                                     {
  for (size_t i = 0; i < arity; i++)
        args[i] = args[i]->make_copy_with_new_vars_helper(vi, ti, new_vars);
}

make_empty()

void Literal::make_empty ( )

inline

Basic manipulation - entirely self-explanatory.

Definition at line 111 of file Literal.hpp.

{ pred = nullptr; }

make_Graphviz()

string Literal::make_Graphviz

(

bool

subbed = false

)

const

Make a useable Graphviz version.

Parameters

subbed

Implement substitutions if true.

Definition at line 270 of file Literal.cpp.

                                               {
  string s;
  if (!polarity)
    s += unicode_symbols::LogSym::neg;
  s += pred->make_Graphviz();
  if (arity > 0) {
    s += "(";
    commas::comma com(arity);
    for (Term* p : args) {
        s += p->make_Graphviz(subbed);
        s += com();    
    }
    s += ")";
  }
  return s;
}

make_LaTeX()

string Literal::make_LaTeX

(

bool

subbed = false

)

const

Make a useable LaTeX version.

Assumes you are typesetting in Math Mode.

Parameters

subbed

Implement substitutions if true.

Definition at line 253 of file Literal.cpp.

                                            {
  string s;
  if (!polarity)
    s += "\\neg ";
  s += pred->make_LaTeX();
  if (arity > 0) {
    s += "(";
    commas::comma com(arity);
    for (Term* p : args) {
        s += p->make_LaTeX(subbed);
        s += com();    
    }
    s += ")";
  }
  return s;
}

make_negative()

void Literal::make_negative ( )

inline

Basic manipulation - entirely self-explanatory.

Definition at line 103 of file Literal.hpp.

{ polarity = false; }

make_positive()

void Literal::make_positive ( )

inline

Basic manipulation - entirely self-explanatory.

Definition at line 99 of file Literal.hpp.

{ polarity = true; }

operator==()

bool Literal::operator==

(

const Literal &

l

)

const

Equality without taking account of substutions.

Parameters

l	Literal to compare with.

Definition at line 149 of file Literal.cpp.

                                               {
  #ifdef DEBUGMESSAGES
    if (pred == nullptr || l.pred == nullptr) {
      cerr << "You shouldn't be checking equality of empty Literals" << endl;
    }
  #endif
    return (pred == l.pred &&
            args == l.args &&
            arity == l.arity &&
            polarity == l.polarity);
}

operator[]()

Term * Literal::operator[] ( size_t i ) const

inline

Basic get method.

Definition at line 87 of file Literal.hpp.

{ return args[i]; }

replace_variable()

void Literal::replace_variable	(	Variable *	new_var,
		Variable *	old_var,
		TermIndex *	ti )

Replace one variable with another throughout.

Iterate over the args using the replace_variable_in_term method in TermIndex to do the real work.

Parameters

new_var	Pointer to new Variable
old_var	Pointer to old Variable
ti	Pointer to the TermIndex

Definition at line 287 of file Literal.cpp.

                                              {
#ifdef DEBUGMESSAGES
  if (pred == nullptr)
    cerr << "You shouldn't be replacing variables in an empty Literal" << endl;
#endif
  for (size_t i = 0; i < arity; i++) {
    args[i] = ti->replace_variable_in_term(new_var, old_var, args[i]);
  }
}

replace_variable_with_term()

void Literal::replace_variable_with_term	(	Term *	new_term,
		Variable *	old_var,
		TermIndex *	ti )

Replace one variable with a term throughout.

Iterate over the args using the replace_variable_in_term_with_term method in TermIndex to do the real work.

Parameters

new_term	Pointer to new Term
old_var	Pointer to old Variable
ti	Pointer to the TermIndex

Definition at line 298 of file Literal.cpp.

                                              {
#ifdef DEBUGMESSAGES
   if (pred == nullptr)
    cerr << "You shouldn't be subbing terms in an empty Literal" << endl;
#endif
  for (size_t i = 0; i < arity; i++) {
    args[i] = ti->replace_variable_in_term_with_term(new_term, old_var, args[i]);
  }
}

subbed_equal()

bool Literal::subbed_equal

(

Literal *

l

)

const

Equality, taking account of substitutions.

Parameters

l	Pointer to Literal to compare with

Definition at line 161 of file Literal.cpp.

                                           {
  #ifdef DEBUGMESSAGES
    if (pred == nullptr || l->pred == nullptr) {
      cerr << "You shouldn't be checking subbed equality of empty Literals" << endl;
    }
  #endif
    if (!is_compatible_with(l)) {
        return false;
    }
    for (size_t i = 0; i < arity; i++) {
      if (!(args[i]->subbed_equal((l->args)[i])))
        return false;
    }
    return true;
}

to_prolog_string()

string Literal::to_prolog_string

(

)

const

Convert to a string in a format readable by Prolog.

Does not apply substitutions.

Definition at line 205 of file Literal.cpp.

                                       {
  string result;
  if (!polarity)
      result += "-";
  string name = pred->get_name();
  if (name == "=")
    name = "equal";
  result += name;
  if (arity > 0) {
    result += "(";
    commas::comma com(args.size());
    for (Term* p : args) {
      result += p->to_prolog_string();
      result += com();
    }
    result += ")";
  }
  return result;
}

to_string()

string Literal::to_string

(

bool

subbed = false

)

const

Full conversion of Literal to string.

Parameters

subbed

Implement substitutions if true.

Definition at line 185 of file Literal.cpp.

                                           {
  string result("Empty literal");
  if (!is_empty()) {
    if (pred->get_name() == string("=")) {
      result = "( ";
      result += args[0]->to_string(subbed);
      result += " ";
      result += polarity ? "=" : unicode_symbols::LogSym::neq;
      result += " ";
      result += args[1]->to_string(subbed);
      result += " )";
    }
    else {
      result = get_small_lit();
      result += vector_to_string(args, subbed);
    }
  }
  return result;
}

to_tptp_string()

string Literal::to_tptp_string

(

bool

subbed = false

)

const

Convert to a string in a format compatible with the TPTP.

Apply substitutions if argument is true.

Definition at line 225 of file Literal.cpp.

                                                {
  string result;
  string name = pred->get_name();
  if (name != "=") {
    if (!polarity)
      result += "~";
    result += name;
    if (arity > 0) {
      result += "(";
      commas::comma com(args.size());
      for (Term* p : args) {
        result += p->to_prolog_string(subbed);
        result += com();
      }
      result += ")";
    }
  }
  else {
    result += args[0]->to_prolog_string(subbed);
    if (polarity)
      result += " = ";
    else 
      result += " != ";
    result += args[1]->to_prolog_string(subbed);
  }
  return result;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Literal & l )

friend

Definition at line 309 of file Literal.cpp.

                                                    {
  if (l.is_empty())
    out << "Empty literal";
  else {
    if (!l.polarity)
      out << unicode_symbols::LogSym::neg;
    out << l.pred->to_string();
    out << vector_to_string(l.args);
  }
  return out;
}

Member Data Documentation

args

vector<Term*> Literal::args

private

Definition at line 53 of file Literal.hpp.

arity

Arity Literal::arity

private

Definition at line 54 of file Literal.hpp.

polarity

bool Literal::polarity

private

Definition at line 55 of file Literal.hpp.

pred

Predicate* Literal::pred

private

Definition at line 52 of file Literal.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/literal/Literal.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/literal/Literal.cpp