Representation of the Matrix within a proof. More...

#include <Matrix.hpp>

Collaboration diagram for Matrix:

[legend]

Public Member Functions
	Matrix ()
	Use this constructor if you really want an empty Matrix.

	Matrix (size_t)
	Use this constructor when you know how many predicates there are.

	Matrix (const Matrix &)=delete
	You're never going to need to copy a Matrix.

	Matrix (const Matrix &&)=delete

Matrix &	operator= (const Matrix &)=delete

Matrix &	operator= (const Matrix &&)=delete

ClauseNum	get_num_clauses () const
	Straightforward get method.

size_t	get_index_entry_size (size_t _i) const
	The ExtensionEnumerator needs to know this.

MatrixPairType	get_index_entry (size_t _i, size_t _j) const
	The ExtensionEnumerator needs to know this.

const Clause &	operator[] (size_t i) const
	Straightforward get method.

const Literal &	inspect_literal (size_t i, size_t j)
	Straightforward get method.

const Literal &	inspect_index_literal (size_t i, size_t j)
	Straightforward get method.

bool	is_positive (size_t i) const
	Is a particular Clause positive?

bool	is_negative (size_t i) const
	Is a particular Clause negative?

bool	is_ground (size_t i) const
	Is a particular Clause ground?

bool	is_conjecture (size_t i) const
	Is a particular Clause a conjecture?

void	set_num_equals (uint32_t n)
	Straightforward set method.

pair< bool, size_t >	find_start () const
	Use a simple heuristic to find a good start clause.

void	set_num_preds (size_t)
	Make an empty index.

string	get_name (size_t _i) const
	Retrieve the name of one of the clauses in the matrix.

void	add_clause (Clause &, string="", string="")
	Add a Clause to the Matrix and update the index accordingly.

void	deterministic_reorder (size_t)
	Deterministic reorder of the clauses.

void	random_reorder ()
	Randomly reorder the matrix.

void	random_reorder_literals ()
	Randomly reorder the literals in each clause in the matrix.

void	move_equals_to_start ()
	Self-explanatory.

vector< Clause >::const_iterator	cbegin () const

vector< Clause >::const_iterator	cend () const

vector< Clause >::iterator	begin ()

vector< Clause >::iterator	end ()

string	to_string () const
	Make a string representation.

string	make_LaTeX (bool=false) const
	Make a usable LaTeX representation.

void	write_to_prolog_file (const path &) const
	Write to a file that can be read by Prolog.

void	show_tptp () const
	Output in TPTP compatible format.

void	sort_clauses_by_increasing_size ()
	Self-explanatory.

void	get_literal_clause_pair (LitNum, size_t, Literal &, Clause &) const
	Get a literal and clause from the index.

void	make_copy_with_new_unique_vars (size_t, Clause &, VariableIndex &, TermIndex &) const
	Make a new copy of a clause in the matrix.

Private Member Functions
void	make_clauses_copy ()
	Store a copy of the clauses.

void	rebuild_index (vector< Clause > &, vector< string > &, vector< string > &)
	Rebuild the index after, for example, reordering.

template<class Comparison >
void	sort_clauses (Comparison comparison)
	Template method for general sorting of clauses, which sorts roles and names at the same time.

Private Attributes
vector< Clause >	clauses
	The Matrix itself is just a set of Clauses.

vector< bool >	positive_clauses
	Keep track of which clauses are positive.

vector< bool >	negative_clauses
	Keep track of which clauses are negative.

vector< bool >	ground_clauses
	We need to know this to control backtracking.

vector< string >	clause_roles
	Keep track of which clauses are conjectures etc.

vector< string >	clause_names
	Keep track of the names of the clauses.

uint32_t	num_equals
	You need to know how many equality axioms there are in case you want to move them around.

vector< Clause >	clauses_copy
	It makes sense to keep a copy of the clauses if your schedule reorders multiple times.

vector< string >	roles_copy
	It makes sense to keep a copy of the roles if your schedule reorders multiple times.

vector< string >	names_copy
	It makes sense to keep a copy of the names if your schedule reorders multiple times.

bool	copy_saved
	Remember whether you've saved a copy.

vector< vector< MatrixPairType > >	index
	We want to be able to quickly identify where in each clause a particular literal lives.

vector< vector< LiteralClausePairType > >	literal_clause_index
	This corresponds closely to index, but has the actual Literal, and the Clause after the Literal's removal.

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

Friends
ostream &	operator<< (ostream &out, const Matrix &m)

Detailed Description

Representation of the Matrix within a proof.

The Matrix itself never actually changes. However we do want to be able to look things up quickly when finding possible extension steps, so we build a pair of indexes to help with that.

Definition at line 74 of file Matrix.hpp.

Constructor & Destructor Documentation

◆ Matrix() [1/3]

Matrix::Matrix ( )

inline

Use this constructor if you really want an empty Matrix.

Definition at line 210 of file Matrix.hpp.

    : clauses()
    , index()
    , literal_clause_index()
    , positive_clauses()
    , negative_clauses()
    , ground_clauses()
    , clause_roles()
    , clause_names()
    , num_equals(0)
    , clauses_copy()
    , roles_copy()
    , names_copy()
    , copy_saved(false)
    {}

◆ Matrix() [2/3]

Matrix::Matrix ( size_t num_predicates )

Use this constructor when you know how many predicates there are.

Parameters

num_predicates Number of predicates.

Definition at line 30 of file Matrix.cpp.

: clauses()
, index((num_predicates * 2), vector<MatrixPairType>())
, literal_clause_index((num_predicates * 2), vector<LiteralClausePairType>())
, positive_clauses()
, negative_clauses()
, ground_clauses()
, clause_roles()
, clause_names()
, num_equals(0)
, clauses_copy()
, roles_copy()
, names_copy()
, copy_saved(false)
{}

◆ Matrix() [3/3]

Matrix::Matrix ( const Matrix & )

delete

You're never going to need to copy a Matrix.

Let the compiler be your friend.

Member Function Documentation

◆ add_clause()

void Matrix::add_clause	(	Clause &	clause,
		string	role = "",
		string	name = "" )

Add a Clause to the Matrix and update the index accordingly.

Optionally add a clause role.

Parameters

clause	Reference to the Clause.
role	A string denoting the role of the clause.
name	The name of the clause.

Definition at line 99 of file Matrix.cpp.

                                                                {
    ClauseNum clause_number = clauses.size();
    LitNum literal_number = 0;
    for (size_t j = 0; j < clause.size(); j++) {
        size_t i = clause[j].get_pred_as_index();
        index[i].push_back(MatrixPairType(clause_number, literal_number));
        Clause new_clause = clause;
        new_clause.drop_literal(literal_number);
        literal_clause_index[i].push_back(LiteralClausePairType(clause[j], new_clause));
        literal_number++;
    }
    clauses.push_back(clause);
    positive_clauses.push_back(clause.is_positive());
    negative_clauses.push_back(clause.is_negative());
    ground_clauses.push_back(clause.is_ground());
    clause_roles.push_back(role);
    clause_names.push_back(name);
}

◆ begin()

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

inline

Definition at line 377 of file Matrix.hpp.

377{ return clauses.begin(); }

◆ cbegin()

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

inline

Definition at line 375 of file Matrix.hpp.

375{ return clauses.cbegin(); }

◆ cend()

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

inline

Definition at line 376 of file Matrix.hpp.

376{ return clauses.cend(); }

◆ deterministic_reorder()

void Matrix::deterministic_reorder ( size_t n )

Deterministic reorder of the clauses.

Call the reorder algorithm the specified number of times. This assumes you have stored a copy of the original clauses.

Parameters

n	Number of times to call the reorder algorithm

Only store a copy of the clauses the first time you do this.

Definition at line 139 of file Matrix.cpp.

                                           {
  if (!copy_saved) {
    copy_saved = true;
    make_clauses_copy();
  }
  /*
  * Find a suitably reordered set of indices.
  */
  vector<uint32_t> new_order;
  size_t s = clauses.size();
  for (size_t i = 0; i < s; i++)
    new_order.push_back(i);
  new_order = deterministic_reorder_n_times<uint32_t>(new_order, n);
  /*
  * Do the reordering.
  */
  vector<Clause> cs;
  vector<string> ss;
  vector<string> ns;
  for (size_t i = 0; i < s; i++) {
    size_t j = new_order[i];
    cs.push_back(clauses_copy[j]);
    ss.push_back(roles_copy[j]);
    ns.push_back(names_copy[j]);
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(cs, ss, ns);
}

◆ end()

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

inline

Definition at line 378 of file Matrix.hpp.

378{ return clauses.end(); }

◆ find_start()

pair< bool, size_t > Matrix::find_start ( ) const

Use a simple heuristic to find a good start clause.

Find a start clause that is positive/negative according to the –negative flag, and if possible also a conjecture clause. Also, indicate if there is no positive/negative clause, which means the problem is trivial.

Definition at line 56 of file Matrix.cpp.

                                           {
  bool found_positive = false;
  bool found_negative = false;
  size_t first_positive = 0;
  size_t first_negative = 0;
  bool found_candidate = false;
  size_t candidate = 0;
  size_t i = 0;
  for (bool positive : positive_clauses) {
    if (positive_clauses[i]) {
      if (!found_positive) {
        first_positive = i;
        found_positive = true;
      }
    }
    if (negative_clauses[i]) {
      if (!found_negative) {
        first_negative = i;
        found_negative = true;
      }
    }
    if (is_conjecture(i) && !found_candidate) {
      if ((params::positive_representation && positive_clauses[i]) ||
         (!params::positive_representation && negative_clauses[i])) {
            found_candidate = true;
            candidate = i;
      }
    }
    i++;
  }
  if (!(found_positive && found_negative))
    return pair<bool,size_t>(false, 0);
  if (found_candidate)
    return pair<bool, size_t>(true, candidate);
  else if (params::positive_representation)
    return pair<bool, size_t>(true, first_positive);
  else
    return pair<bool, size_t>(true, first_negative);
}

◆ get_index_entry()

MatrixPairType Matrix::get_index_entry	(	size_t	_i,
		size_t	_j ) const

inline

The ExtensionEnumerator needs to know this.

Definition at line 254 of file Matrix.hpp.

                                                                      {
      return (index[_i])[_j];
    }

◆ get_index_entry_size()

size_t Matrix::get_index_entry_size ( size_t _i ) const

inline

The ExtensionEnumerator needs to know this.

Definition at line 248 of file Matrix.hpp.

                                                        {
      return index[_i].size();
    }

◆ get_literal_clause_pair()

void Matrix::get_literal_clause_pair	(	LitNum	_l,
		size_t	_i,
		Literal &	_lit,
		Clause &	_clause ) const

Get a literal and clause from the index.

Parameters

_l	Index for the literal of interest.
_i	Index for where the pair is in _lit's vector.
_lit	Result literal.
_clause	Result clause.

Definition at line 321 of file Matrix.cpp.

                                                                                               {
  LiteralClausePairType result = (literal_clause_index[_l])[_i];
  _lit = result.first;
  _clause = result.second;
}

◆ get_name()

string Matrix::get_name ( size_t _i ) const

inline

Retrieve the name of one of the clauses in the matrix.

Definition at line 333 of file Matrix.hpp.

                                     {
      return clause_names[_i];
    }

◆ get_num_clauses()

ClauseNum Matrix::get_num_clauses ( ) const

inline

Straightforward get method.

Definition at line 244 of file Matrix.hpp.

244{ return clauses.size(); }

◆ inspect_index_literal()

const Literal & Matrix::inspect_index_literal	(	size_t	i,
		size_t	j )

inline

Straightforward get method.

Beware - the parameters are not checked, so behave!

Parameters

i	Index in literal_clause_index;
j	Index of required entry.

Definition at line 284 of file Matrix.hpp.

                                                                    { 
      return (literal_clause_index[i])[j].first; 
    }

◆ inspect_literal()

const Literal & Matrix::inspect_literal	(	size_t	i,
		size_t	j )

inline

Straightforward get method.

Beware - the parameters are not checked, so behave!

Parameters

i	Index of clause to get.
j	Index of literal in clause.

Definition at line 273 of file Matrix.hpp.

                                                              { 
      return (clauses[i])[j]; 
    }

◆ is_conjecture()

bool Matrix::is_conjecture ( size_t i ) const

Is a particular Clause a conjecture?

Parameters

i	Index of Clause to check.

Definition at line 51 of file Matrix.cpp.

                                         {
  return clause_roles[i] == "negated_conjecture" ||
         clause_roles[i] == "conjecture";
}

◆ is_ground()

bool Matrix::is_ground ( size_t i ) const

inline

Is a particular Clause ground?

Parameters

i	Index of Clause to check.

Definition at line 304 of file Matrix.hpp.

304{ return ground_clauses[i]; }

◆ is_negative()

bool Matrix::is_negative ( size_t i ) const

inline

Is a particular Clause negative?

Parameters

i	Index of Clause to check.

Definition at line 298 of file Matrix.hpp.

298{ return negative_clauses[i]; }

◆ is_positive()

bool Matrix::is_positive ( size_t i ) const

inline

Is a particular Clause positive?

Parameters

i	Index of Clause to check.

Definition at line 292 of file Matrix.hpp.

292{ return positive_clauses[i]; }

◆ make_clauses_copy()

void Matrix::make_clauses_copy ( )

inlineprivate

Store a copy of the clauses.

Definition at line 153 of file Matrix.hpp.

                             {
      clauses_copy.clear();
      clauses_copy = clauses;
      roles_copy.clear();
      roles_copy = clause_roles;
      names_copy.clear();
      names_copy = clause_names;
    }

◆ make_copy_with_new_unique_vars()

void Matrix::make_copy_with_new_unique_vars	(	size_t	_index,
		Clause &	_c,
		VariableIndex &	_vi,
		TermIndex &	_ti ) const

Make a new copy of a clause in the matrix.

Parameters

_index	Clause to copy.
_c	Newly copied clause.
_vi	Reference to variable index.
_ti	Reference to term index.

Definition at line 327 of file Matrix.cpp.

                                                                      {
      _c = clauses[_index].make_copy_with_new_unique_vars(_vi, _ti);
}

◆ make_LaTeX()

string Matrix::make_LaTeX ( bool subbed = false ) const

Make a usable LaTeX representation.

Parameters

subbed Implement substitutions if true.

Definition at line 277 of file Matrix.cpp.

                                           {
  string s ("\\[\n\\begin{split}\n");
  s += "\\textcolor{magenta}{M} = ";
  size_t i = 0;
  for (const Clause& c : clauses) {
    s += std::to_string(i++);
    s += "&:";
    s += c.make_LaTeX(subbed);
    s += "\\\\";
  }
  s += "\n\\end{split}\n\\]\n";
 
  return s;
}

◆ move_equals_to_start()

void Matrix::move_equals_to_start ( )

Self-explanatory.

BUT only do this to the matrix built at the start of the process, as it assumes the equality axioms are at the end of the matrix.

Definition at line 222 of file Matrix.cpp.

                                  {
  if (num_equals == 0) {
    cerr << "Why are you trying to move equality axioms - there aren't any?" << endl;
    return;
  }
  make_clauses_copy();
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  ground_clauses.clear();
  clause_roles.clear();
  clause_names.clear();
  size_t s2 = index.size();
  size_t s3 = literal_clause_index.size();
  index.clear();
  literal_clause_index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  literal_clause_index = vector<vector<LiteralClausePairType> >(s3, vector<LiteralClausePairType>());
  size_t n_clauses = clauses_copy.size();
  for (size_t i = n_clauses - num_equals; i < n_clauses; i++) {
    add_clause(clauses_copy[i], roles_copy[i], names_copy[i]);
  }
  for (size_t i = 0; i < n_clauses - num_equals; i++) {
    add_clause(clauses_copy[i], roles_copy[i], names_copy[i]);
  }
  clauses_copy.clear();
  roles_copy.clear();
  names_copy.clear();
}

◆ operator[]()

const Clause & Matrix::operator[] ( size_t i ) const

inline

Straightforward get method.

Beware - the parameter is not checked, so behave!

Parameters

i	Index of item to get.

Definition at line 264 of file Matrix.hpp.

264{ return clauses[i]; }

◆ random_reorder()

void Matrix::random_reorder ( )

Randomly reorder the matrix.

Definition at line 173 of file Matrix.cpp.

                            {
  vector<Clause> saved_clauses(clauses);
  vector<string> saved_clause_roles(clause_roles);
  vector<string> saved_clause_names(clause_names);
  /*
  * Find a suitably reordered set of indices.
  */
  vector<uint32_t> new_order;
  size_t s = clauses.size();
  for (size_t i = 0; i < s; i++)
    new_order.push_back(i);
  std::shuffle(new_order.begin(), new_order.end(), d);
  /*
  * Do the reordering.
  */
  vector<Clause> cs;
  vector<string> ss;
  vector<string> ns;
  for (size_t i = 0; i < s; i++) {
    size_t j = new_order[i];
    cs.push_back(saved_clauses[j]);
    ss.push_back(saved_clause_roles[j]);
    ns.push_back(saved_clause_names[j]);
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(cs, ss, ns);
}

◆ random_reorder_literals()

void Matrix::random_reorder_literals ( )

Randomly reorder the literals in each clause in the matrix.

Definition at line 203 of file Matrix.cpp.

                                     {
  vector<Clause> saved_clauses(clauses);
  vector<string> saved_clause_roles(clause_roles);
  vector<string> saved_clause_names(clause_names);
  size_t s = clauses.size();
  /*
  * Reorder.
  */
  for (size_t i = 0; i < s; i++) {
    Clause c(saved_clauses[i]);
    c.random_reorder();
    saved_clauses[i] = c;
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(saved_clauses, saved_clause_roles, saved_clause_names);
}

◆ rebuild_index()

void Matrix::rebuild_index	(	vector< Clause > &	cs,
		vector< string > &	ss,
		vector< string > &	ns )

private

Rebuild the index after, for example, reordering.

Parameters

cs	Vector of clauses - matrix.
ss	Vector of strings - roles.
ss	Vector of strings - names.

Definition at line 118 of file Matrix.cpp.

                                               {
  size_t s = clauses.size();
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  ground_clauses.clear();
  clause_roles.clear();
  clause_names.clear();
  size_t s2 = index.size();
  size_t s3 = literal_clause_index.size();
  index.clear();
  literal_clause_index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  literal_clause_index = vector<vector<LiteralClausePairType> >(s3, vector<LiteralClausePairType>());
  for (size_t i = 0; i < s; i++) {
    add_clause(cs[i], ss[i], ns[i]);
  }
}

◆ set_num_equals()

void Matrix::set_num_equals ( uint32_t n )

inline

Straightforward set method.

Parameters

n	Number of equality axioms.

Definition at line 316 of file Matrix.hpp.

316{ num_equals = n; }

◆ set_num_preds()

void Matrix::set_num_preds ( size_t num_predicates )

Make an empty index.

Definition at line 46 of file Matrix.cpp.

                                                {
    index = vector<vector<MatrixPairType> >((num_predicates * 2), vector<MatrixPairType>());
    literal_clause_index = vector<vector<LiteralClausePairType> >((num_predicates * 2), vector<LiteralClausePairType>());
}

◆ show_tptp()

void Matrix::show_tptp ( ) const

Output in TPTP compatible format.

Definition at line 309 of file Matrix.cpp.

                             {
  size_t matrix_i = 0;
  for (const Clause& c : clauses) {
    cout << "cnf(matrix-";
    cout << std::to_string(matrix_i++);
    cout << ", plain, ";
    cout << c.to_tptp_string();
    cout << ").";
    cout << std::endl;
  }
}

◆ sort_clauses()

template<class Comparison >

void Matrix::sort_clauses ( Comparison comparison )

inlineprivate

Template method for general sorting of clauses, which sorts roles and names at the same time.

ClauseComparisons.hpp contains function objects that can be used with this to implement different orderings.

Definition at line 177 of file Matrix.hpp.

                                             {
      /*
      * Combine the clauses with their roles.
      */
      vector<ClauseRoleName> cr;
      size_t s = clauses.size();
      for (size_t i = 0; i < s; i++) {
        cr.push_back(ClauseRoleName(clauses[i], pair<string, string>(clause_roles[i], clause_names[i])));
      }
      /*
      * Sort them according to the relevant ordering.
      */
      std::sort(cr.begin(), cr.end(), comparison);
      /*
      * Split them again and re-build the index.
      */
      clauses.clear();
      positive_clauses.clear();
      negative_clauses.clear();
      clause_roles.clear();
      clause_names.clear();
      size_t s2 = index.size();
      index.clear();
      index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
      for (size_t i = 0; i < s; i++) {
        add_clause(std::get<0>(cr[i]), std::get<1>(cr[i]).first, std::get<1>(cr[i]).second);
      }
    }

◆ sort_clauses_by_increasing_size()

void Matrix::sort_clauses_by_increasing_size ( )

inline

Self-explanatory.

Inspired by "Machine Learning Guidance for Connection Tableaux," Farber et al. 2020 although with a different measure of size and happening at a different place.

Makes use of the sort_clauses template.

Definition at line 411 of file Matrix.hpp.

                                           {
      ClauseLengthCompare comparison;
      sort_clauses<ClauseLengthCompare>(comparison);
    }

◆ to_string()

string Matrix::to_string ( ) const

Make a string representation.

Definition at line 252 of file Matrix.cpp.

                               {
  string result;
  colour_string::ColourString cs(params::use_colours);
  size_t i = 0;
  for (const Clause& c : clauses) {
    if (is_conjecture(i))
      result += cs("*").orange();
    else
      result += " ";
    if (positive_clauses[i])
      result += cs("+").orange();
    else if (negative_clauses[i])
      result += cs("-").orange();
    else
      result += " ";
    result += " ";
    result += c.to_string();
    result += " ( ";
    result += clause_names[i];
    result += " )\n";
    i++;
  }
  return result;
}

◆ write_to_prolog_file()

void Matrix::write_to_prolog_file ( const path & path_to_file ) const

Write to a file that can be read by Prolog.

This is for proof checking.

Parameters

path_to_file Reference to path object.

Definition at line 292 of file Matrix.cpp.

                                                                {
  std::ofstream file(path_to_file);
  size_t matrix_i = 0;
  // Nasty hack needed to stop the proof checker from printing 
  // a bunch of warnings when reading the matrix.
  file << ":- style_check(-singleton)." << std::endl;
  for (const Clause& c : clauses) {
    file << "matrix(";
    file << std::to_string(matrix_i++);
    file << ", ";
    file << c.to_prolog_string();
    file << ").";
    file << std::endl;
  }
  file.close();
}

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<<	(	ostream &	out,
		const Matrix &	m )

friend

Definition at line 332 of file Matrix.cpp.

                                                   {
    out << "Clauses in matrix:" << endl;
    out << "------------------" << endl;
    size_t i = 0;
    for (const Clause& c : m.clauses) {
        out << setw(params::output_width) << i
        << ": " << c;
        if (m.ground_clauses[i]) {
          out << " (ground)";
        }
        cout << " " << m.clause_names[i] << " " << m.clause_roles[i];
        i++;
        out << endl;
    }
    vector<string> index_lits(m.index.size(), string(""));
    for (Clause c : m.clauses)
      for (size_t i = 0; i < c.size(); i++)
        index_lits[c[i].get_pred_as_index()] = c[i].get_small_lit();
    i = 0;
    out << endl << "Index: (Clause, Literal):" << endl;
    out <<         "-------------------------" << endl;
    for (vector<MatrixPairType> v : m.index) {
        out << setw(params::output_width + 20) << index_lits[i++] << ": ";
        for (MatrixPairType p : v) {
            out << "(" << p.first << ", " << p.second << ") ";
        }
        out << endl;
    }
    out << endl << "Index: (Literal, Clause without Literal):" << endl;
    out <<         "-----------------------------------------" << endl;
    i = 0;
    for (vector<LiteralClausePairType> v : m.literal_clause_index) {
        out << setw(params::output_width + 20) << index_lits[i++] << ": "  << endl;;
        for (LiteralClausePairType p : v) {
            out << p.first.to_string() << " --- " << p.second.to_string() << endl;
        }
        out << endl;
    }
    return out;
}

Member Data Documentation

◆ clause_names

vector<string> Matrix::clause_names

private

Keep track of the names of the clauses.

This allows us to keep track of everything when producing TPTP output.

Definition at line 108 of file Matrix.hpp.

◆ clause_roles

vector<string> Matrix::clause_roles

private

Keep track of which clauses are conjectures etc.

This allows start clause heuristics to be applied.

Definition at line 101 of file Matrix.hpp.

◆ clauses

vector<Clause> Matrix::clauses

private

The Matrix itself is just a set of Clauses.

Definition at line 79 of file Matrix.hpp.

◆ clauses_copy

vector<Clause> Matrix::clauses_copy

private

It makes sense to keep a copy of the clauses if your schedule reorders multiple times.

Definition at line 118 of file Matrix.hpp.

◆ copy_saved

bool Matrix::copy_saved

private

Remember whether you've saved a copy.

Definition at line 132 of file Matrix.hpp.

◆ d

std::mt19937 Matrix::d

staticprivate

Randomness for random reordering.

Definition at line 149 of file Matrix.hpp.

◆ ground_clauses

vector<bool> Matrix::ground_clauses

private

We need to know this to control backtracking.

Definition at line 95 of file Matrix.hpp.

◆ index

vector<vector<MatrixPairType> > Matrix::index

private

We want to be able to quickly identify where in each clause a particular literal lives.

Store clause and position as pairs in a row corresponding to the literal.

Definition at line 140 of file Matrix.hpp.

◆ literal_clause_index

vector<vector<LiteralClausePairType> > Matrix::literal_clause_index

private

This corresponds closely to index, but has the actual Literal, and the Clause after the Literal's removal.

Definition at line 145 of file Matrix.hpp.

◆ names_copy

vector<string> Matrix::names_copy

private

It makes sense to keep a copy of the names if your schedule reorders multiple times.

Definition at line 128 of file Matrix.hpp.

◆ negative_clauses

vector<bool> Matrix::negative_clauses

private

Keep track of which clauses are negative.

This allows start clause heuristics to be applied.

Definition at line 91 of file Matrix.hpp.

◆ num_equals

uint32_t Matrix::num_equals

private

You need to know how many equality axioms there are in case you want to move them around.

Definition at line 113 of file Matrix.hpp.

◆ positive_clauses

vector<bool> Matrix::positive_clauses

private

Keep track of which clauses are positive.

This allows start clause heuristics to be applied.

Definition at line 85 of file Matrix.hpp.

◆ roles_copy

vector<string> Matrix::roles_copy

private

It makes sense to keep a copy of the roles if your schedule reorders multiple times.

Definition at line 123 of file Matrix.hpp.

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

/Users/sbh11/Desktop/connection-prover/c++/connect++/source/Matrix.hpp
/Users/sbh11/Desktop/connection-prover/c++/connect++/source/Matrix.cpp

Public Member Functions

Private Member Functions

Private Attributes

Static Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Matrix() [1/3]

◆ Matrix() [2/3]

◆ Matrix() [3/3]

Member Function Documentation

◆ add_clause()

◆ begin()

◆ cbegin()

◆ cend()

◆ deterministic_reorder()

◆ end()

◆ find_start()

◆ get_index_entry()

◆ get_index_entry_size()

◆ get_literal_clause_pair()

◆ get_name()

◆ get_num_clauses()

◆ inspect_index_literal()

◆ inspect_literal()

◆ is_conjecture()

◆ is_ground()

◆ is_negative()

◆ is_positive()

◆ make_clauses_copy()

◆ make_copy_with_new_unique_vars()

◆ make_LaTeX()

◆ move_equals_to_start()

◆ operator[]()

◆ random_reorder()

◆ random_reorder_literals()

◆ rebuild_index()

◆ set_num_equals()

◆ set_num_preds()

◆ show_tptp()

◆ sort_clauses()

◆ sort_clauses_by_increasing_size()

◆ to_string()

◆ write_to_prolog_file()

Friends And Related Symbol Documentation

◆ operator<<

Member Data Documentation

◆ clause_names

◆ clause_roles

◆ clauses

◆ clauses_copy

◆ copy_saved

◆ d

◆ ground_clauses

◆ index

◆ literal_clause_index

◆ names_copy

◆ negative_clauses

◆ num_equals

◆ positive_clauses

◆ roles_copy